chore: bump toolchain to v4.22.0-rc2

LeroyCompilerVerificationCourse/Compil.lean

@@ -284,7 +284,7 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int)
           next c1 c3 a =>
             have h1 := instr_a instr.Iadd c3 (c1 ++ compile_aexp a1 ++ compile_aexp a2) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) (by grind)
             have h2 := @transition.trans_add ((c1 ++ compile_aexp a1 ++ compile_aexp a2) ++ (instr.Iadd :: c3)) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) stk s (aeval s a1) (aeval s a2) (by grind)
-            simp [codelen_app, codelen_cons, codelen] at *
+            simp [codelen] at *
             grind
     next a1 a2 a1_ih a2_ih =>
       simp [aeval, compile_aexp]
@@ -456,7 +456,7 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
       apply code_at_app_left
       exact h
     . specialize c2_ih C (pc + codelen (compile_com c1)) stk
-      simp [compile_com, codelen_app, Int.add_assoc]
+      simp [compile_com, codelen_app]
       simp [Int.add_assoc] at c2_ih
       apply c2_ih
       grind
@@ -763,7 +763,7 @@ theorem simulation_step:
               simp [isFalse] at *
               rw [h₅]
               have := @code_at_app_right C pc (codeb ++ code1 ++ [instr.Ibranch (codelen code2)]) code2 (by grind [List.append_assoc, List.cons_append, List.nil_append])
-              simp [codelen_cons, codelen_singleton, codelen_app] at this
+              simp [codelen_cons, codelen_app] at this
               simp [codelen] at *
               grind
           . by_cases beval st b = true

LeroyCompilerVerificationCourse/Fixpoints.lean

@@ -365,7 +365,7 @@ noncomputable def Cexec' : (c : com) →  {F : Store → Store // ∀ x y, le x
       generalize heq : Beval y b = h
       cases h
       case none =>
-        simp [heq]
+        simp
         apply le_trans
         rotate_right
         . exact Join (f₁ x) (f₂ x)

LeroyCompilerVerificationCourse/Sequences.lean

@@ -6,7 +6,7 @@ Authors: Wojciech Różowski
 
 def infseq {α} (R : α → α → Prop) : α → Prop :=
   λ x : α => ∃ y, R x y ∧ infseq R y
-  greatest_fixpoint
+  coinductive_fixpoint
 
 -- Application of the rewrite rule
 def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
@@ -16,18 +16,18 @@ def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
 -- The associated coinduction principle
 theorem infseq.coind {α} (h : α → Prop) (R : α → α → Prop)
     (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by
-  apply infseq.fixpoint_induct
+  apply infseq.coinduct
   grind
 
 /--
-info: infseq.fixpoint_induct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop)
-  (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y) (x✝ : α) : x x✝ → infseq R x✝
+info: infseq.coinduct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop) (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y)
+  (x✝ : α) : x x✝ → infseq R x✝
 -/
-#guard_msgs in #check infseq.fixpoint_induct
+#guard_msgs in #check infseq.coinduct
 
 -- Simple proof by coinduction
 theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x := by
-  apply infseq.fixpoint_induct R (λ m => R m m)
+  apply infseq.coinduct R (λ m => R m m)
   grind
 
 @[grind] inductive star (R : α → α → Prop) : α → α → Prop where
@@ -96,7 +96,7 @@ def all_seq_inf (R : α → α → Prop) (x : α) : Prop :=
   ∀ y : α, star R x y → ∃ z, R y z
 
 def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → infseq R x := by
-  apply infseq.fixpoint_induct
+  apply infseq.coinduct
   intro x H
   apply Exists.elim (H x (by simp only [star.star_refl]))
   intro y Rxy
@@ -114,7 +114,7 @@ theorem infseq_coinduction_principle_2:
   ∀ (a : α), x a → infseq R a := by
     intro X
     intro h₁ a rel
-    apply infseq.fixpoint_induct _ (fun a => ∃ b, star R a b ∧ X b)
+    apply infseq.coinduct _ (fun a => ∃ b, star R a b ∧ X b)
     case x => grind
     case y => grind [cases plus]
 

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "rev": "3adabe76bed51fc81d04ae65bb7c3893333e3d63",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.22.0-rc2",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "LeroyCompilerVerificationCourse",

lakefile.toml

@@ -5,7 +5,7 @@ defaultTargets = ["LeroyCompilerVerificationCourse"]
 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
-rev = "v4.21.0"
+rev = "v4.22.0-rc2"
 
 [[lean_lib]]
 name = "LeroyCompilerVerificationCourse"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.21.0
+leanprover/lean4:v4.22.0-rc2