diff --git a/FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean b/FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean index 7533b21..1396892 100644 --- a/FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean +++ b/FormalSystems/Chomsky/ContextFree/ContextFreeGrammar.lean @@ -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 diff --git a/FormalSystems/Chomsky/Regular/RegularGrammar.lean b/FormalSystems/Chomsky/Regular/RegularGrammar.lean index b839eec..96b76d8 100644 --- a/FormalSystems/Chomsky/Regular/RegularGrammar.lean +++ b/FormalSystems/Chomsky/Regular/RegularGrammar.lean @@ -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 diff --git a/FormalSystems/Chomsky/Regular/TotalDFA.lean b/FormalSystems/Chomsky/Regular/TotalDFA.lean index 035f0f9..977b8fa 100644 --- a/FormalSystems/Chomsky/Regular/TotalDFA.lean +++ b/FormalSystems/Chomsky/Regular/TotalDFA.lean @@ -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 diff --git a/FormalSystems/Computability/Loop.lean b/FormalSystems/Computability/Loop.lean index 62c5f78..53496e9 100644 --- a/FormalSystems/Computability/Loop.lean +++ b/FormalSystems/Computability/Loop.lean @@ -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 diff --git a/FormalSystems/Preliminaries/Word.lean b/FormalSystems/Preliminaries/Word.lean index 8136943..031f8bb 100644 --- a/FormalSystems/Preliminaries/Word.lean +++ b/FormalSystems/Preliminaries/Word.lean @@ -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 @@ -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 diff --git a/lake-manifest.json b/lake-manifest.json index 0f3d6d2..43e7c6c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -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", @@ -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", @@ -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", @@ -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", diff --git a/lakefile.lean b/lakefile.lean index 4551fd4..976eb13 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -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 diff --git a/lean-toolchain b/lean-toolchain index bd59abf..f96d662 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.5.0 +leanprover/lean4:v4.6.1