From a600d36a88afa3fd4c4e60c1942358d287a51075 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 1 Jul 2025 23:32:58 +1000
Subject: [PATCH 1/4] blindly grinding

---
 LeroyCompilerVerificationCourse/Compil.lean   | 43 ++++---------------
 .../Sequences.lean                            | 33 ++++----------
 2 files changed, 18 insertions(+), 58 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index dd68bd6..3bc6ffc 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -148,30 +148,16 @@ def smart_Ibranch (d: Int) : List instr:=
 
 @[grind =>] theorem instr_a : forall i c2 c1 pc,
   pc = codelen c1 ->
-  instr_at (c1.append (i :: c2) ) pc = .some i := by
+  instr_at (c1 ++ (i :: c2) ) pc = .some i := by
     intro i c2 c1 pc
-    induction c1 generalizing pc
-    case nil =>
-      dsimp [instr_at, codelen]
-      grind
-    case cons h t ih =>
-      dsimp [codelen, instr_at]
-      intro h1
-      split
-      all_goals grind [List.append_eq]
+    induction c1 generalizing pc with grind
 
 @[grind] theorem instr_at_app:
   ∀ i c2 c1 pc,
   pc = codelen c1 ->
-  instr_at (c1.append (i :: c2)) pc = .some i := by
+  instr_at (c1 ++ (i :: c2)) pc = .some i := by
     intro i c2 c1 pc pc_eq
-    induction c1 generalizing pc
-    case nil =>
-      dsimp [instr_at]
-      dsimp [codelen] at pc_eq
-      grind
-    case cons h t t_ih =>
-      grind [instr_at, codelen, List.append_eq]
+    induction c1 generalizing pc with grind
 
 theorem code_at_head :
   forall C pc i C',
@@ -183,15 +169,7 @@ theorem code_at_head :
     induction H
     case code_at_intro c1 c2 c3 oc a =>
       unfold instr_at
-      rw [←heq1]
-      induction c1 generalizing oc
-      case nil =>
-        grind
-      case cons h t t_ih =>
-        have _ : oc ≠ 0 := by grind
-        have _ : t ++ i :: (C' ++ c3) ≠ [] := by grind
-        dsimp
-        grind
+      induction c1 generalizing oc with grind
 
 @[grind] theorem code_at_tail :
    forall C pc i C',
@@ -232,7 +210,7 @@ theorem code_at_head :
     cases h
     case code_at_intro b e a =>
       have := code_at.code_at_intro (b ++ c1) c2 (c3 ++ e) (pc + codelen c1) (by grind)
-      grind [List.append_assoc]
+      grind
 
 @[grind] theorem code_at_nil : forall C pc C1,
   code_at C pc C1 -> code_at C pc [] := by
@@ -256,9 +234,7 @@ theorem code_at_head :
         specialize t_ih (pc - 1) i h
         cases t_ih
         next c1 c3 a =>
-          simp
-          have := code_at.code_at_intro (f :: c1) [] c3 pc
-          grind
+          grind [← code_at.code_at_intro]
       next z =>
         have := code_at.code_at_intro [] [] (f :: t) pc
         grind [List.nil_append]
@@ -303,7 +279,7 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int)
           cases a
           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).append (instr.Iadd :: c3)) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) stk s (aeval s a1) (aeval s 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 *
             grind
     next a1 a2 a1_ih a2_ih =>
@@ -915,8 +891,7 @@ theorem simulation_steps:
         . exact match3
 
 theorem instr_at_len : instr_at (C ++ [i]) (codelen C) = .some i := by
-  induction C
-  any_goals grind
+  induction C with grind
 
 theorem match_initial_configs:
   forall c s,
diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean
index c15f64b..6436166 100644
--- a/LeroyCompilerVerificationCourse/Sequences.lean
+++ b/LeroyCompilerVerificationCourse/Sequences.lean
@@ -53,8 +53,8 @@ inductive plus (R : α → α → Prop) : α → α → Prop where
 theorem plus_one : ∀ a b, R a b → plus R a b := by
   intro a b Rab
   apply plus.plus_left
-  exact Rab
-  apply star.star_refl
+  · exact Rab
+  · grind
 
 @[grind] theorem plus_star : ∀ a b, plus R a b → star R a b := by
     intro a b h
@@ -79,11 +79,8 @@ theorem star_plus_trans:
       grind
     case star_step y a1 a2 =>
       apply plus.plus_left
-      . exact a1
-      . apply star_trans
-        exact a2
-        apply plus_star
-        exact H1
+      · exact a1
+      · grind
 
 theorem plus_right:
   forall a b c, star R a b -> R b c -> plus R a c := by
@@ -103,7 +100,8 @@ def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x →
   constructor
   . exact Rxy
   . intro y' Ryy'
-    apply H y'
+    unfold all_seq_inf at H
+    apply H
     grind
 
 theorem infseq_coinduction_principle_2:
@@ -112,21 +110,8 @@ 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)
-    case x =>
-      apply Exists.elim (h₁ a rel)
-      intro a' _
-      exists a'
-      grind
-    case y =>
-      intro a0 h₂
-      apply Exists.elim h₂
-      intro a1 ⟨ h₃ , h₄ ⟩
-      have h₁' := h₁ a1 h₄
-      apply Exists.elim h₁'
-      intro mid ⟨ h₅, h₆⟩
-      have t := plus_star_trans R a0 a1 mid h₃ h₅
-      cases t
-      any_goals grind
+    apply infseq.fixpoint_induct _ (fun a => ∃ b, star R a b ∧ X b)
+    case x => grind
+    case y => grind [cases plus]
 
 @[grind] def irred (R : α → α → Prop) (a : α) : Prop := forall b, ¬(R a b)

From ac230364b073b815b625c1b41dada0296dce298f Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 2 Jul 2025 05:51:40 +0200
Subject: [PATCH 2/4] turn off warnings

---
 LeroyCompilerVerificationCourse/Compil.lean    | 2 --
 LeroyCompilerVerificationCourse/Constprop.lean | 3 ---
 LeroyCompilerVerificationCourse/Deadcode.lean  | 3 +--
 LeroyCompilerVerificationCourse/Fixpoints.lean | 2 --
 LeroyCompilerVerificationCourse/Imp.lean       | 1 -
 LeroyCompilerVerificationCourse/Sequences.lean | 2 --
 6 files changed, 1 insertion(+), 12 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index 3bc6ffc..eb7e2e3 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -2,8 +2,6 @@ import LeroyCompilerVerificationCourse.Sequences
 import LeroyCompilerVerificationCourse.Imp
 import Init.Data.List.Basic
 
-set_option grind.warning false
-
 @[grind] inductive instr : Type where
   | Iconst (n: Int)
   | Ivar (x: ident)
diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean
index eff2afa..1bedc7e 100644
--- a/LeroyCompilerVerificationCourse/Constprop.lean
+++ b/LeroyCompilerVerificationCourse/Constprop.lean
@@ -13,9 +13,6 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where
       | some v => if e.2 != v then return false
     return true
 
-set_option grind.debug true
-set_option grind.warning false
-
 @[grind] def mk_PLUS_CONST (a: aexp) (n: Int) : aexp :=
   if n = 0 then a else
   match a with
diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean
index 37d55cd..efc6197 100644
--- a/LeroyCompilerVerificationCourse/Deadcode.lean
+++ b/LeroyCompilerVerificationCourse/Deadcode.lean
@@ -3,9 +3,8 @@ import LeroyCompilerVerificationCourse.Imp
 import Init.Data.List.Basic
 import Std.Data.HashSet
 import Std.Data.HashSet.Lemmas
-set_option grind.warning false
-open Classical in
 
+open Classical in
 @[grind] def IdentSet := Std.HashSet ident
   deriving Membership, Union, EmptyCollection
 
diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean
index 96f7fd4..93ff7d6 100644
--- a/LeroyCompilerVerificationCourse/Fixpoints.lean
+++ b/LeroyCompilerVerificationCourse/Fixpoints.lean
@@ -11,8 +11,6 @@ import Init.Data.List.Basic
 
 universe u
 
-set_option grind.warning false
-
 @[grind] class OrderStruct (α : Sort u) where
   eq : α → α → Prop
   le : α → α → Prop
diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean
index f9860f9..b7a0568 100644
--- a/LeroyCompilerVerificationCourse/Imp.lean
+++ b/LeroyCompilerVerificationCourse/Imp.lean
@@ -1,5 +1,4 @@
 import LeroyCompilerVerificationCourse.Sequences
-set_option grind.warning false
 
 def ident := String deriving BEq, Repr, Hashable
 
diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean
index 6436166..7784a74 100644
--- a/LeroyCompilerVerificationCourse/Sequences.lean
+++ b/LeroyCompilerVerificationCourse/Sequences.lean
@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def infseq {α} (R : α → α → Prop) : α → Prop :=
   λ x : α => ∃ y, R x y ∧ infseq R y
  greatest_fixpoint

From e6e125a3c9bf022f997f9db148e894bd7cda75dd Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 2 Jul 2025 06:14:02 +0200
Subject: [PATCH 3/4] .

---
 LeroyCompilerVerificationCourse/Sequences.lean | 9 +++++----
 lean-toolchain                                 | 2 +-
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean
index 7784a74..e96c2ab 100644
--- a/LeroyCompilerVerificationCourse/Sequences.lean
+++ b/LeroyCompilerVerificationCourse/Sequences.lean
@@ -1,17 +1,18 @@
 def infseq {α} (R : α → α → Prop) : α → Prop :=
   λ x : α => ∃ y, R x y ∧ infseq R y
- greatest_fixpoint
+greatest_fixpoint
 
 -- Application of the rewrite rule
 def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
-  infseq R x = ∃ y, R x y ∧ infseq R y := by
-    rw [infseq]
+    infseq R x = ∃ y, R x y ∧ infseq R y := by
+  rw [infseq]
 
 -- 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
+    (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by
   apply infseq.fixpoint_induct
   exact prem
+
 /--
 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✝
diff --git a/lean-toolchain b/lean-toolchain
index b9f9eea..52782c4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.21.0
\ No newline at end of file
+leanprover/lean4:v4.22.0-rc2
\ No newline at end of file

From 6a8b0b6e2a7b1147a071058c0dd720f720b99fa8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 2 Jul 2025 06:35:18 +0200
Subject: [PATCH 4/4] .

---
 LeroyCompilerVerificationCourse/Sequences.lean | 5 ++---
 lake-manifest.json                             | 4 ++--
 lakefile.toml                                  | 8 ++------
 lean-toolchain                                 | 2 +-
 4 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean
index a548e90..746c72b 100644
--- a/LeroyCompilerVerificationCourse/Sequences.lean
+++ b/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
+  greatest_fixpoint
 
 -- Application of the rewrite rule
 def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
@@ -17,7 +17,7 @@ def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
 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
-  exact prem
+  grind
 
 /--
 info: infseq.fixpoint_induct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop)
@@ -28,7 +28,6 @@ info: infseq.fixpoint_induct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x :
 -- 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)
-  intros
   grind
 
 @[grind] inductive star (R : α → α → Prop) : α → α → Prop where
diff --git a/lake-manifest.json b/lake-manifest.json
index fbc9d06..34498a2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "08681ddeb7536a50dea8026c6693cb9b07f01717",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0-rc3",
+   "inputRev": "v4.21.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "LeroyCompilerVerificationCourse",
diff --git a/lakefile.toml b/lakefile.toml
index 41ae5c0..22b60d1 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,16 +1,12 @@
 name = "LeroyCompilerVerificationCourse"
 version = "0.1.0"
-keywords = ["math"]
 defaultTargets = ["LeroyCompilerVerificationCourse"]
 
-[leanOptions]
-pp.unicode.fun = true # pretty-prints `fun a ↦ b`
-autoImplicit = true
-
 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
-rev = "v4.21.0-rc3"
+rev = "v4.21.0"
 
 [[lean_lib]]
 name = "LeroyCompilerVerificationCourse"
+leanOptions = [["grind.warning", false]]
diff --git a/lean-toolchain b/lean-toolchain
index 52782c4..b9f9eea 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.21.0
\ No newline at end of file