From c6c1e8c2d888a95c38ecc8b87b7c4d14c839463b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Jul 2025 06:56:29 +0200 Subject: [PATCH 1/2] chore: bump toolchain to v4.22.0-rc2 --- LeroyCompilerVerificationCourse/Sequences.lean | 16 ++++++++-------- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean index 746c72b..c26379d 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 + coinductive_fixpoint -- Application of the rewrite rule def infseq_fixpoint {α} (R : α → α → Prop) (x : α) : @@ -16,18 +16,18 @@ def infseq_fixpoint {α} (R : α → α → Prop) (x : α) : -- The associated coinduction principle theorem infseq.coind {α} (h : α → Prop) (R : α → α → Prop) (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by - apply infseq.fixpoint_induct + apply infseq.coinduct grind /-- -info: infseq.fixpoint_induct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop) - (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y) (x✝ : α) : x x✝ → infseq R x✝ +info: infseq.coinduct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop) (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y) + (x✝ : α) : x x✝ → infseq R x✝ -/ -#guard_msgs in #check infseq.fixpoint_induct +#guard_msgs in #check infseq.coinduct -- Simple proof by coinduction theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x := by - apply infseq.fixpoint_induct R (λ m => R m m) + apply infseq.coinduct R (λ m => R m m) grind @[grind] inductive star (R : α → α → Prop) : α → α → Prop where @@ -96,7 +96,7 @@ def all_seq_inf (R : α → α → Prop) (x : α) : Prop := ∀ y : α, star R x y → ∃ z, R y z def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → infseq R x := by - apply infseq.fixpoint_induct + apply infseq.coinduct intro x H apply Exists.elim (H x (by simp only [star.star_refl])) intro y Rxy @@ -114,7 +114,7 @@ theorem infseq_coinduction_principle_2: ∀ (a : α), x a → infseq R a := by intro X intro h₁ a rel - apply infseq.fixpoint_induct _ (fun a => ∃ b, star R a b ∧ X b) + apply infseq.coinduct _ (fun a => ∃ b, star R a b ∧ X b) case x => grind case y => grind [cases plus] diff --git a/lake-manifest.json b/lake-manifest.json index 34498a2..434a219 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8d2067bf518731a70a255d4a61b5c103922c772e", + "rev": "3adabe76bed51fc81d04ae65bb7c3893333e3d63", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", + "inputRev": "v4.22.0-rc2", "inherited": false, "configFile": "lakefile.toml"}], "name": "LeroyCompilerVerificationCourse", diff --git a/lakefile.toml b/lakefile.toml index 22b60d1..41ad23f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -5,7 +5,7 @@ defaultTargets = ["LeroyCompilerVerificationCourse"] [[require]] name = "batteries" git = "https://github.com/leanprover-community/batteries" -rev = "v4.21.0" +rev = "v4.22.0-rc2" [[lean_lib]] name = "LeroyCompilerVerificationCourse" 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 3d30cecf88066ab0324a4cca878f9e54c2c57d3b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Jul 2025 06:58:47 +0200 Subject: [PATCH 2/2] unsedSimpArgs --- LeroyCompilerVerificationCourse/Compil.lean | 6 +++--- LeroyCompilerVerificationCourse/Fixpoints.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean index 9534afd..f9aacc2 100644 --- a/LeroyCompilerVerificationCourse/Compil.lean +++ b/LeroyCompilerVerificationCourse/Compil.lean @@ -284,7 +284,7 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int) next c1 c3 a => have h1 := instr_a instr.Iadd c3 (c1 ++ compile_aexp a1 ++ compile_aexp a2) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) (by grind) have h2 := @transition.trans_add ((c1 ++ compile_aexp a1 ++ compile_aexp a2) ++ (instr.Iadd :: c3)) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) stk s (aeval s a1) (aeval s a2) (by grind) - simp [codelen_app, codelen_cons, codelen] at * + simp [codelen] at * grind next a1 a2 a1_ih a2_ih => simp [aeval, compile_aexp] @@ -456,7 +456,7 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s apply code_at_app_left exact h . specialize c2_ih C (pc + codelen (compile_com c1)) stk - simp [compile_com, codelen_app, Int.add_assoc] + simp [compile_com, codelen_app] simp [Int.add_assoc] at c2_ih apply c2_ih grind @@ -763,7 +763,7 @@ theorem simulation_step: simp [isFalse] at * rw [h₅] have := @code_at_app_right C pc (codeb ++ code1 ++ [instr.Ibranch (codelen code2)]) code2 (by grind [List.append_assoc, List.cons_append, List.nil_append]) - simp [codelen_cons, codelen_singleton, codelen_app] at this + simp [codelen_cons, codelen_app] at this simp [codelen] at * grind . by_cases beval st b = true diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean index b7ea821..e9a7758 100644 --- a/LeroyCompilerVerificationCourse/Fixpoints.lean +++ b/LeroyCompilerVerificationCourse/Fixpoints.lean @@ -365,7 +365,7 @@ noncomputable def Cexec' : (c : com) → {F : Store → Store // ∀ x y, le x generalize heq : Beval y b = h cases h case none => - simp [heq] + simp apply le_trans rotate_right . exact Join (f₁ x) (f₂ x)