feat: initial compression of proofs using grind

LeroyCompilerVerificationCourse/Compil.lean

@@ -8,8 +8,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)
@@ -156,30 +154,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',
@@ -191,15 +175,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',
@@ -240,7 +216,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
@@ -264,9 +240,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]
@@ -311,7 +285,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 =>
@@ -923,8 +897,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,

LeroyCompilerVerificationCourse/Constprop.lean

@@ -19,9 +19,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

LeroyCompilerVerificationCourse/Deadcode.lean

@@ -9,9 +9,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
 

LeroyCompilerVerificationCourse/Fixpoints.lean

@@ -17,8 +17,6 @@ import Init.Data.List.Basic
 
 universe u
 
-set_option grind.warning false
-
 @[grind] class OrderStruct (α : Sort u) where
   eq : α → α → Prop
   le : α → α → Prop

LeroyCompilerVerificationCourse/Imp.lean

@@ -5,7 +5,6 @@ Authors: Wojciech Różowski
 -/
 
 import LeroyCompilerVerificationCourse.Sequences
-set_option grind.warning false
 
 def ident := String deriving BEq, Repr, Hashable
 

LeroyCompilerVerificationCourse/Sequences.lean

@@ -4,22 +4,21 @@ 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 :=
   λ 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
+  grind
+
 /--
 info: infseq.fixpoint_induct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop)
   (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y) (x✝ : α) : x x✝ → infseq R x✝
@@ -29,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
@@ -59,8 +57,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
@@ -85,11 +83,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
@@ -109,7 +104,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:
@@ -118,21 +114,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)

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

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