Upgrade to Lean 4.6.1

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

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

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

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

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

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",

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.1