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 diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean index db53083..dae5e7a 100644 --- a/LeroyCompilerVerificationCourse/Deadcode.lean +++ b/LeroyCompilerVerificationCourse/Deadcode.lean @@ -86,12 +86,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 @@ -159,7 +154,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 @@ -171,7 +165,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 @@ -187,18 +181,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 diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean index f588561..0d310d2 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,13 @@ 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 +attribute [grind <=] cexec.cexec_seq + +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 +136,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 +148,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 +160,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 +173,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 +194,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 +229,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 +237,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 +246,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 +296,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 +335,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]