chore: bump toolchain to v4.23.0-rc2

LeroyCompilerVerificationCourse/Compil.lean

@@ -133,18 +133,18 @@ def compile_program (p : com) : List instr :=
 def smart_Ibranch (d : Int) : List instr :=
   if d = 0 then [] else .Ibranch d :: []
 
-@[grind] inductive code_at : List instr -> Int -> List instr-> Prop where
+@[grind] inductive code_at : List instr → Int → List instr → Prop where
   | code_at_intro : ∀ C1 C2 C3 pc,
       pc = codelen C1 ->
       code_at (C1 ++ C2 ++ C3) pc C2
 
-@[grind] theorem codelen_cons :
+@[grind =] theorem codelen_cons :
   ∀ i c, codelen (i :: c) = codelen c + 1 := by grind
 
-@[grind] theorem codelen_singleton : codelen [i] = 1 := by
+@[grind =] theorem codelen_singleton : codelen [i] = 1 := by
   dsimp [codelen]
 
-@[grind] theorem codelen_app :
+@[grind =] theorem codelen_app :
   ∀ c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2 := by
     intro c1 _
     induction c1 with grind
@@ -192,7 +192,7 @@ theorem code_at_head :
     cases h
     case code_at_intro c1 c3 a =>
       have := code_at.code_at_intro c1 m1 (m2 ++ c3) pc a
-      grind [List.append_assoc]
+      grind
 
 @[grind] theorem code_at_app_right :
   ∀ C pc C1 C2,
@@ -202,7 +202,7 @@ theorem code_at_head :
     cases h
     case code_at_intro b e a =>
       have := code_at.code_at_intro (b ++ c1) c2 e (pc + codelen c1) (by grind)
-      grind [List.append_assoc]
+      grind
 
 @[grind] theorem code_at_app_right2 : ∀ C pc C1 C2 C3,
   code_at C pc (C1 ++ C2 ++ C3) →
@@ -219,7 +219,7 @@ theorem code_at_head :
     cases h
     case code_at_intro b e a =>
       have := code_at.code_at_intro b [] (c1 ++ e) pc a
-      grind [List.append_nil, List.append_assoc]
+      grind
 
 @[grind] theorem instr_at_code_at_nil :
   ∀ C pc i, instr_at C pc = .some i -> code_at C pc [] := by
@@ -231,21 +231,17 @@ theorem code_at_head :
       by_cases pc = 0
       rotate_left
       next nz =>
-        simp [nz] at h
-        specialize t_ih (pc - 1) i h
-        cases t_ih
-        next c1 c3 a =>
-          grind [← code_at.code_at_intro]
+        grind
       next z =>
         have := code_at.code_at_intro [] [] (f :: t) pc
-        grind [List.nil_append]
+        grind
 
 @[grind] theorem code_at_to_instr_at : code_at C pc (c1 ++ i :: c2) → instr_at C (pc + codelen c1) = .some i := by
     intro h
     cases h
     next b e a =>
       have := instr_at_app i (c2 ++ e) (b ++ c1) (pc + codelen c1) (by simp [codelen]; grind)
-      grind [List.append_assoc, List.append_eq]
+      grind [List.append_eq]
 
 theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int) (stk : stack) :
   code_at C pc (compile_aexp a) →
@@ -298,7 +294,7 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int)
               apply this
               grind
           · apply star_one
-            · have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp])  instr.Iadd [] (by grind [List.append_assoc, List.cons_append, List.nil_append])
+            · have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp])  instr.Iadd [] (by grind)
               have := @transition.trans_add C (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2) + 1) stk s (aeval s a1) (-aeval s a2) (by simp [codelen] at *; grind)
               grind
 -- Miss 5
@@ -318,7 +314,7 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
         simp [is_not_zero, codelen]
         apply transition.trans_branch _ _ _ d1
         · simp [compile_bexp, is_not_zero] at h
-          have := @code_at_to_instr_at C pc [] (instr.Ibranch d1) [] (by grind [List.append_assoc, List.nil_append])
+          have := @code_at_to_instr_at C pc [] (instr.Ibranch d1) [] (by grind)
           grind
         · grind
     next =>
@@ -332,7 +328,7 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
         simp [is_not_zero, codelen]
         apply transition.trans_branch _ _ _ d0
         · simp [compile_bexp, is_not_zero] at h
-          have := @code_at_to_instr_at C pc [] (instr.Ibranch d0) [] (by grind [List.append_assoc, List.nil_append])
+          have := @code_at_to_instr_at C pc [] (instr.Ibranch d0) [] (by grind)
           grind
         · grind
     next a1 a2 =>
@@ -712,7 +708,7 @@ theorem simulation_step :
             case neg isFalse =>
               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])
+              have := @code_at_app_right C pc (codeb ++ code1 ++ [instr.Ibranch (codelen code2)]) code2 (by grind)
               simp [codelen_cons, codelen_app] at this
               simp [codelen] at *
               grind
@@ -851,7 +847,7 @@ theorem match_initial_configs :
     constructor
     · simp [compile_program]
       have := code_at.code_at_intro [] C [instr.Ihalt] 0 (by simp [codelen])
-      grind [List.nil_append]
+      grind
     · simp [compile_program, heq]
       constructor
       grind

LeroyCompilerVerificationCourse/Constprop.lean

@@ -412,7 +412,7 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint
           · apply Le_Join_l
           · exact MATCHES
 
-@[grind] def cp_aexp (S : Store) (a : aexp) : aexp :=
+@[grind =] def cp_aexp (S : Store) (a : aexp) : aexp :=
   match a with
   | .CONST n => .CONST n
   | .VAR x => match S.get? x with
@@ -435,7 +435,10 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint
   ∀ s S, matches' s S ->
   ∀ a, aeval s (cp_aexp S a) = aeval s a := by
     intro s S AG a
-    induction a <;> grind [mk_PLUS_sound, mk_MINUS_sound]
+    induction a
+    all_goals try grind
+    -- Unfortunately this grind call explodes on one of the goals since v4.23.0-rc2
+    all_goals grind [mk_PLUS_sound, mk_MINUS_sound]
 
 theorem cp_bexp_sound :
   ∀ s S, matches' s S ->

LeroyCompilerVerificationCourse/Deadcode.lean

@@ -32,7 +32,7 @@ open Classical in
 
 
 @[grind] theorem insert_characterisation (a : IdentSet) (x : ident) : x ∈ a.insert x := by
-  grind [Std.HashSet.contains_insert]
+  grind
 
 @[grind] def fv_aexp (a : aexp) : IdentSet :=
   match a with

LeroyCompilerVerificationCourse/Fixpoints.lean

@@ -155,7 +155,7 @@ theorem hash_set_incl_size_leq (S1 S2 : Store) : Le S2 S1 → List.Subperm (S1.t
   Le T S ->
   S.size <= T.size ∧ (S.size = T.size → Equal S T) := by
     intro S T hyp
-    have size_eq : ∀ (S : Store), S.size = S.toList.length := by grind [length_toList]
+    have size_eq : ∀ (S : Store), S.size = S.toList.length := by grind
     rw [size_eq S, size_eq T]
     constructor
     case left =>

LeroyCompilerVerificationCourse/Imp.lean

@@ -328,12 +328,6 @@ theorem red_progress :
     intro c
     induction c
     any_goals grind
-    case ASSIGN identifier expression =>
-      intro s
-      apply Or.intro_right
-      exists com.SKIP
-      exists update identifier (aeval s expression) s
-      grind
     case SEQ c1 c2 c1_ih c2_ih =>
       intro s
       apply Or.intro_right
@@ -352,48 +346,6 @@ theorem red_progress :
         exists .SEQ c1' c2
         exists s'
         grind
-    case IFTHENELSE b c1 c2 c1_ih c2_ih =>
-      intro s
-      apply Or.intro_right
-      have h : beval s b = true ∨ beval s b = false := by grind
-      apply Or.elim h
-      case h.left =>
-        intro is_true
-        apply Or.elim (c1_ih s)
-        case left =>
-          intro c1_skip
-          exists .SKIP
-          exists s
-          grind
-        case right => grind
-      case h.right =>
-        intro is_false
-        apply Or.elim (c2_ih s)
-        case left =>
-          intro c2_skip
-          exists .SKIP
-          exists s
-          grind
-        case right => grind
-    case WHILE b c ih =>
-      intro s
-      apply Or.intro_right
-      have h : beval s b = true ∨ beval s b = false := by grind
-      apply Or.elim h
-      case left =>
-        intro _
-        apply Or.elim (ih s)
-        any_goals grind
-        case left =>
-          intro _
-          exists (.SEQ .SKIP  (.WHILE b c))
-          exists s
-          grind
-      case right =>
-        intros
-        exists .SKIP
-        exists s
-        grind
 
 def goes_wrong (c : com) (s : store) : Prop := ∃ c', ∃ s', star red (c, s) (c', s') ∧ irred red (c', s') ∧ c' ≠ .SKIP
 

LeroyCompilerVerificationCourse/Sequences.lean

@@ -20,8 +20,8 @@ theorem infseq_coinduction_principle {α} (h : α → Prop) (R : α → α → P
   grind
 
 /--
-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✝
+info: infseq.coinduct.{u_1} {α : Sort u_1} (R : α → α → Prop) (pred : α → Prop)
+  (hyp : ∀ (x : α), pred x → ∃ y, R x y ∧ pred y) (x✝ : α) : pred x✝ → infseq R x✝
 -/
 #guard_msgs in #check infseq.coinduct
 

lake-manifest.json

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

lakefile.toml

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

lean-toolchain

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