Skip to content

Commit

Permalink
Merge pull request #23 from knowsys/upgrade-to-lean-4.6.1
Browse files Browse the repository at this point in the history 
Upgrade to Lean 4.6.1
  • Loading branch information
@monsterkrampe
monsterkrampe authored Mar 11, 2024
2 parents 5ed5163 + ddc0e76 commit 5352caa
Show file tree
Hide file tree
Showing 8 changed files with 134 additions and 139 deletions.
5 changes: 2 additions & 3 deletions FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,9 +85,8 @@ def Grammar.DerivationStep.cancelLeft
val := { d with
pre := d.pre.tail
sound := by
simp;
have hxs : xs = lhs.tail
simp [h_lhs]
simp
have hxs : xs = lhs.tail := by simp [h_lhs]
simp [hxs, HMul.hMul, Mul.mul]
rw [<- List.tail_append_of_ne_nil]
congr
Expand Down
232 changes: 114 additions & 118 deletions FormalSystems/Chomsky/Regular/RegularGrammar.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,128 +121,124 @@ inductive RegularDerivation (G: RegularGrammar α nt): (v: G.V) → (w: Word G.Z
G.RegularDerivation v' w' → G.RegularDerivation v w

mutual
def RegularDerivation.fromDerivation
(derivation: G.Derivation [.inl X] w')
(h: Sum.inr <$> w = w'):
G.RegularDerivation X w := by
match derivation with
| .same h_same =>
cases w <;> simp [<- h_same] at h
rw [List.cons_eq_cons] at h
have ⟨_, _⟩ := h
contradiction

| .step s d' hd =>
apply fromStep
repeat assumption
termination_by (derivation.len, 0)
decreasing_by
apply (Prod.Lex.lt_iff _ _).mpr
try { simp [RegularProduction.getRhs, Derivation.len] }

def RegularDerivation.fromDerivation
(derivation: G.Derivation [.inl X] w')
(h: Sum.inr <$> w = w'):
G.RegularDerivation X w := by
match derivation with
| .same h_same =>
cases w <;> simp [<- h_same] at h
rw [List.cons_eq_cons] at h
have ⟨_, _⟩ := h
contradiction

| .step s d' hd =>
apply fromStep
repeat assumption

def RegularDerivation.fromStep
(step: G.DerivationStep [.inl X])
(derivation: G.Derivation u w')
(h_u: step.result = u)
(h_w: Sum.inr <$> w = w'):
G.RegularDerivation X w := by
have ⟨left, pre, suf⟩ := step.lhs_singleton
unfold DerivationStep.result at h_u
match hp:step.prod.val with
| .eps _ =>
apply RegularDerivation.eps

. rw [hp,
RegularProduction.lhs_eq_production_lhs,
List.cons_eq_cons]
at left
simp [RegularProduction.lhs] at left
rw [<- left, <- hp]
exact step.prod.prop

. simp [hp, RegularProduction.rhs_eq_deconstr_rhs,
Word.mk, <- Word.eps_eq_nil] at h_u
simp [<-h_u, pre, suf] at derivation
cases derivation
case same h_same =>
dsimp [RegularProduction.getRhs] at h_same
simp [<-h_same, <-Word.eps_eq_nil] at h_w
rw [Word.eps_eq_nil, List.map_eq_nil] at h_w
exact h_w
case step s' _ _ =>
have contra := s'.sound.symm
simp [RegularProduction.getRhs, <-Word.eps_eq_nil, List.map] at contra
simp [Word.mul_eq_eps] at contra
have _ := contra.1.2
contradiction

| .alpha _ a =>
apply RegularDerivation.alpha

. rw [hp,
RegularProduction.lhs_eq_production_lhs,
List.cons_eq_cons]
at left
simp [RegularProduction.lhs] at left
rw [<- left, <- hp]
exact step.prod.prop

. simp [hp, RegularProduction.rhs_eq_deconstr_rhs, Word.mk] at h_u
simp [<-h_u, pre, suf] at derivation
cases derivation

case same h_same =>
simp [HMul.hMul, Mul.mul] at h_same
rw [<- h_same] at h_w
cases w
contradiction
simp [List.map_cons] at h_w
have ⟨h1, h2⟩ := List.cons_eq_cons.mp h_w
simp [Sum.inr_injective] at h1
simp [List.map_eq_nil, RegularProduction.getRhs] at h2
rw [h1, h2]

case step s' _ _ =>
apply False.elim
have contra := s'.sound.symm
rw [RegularProduction.lhs_eq_production_lhs] at contra
simp [HMul.hMul, Mul.mul, RegularProduction.getRhs] at contra
rw [List.append_eq_cons] at contra
cases contra
case inl h =>
have ⟨_, h⟩ := h
simp at h
case inr h =>
have ⟨_, h⟩ := h
simp at h

| .cons _ (a, X') =>
simp [hp, RegularProduction.rhs_eq_deconstr_rhs, pre, suf] at h_u
simp [Word.mk, HMul.hMul, Mul.mul] at h_u

apply RegularDerivation.step
. have : step.prod.val = .cons X (a, X') := by
rw [Production.prod_ext]; constructor
assumption; simp [hp]; rfl
rw [<- this]; exact step.prod.prop

. apply ContextFreeGrammar.derivation_preserves_prefix derivation
exact h_u.symm
exact h_w.symm

. apply RegularDerivation.fromDerivation
exact derivation.cancelLeft h_u.symm h_w.symm
rfl

end

termination_by
fromDerivation d _ => (d.len, 0)
fromStep _ d _ _ => (d.len, 1)

decreasing_by
fromDerivation =>
def RegularDerivation.fromStep
(step: G.DerivationStep [.inl X])
(derivation: G.Derivation u w')
(h_u: step.result = u)
(h_w: Sum.inr <$> w = w'):
G.RegularDerivation X w := by
have ⟨left, pre, suf⟩ := step.lhs_singleton
unfold DerivationStep.result at h_u
match hp:step.prod.val with
| .eps _ =>
apply RegularDerivation.eps

. rw [hp,
RegularProduction.lhs_eq_production_lhs,
List.cons_eq_cons]
at left
simp [RegularProduction.lhs] at left
rw [<- left, <- hp]
exact step.prod.prop

. simp [hp, RegularProduction.rhs_eq_deconstr_rhs,
Word.mk, <- Word.eps_eq_nil] at h_u
simp [<-h_u, pre, suf] at derivation
cases derivation
case same h_same =>
dsimp [RegularProduction.getRhs] at h_same
simp [<-h_same, <-Word.eps_eq_nil] at h_w
rw [Word.eps_eq_nil, List.map_eq_nil] at h_w
exact h_w
case step s' _ _ =>
have contra := s'.sound.symm
simp [RegularProduction.getRhs, <-Word.eps_eq_nil, List.map] at contra
simp [Word.mul_eq_eps] at contra
have _ := contra.1.2
contradiction

| .alpha _ a =>
apply RegularDerivation.alpha

. rw [hp,
RegularProduction.lhs_eq_production_lhs,
List.cons_eq_cons]
at left
simp [RegularProduction.lhs] at left
rw [<- left, <- hp]
exact step.prod.prop

. simp [hp, RegularProduction.rhs_eq_deconstr_rhs, Word.mk] at h_u
simp [<-h_u, pre, suf] at derivation
cases derivation

case same h_same =>
simp [HMul.hMul, Mul.mul] at h_same
rw [<- h_same] at h_w
cases w
contradiction
simp [List.map_cons] at h_w
have ⟨h1, h2⟩ := List.cons_eq_cons.mp h_w
simp [Sum.inr_injective] at h1
simp [List.map_eq_nil, RegularProduction.getRhs] at h2
rw [h1, h2]

case step s' _ _ =>
apply False.elim
have contra := s'.sound.symm
rw [RegularProduction.lhs_eq_production_lhs] at contra
simp [HMul.hMul, Mul.mul, RegularProduction.getRhs] at contra
rw [List.append_eq_cons] at contra
cases contra
case inl h =>
have ⟨_, h⟩ := h
simp at h
case inr h =>
have ⟨_, h⟩ := h
simp at h

| .cons _ (a, X') =>
simp [hp, RegularProduction.rhs_eq_deconstr_rhs, pre, suf] at h_u
simp [Word.mk, HMul.hMul, Mul.mul] at h_u

apply RegularDerivation.step
. have : step.prod.val = .cons X (a, X') := by
rw [Production.prod_ext]; constructor
assumption; simp [hp]; rfl
rw [<- this]; exact step.prod.prop

. apply ContextFreeGrammar.derivation_preserves_prefix derivation
exact h_u.symm
exact h_w.symm

. apply RegularDerivation.fromDerivation
exact derivation.cancelLeft h_u.symm h_w.symm
rfl
termination_by (derivation.len, 1)
decreasing_by
apply (Prod.Lex.lt_iff _ _).mpr
try { simp [RegularProduction.getRhs, Derivation.len] }
try { simp [Derivation.cancelLeft_len _] }

end

def RegularDerivation.toDerivation (d: G.RegularDerivation v w):
G.Derivation [.inl v] (Sum.inr <$> w) := by
Expand Down
2 changes: 1 addition & 1 deletion FormalSystems/Chomsky/Regular/TotalDFA.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ theorem total_del_eq (M: TotalDFA α qs):
def del_star' (M: TotalDFA α qs): M.Q × Word (M.Z) → M.Q
| (q, ε) => q
| (q, x :: xs) => M.del_star' (M.δ' (q, x), xs)
termination_by _ p => p.2.length
termination_by p => p.2.length

theorem total_del_star_eq {M: TotalDFA α qs} {q: _} {w: _}:
M.del_star (q, w) = some (M.del_star' (q, w)) := by
Expand Down
2 changes: 1 addition & 1 deletion FormalSystems/Computability/Loop.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ theorem LoopProgram.ofLen_stmt_complete
rw [Nat.succ_add, Nat.succ_add, Nat.succ_eq_add_one]
apply ofLen_stmt_complete _ h_stmt
cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
termination_by _ => x + y + n
termination_by x + y + n

theorem LoopProgram.ofLen_complete:
∀ p: LoopProgram, p ∈ LoopProgram.ofLen p.len := by
Expand Down
8 changes: 4 additions & 4 deletions FormalSystems/Preliminaries/Word.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,8 @@ def Nat.fin_mod (n : ℕ) (h: N > 0) : Fin N := ⟨ n % N, Nat.mod_lt n h ⟩
def Word.decode [inst: Alphabet α]: (n : ℕ) → Word α
| Nat.zero => []
| Nat.succ n => inst.decode_fin (Nat.fin_mod n Alphabet.card_pos) :: Word.decode (n / inst.card)
termination_by Word.decode n => n
decreasing_by Word.decode =>
termination_by n => n
decreasing_by
simp [InvImage]
apply Nat.lt_of_le_of_lt
exact Nat.div_le_self n inst.card
Expand Down Expand Up @@ -64,8 +64,8 @@ def Word.encode [inst: Alphabet α]: (w : Word α) → ℕ
simp [ih, FinDenumerable.decode_fin_eq_option_get]
rw [<- inst.encode_fin_eq_encode _, inst.decodenk]
simp [Nat.fin_mod, Nat.mul_comm, Nat.div_add_mod n inst.card]
termination_by Word.decodenk n => n
decreasing_by Word.decodenk =>
termination_by n => n
decreasing_by
simp [InvImage]
apply Nat.lt_of_le_of_lt
exact Nat.div_le_self n inst.card
Expand Down
20 changes: 10 additions & 10 deletions lake-manifest.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,16 @@
[{"url": "https://github.com/leanprover/std4",
"type": "git",
"subDir": null,
"rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
"rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inputRev": "v4.6.1",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "1c88406514a636d241903e2e288d21dc6d861e01",
"rev": "fd760831487e6835944e7eeed505522c9dd47563",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand All @@ -22,19 +22,19 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520",
"rev": "ae76973be902b1da1589b28d10648c4e57333cad",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inputRev": "v4.6.1",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
"rev": "16cae05860b208925f54e5581ec5fd264823440c",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.25",
"inputRev": "v0.0.29",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
Expand All @@ -49,7 +49,7 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
"rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -58,10 +58,10 @@
{"url": "https://github.com/leanprover-community/mathlib4",
"type": "git",
"subDir": null,
"rev": "feec58a7ee9185f92abddcf7631643b53181a7d3",
"rev": "5bb630b0e53879b30dc48637d83822677a64065b",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.5.0",
"inputRev": "v4.6.1",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "formal_systems",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ open Lake DSL
package formal_systems

require mathlib
from git "https://github.com/leanprover-community/mathlib4"@"v4.5.0"
from git "https://github.com/leanprover-community/mathlib4"@"v4.6.1"

@[default_target]
lean_lib FormalSystems
2 changes: 1 addition & 1 deletion lean-toolchain
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.5.0
leanprover/lean4:v4.6.1

0 comments on commit 5352caa

Please sign in to comment.