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 01/10] 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 57ea62b30597f932295be9495e7a11179733d8a2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 2 Jul 2025 09:51:01 +1000
Subject: [PATCH 02/10] .

---
 LeroyCompilerVerificationCourse/Deadcode.lean | 17 +++++------------
 1 file changed, 5 insertions(+), 12 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean
index 37d55cd..faf3588 100644
--- a/LeroyCompilerVerificationCourse/Deadcode.lean
+++ b/LeroyCompilerVerificationCourse/Deadcode.lean
@@ -84,12 +84,7 @@ theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F
       unfold instHasSubsetIdentSet
       grind
     case succ n ih =>
-      unfold deadcode_fixpoint_rec
-      simp
-      intro x hyp
-      split
-      case isTrue => grind
-      case isFalse => grind
+      grind
   apply this
   unfold Subset
   unfold instHasSubsetIdentSet
@@ -157,7 +152,6 @@ theorem live_upper_bound:
       have : y ∈ fv_bexp b ∨ y ∈ L ∨ y ∈ live c1 x := by grind
       apply Or.elim this
       next =>
-        intro hyp3
         grind
       next =>
         intro hyp3
@@ -169,7 +163,7 @@ theorem live_upper_bound:
           specialize c1_ih x y hyp3
           have : y ∈ fv_com c1 ∨ y ∈ x := by grind
           apply Or.elim this
-          next => intros; grind
+          next => grind
           next =>
             intro hyp4
             specialize hyp y hyp4
@@ -185,18 +179,17 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet)
       constructor
       case left =>
         intro y contained
-        specialize included y (by grind)
+        specialize included y
         grind
       case right =>
         constructor
         case left =>
           intro y mem
-          specialize included y (by grind)
+          specialize included y
           grind
         case right =>
           intro y mem
-          rw [eq]
-          specialize included y (by grind)
+          specialize included y
           grind
     case right =>
       intro equal

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 03/10] 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 329da85966daf541f0b4eebd23ed02c939e6d9d7 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 2 Jul 2025 05:53:42 +0200
Subject: [PATCH 04/10] chore: silence build

---
 LeroyCompilerVerificationCourse/Compil.lean    | 2 ++
 LeroyCompilerVerificationCourse/Constprop.lean | 2 ++
 LeroyCompilerVerificationCourse/Fixpoints.lean | 2 --
 LeroyCompilerVerificationCourse/Imp.lean       | 4 ++--
 4 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index dd68bd6..00b5f49 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -124,6 +124,8 @@ def machine_goes_wrong (C: List instr) (s_init: store) : Prop :=
 def compile_program (p: com) : List instr:=
   compile_com p ++ .Ihalt :: []
 
+/-- info: [instr.Ivar "x", instr.Iconst 1, instr.Iadd, instr.Isetvar "x", instr.Ihalt] -/
+#guard_msgs in
 #eval (compile_program (.ASSIGN "x" (.PLUS (.VAR "x") (.CONST 1))))
 
 def smart_Ibranch (d: Int) : List instr:=
diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean
index eff2afa..02b01c2 100644
--- a/LeroyCompilerVerificationCourse/Constprop.lean
+++ b/LeroyCompilerVerificationCourse/Constprop.lean
@@ -47,6 +47,8 @@ set_option grind.warning false
   | .PLUS a1 a2 => mk_PLUS (simplif_aexp a1) (simplif_aexp a2)
   | .MINUS a1 a2 => mk_MINUS (simplif_aexp a1) (simplif_aexp a2)
 
+/-- info: aexp.MINUS (aexp.VAR "x") (aexp.VAR "y") -/
+#guard_msgs in
 #eval simplif_aexp (.MINUS (.PLUS (.VAR "x") (.CONST 1)) (.PLUS (.VAR "y") (.CONST 1)))
 
 @[grind] theorem mk_PLUS_CONST_sound:
diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean
index 96f7fd4..b9da5e5 100644
--- a/LeroyCompilerVerificationCourse/Fixpoints.lean
+++ b/LeroyCompilerVerificationCourse/Fixpoints.lean
@@ -80,8 +80,6 @@ instance : WellFoundedRelation α  where
   decreasing_by
     grind [beq_false']
 
-#check iterate
-
 @[grind] theorem iterate_correct (x : α) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z) (heq : y = iterate _ F x PRE SMALL ) : eq y (F y) ∧ ∀ z, le (F z) z → le y z := by
   fun_induction iterate
   case case1 x' PRE SMALL isTrue  =>
diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean
index f9860f9..a3b2a91 100644
--- a/LeroyCompilerVerificationCourse/Imp.lean
+++ b/LeroyCompilerVerificationCourse/Imp.lean
@@ -18,6 +18,8 @@ def store : Type := ident → Int
   | .PLUS a1 a2 => aeval s a1 + aeval s a2
   | .MINUS a1 a2 => aeval s a1 - aeval s a2
 
+/-- info: 3 -/
+#guard_msgs in
 #eval aeval (λ _ => 2) (.PLUS (.VAR "x") (.MINUS (.VAR "x") (.CONST 1)))
 
 theorem aeval_xplus1 : ∀ s x, aeval s (.PLUS (.VAR x) (.CONST 1)) > aeval s (.VAR x) := by
@@ -76,8 +78,6 @@ inductive com: Type where
 
 notation:10 l:10 " ;; " r:11 => com.SEQ l r
 
-#check .SKIP ;; .SKIP
-
 def Euclidean_division :=
   .ASSIGN "r" (.VAR "a") ;;
   .ASSIGN "q" (.CONST 0) ;;

From 23696c58c5f97afae5c3f9671ab84dbd433cfbbc Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 2 Jul 2025 06:03:20 +0200
Subject: [PATCH 05/10] Add copyright headers and documentation

- Add copyright headers to all Lean files
- Create COPYRIGHT.md with derivative work acknowledgment
- Update README.md with project description
- Credit original work by Xavier Leroy and port authors
---
 COPYRIGHT.md                                  |   6 +
 LICENSE.md                                    | 502 ++++++++++++++++++
 LeroyCompilerVerificationCourse.lean          |   6 +
 LeroyCompilerVerificationCourse/Compil.lean   |   6 +
 .../Constprop.lean                            |   6 +
 LeroyCompilerVerificationCourse/Deadcode.lean |   6 +
 .../Fixpoints.lean                            |   6 +
 LeroyCompilerVerificationCourse/Imp.lean      |   6 +
 .../Sequences.lean                            |   6 +
 README.md                                     |   4 +-
 10 files changed, 553 insertions(+), 1 deletion(-)
 create mode 100644 COPYRIGHT.md
 create mode 100644 LICENSE.md

diff --git a/COPYRIGHT.md b/COPYRIGHT.md
new file mode 100644
index 0000000..7612bda
--- /dev/null
+++ b/COPYRIGHT.md
@@ -0,0 +1,6 @@
+# Copyright Notice
+
+This project is a derivative work based on Xavier Leroy's [EUTypes 2019 summer school course on "Proving the correctness of a compiler"](https://xavierleroy.org/courses/EUTypes-2019/). Both works are licensed under the GNU Lesser General Public License version 2.1.
+
+This project ports the original Rocq implementation to Lean,
+and adapts the pedagogical material to the new implementation.
\ No newline at end of file
diff --git a/LICENSE.md b/LICENSE.md
new file mode 100644
index 0000000..6ac1b0b
--- /dev/null
+++ b/LICENSE.md
@@ -0,0 +1,502 @@
+# GNU LESSER GENERAL PUBLIC LICENSE
+
+Version 2.1, February 1999
+
+    Copyright (C) 1991, 1999 Free Software Foundation, Inc.
+    <https://fsf.org/>
+    
+    Everyone is permitted to copy and distribute verbatim copies
+    of this license document, but changing it is not allowed.
+
+    [This is the first released version of the Lesser GPL.  It also counts
+     as the successor of the GNU Library Public License, version 2, hence
+     the version number 2.1.]
+
+## Preamble
+
+The licenses for most software are designed to take away your freedom
+to share and change it. By contrast, the GNU General Public Licenses
+are intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users.
+
+This license, the Lesser General Public License, applies to some
+specially designated software packages--typically libraries--of the
+Free Software Foundation and other authors who decide to use it. You
+can use it too, but we suggest you first think carefully about whether
+this license or the ordinary General Public License is the better
+strategy to use in any particular case, based on the explanations
+below.
+
+When we speak of free software, we are referring to freedom of use,
+not price. Our General Public Licenses are designed to make sure that
+you have the freedom to distribute copies of free software (and charge
+for this service if you wish); that you receive source code or can get
+it if you want it; that you can change the software and use pieces of
+it in new free programs; and that you are informed that you can do
+these things.
+
+To protect your rights, we need to make restrictions that forbid
+distributors to deny you these rights or to ask you to surrender these
+rights. These restrictions translate to certain responsibilities for
+you if you distribute copies of the library or if you modify it.
+
+For example, if you distribute copies of the library, whether gratis
+or for a fee, you must give the recipients all the rights that we gave
+you. You must make sure that they, too, receive or can get the source
+code. If you link other code with the library, you must provide
+complete object files to the recipients, so that they can relink them
+with the library after making changes to the library and recompiling
+it. And you must show them these terms so they know their rights.
+
+We protect your rights with a two-step method: (1) we copyright the
+library, and (2) we offer you this license, which gives you legal
+permission to copy, distribute and/or modify the library.
+
+To protect each distributor, we want to make it very clear that there
+is no warranty for the free library. Also, if the library is modified
+by someone else and passed on, the recipients should know that what
+they have is not the original version, so that the original author's
+reputation will not be affected by problems that might be introduced
+by others.
+
+Finally, software patents pose a constant threat to the existence of
+any free program. We wish to make sure that a company cannot
+effectively restrict the users of a free program by obtaining a
+restrictive license from a patent holder. Therefore, we insist that
+any patent license obtained for a version of the library must be
+consistent with the full freedom of use specified in this license.
+
+Most GNU software, including some libraries, is covered by the
+ordinary GNU General Public License. This license, the GNU Lesser
+General Public License, applies to certain designated libraries, and
+is quite different from the ordinary General Public License. We use
+this license for certain libraries in order to permit linking those
+libraries into non-free programs.
+
+When a program is linked with a library, whether statically or using a
+shared library, the combination of the two is legally speaking a
+combined work, a derivative of the original library. The ordinary
+General Public License therefore permits such linking only if the
+entire combination fits its criteria of freedom. The Lesser General
+Public License permits more lax criteria for linking other code with
+the library.
+
+We call this license the "Lesser" General Public License because it
+does Less to protect the user's freedom than the ordinary General
+Public License. It also provides other free software developers Less
+of an advantage over competing non-free programs. These disadvantages
+are the reason we use the ordinary General Public License for many
+libraries. However, the Lesser license provides advantages in certain
+special circumstances.
+
+For example, on rare occasions, there may be a special need to
+encourage the widest possible use of a certain library, so that it
+becomes a de-facto standard. To achieve this, non-free programs must
+be allowed to use the library. A more frequent case is that a free
+library does the same job as widely used non-free libraries. In this
+case, there is little to gain by limiting the free library to free
+software only, so we use the Lesser General Public License.
+
+In other cases, permission to use a particular library in non-free
+programs enables a greater number of people to use a large body of
+free software. For example, permission to use the GNU C Library in
+non-free programs enables many more people to use the whole GNU
+operating system, as well as its variant, the GNU/Linux operating
+system.
+
+Although the Lesser General Public License is Less protective of the
+users' freedom, it does ensure that the user of a program that is
+linked with the Library has the freedom and the wherewithal to run
+that program using a modified version of the Library.
+
+The precise terms and conditions for copying, distribution and
+modification follow. Pay close attention to the difference between a
+"work based on the library" and a "work that uses the library". The
+former contains code derived from the library, whereas the latter must
+be combined with the library in order to run.
+
+## TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+**0.** This License Agreement applies to any software library or other
+program which contains a notice placed by the copyright holder or
+other authorized party saying it may be distributed under the terms of
+this Lesser General Public License (also called "this License"). Each
+licensee is addressed as "you".
+
+A "library" means a collection of software functions and/or data
+prepared so as to be conveniently linked with application programs
+(which use some of those functions and data) to form executables.
+
+The "Library", below, refers to any such software library or work
+which has been distributed under these terms. A "work based on the
+Library" means either the Library or any derivative work under
+copyright law: that is to say, a work containing the Library or a
+portion of it, either verbatim or with modifications and/or translated
+straightforwardly into another language. (Hereinafter, translation is
+included without limitation in the term "modification".)
+
+"Source code" for a work means the preferred form of the work for
+making modifications to it. For a library, complete source code means
+all the source code for all modules it contains, plus any associated
+interface definition files, plus the scripts used to control
+compilation and installation of the library.
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope. The act of
+running a program using the Library is not restricted, and output from
+such a program is covered only if its contents constitute a work based
+on the Library (independent of the use of the Library in a tool for
+writing it). Whether that is true depends on what the Library does and
+what the program that uses the Library does.
+
+**1.** You may copy and distribute verbatim copies of the Library's
+complete source code as you receive it, in any medium, provided that
+you conspicuously and appropriately publish on each copy an
+appropriate copyright notice and disclaimer of warranty; keep intact
+all the notices that refer to this License and to the absence of any
+warranty; and distribute a copy of this License along with the
+Library.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a
+fee.
+
+**2.** You may modify your copy or copies of the Library or any
+portion of it, thus forming a work based on the Library, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+-   **a)** The modified work must itself be a software library.
+-   **b)** You must cause the files modified to carry prominent
+    notices stating that you changed the files and the date of
+    any change.
+-   **c)** You must cause the whole of the work to be licensed at no
+    charge to all third parties under the terms of this License.
+-   **d)** If a facility in the modified Library refers to a function
+    or a table of data to be supplied by an application program that
+    uses the facility, other than as an argument passed when the
+    facility is invoked, then you must make a good faith effort to
+    ensure that, in the event an application does not supply such
+    function or table, the facility still operates, and performs
+    whatever part of its purpose remains meaningful.
+
+    (For example, a function in a library to compute square roots has
+    a purpose that is entirely well-defined independent of
+    the application. Therefore, Subsection 2d requires that any
+    application-supplied function or table used by this function must
+    be optional: if the application does not supply it, the square
+    root function must still compute square roots.)
+
+These requirements apply to the modified work as a whole. If
+identifiable sections of that work are not derived from the Library,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works. But when you
+distribute the same sections as part of a whole which is a work based
+on the Library, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote
+it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Library.
+
+In addition, mere aggregation of another work not based on the Library
+with the Library (or with a work based on the Library) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+**3.** You may opt to apply the terms of the ordinary GNU General
+Public License instead of this License to a given copy of the Library.
+To do this, you must alter all the notices that refer to this License,
+so that they refer to the ordinary GNU General Public License, version
+2, instead of to this License. (If a newer version than version 2 of
+the ordinary GNU General Public License has appeared, then you can
+specify that version instead if you wish.) Do not make any other
+change in these notices.
+
+Once this change is made in a given copy, it is irreversible for that
+copy, so the ordinary GNU General Public License applies to all
+subsequent copies and derivative works made from that copy.
+
+This option is useful when you wish to copy part of the code of the
+Library into a program that is not a library.
+
+**4.** You may copy and distribute the Library (or a portion or
+derivative of it, under Section 2) in object code or executable form
+under the terms of Sections 1 and 2 above provided that you accompany
+it with the complete corresponding machine-readable source code, which
+must be distributed under the terms of Sections 1 and 2 above on a
+medium customarily used for software interchange.
+
+If distribution of object code is made by offering access to copy from
+a designated place, then offering equivalent access to copy the source
+code from the same place satisfies the requirement to distribute the
+source code, even though third parties are not compelled to copy the
+source along with the object code.
+
+**5.** A program that contains no derivative of any portion of the
+Library, but is designed to work with the Library by being compiled or
+linked with it, is called a "work that uses the Library". Such a work,
+in isolation, is not a derivative work of the Library, and therefore
+falls outside the scope of this License.
+
+However, linking a "work that uses the Library" with the Library
+creates an executable that is a derivative of the Library (because it
+contains portions of the Library), rather than a "work that uses the
+library". The executable is therefore covered by this License. Section
+6 states terms for distribution of such executables.
+
+When a "work that uses the Library" uses material from a header file
+that is part of the Library, the object code for the work may be a
+derivative work of the Library even though the source code is not.
+Whether this is true is especially significant if the work can be
+linked without the Library, or if the work is itself a library. The
+threshold for this to be true is not precisely defined by law.
+
+If such an object file uses only numerical parameters, data structure
+layouts and accessors, and small macros and small inline functions
+(ten lines or less in length), then the use of the object file is
+unrestricted, regardless of whether it is legally a derivative work.
+(Executables containing this object code plus portions of the Library
+will still fall under Section 6.)
+
+Otherwise, if the work is a derivative of the Library, you may
+distribute the object code for the work under the terms of Section 6.
+Any executables containing that work also fall under Section 6,
+whether or not they are linked directly with the Library itself.
+
+**6.** As an exception to the Sections above, you may also combine or
+link a "work that uses the Library" with the Library to produce a work
+containing portions of the Library, and distribute that work under
+terms of your choice, provided that the terms permit modification of
+the work for the customer's own use and reverse engineering for
+debugging such modifications.
+
+You must give prominent notice with each copy of the work that the
+Library is used in it and that the Library and its use are covered by
+this License. You must supply a copy of this License. If the work
+during execution displays copyright notices, you must include the
+copyright notice for the Library among them, as well as a reference
+directing the user to the copy of this License. Also, you must do one
+of these things:
+
+-   **a)** Accompany the work with the complete corresponding
+    machine-readable source code for the Library including whatever
+    changes were used in the work (which must be distributed under
+    Sections 1 and 2 above); and, if the work is an executable linked
+    with the Library, with the complete machine-readable "work that
+    uses the Library", as object code and/or source code, so that the
+    user can modify the Library and then relink to produce a modified
+    executable containing the modified Library. (It is understood that
+    the user who changes the contents of definitions files in the
+    Library will not necessarily be able to recompile the application
+    to use the modified definitions.)
+-   **b)** Use a suitable shared library mechanism for linking with
+    the Library. A suitable mechanism is one that (1) uses at run time
+    a copy of the library already present on the user's computer
+    system, rather than copying library functions into the executable,
+    and (2) will operate properly with a modified version of the
+    library, if the user installs one, as long as the modified version
+    is interface-compatible with the version that the work was
+    made with.
+-   **c)** Accompany the work with a written offer, valid for at least
+    three years, to give the same user the materials specified in
+    Subsection 6a, above, for a charge no more than the cost of
+    performing this distribution.
+-   **d)** If distribution of the work is made by offering access to
+    copy from a designated place, offer equivalent access to copy the
+    above specified materials from the same place.
+-   **e)** Verify that the user has already received a copy of these
+    materials or that you have already sent this user a copy.
+
+For an executable, the required form of the "work that uses the
+Library" must include any data and utility programs needed for
+reproducing the executable from it. However, as a special exception,
+the materials to be distributed need not include anything that is
+normally distributed (in either source or binary form) with the major
+components (compiler, kernel, and so on) of the operating system on
+which the executable runs, unless that component itself accompanies
+the executable.
+
+It may happen that this requirement contradicts the license
+restrictions of other proprietary libraries that do not normally
+accompany the operating system. Such a contradiction means you cannot
+use both them and the Library together in an executable that you
+distribute.
+
+**7.** You may place library facilities that are a work based on the
+Library side-by-side in a single library together with other library
+facilities not covered by this License, and distribute such a combined
+library, provided that the separate distribution of the work based on
+the Library and of the other library facilities is otherwise
+permitted, and provided that you do these two things:
+
+-   **a)** Accompany the combined library with a copy of the same work
+    based on the Library, uncombined with any other
+    library facilities. This must be distributed under the terms of
+    the Sections above.
+-   **b)** Give prominent notice with the combined library of the fact
+    that part of it is a work based on the Library, and explaining
+    where to find the accompanying uncombined form of the same work.
+
+**8.** You may not copy, modify, sublicense, link with, or distribute
+the Library except as expressly provided under this License. Any
+attempt otherwise to copy, modify, sublicense, link with, or
+distribute the Library is void, and will automatically terminate your
+rights under this License. However, parties who have received copies,
+or rights, from you under this License will not have their licenses
+terminated so long as such parties remain in full compliance.
+
+**9.** You are not required to accept this License, since you have not
+signed it. However, nothing else grants you permission to modify or
+distribute the Library or its derivative works. These actions are
+prohibited by law if you do not accept this License. Therefore, by
+modifying or distributing the Library (or any work based on the
+Library), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Library or works based on it.
+
+**10.** Each time you redistribute the Library (or any work based on
+the Library), the recipient automatically receives a license from the
+original licensor to copy, distribute, link with or modify the Library
+subject to these terms and conditions. You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties with
+this License.
+
+**11.** If, as a consequence of a court judgment or allegation of
+patent infringement or for any other reason (not limited to patent
+issues), conditions are imposed on you (whether by court order,
+agreement or otherwise) that contradict the conditions of this
+License, they do not excuse you from the conditions of this License.
+If you cannot distribute so as to satisfy simultaneously your
+obligations under this License and any other pertinent obligations,
+then as a consequence you may not distribute the Library at all. For
+example, if a patent license would not permit royalty-free
+redistribution of the Library by all those who receive copies directly
+or indirectly through you, then the only way you could satisfy both it
+and this License would be to refrain entirely from distribution of the
+Library.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply, and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system which is
+implemented by public license practices. Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+**12.** If the distribution and/or use of the Library is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Library under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded. In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+**13.** The Free Software Foundation may publish revised and/or new
+versions of the Lesser General Public License from time to time. Such
+new versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Library
+specifies a version number of this License which applies to it and
+"any later version", you have the option of following the terms and
+conditions either of that version or of any later version published by
+the Free Software Foundation. If the Library does not specify a
+license version number, you may choose any version ever published by
+the Free Software Foundation.
+
+**14.** If you wish to incorporate parts of the Library into other
+free programs whose distribution conditions are incompatible with
+these, write to the author to ask for permission. For software which
+is copyrighted by the Free Software Foundation, write to the Free
+Software Foundation; we sometimes make exceptions for this. Our
+decision will be guided by the two goals of preserving the free status
+of all derivatives of our free software and of promoting the sharing
+and reuse of software generally.
+
+**NO WARRANTY**
+
+**15.** BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO
+WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW.
+EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR
+OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY
+KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
+LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME
+THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+**16.** IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN
+WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY
+AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU
+FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR
+CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE
+LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
+RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
+FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF
+SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGES.
+
+END OF TERMS AND CONDITIONS
+
+## How to Apply These Terms to Your New Libraries
+
+If you develop a new library, and you want it to be of the greatest
+possible use to the public, we recommend making it free software that
+everyone can redistribute and change. You can do so by permitting
+redistribution under these terms (or, alternatively, under the terms
+of the ordinary General Public License).
+
+To apply these terms, attach the following notices to the library. It
+is safest to attach them to the start of each source file to most
+effectively convey the exclusion of warranty; and each file should
+have at least the "copyright" line and a pointer to where the full
+notice is found.
+
+    one line to give the library's name and an idea of what it does.
+    Copyright (C) year  name of author
+
+    This library is free software; you can redistribute it and/or
+    modify it under the terms of the GNU Lesser General Public
+    License as published by the Free Software Foundation; either
+    version 2.1 of the License, or (at your option) any later version.
+
+    This library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+    Lesser General Public License for more details.
+
+    You should have received a copy of the GNU Lesser General Public
+    License along with this library; if not, see <https://www.gnu.org/licenses/>.
+
+Also add information on how to contact you by electronic and paper
+mail.
+
+You should also get your employer (if you work as a programmer) or
+your school, if any, to sign a "copyright disclaimer" for the library,
+if necessary. Here is a sample; alter the names:
+
+    Yoyodyne, Inc., hereby disclaims all copyright interest in
+    the library `Frob' (a library for tweaking knobs) written
+    by James Random Hacker.
+
+    signature of Moe Ghoul, 1 April 1990
+    Moe Ghoul, President of Vice
+
+That's all there is to it!
diff --git a/LeroyCompilerVerificationCourse.lean b/LeroyCompilerVerificationCourse.lean
index 8fa57b2..22431fe 100644
--- a/LeroyCompilerVerificationCourse.lean
+++ b/LeroyCompilerVerificationCourse.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under LGPL 2.1 license as described in the file LICENSE.md.
+Authors: Wojciech Różowski
+-/
+
 -- This module serves as the root of the `LeroyCompilerVerificationCourse` library.
 -- Import modules here that should be built as part of the library.
 import LeroyCompilerVerificationCourse.Imp
diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index dd68bd6..fb001a2 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under LGPL 2.1 license as described in the file LICENSE.md.
+Authors: Wojciech Różowski
+-/
+
 import LeroyCompilerVerificationCourse.Sequences
 import LeroyCompilerVerificationCourse.Imp
 import Init.Data.List.Basic
diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean
index eff2afa..57845c7 100644
--- a/LeroyCompilerVerificationCourse/Constprop.lean
+++ b/LeroyCompilerVerificationCourse/Constprop.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under LGPL 2.1 license as described in the file LICENSE.md.
+Authors: Wojciech Różowski
+-/
+
 import LeroyCompilerVerificationCourse.Sequences
 import LeroyCompilerVerificationCourse.Imp
 import Init.Data.List.Basic
diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean
index 37d55cd..9de3d73 100644
--- a/LeroyCompilerVerificationCourse/Deadcode.lean
+++ b/LeroyCompilerVerificationCourse/Deadcode.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under LGPL 2.1 license as described in the file LICENSE.md.
+Authors: Wojciech Różowski
+-/
+
 import LeroyCompilerVerificationCourse.Sequences
 import LeroyCompilerVerificationCourse.Imp
 import Init.Data.List.Basic
diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean
index 96f7fd4..2865ecd 100644
--- a/LeroyCompilerVerificationCourse/Fixpoints.lean
+++ b/LeroyCompilerVerificationCourse/Fixpoints.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under LGPL 2.1 license as described in the file LICENSE.md.
+Authors: Wojciech Różowski
+-/
+
 import LeroyCompilerVerificationCourse.Imp
 import LeroyCompilerVerificationCourse.Constprop
 import Init.WF
diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean
index f9860f9..88206fa 100644
--- a/LeroyCompilerVerificationCourse/Imp.lean
+++ b/LeroyCompilerVerificationCourse/Imp.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under LGPL 2.1 license as described in the file LICENSE.md.
+Authors: Wojciech Różowski
+-/
+
 import LeroyCompilerVerificationCourse.Sequences
 set_option grind.warning false
 
diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean
index c15f64b..92db327 100644
--- a/LeroyCompilerVerificationCourse/Sequences.lean
+++ b/LeroyCompilerVerificationCourse/Sequences.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under LGPL 2.1 license as described in the file LICENSE.md.
+Authors: Wojciech Różowski
+-/
+
 set_option grind.warning false
 
 def infseq {α} (R : α → α → Prop) : α → Prop :=
diff --git a/README.md b/README.md
index d64e388..48fc9d8 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,3 @@
-# LeroyCompilerVerificationCourse
\ No newline at end of file
+# LeroyCompilerVerificationCourse
+
+This project is a Lean port of Xavier Leroy's [EUTypes 2019 summer school course on "Proving the correctness of a compiler"](https://xavierleroy.org/courses/EUTypes-2019/). The original course material was written in Coq and demonstrates formal verification techniques for compiler correctness using a simple IMP language. This Lean implementation preserves the same theoretical foundations and proof structure while adapting the formalization to Lean's theorem proving system.
\ No newline at end of file

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 06/10] .

---
 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 07/10] .

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

From 1f1d4e3d159154d6f8d6b56ac403bdb9f76796e7 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 3 Jul 2025 21:50:22 +1000
Subject: [PATCH 08/10] more grind

---
 LeroyCompilerVerificationCourse/Imp.lean      | 156 +++++-------------
 .../Sequences.lean                            |  98 ++++-------
 2 files changed, 79 insertions(+), 175 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean
index f588561..496b679 100644
--- a/LeroyCompilerVerificationCourse/Imp.lean
+++ b/LeroyCompilerVerificationCourse/Imp.lean
@@ -30,19 +30,16 @@ def store : Type := ident → Int
 theorem aeval_xplus1 : ∀ s x, aeval s (.PLUS (.VAR x) (.CONST 1)) > aeval s (.VAR x) := by
   grind
 
-
 @[grind] def free_in_aexp (x : ident) (a : aexp) : Prop :=
   match a with
   | .CONST _ => False
   | .VAR y => y = x
-  | .PLUS a1 a2 | .MINUS a1 a2 => free_in_aexp x a1 ∨ free_in_aexp x a2
+  | .PLUS a1 a2
+  | .MINUS a1 a2 => free_in_aexp x a1 ∨ free_in_aexp x a2
 
-theorem aeval_free :
-  ∀ s1 s2 a,
-  (∀ x, free_in_aexp x a → s1 x = s2 x) →
-  aeval s1 a = aeval s2 a := by
-    intro s1 _ a _
-    fun_induction aeval s1 a with grind
+theorem aeval_free (s1 s2 a) (h : ∀ x, free_in_aexp x a → s1 x = s2 x) :
+    aeval s1 a = aeval s2 a := by
+  fun_induction aeval s1 a with grind
 
 inductive bexp : Type where
   | TRUE
@@ -71,8 +68,7 @@ def LESS (a1 a2 : aexp) : bexp := GREATER a2 a1
   | .NOT b1 =>  !(beval s b1)
   | .AND b1 b2 => beval s b1 && beval s b2
 
-theorem beval_OR :
-  ∀ s b1 b2, beval s (OR b1 b2) = beval s b1 ∨ beval s b2 := by grind
+theorem beval_OR : beval s (OR b1 b2) = beval s b1 ∨ beval s b2 := by grind
 
 inductive com : Type where
   | SKIP
@@ -111,14 +107,14 @@ def Euclidean_division :=
       beval s b = true -> cexec s c s' -> cexec s' (.WHILE b c) s'' ->
       cexec s (.WHILE b c) s''
 
-theorem cexec_infinite_loop :
-  ∀ s, ¬ ∃ s', cexec s (.WHILE .TRUE .SKIP) s' := by
-  intro _ h
-  apply Exists.elim h
-  intro s'
-  generalize heq : (com.WHILE .TRUE .SKIP) = c
-  intro h₂
-  induction h₂ <;> grind
+attribute [grind] cexec.cexec_skip
+grind_pattern cexec.cexec_seq => cexec s c1 s', cexec s (.SEQ c1 c2) s''
+grind_pattern cexec.cexec_seq => cexec s' c2 s'', cexec s (.SEQ c1 c2) s''
+
+theorem cexec_infinite_loop (s : store) : ¬ ∃ s', cexec s (.WHILE .TRUE .SKIP) s' := by
+  rintro ⟨s', h₂⟩
+  generalize heq : com.WHILE .TRUE .SKIP = c at h₂
+  induction h₂ with grind
 
 @[grind] def cexec_bounded (fuel : Nat) (s : store) (c : com) : Option store :=
   match fuel with
@@ -141,16 +137,9 @@ theorem cexec_infinite_loop :
       else
         .some s
 
-theorem cexec_bounded_sound : ∀ fuel s c s',
-    cexec_bounded fuel s c = .some s'
-  → cexec s c s' := by
-  intro fuel
-  induction fuel
-  case succ fuel ih =>
-    intros _ c
-    cases c
-    all_goals grind
-  all_goals grind
+theorem cexec_bounded_sound {fuel s c s'} :
+    cexec_bounded fuel s c = .some s' → cexec s c s' := by
+  induction fuel generalizing s c s' with grind [cases com]
 
 theorem cexec_bounded_complete (s s' : store) (c : com) :
   cexec s c s' →
@@ -160,13 +149,11 @@ theorem cexec_bounded_complete (s s' : store) (c : com) :
     case cexec_skip =>
       exists 1
       intro fuel' fgt
-      induction fgt
-      all_goals grind
+      induction fgt with grind
     case cexec_assign =>
       exists 1
       intro fuel' fgt
-      induction fgt
-      any_goals grind
+      induction fgt with grind
     case cexec_seq a_ih1 a_ih2 =>
       apply Exists.elim a_ih1
       intro fuel1 a_ih1
@@ -174,7 +161,7 @@ theorem cexec_bounded_complete (s s' : store) (c : com) :
       intro fuel2 a_ih2
       exists (fuel1 + fuel2)
       intro fuel' fgt
-      have t : fuel' ≥ fuel1 ∧  fuel' ≥ fuel2 := by grind
+      have t : fuel' ≥ fuel1 ∧ fuel' ≥ fuel2 := by grind
       have t1 : fuel1 > 0 := by
         false_or_by_contra
         rename_i hyp
@@ -187,40 +174,18 @@ theorem cexec_bounded_complete (s s' : store) (c : com) :
         simp at hyp
         specialize a_ih2 0 (by grind)
         grind
-      induction fuel'
-      case zero => grind
-      case succ m ih  =>
-        specialize a_ih1 m (by grind)
-        simp only [cexec_bounded, a_ih1]
-        specialize a_ih2 m (by grind)
-        exact a_ih2
+      induction fuel' with grind
     case cexec_ifthenelse s b c1 c2 s' a a_ih =>
       apply Exists.elim a_ih
       intro fuel
       intro a_ih
       exists (fuel + 1)
-      intro bigger_fuel
-      intro gt
       unfold cexec_bounded
-      have gt' : bigger_fuel > 0 := by grind
-      split
-      case h_1 => grind
-      case h_2 f =>
-        simp
-        split
-        case isTrue w =>
-          specialize a_ih f (by grind)
-          simp [w] at a_ih
-          exact a_ih
-        case isFalse w =>
-          specialize a_ih f (by grind)
-          simp [w] at a_ih
-          exact a_ih
+      grind
     case cexec_while_done =>
       exists 1
       intro fuel fgt
-      induction fgt
-      all_goals grind
+      induction fgt with grind
     case cexec_while_loop a_ih1 a_ih2 =>
       apply Exists.elim a_ih1
       intro fuel1 a_ih1
@@ -230,21 +195,14 @@ theorem cexec_bounded_complete (s s' : store) (c : com) :
       intro fuel' fgt
       have t1 : fuel1 > 0 := by
         false_or_by_contra
-        rename_i hyp
         specialize a_ih1 0 (by grind)
-        dsimp [cexec_bounded] at a_ih1
-        contradiction
+        grind
       have t2 : fuel2 > 0 := by
         false_or_by_contra
-        rename_i hyp
         specialize a_ih2 0 (by grind)
-        dsimp [cexec_bounded] at a_ih2
-        contradiction
-      induction fgt
-      any_goals grind
-      case refl =>
-        unfold cexec_bounded
         grind
+      unfold cexec_bounded
+      induction fgt with grind
 
 @[grind] inductive red : com × store → com × store → Prop where
   | red_assign : ∀ x a s,
@@ -272,7 +230,7 @@ theorem red_progress :
       intro s
       apply Or.intro_right
       exists com.SKIP
-      exists (update identifier (aeval s expression) s)
+      exists update identifier (aeval s expression) s
       grind
     case SEQ c1 c2 c1_ih c2_ih =>
       intro s
@@ -280,7 +238,6 @@ theorem red_progress :
       apply Or.elim (c1_ih s)
       case h.left =>
         intro c1_eq
-        rw [c1_eq]
         exists c2
         exists s
         grind
@@ -290,7 +247,7 @@ theorem red_progress :
         intro c1' h
         apply Exists.elim h
         intro s' h
-        exists (.SEQ c1' c2)
+        exists .SEQ c1' c2
         exists s'
         grind
     case IFTHENELSE b c1 c2 c1_ih c2_ih =>
@@ -340,23 +297,20 @@ def goes_wrong (c : com) (s : store) : Prop := ∃ c', ∃ s', star red (c, s) (
 
 @[grind] theorem red_seq_steps (c2 c c' : com) (s s' : store) : star red (c, s) (c', s') → star red ((c;;c2), s) ((c';;c2), s') := by
   intro H
-  generalize h₁ : (c,s) = v₁
-  generalize h₂ : (c',s') = v₂
+  generalize h₁ : (c, s) = v₁
+  generalize h₂ : (c', s') = v₂
   rw [h₁, h₂] at H
   induction H generalizing c s
   case star_refl =>
-   grind
+    grind
   case star_step x y _ a₁ a₂ a_ih =>
     apply star.star_step
     · apply red.red_seq_step
       rotate_left
       · exact y.1
       · exact y.2
-      · rw [h₁]
-        exact a₁
-    · apply a_ih
-      · rfl
-      · exact h₂
+      · grind
+    · grind
 
 theorem cexec_to_reds (s s' : store) (c : com) : cexec s c s' → star red (c, s) (.SKIP, s') := by
   intro h
@@ -382,39 +336,17 @@ theorem cexec_to_reds (s s' : store) (c : com) : cexec s c s' → star red (c, s
         · apply ih2
         · grind
 
-@[grind] theorem red_append_cexec (c1 c2 : com) (s1 s2 : store) :
-  red (c1, s1) (c2, s2) →
-  ∀ s', cexec s2 c2 s' → cexec s1 c1 s' := by
-    intro h s h2
-    generalize heq1 : (c1, s1) = h1
-    generalize heq2 : (c2, s2) = h2
-    rw [heq1, heq2] at h
-    induction h generalizing c1 c2 s
-    case red_seq_done =>
-      simp only [Prod.mk.injEq] at heq1 heq2
-      rw [←heq2.1, ←heq2.2] at heq1
-      rw [heq1.1, heq1.2]
-      apply cexec.cexec_seq
-      · -- Could be good to have an error about a metavariable in here
-        apply cexec.cexec_skip
-      · exact h2
-    all_goals grind
-
-theorem reds_to_cexec (s s' : store) (c : com) :
-  star red (c, s) (.SKIP, s') → cexec s c s' := by
-    intro h
-    generalize heq1 : (c, s) = h1
-    generalize heq2 : (com.SKIP, s') = h2
-    rw [heq1, heq2] at h
-    induction h generalizing s c s'
-    case star_refl =>
-      grind
-    case star_step r _ a_ih =>
-      apply red_append_cexec
-      · rw [←heq1] at r
-        exact r
-      · apply a_ih
-        all_goals grind
+@[grind] theorem red_append_cexec (c1 c2 : com) (s1 s2 : store) (h : red (c1, s1) (c2, s2)) (h₂ : cexec s2 c2 s) :
+    cexec s1 c1 s := by
+  generalize heq1 : (c1, s1) = h1 at h
+  generalize heq2 : (c2, s2) = h2 at h
+  induction h generalizing c1 c2 s with grind
+
+theorem reds_to_cexec (s s' : store) (c : com) (h : star red (c, s) (.SKIP, s')) :
+    cexec s c s' := by
+  generalize heq1 : (c, s) = h1 at h
+  generalize heq2 : (com.SKIP, s') = h2 at h
+  induction h generalizing s c s' with grind
 
 @[grind] inductive cont where
 | Kstop
diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean
index 5d5fba1..6917d2b 100644
--- a/LeroyCompilerVerificationCourse/Sequences.lean
+++ b/LeroyCompilerVerificationCourse/Sequences.lean
@@ -26,50 +26,40 @@ info: infseq.coinduct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α →
 #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.coinduct R (λ m => R m m)
-  grind
+theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x :=
+  infseq.coinduct R (λ m => R m m) (by grind) _
 
 @[grind] inductive star (R : α → α → Prop) : α → α → Prop where
   | star_refl : ∀ x : α, star R x x
-  | star_step : ∀ x y z, R x y → star R y z → star R x z
+  | star_step : ∀ {x y z}, R x y → star R y z → star R x z
 
-@[grind] theorem star_one (R : α → α → Prop) : ∀ a b : α, R a b → star R a b := by
-  intros a b Rab
-  apply star.star_step
-  exact Rab
-  grind
+-- Whenever we have `star R y z` and want to prove `star R x z`, look for `R x y`:
+attribute [grind =>] star.star_step
 
-@[grind] theorem star_trans {α} (R : α → α → Prop) : ∀ (a b : α), star R a b → ∀ c : α, star R b c → star R a c := by
-  intros a b sab
-  intro c
-  intro sbc
-  induction sab
-  case star_refl => exact sbc
-  case star_step rel m ih =>
-    apply star.star_step
-    exact rel
-    grind
+@[grind] theorem star_one (R : α → α → Prop) {a b : α} (h : R a b) : star R a b :=
+  star.star_step h (by grind)
 
+@[grind] theorem star_trans {α} (R : α → α → Prop) (a b : α) (sab : star R a b) : ∀ c : α, star R b c → star R a c := by
+  induction sab with grind
+
+@[grind cases]
 inductive plus (R : α → α → Prop) : α → α → Prop where
-| plus_left : ∀ a b c, R a b → star R b c → plus R a c
+| plus_left : ∀ {a b c}, R a b → star R b c → plus R a c
+
+-- Whenever we have `star R b c` and want to prove `plus R a c`, look for `R a b`:
+grind_pattern plus.plus_left => star R b c, plus R a c
 
-theorem plus_one : ∀ a b, R a b → plus R a b := by
-  intro a b Rab
-  apply plus.plus_left
-  · exact Rab
-  · grind
+@[grind ←]
+theorem plus_one {a b} (h : R a b) : plus R a b :=
+  plus.plus_left h (by grind)
 
-@[grind] theorem plus_star : ∀ a b, plus R a b → star R a b := by
-    intro a b h
-    cases h
-    case plus_left h₁ h₂ h₃ =>
-      grind [star.star_step]
+@[grind] theorem plus_star {a b} (h : plus R a b) : star R a b := by
+    grind
 
 @[grind] theorem plus_star_trans (R : α → α → Prop) : ∀ (a b c : α), star R a b → plus R b c → plus R a c := by
   intro a b c s p
   induction s
-  any_goals grind
+  case star_refl => grind
   case star_step d e f rel s2 ih =>
     apply plus.plus_left
     exact rel
@@ -86,11 +76,9 @@ theorem star_plus_trans :
       · exact a1
       · grind
 
-theorem plus_right :
-  ∀ a b c, star R a b -> R b c -> plus R a c := by
-  intro a b c h₁ h₂
-  grind [star_plus_trans, plus_one]
+-- grind_pattern star_plus_trans => star R a b, plus R b c
 
+theorem plus_right : star R a b -> R b c -> plus R a c := by grind
 
 def all_seq_inf (R : α → α → Prop) (x : α) : Prop :=
   ∀ y : α, star R x y → ∃ z, R y z
@@ -101,7 +89,7 @@ def infseq_with_function (R : α → α → Prop) (a: α) : Prop :=
 def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → infseq R x := by
   apply infseq.coinduct
   intro x H
-  apply Exists.elim (H x (by simp only [star.star_refl]))
+  apply Exists.elim (H x (by grind))
   intro y Rxy
   exists y
   constructor
@@ -111,15 +99,9 @@ def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x →
     apply H
     grind
 
-theorem infseq_coinduction_principle_2 :
-  ∀ (x : α → Prop),
-  (∀ (a : α), x a → ∃ b, plus R a b ∧ x b) →
-  ∀ (a : α), x a → infseq R a := by
-    intro X
-    intro h₁ a rel
-    apply infseq.coinduct _ (fun a => ∃ b, star R a b ∧ X b)
-    case x => grind
-    case y => grind [cases plus]
+theorem infseq_coinduction_principle_2
+    (X : α → Prop) (h₁ : ∀ (a : α), X a → ∃ b, plus R a b ∧ X b) (a : α) (rel : X a) : infseq R a := by
+  apply infseq.coinduct _ (fun a => ∃ b, star R a b ∧ X b) <;> grind
 
 theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a := by
   apply infseq.coinduct
@@ -129,41 +111,31 @@ theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a :=
   refine ⟨f 1, ?_⟩
   refine ⟨by grind, ?_⟩
   unfold infseq_with_function
-  refine ⟨fun n => f (n + 1), ?_⟩
-  refine ⟨by grind, ?_⟩
-  intro i
-  specialize hsucc (i + 1)
-  grind
+  refine ⟨fun n => f (n + 1), by grind⟩
 
 @[grind] def irred (R : α → α → Prop) (a : α) : Prop := ∀ b, ¬(R a b)
 
-theorem star_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) : ∀ a b, star R a b -> forall c, star R a c → star R b c ∨ star R c b := by
-  intro _ _ sab
+theorem star_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) (sab : star R a b) :
+    ∀ c, star R a c → star R b c ∨ star R c b := by
   induction sab <;> grind
 
 theorem finseq_unique (R_functional : ∀ a b c, R a b -> R a c -> b = c) :
   ∀ a b b', star R a b → irred R b → star R a b' → irred R b' → b = b' := by
     intro a b b' sab ib sab' ib'
-    apply Or.elim (star_star_inv R_functional a b sab b' sab') <;> grind
+    apply Or.elim (star_star_inv R_functional sab b' sab') <;> grind
 
-@[grind ]theorem infseq_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) : ∀ a b, star R a b → infseq R a → infseq R b := by
+@[grind] theorem infseq_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) : ∀ a b, star R a b → infseq R a → infseq R b := by
   intro a b sab ia
-  induction sab
-  case star_refl => grind
-  case star_step x y z rxy syz ih =>
-    unfold infseq at ia
-    grind
+  induction sab with grind [infseq]
 
 theorem infseq_finseq_excl (R_functional : ∀ a b c, R a b -> R a c -> b = c): ∀ a b, star R a b → irred R b → infseq R a → False := by
   intro a b sab irb ia
   have h : infseq R b := by grind
-  unfold infseq at h
-  grind
+  grind [infseq]
 
 theorem infseq_all_seq_inf (R_functional : ∀ a b c, R a b -> R a c -> b = c): ∀ a, infseq R a → all_seq_inf R a := by
   intro a ia
   unfold all_seq_inf
   intro b sab
   have h : infseq R b := by grind
-  unfold infseq at h
-  grind
+  grind [infseq]

From 207b0ecd97dec9d6af511a4b86a9900e7b8f3eb1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 3 Jul 2025 21:52:28 +1000
Subject: [PATCH 09/10] .

---
 LeroyCompilerVerificationCourse/Imp.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean
index 496b679..0d310d2 100644
--- a/LeroyCompilerVerificationCourse/Imp.lean
+++ b/LeroyCompilerVerificationCourse/Imp.lean
@@ -108,8 +108,7 @@ def Euclidean_division :=
       cexec s (.WHILE b c) s''
 
 attribute [grind] cexec.cexec_skip
-grind_pattern cexec.cexec_seq => cexec s c1 s', cexec s (.SEQ c1 c2) s''
-grind_pattern cexec.cexec_seq => cexec s' c2 s'', cexec s (.SEQ c1 c2) s''
+attribute [grind <=] cexec.cexec_seq
 
 theorem cexec_infinite_loop (s : store) : ¬ ∃ s', cexec s (.WHILE .TRUE .SKIP) s' := by
   rintro ⟨s', h₂⟩

From 43d26b1dd18e6d10de11dad620b8f4e5d12099f3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 4 Jul 2025 11:16:55 +1000
Subject: [PATCH 10/10] remove case proved by grind

---
 LeroyCompilerVerificationCourse/Compil.lean | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index 78a998e..6c747ef 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -631,14 +631,6 @@ theorem compile_cont_Kwhile_inv (C : List instr) (b : bexp) (c : com) (k : cont)
           · exact rfl
           · grind
       · grind
-    case ccont_while b' c' k' pc₂ d pc₃ pc₄ h₃ h₄ h₅ h₆ h₇ ih =>
-      exists (pc + 1 + d)
-      constructor
-      apply plus_one
-      apply transition.trans_branch
-      rotate_left 2
-      · exact d
-      any_goals grind
 
 theorem match_config_skip (C : List instr) (k : cont) (s : store) (pc : Int) (H : compile_cont C k pc) :
  match_config C (.SKIP, k, s) (pc, [], s) := by