diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean index 1978d4b..ba9eeb1 100644 --- a/LeroyCompilerVerificationCourse/Compil.lean +++ b/LeroyCompilerVerificationCourse/Compil.lean @@ -34,33 +34,33 @@ def config : Type := Int × stack × store instr_at C pc = .some (.Iconst n) → transition C (pc , stk , s) (pc + 1, n :: stk, s) - | trans_var : forall pc stk s x, + | trans_var : ∀ pc stk s x, instr_at C pc = .some (.Ivar x) -> transition C (pc , stk , s) (pc + 1, s x :: stk, s) - | trans_setvar: forall pc stk s x n, + | trans_setvar: ∀ pc stk s x n, instr_at C pc = .some (.Isetvar x) -> transition C (pc , n :: stk, s) (pc + 1, stk , update x n s) - | trans_add: forall pc stk s n1 n2, + | trans_add: ∀ pc stk s n1 n2, instr_at C pc = .some (.Iadd) -> transition C (pc , n2 :: n1 :: stk , s) (pc + 1, (n1 + n2) :: stk, s) - | trans_opp: forall pc stk s n, + | trans_opp: ∀ pc stk s n, instr_at C pc = .some (.Iopp) -> transition C (pc , n :: stk , s) (pc + 1, (- n) :: stk, s) - | trans_branch: forall pc stk s d pc', + | trans_branch: ∀ pc stk s d pc', instr_at C pc = .some (.Ibranch d) -> pc' = pc + 1 + d -> transition C (pc , stk, s) (pc', stk, s) - | trans_beq: forall pc stk s d1 d0 n1 n2 pc', + | trans_beq: ∀ pc stk s d1 d0 n1 n2 pc', instr_at C pc = .some (.Ibeq d1 d0) -> pc' = pc + 1 + (if n1 = n2 then d1 else d0) -> transition C (pc , n2 :: n1 :: stk, s) (pc', stk , s) - | trans_ble: forall pc stk s d1 d0 n1 n2 pc', + | trans_ble: ∀ pc stk s d1 d0 n1 n2 pc', instr_at C pc = .some (.Ible d1 d0) -> pc' = pc + 1 + (if n1 ≤ n2 then d1 else d0) -> transition C (pc , n2 :: n1 :: stk, s) @@ -70,14 +70,14 @@ def config : Type := Int × stack × store star (transition C) def machine_terminates (C: List instr) (s_init: store) (s_final: store) : Prop := - exists pc, transitions C (0, [], s_init) (pc, [], s_final) + ∃ pc, transitions C (0, [], s_init) (pc, [], s_final) ∧ instr_at C pc = .some .Ihalt def machine_diverges (C: List instr) (s_init: store) : Prop := infseq (transition C) (0, [], s_init) def machine_goes_wrong (C: List instr) (s_init: store) : Prop := - exists pc stk s, + ∃ pc stk s, transitions C (0, [], s_init) (pc, stk, s) ∧ irred (transition C) (pc, stk, s) ∧ (instr_at C pc ≠ .some .Ihalt ∨ stk ≠ []) @@ -134,22 +134,22 @@ def smart_Ibranch (d: Int) : List instr:= if d = 0 then [] else .Ibranch d :: [] @[grind] inductive code_at: List instr -> Int -> List instr-> Prop where - | code_at_intro: forall C1 C2 C3 pc, + | code_at_intro: ∀ C1 C2 C3 pc, pc = codelen C1 -> code_at (C1 ++ C2 ++ C3) pc C2 @[grind] theorem codelen_cons: - forall i c, codelen (i :: c) = codelen c + 1 := by grind + ∀ i c, codelen (i :: c) = codelen c + 1 := by grind @[grind] theorem codelen_singleton : codelen [i] = 1 := by dsimp [codelen] @[grind] theorem codelen_app: - forall c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2 := by + ∀ c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2 := by intro c1 _ induction c1 with grind -@[grind =>] theorem instr_a : forall i c2 c1 pc, +@[grind =>] theorem instr_a : ∀ i c2 c1 pc, pc = codelen c1 -> instr_at (c1 ++ (i :: c2) ) pc = .some i := by intro i c2 c1 pc @@ -163,7 +163,7 @@ def smart_Ibranch (d: Int) : List instr:= induction c1 generalizing pc with grind theorem code_at_head : - forall C pc i C', + ∀ C pc i C', code_at C pc (i :: C') -> instr_at C pc = .some i := by intro C pc i C' H @@ -175,7 +175,7 @@ theorem code_at_head : induction c1 generalizing oc with grind @[grind] theorem code_at_tail : - forall C pc i C', + ∀ C pc i C', code_at C pc (i :: C') → code_at C (pc + 1) C' := by intro C pc i C' h @@ -185,7 +185,7 @@ theorem code_at_head : grind @[grind] theorem code_at_app_left: - forall C pc C1 C2, + ∀ C pc C1 C2, code_at C pc (C1 ++ C2) -> code_at C pc C1 := by intro c pc m1 m2 h @@ -195,7 +195,7 @@ theorem code_at_head : grind [List.append_assoc] @[grind] theorem code_at_app_right: - forall C pc C1 C2, + ∀ C pc C1 C2, code_at C pc (C1 ++ C2) -> code_at C (pc + codelen C1) C2 := by intro C pc c1 c2 h @@ -204,7 +204,7 @@ theorem code_at_head : have := code_at.code_at_intro (b ++ c1) c2 e (pc + codelen c1) (by grind) grind [List.append_assoc] -@[grind] theorem code_at_app_right2 : forall C pc C1 C2 C3, +@[grind] theorem code_at_app_right2 : ∀ C pc C1 C2 C3, code_at C pc (C1 ++ C2 ++ C3) → code_at C (pc + codelen C1) C2 := by intro C pc c1 c2 c3 h @@ -213,7 +213,7 @@ theorem code_at_head : have := code_at.code_at_intro (b ++ c1) c2 (c3 ++ e) (pc + codelen c1) (by grind) grind -@[grind] theorem code_at_nil : forall C pc C1, +@[grind] theorem code_at_nil : ∀ C pc C1, code_at C pc C1 -> code_at C pc [] := by intro C pc c1 h cases h @@ -222,7 +222,7 @@ theorem code_at_head : grind [List.append_nil, List.append_assoc] @[grind] theorem instr_at_code_at_nil : - forall C pc i, instr_at C pc = .some i -> code_at C pc [] := by + ∀ C pc i, instr_at C pc = .some i -> code_at C pc [] := by intro C pc i h induction C generalizing pc i case nil => grind @@ -270,13 +270,13 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int) simp [aeval, compile_aexp] intro a apply star_trans - . apply a1_ih + · apply a1_ih grind - . apply star_trans - . specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk) + · apply star_trans + · specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk) apply a2_ih grind - . apply star_one + · apply star_one 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) @@ -286,19 +286,19 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int) simp [aeval, compile_aexp] intro a apply star_trans - . apply a1_ih + · apply a1_ih grind - . apply star_trans - . specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk) + · apply star_trans + · specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk) apply a2_ih grind - . apply star_trans - . apply star_one - . have := @transition.trans_opp C (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) ((aeval s a1) :: stk) s (aeval s a2) + · apply star_trans + · apply star_one + · have := @transition.trans_opp C (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) ((aeval s a1) :: stk) s (aeval s a2) apply this grind - . apply star_one - . have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp]) instr.Iadd [] (by grind [List.append_assoc, List.cons_append, List.nil_append]) + · apply star_one + · have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp]) instr.Iadd [] (by grind [List.append_assoc, List.cons_append, List.nil_append]) have := @transition.trans_add C (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2) + 1) stk s (aeval s a1) (-aeval s a2) (by simp [codelen] at *; grind) grind -- Miss 5 @@ -317,10 +317,10 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In apply star_one simp [is_not_zero, codelen] apply transition.trans_branch _ _ _ d1 - . simp [compile_bexp, is_not_zero] at h + · simp [compile_bexp, is_not_zero] at h have := @code_at_to_instr_at C pc [] (instr.Ibranch d1) [] (by grind [List.append_assoc, List.nil_append]) grind - . grind + · grind next => simp [compile_bexp, beval] by_cases d0 = 0 @@ -331,50 +331,50 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In apply star_one simp [is_not_zero, codelen] apply transition.trans_branch _ _ _ d0 - . simp [compile_bexp, is_not_zero] at h + · simp [compile_bexp, is_not_zero] at h have := @code_at_to_instr_at C pc [] (instr.Ibranch d0) [] (by grind [List.append_assoc, List.nil_append]) grind - . grind + · grind next a1 a2 => simp [compile_bexp, beval] apply star_trans - . apply compile_aexp_correct + · apply compile_aexp_correct rotate_left - . exact a1 - . grind - . apply star_trans - . apply compile_aexp_correct + · exact a1 + · grind + · apply star_trans + · apply compile_aexp_correct rotate_right - . exact a2 - . grind - . apply star_one - . apply transition.trans_beq + · exact a2 + · grind + · apply star_one + · apply transition.trans_beq rotate_left; rotate_left - . exact d1 - . exact d0 - . simp [compile_bexp] at h + · exact d1 + · exact d0 + · simp [compile_bexp] at h grind - . grind + · grind next a1 a2 => simp [compile_bexp, beval] apply star_trans - . apply compile_aexp_correct + · apply compile_aexp_correct rotate_left - . exact a1 - . grind - . apply star_trans - . apply compile_aexp_correct + · exact a1 + · grind + · apply star_trans + · apply compile_aexp_correct rotate_right - . exact a2 - . grind - . apply star_one - . apply transition.trans_ble + · exact a2 + · grind + · apply star_one + · apply transition.trans_ble rotate_left; rotate_left - . exact d1 - . exact d0 - . simp [compile_bexp] at h + · exact d1 + · exact d0 + · simp [compile_bexp] at h grind - . grind + · grind next b1 ih => grind next b1 b2 b1_ih b2_ih => @@ -383,12 +383,12 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In unfold compile_bexp simp [heq1, heq2] apply star_trans - . apply b1_ih + · apply b1_ih rotate_left - . exact 0 - . exact (codelen code2 + d0) - . grind - . by_cases beval s b1 = true + · exact 0 + · exact (codelen code2 + d0) + · grind + · by_cases beval s b1 = true case pos isTrue => simp [isTrue] rw [heq2] @@ -422,13 +422,13 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s intro C pc stk h unfold compile_com apply star_trans - . apply compile_aexp_correct + · apply compile_aexp_correct rotate_left - . exact a - . unfold compile_com at h + · exact a + · unfold compile_com at h grind - . apply star_one - . have := @transition.trans_setvar C (pc + codelen (compile_aexp a)) stk s x (aeval s a) + · apply star_one + · have := @transition.trans_setvar C (pc + codelen (compile_aexp a)) stk s x (aeval s a) rw [codelen_app, codelen_singleton] suffices transition C (pc + codelen (compile_aexp a), aeval s a :: stk, s) (pc + codelen (compile_aexp a) + 1, stk, update x (aeval s a) s) from by grind apply this @@ -436,11 +436,11 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s case cexec_seq s'2 c1 s1 c2 s2 cexec1 cexec2 c1_ih c2_ih => intro C pc stk h apply star_trans - . apply c1_ih + · apply c1_ih unfold compile_com at h apply code_at_app_left exact h - . specialize c2_ih C (pc + codelen (compile_com c1)) stk + · specialize c2_ih C (pc + codelen (compile_com c1)) stk simp [compile_com, codelen_app] simp [Int.add_assoc] at c2_ih apply c2_ih @@ -454,20 +454,20 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s rw [heq1, heq2, heq3] intro h apply star_trans - . have := compile_bexp_correct C s b 0 (codelen code1 + 1) pc stk (by grind) + · have := compile_bexp_correct C s b 0 (codelen code1 + 1) pc stk (by grind) apply this - . by_cases beval s b = true + · by_cases beval s b = true case pos isTrue => simp [isTrue] apply star_trans - . apply ih + · apply ih grind - . apply star_one - . apply transition.trans_branch + · apply star_one + · apply transition.trans_branch rotate_right - . exact codelen code2 - . grind - . grind + · exact codelen code2 + · grind + · grind case neg isFalse => simp [isFalse] rw [heq3] @@ -490,8 +490,8 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s rw [heq1, heq2, heq3] simp [codelen_app, codelen_singleton] apply star_trans - . apply compile_bexp_correct C s b 0 (codelen code_body + 1) pc stk (by grind) - . grind + · apply compile_bexp_correct C s b 0 (codelen code_body + 1) pc stk (by grind) + · grind case cexec_while_loop s b c1 s_intermediate s' isTrue cexec1 cexec2 ih1 ih2 => intro C pc stk generalize heq1 : compile_com c1 = code_body @@ -501,23 +501,23 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s rw [heq1, heq2, heq3] intro h apply star_trans - . apply compile_bexp_correct C s b 0 (codelen code_body + 1) pc stk (by grind) - . apply star_trans - . simp [isTrue] + · apply compile_bexp_correct C s b 0 (codelen code_body + 1) pc stk (by grind) + · apply star_trans + · simp [isTrue] rw [heq2] specialize ih1 C (pc + codelen code_branch) stk apply ih1 grind - . apply star_trans - . apply star_one + · apply star_trans + · apply star_one apply transition.trans_branch rotate_left rotate_left - . exact d - . exact (pc + codelen code_branch + codelen code_body + 1 + d) - . grind - . grind - . specialize ih2 C (pc + codelen code_branch + codelen code_body + 1 + d) stk + · exact d + · exact (pc + codelen code_branch + codelen code_body + 1 + d) + · grind + · grind + · specialize ih2 C (pc + codelen code_branch + codelen code_body + 1 + d) stk suffices h2 : code_at C (pc + codelen code_branch + codelen code_body + 1 + d) (compile_com (com.WHILE b c1)) from by specialize ih2 h2 simp [compile_com] at ih2 @@ -532,29 +532,29 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s grind inductive compile_cont (C: List instr) : cont -> Int -> Prop where - | ccont_stop: forall pc, + | ccont_stop: ∀ pc, instr_at C pc = .some .Ihalt -> compile_cont C .Kstop pc - | ccont_seq: forall c k pc pc', + | ccont_seq: ∀ c k pc pc', code_at C pc (compile_com c) -> pc' = pc + codelen (compile_com c) -> compile_cont C k pc' -> compile_cont C (.Kseq c k) pc - | ccont_while: forall b c k pc d pc' pc'', + | ccont_while: ∀ b c k pc d pc' pc'', instr_at C pc = .some (.Ibranch d) -> pc' = pc + 1 + d -> code_at C pc' (compile_com (.WHILE b c)) -> pc'' = pc' + codelen (compile_com (.WHILE b c)) -> compile_cont C k pc'' -> compile_cont C (.Kwhile b c k) pc - | ccont_branch: forall d k pc pc', + | ccont_branch: ∀ d k pc pc', instr_at C pc = .some (.Ibranch d) -> pc' = pc + 1 + d -> compile_cont C k pc' -> compile_cont C k pc inductive match_config (C: List instr): com × cont × store -> config -> Prop where - | match_config_intro: forall c k st pc, + | match_config_intro: ∀ c k st pc, code_at C pc (compile_com c) -> compile_cont C k (pc + codelen (compile_com c)) -> match_config C (c, k, st) (pc, [], st) @@ -568,9 +568,9 @@ def com_size (c: com) : Nat := | .WHILE _ c1 => (com_size c1 + 1) -theorem com_size_nonzero: forall c, (com_size c > 0) := by +theorem com_size_nonzero: ∀ c, (com_size c > 0) := by intro c - fun_induction com_size <;> grind + fun_induction com_size with grind def cont_size (k: cont) : Nat := match k with @@ -619,38 +619,38 @@ theorem compile_cont_Kwhile_inv (C : List instr) (b : bexp) (c : com) (k : cont) intro pc₄ ih exists pc₄ apply And.intro - . rw [h₄] at ih + · rw [h₄] at ih rw [←h₂] rw [←h₂] at ih apply plus.plus_left rotate_left - . apply plus_star + · apply plus_star exact ih.1 - . apply transition.trans_branch + · apply transition.trans_branch rotate_left - . exact rfl - . grind - . grind + · 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 + · 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 constructor - . cases H <;> grind - . grind + · cases H <;> grind + · grind theorem simulation_step: - forall C impconf1 impconf2 machconf1, + ∀ C impconf1 impconf2 machconf1, step impconf1 impconf2 -> match_config C impconf1 machconf1 -> - exists machconf2, + ∃ machconf2, (plus (transition C) machconf1 machconf2 \/ (star (transition C) machconf1 machconf2 /\ (measure' impconf2 < measure' impconf1))) @@ -670,8 +670,8 @@ theorem simulation_step: rotate_left exact a rotate_left - . grind - . apply transition.trans_setvar + · grind + · apply transition.trans_setvar rotate_left exact x grind @@ -689,11 +689,11 @@ theorem simulation_step: simp [compile_com] at h₁ grind apply compile_cont.ccont_seq - . grind + · grind rotate_right - . exact pc + codelen (compile_com c') + codelen (compile_com c2) - . rfl - . grind + · exact pc + codelen (compile_com c') + codelen (compile_com c2) + · rfl + · grind next b c1 c2 => generalize h₃ : compile_com c1 = code1 generalize h₄ : compile_bexp b 0 (codelen code1 + 1) = codeb @@ -703,17 +703,17 @@ theorem simulation_step: constructor apply Or.intro_right constructor - . apply compile_bexp_correct + · apply compile_bexp_correct rotate_left - . exact b - . exact 0 - . exact (codelen code1 + 1) - . grind - . simp [measure', com_size] + · exact b + · exact 0 + · exact (codelen code1 + 1) + · grind + · simp [measure', com_size] grind - . rw [h₄] + · rw [h₄] constructor - . by_cases beval st b = true + · by_cases beval st b = true case pos isTrue => simp [isTrue] at * grind @@ -724,14 +724,14 @@ theorem simulation_step: simp [codelen_cons, codelen_app] at this simp [codelen] at * grind - . by_cases beval st b = true + · by_cases beval st b = true case pos isTrue => simp [isTrue] at * apply compile_cont.ccont_branch rotate_right - . exact (pc + codelen (codeb ++ (code1 ++ instr.Ibranch (codelen code2) :: code2))) + · exact (pc + codelen (codeb ++ (code1 ++ instr.Ibranch (codelen code2) :: code2))) rotate_right - . exact codelen code2 + · exact codelen code2 any_goals grind case neg isFalse => simp [isFalse] at * @@ -743,52 +743,52 @@ theorem simulation_step: constructor apply Or.intro_right constructor - . apply compile_bexp_correct + · apply compile_bexp_correct rotate_left - . exact b - . exact 0 - . exact (codelen codec + 1) - . grind - . simp [measure', com_size] - fun_induction com_size <;> grind - . simp [isFalse] + · exact b + · exact 0 + · exact (codelen codec + 1) + · grind + · simp [measure', com_size] + fun_induction com_size with grind + · simp [isFalse] rw [h₄] simp [compile_com] at h₂ h₁ rw [h₃, h₄] at h₂ h₁ constructor - . grind - . grind + · grind + · grind next b isTrue => generalize h₃ : compile_com c' = codec generalize h₄ : compile_bexp b 0 (codelen codec + 1) = codeb constructor constructor - . apply Or.intro_right + · apply Or.intro_right constructor - . apply compile_bexp_correct + · apply compile_bexp_correct rotate_left - . exact b - . exact 0 - . exact (codelen codec + 1) - . grind - . simp [measure', cont_size, com_size] - . simp [isTrue] + · exact b + · exact 0 + · exact (codelen codec + 1) + · grind + · simp [measure', cont_size, com_size] + · simp [isTrue] rw [h₄] constructor - . simp [compile_com] at h₁ + · simp [compile_com] at h₁ rw [h₃, h₄] at h₁ grind - . simp [compile_com, h₃, h₄] at h₁ h₂ + · simp [compile_com, h₃, h₄] at h₁ h₂ apply compile_cont.ccont_while rotate_left 4 - . exact h₂ - . exact (-(codelen codeb + codelen codec + 1)) + · exact h₂ + · exact (-(codelen codeb + codelen codec + 1)) rotate_left 3 - . simp [compile_com, h₃, h₄] + · simp [compile_com, h₃, h₄] exact h₁ - . grind - . grind - . grind + · grind + · grind + · grind next => have := compile_cont_Kseq_inv C c' k' pc st (by simp [compile_com, codelen] at h₂; grind) apply Exists.elim this @@ -796,13 +796,13 @@ theorem simulation_step: intro ⟨w₁, w₂⟩ exists (pc', [], st) constructor - . apply Or.intro_right + · apply Or.intro_right constructor - . exact w₁ - . simp [measure', cont_size, com_size] - . constructor - . exact w₂.1 - . simp [compile_com, codelen] at h₂ + · exact w₁ + · simp [measure', cont_size, com_size] + · constructor + · exact w₂.1 + · simp [compile_com, codelen] at h₂ grind next b c => have := compile_cont_Kwhile_inv C b c k' pc st (by simp [compile_com, codelen] at h₂; grind) @@ -811,16 +811,16 @@ theorem simulation_step: intro ⟨ w₁, w₂ ⟩ exists (pc', [], st) constructor - . apply Or.intro_left - . exact w₁ - . constructor - . exact w₂.1 - . exact w₂.2 + · apply Or.intro_left + · exact w₁ + · constructor + · exact w₂.1 + · exact w₂.2 theorem simulation_steps: - forall C impconf1 impconf2, star step impconf1 impconf2 -> - forall machconf1, match_config C impconf1 machconf1 -> - exists machconf2, + ∀ C impconf1 impconf2, star step impconf1 impconf2 -> + ∀ machconf1, match_config C impconf1 machconf1 -> + ∃ machconf2, star (transition C) machconf1 machconf2 /\ match_config C impconf2 machconf2 := by intro C impconf1 impconf2 STAR machconf1 MATCH @@ -828,8 +828,8 @@ theorem simulation_steps: case star_refl x => exists machconf1 constructor - . apply star.star_refl - . exact MATCH + · apply star.star_refl + · exact MATCH case star_step x y z STEP STAR ih => have ⟨ machconf2, steps2, match2 ⟩ := simulation_step C x y machconf1 STEP MATCH specialize ih machconf2 match2 @@ -843,29 +843,29 @@ theorem simulation_steps: case inr h => exact h.1 constructor - . apply star_trans - . exact w - . exact steps3 - . exact match3 + · apply star_trans + · exact w + · exact steps3 + · exact match3 theorem instr_at_len : instr_at (C ++ [i]) (codelen C) = .some i := by induction C with grind theorem match_initial_configs: - forall c s, + ∀ c s, match_config (compile_program c) (c, .Kstop, s) (0, [], s) := by intro c s generalize heq : compile_com c = C constructor - . simp [compile_program] + · simp [compile_program] have := code_at.code_at_intro [] C [instr.Ihalt] 0 (by simp [codelen]) grind [List.nil_append] - . simp [compile_program, heq] + · simp [compile_program, heq] constructor grind theorem compile_program_correct_terminating_2: - forall c s s', + ∀ c s s', star step (c, .Kstop, s) (.SKIP, .Kstop, s') -> machine_terminates (compile_program c) s s' := by intro c s s' STAR @@ -876,17 +876,17 @@ theorem compile_program_correct_terminating_2: have ⟨pc', D, E ⟩ := compile_cont_Kstop_inv C (pc + codelen (compile_com com.SKIP)) s' w2 exists pc' constructor - . apply star_trans - . exact A - . simp [compile_com, codelen] at D + · apply star_trans + · exact A + · simp [compile_com, codelen] at D exact D - . exact E + · exact E theorem simulation_infseq_inv: - forall C n impconf1 machconf1, + ∀ C n impconf1 machconf1, infseq step impconf1 -> match_config C impconf1 machconf1 -> (measure' impconf1 < n) -> - exists impconf2 machconf2, + ∃ impconf2 machconf2, infseq step impconf2 /\ plus (transition C) machconf1 machconf2 /\ match_config C impconf2 machconf2 := by @@ -908,15 +908,15 @@ theorem simulation_infseq_inv: exists c1 exists m1 constructor - . exact w.1 - . constructor - . apply star_plus_trans - . exact STAR - . exact w.2.1 - . exact w.2.2 + · exact w.1 + · constructor + · apply star_plus_trans + · exact STAR + · exact w.2.1 + · exact w.2.2 theorem compile_program_correct_diverging: - forall c s, + ∀ c s, infseq step (c, .Kstop, s) -> machine_diverges (compile_program c) s := by intro c s H @@ -924,14 +924,14 @@ theorem compile_program_correct_diverging: unfold machine_diverges apply infseq_coinduction_principle_2 (fun machconf => ∃ impconf, infseq step impconf /\ match_config C impconf machconf) rotate_left - . exists (c, .Kstop, s) + · exists (c, .Kstop, s) constructor - . exact H - . have := match_initial_configs c s + · exact H + · have := match_initial_configs c s grind - . intro machconf ⟨ impconf , ⟨INFSEQ, MATCH ⟩⟩ + · intro machconf ⟨ impconf , ⟨INFSEQ, MATCH ⟩⟩ have ⟨impconf2 , machconf2, INFSEQ2 , PLUS , MATCH2⟩ := simulation_infseq_inv C (measure' impconf +1) impconf machconf INFSEQ MATCH (by omega) exists machconf2 constructor - . exact PLUS - . exists impconf2 + · exact PLUS + · exists impconf2 diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean index 9f9b96a..79439da 100644 --- a/LeroyCompilerVerificationCourse/Constprop.lean +++ b/LeroyCompilerVerificationCourse/Constprop.lean @@ -52,12 +52,12 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where #eval simplif_aexp (.MINUS (.PLUS (.VAR "x") (.CONST 1)) (.PLUS (.VAR "y") (.CONST 1))) @[grind] theorem mk_PLUS_CONST_sound: - forall s a n, aeval s (mk_PLUS_CONST a n) = aeval s a + n := by + ∀ s a n, aeval s (mk_PLUS_CONST a n) = aeval s a + n := by intro s a n fun_cases mk_PLUS_CONST a n <;> grind theorem mk_PLUS_sound: - forall s a1 a2, aeval s (mk_PLUS a1 a2) = aeval s a1 + aeval s a2 := by + ∀ s a1 a2, aeval s (mk_PLUS a1 a2) = aeval s a1 + aeval s a2 := by intro s a1 a2 fun_cases mk_PLUS a1 a2 <;> (try (simp [aeval]) ; try (simp [mk_PLUS_CONST_sound ]) ; grind) @@ -65,11 +65,11 @@ theorem mk_PLUS_sound: grind theorem mk_MINUS_sound: - forall s a1 a2, aeval s (mk_MINUS a1 a2) = aeval s a1 - aeval s a2 := by + ∀ s a1 a2, aeval s (mk_MINUS a1 a2) = aeval s a1 - aeval s a2 := by intro s a1 a2 fun_cases mk_MINUS a1 a2 <;> (try (simp [aeval]) ; try (simp [mk_PLUS_CONST_sound ]) ; grind) -theorem simplif_aexp_sound : forall s a, aeval s (simplif_aexp a) = aeval s a := by +theorem simplif_aexp_sound : ∀ s a, aeval s (simplif_aexp a) = aeval s a := by intro s a induction a any_goals grind [mk_PLUS_sound, mk_MINUS_sound] @@ -102,22 +102,22 @@ theorem simplif_aexp_sound : forall s a, aeval s (simplif_aexp a) = aeval s a := | _, _ => .AND b1 b2 theorem mk_EQUAL_sound: - forall s a1 a2, beval s (mk_EQUAL a1 a2) = (aeval s a1 = aeval s a2) := by + ∀ s a1 a2, beval s (mk_EQUAL a1 a2) = (aeval s a1 = aeval s a2) := by intro s a1 a2 fun_cases (mk_EQUAL a1 a2) <;> grind theorem mk_LESSEQUAL_sound: - forall s a1 a2, beval s (mk_LESSEQUAL a1 a2) = (aeval s a1 <= aeval s a2) := by + ∀ s a1 a2, beval s (mk_LESSEQUAL a1 a2) = (aeval s a1 <= aeval s a2) := by intro s a1 a2 fun_cases mk_LESSEQUAL a1 a2 <;> grind theorem mk_NOT_sound : - forall s b, beval s (mk_NOT b) = ¬ (beval s b) := by + ∀ s b, beval s (mk_NOT b) = ¬ (beval s b) := by intros s b fun_cases (mk_NOT b) <;> grind theorem mk_AND_sound: - forall s b1 b2, beval s (mk_AND b1 b2) = (beval s b1 ∧ beval s b2) := by + ∀ s b1 b2, beval s (mk_AND b1 b2) = (beval s b1 ∧ beval s b2) := by intro s b1 b2 fun_cases mk_AND b1 b2 any_goals grind @@ -133,19 +133,19 @@ theorem mk_AND_sound: | .FALSE => .SKIP | _ => .WHILE b c -theorem cexec_mk_IFTHENELSE: forall s1 b c1 c2 s2, +theorem cexec_mk_IFTHENELSE: ∀ s1 b c1 c2 s2, cexec s1 (if beval s1 b then c1 else c2) s2 -> cexec s1 (mk_IFTHENELSE b c1 c2) s2 := by intro s1 b c1 c2 s2 fun_cases (mk_IFTHENELSE b c1 c2) <;> grind -theorem cexec_mk_WHILE_done: forall s1 b c, +theorem cexec_mk_WHILE_done: ∀ s1 b c, beval s1 b = false -> cexec s1 (mk_WHILE b c) s1 := by intro s1 b c H fun_cases mk_WHILE b c <;> grind -theorem cexec_mk_WHILE_loop: forall b c s1 s2 s3, +theorem cexec_mk_WHILE_loop: ∀ b c s1 s2 s3, beval s1 b = true -> cexec s1 c s2 -> cexec s2 (mk_WHILE b c) s3 -> cexec s1 (mk_WHILE b c) s3 := by intro b c s1 s2 s3 h1 h2 h3 @@ -153,10 +153,10 @@ theorem cexec_mk_WHILE_loop: forall b c s1 s2 s3, def Store := Std.HashMap ident Int @[grind] def matches' (s: store) (S: Store): Prop := - forall x n, S.get? x = .some n -> s x = n + ∀ x n, S.get? x = .some n -> s x = n @[grind] def Le (S1 S2: Store) : Prop := - forall x n, S2.get? x = .some n -> S1.get? x = .some n + ∀ x n, S2.get? x = .some n -> S1.get? x = .some n @[grind] def Top : Store := Std.HashMap.emptyWithCapacity @@ -169,17 +169,17 @@ def Equal (S1 S2: Store) := Std.HashMap.Equiv S1 S2 noncomputable instance : Decidable (Equal S' S) := Classical.propDecidable (Equal S' S) -theorem matches_Le: forall s S1 S2, Le S1 S2 -> matches' s S1 -> matches' s S2 := by +theorem matches_Le: ∀ s S1 S2, Le S1 S2 -> matches' s S1 -> matches' s S2 := by intro s S1 S2 h1 h2 grind -theorem Le_Top: forall S, Le S Top := by +theorem Le_Top: ∀ S, Le S Top := by unfold Le Top intros grind [Std.HashMap] @[grind] theorem Join_characterization: -forall S1 S2 x n, +∀ S1 S2 x n, (Join S1 S2).get? x = .some n ↔ S1.get? x = .some n ∧ S2.get? x = .some n := by intro S1 S2 x n @@ -190,11 +190,11 @@ forall S1 S2 x n, simp [Join] grind -theorem Le_Join_l: forall S1 S2, Le S1 (Join S1 S2) := by intros; grind +theorem Le_Join_l: ∀ S1 S2, Le S1 (Join S1 S2) := by intros; grind -theorem Le_Join_r: forall S1 S2, Le S2 (Join S1 S2) := by intros; grind +theorem Le_Join_r: ∀ S1 S2, Le S2 (Join S1 S2) := by intros; grind -theorem Equal_Le: forall S1 S2, Equal S1 S2 -> Le S1 S2 := by +theorem Equal_Le: ∀ S1 S2, Equal S1 S2 -> Le S1 S2 := by intro S1 S2 eq unfold Equal at eq unfold Le @@ -228,8 +228,8 @@ theorem Equal_Le: forall S1 S2, Equal S1 S2 -> Le S1 S2 := by | .AND b1 b2 => lift2 (fun m n => m && n) (Beval S b1) (Beval S b2) @[grind] theorem Aeval_sound: - forall s S, matches' s S -> - forall a n, Aeval S a = .some n -> aeval s a = n := by + ∀ s S, matches' s S -> + ∀ a n, Aeval S a = .some n -> aeval s a = n := by intro s S h1 a n h2 induction a generalizing n any_goals grind @@ -243,8 +243,8 @@ theorem Equal_Le: forall S1 S2, Equal S1 S2 -> Le S1 S2 := by split at h2 <;> grind theorem Beval_sound: - forall s S, matches' s S -> - forall b n, Beval S b = .some n -> beval s b = n := by + ∀ s S, matches' s S -> + ∀ b n, Beval S b = .some n -> beval s b = n := by intro s S h1 b n h2 induction b generalizing n any_goals grind @@ -272,7 +272,7 @@ theorem Beval_sound: | .none => S.erase x | .some n => S.insert x n -@[grind] theorem update_characterisation : forall S x N y, +@[grind] theorem update_characterisation : ∀ S x N y, (Update x N S).get? y = if x == y then N else S.get? y := by intro S x N y simp @@ -287,9 +287,9 @@ theorem Beval_sound: unfold Update grind -theorem matches_update: forall s S x n N, +theorem matches_update: ∀ s S x n N, matches' s S -> - (forall i, N = .some i -> n = i) -> + (∀ i, N = .some i -> n = i) -> matches' (update x n s) (Update x N S) := by intro s S x n N m h grind @@ -308,7 +308,7 @@ theorem matches_update: forall s S x n N, theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint F init_S) : Le (F S) S := by - have A : forall fuel S, + have A : ∀ fuel S, fixpoint_rec F fuel S = Top \/ Equal (F (fixpoint_rec F fuel S)) (fixpoint_rec F fuel S) := by intro fuel @@ -334,7 +334,7 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint fixpoint (fun x => Join S (Cexec x c1)) S @[grind] theorem Cexec_sound: - forall c s1 s2 S1, + ∀ c s1 s2 S1, cexec s1 c s2 -> matches' s1 S1 -> matches' s2 (Cexec S1 c) := by intro c induction c @@ -368,7 +368,7 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint intro s1 s2 S1 EXEC MATCHES generalize eq1 : (fun x => Join S1 (Cexec x c)) = F generalize eq2 : fixpoint F S1 = X - have INNER : forall s1 c1 s2, + have INNER : ∀ s1 c1 s2, cexec s1 c1 s2 -> c1 = .WHILE b c -> matches' s1 X -> @@ -378,12 +378,12 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint any_goals grind case cexec_while_loop s' b' c' s5 s6 EXEC2 EXEC3 EXEC4 _ a_ih2 => apply a_ih2 - . grind - . apply matches_Le + · grind + · apply matches_Le rotate_right - . exact F X - . exact @fixpoint_sound X F S1 (by grind) - . rw [←eq2, ←eq1] + · exact F X + · exact @fixpoint_sound X F S1 (by grind) + · rw [←eq2, ←eq1] simp apply matches_Le apply Le_Join_r @@ -397,20 +397,20 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint unfold Cexec rw [eq1, eq2] apply INNER - . apply EXEC - . rfl - . apply matches_Le + · apply EXEC + · rfl + · apply matches_Le have := @fixpoint_sound X F apply this rotate_left - . exact S1 + · exact S1 rotate_left - . grind - . rw [←eq1] + · grind + · rw [←eq1] simp apply matches_Le - . apply Le_Join_l - . exact MATCHES + · apply Le_Join_l + · exact MATCHES @[grind] def cp_aexp (S: Store) (a: aexp) : aexp := match a with @@ -432,14 +432,14 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint | .AND b1 b2 => mk_AND (cp_bexp S b1) (cp_bexp S b2) @[grind] theorem cp_aexp_sound: - forall s S, matches' s S -> - forall a, aeval s (cp_aexp S a) = aeval s a := by + ∀ s S, matches' s S -> + ∀ a, aeval s (cp_aexp S a) = aeval s a := by intro s S AG a induction a <;> grind [mk_PLUS_sound, mk_MINUS_sound] theorem cp_bexp_sound: - forall s S, matches' s S -> - forall b, beval s (cp_bexp S b) = beval s b := by + ∀ s S, matches' s S -> + ∀ b, beval s (cp_bexp S b) = beval s b := by intro s S AG b induction b any_goals grind [mk_EQUAL_sound, mk_LESSEQUAL_sound, mk_AND_sound, mk_NOT_sound] @@ -458,7 +458,7 @@ theorem cp_bexp_sound: mk_WHILE (cp_bexp sfix b) (cp_com sfix c) theorem cp_com_correct_terminating: - forall c s1 s2 S1, + ∀ c s1 s2 S1, cexec s1 c s2 -> matches' s1 S1 -> cexec s1 (cp_com S1 c) s2 := by intro c s1 s2 S1 EXEC AG induction c generalizing s1 s2 S1 @@ -477,7 +477,7 @@ theorem cp_com_correct_terminating: case WHILE b c c_ih => generalize heq1 : com.WHILE b c = loop generalize heq2 : Cexec S1 (.WHILE b c) = X - have INNER: forall s1 c1 s2, + have INNER: ∀ s1 c1 s2, cexec s1 c1 s2 -> c1 = .WHILE b c -> matches' s1 X -> @@ -494,36 +494,36 @@ theorem cp_com_correct_terminating: any_goals grind case cexec_while_done isFalse => apply cexec_mk_WHILE_done - . grind [cp_bexp_sound] + · grind [cp_bexp_sound] case cexec_while_loop s3 b' c' s4 s5 isTrue EXEC2 EXEC3 a_ih a_ih2 => apply cexec_mk_WHILE_loop - . grind [cp_bexp_sound] - . apply c_ih - . injections heq4 heq5 + · grind [cp_bexp_sound] + · apply c_ih + · injections heq4 heq5 rw [heq2'] at heq5 rw [←heq5] at EXEC2 exact EXEC2 - . exact AG1 - . apply a_ih2 + · exact AG1 + · apply a_ih2 rotate_left - . grind - . apply matches_Le + · grind + · apply matches_Le rw [←heq2] simp [Cexec] apply fixpoint_sound rotate_left - . exact (fun x => Join S1 (Cexec x c)) - . exact S1 + · exact (fun x => Join S1 (Cexec x c)) + · exact S1 rotate_left - . grind - . apply matches_Le - . apply Le_Join_r - . apply Cexec_sound - . rw [←heq2'] + · grind + · apply matches_Le + · apply Le_Join_r + · apply Cexec_sound + · rw [←heq2'] injections heq3 heq4 rw [heq4] exact EXEC2 - . grind + · grind rw [heq1] at EXEC induction EXEC any_goals grind @@ -534,12 +534,12 @@ theorem cp_com_correct_terminating: rw [←heq3, ←heq4, heq2] apply INNER any_goals grind - . rw [←heq2] + · rw [←heq2] simp [Cexec] apply matches_Le - . apply fixpoint_sound + · apply fixpoint_sound rotate_left - . exact (fun x => Join S1 (Cexec x c)) - . exact S1 - . grind - . grind + · exact (fun x => Join S1 (Cexec x c)) + · exact S1 + · grind + · grind diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean index 40643d9..0ae5d85 100644 --- a/LeroyCompilerVerificationCourse/Deadcode.lean +++ b/LeroyCompilerVerificationCourse/Deadcode.lean @@ -114,7 +114,7 @@ theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F deadcode_fixpoint (fun x => L' ∪ (live c x)) default theorem live_upper_bound: - forall c L, + ∀ c L, (live c L) ⊆ ((fv_com c) ∪ L) := by intro c induction c @@ -225,10 +225,10 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet) | .WHILE b c => .WHILE b (dce c (live (.WHILE b c) L)) @[grind] def agree (L: IdentSet) (s1 s2: store) : Prop := - forall x, x ∈ L -> s1 x = s2 x + ∀ x, x ∈ L -> s1 x = s2 x @[grind] theorem agree_mon: - forall L L' s1 s2, + ∀ L L' s1 s2, agree L' s1 s2 -> L ⊆ L' -> agree L s1 s2 := by intro L L' s1 s2 AG sub unfold agree at * @@ -238,8 +238,8 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet) exact AG @[grind] theorem aeval_agree: - forall L s1 s2, agree L s1 s2 -> - forall a, (fv_aexp a) ⊆ L -> aeval s1 a = aeval s2 a := by + ∀ L s1 s2, agree L s1 s2 -> + ∀ a, (fv_aexp a) ⊆ L -> aeval s1 a = aeval s2 a := by intro L s1 s2 AG a induction a any_goals grind @@ -289,7 +289,7 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet) theorem beval_agree: ∀ L s1 s2, agree L s1 s2 -> - forall b, (fv_bexp b) ⊆ L -> beval s1 b = beval s2 b := by + ∀ b, (fv_bexp b) ⊆ L -> beval s1 b = beval s2 b := by intro L s1 s2 AG b induction b any_goals grind @@ -343,7 +343,7 @@ theorem beval_agree: grind theorem agree_update_live: - forall s1 s2 L x v, + ∀ s1 s2 L x v, agree (L.erase x) s1 s2 -> agree L (update x v s1) (update x v s2) := by intro s1 s2 L x v AG @@ -359,7 +359,7 @@ theorem agree_update_live: grind theorem agree_update_dead: - forall s1 s2 L x v, + ∀ s1 s2 L x v, agree L s1 s2 -> ¬x ∈ L -> agree L (update x v s1) s2 := by intro s1 s2 L x v AG not @@ -370,9 +370,9 @@ theorem agree_update_dead: by_cases x=y <;> grind theorem dce_correct_terminating: - forall s c s', cexec s c s' -> - forall L s1, agree (live c L) s s1 -> - exists s1', cexec s1 (dce c L) s1' /\ agree L s' s1' := by + ∀ s c s', cexec s c s' -> + ∀ L s1, agree (live c L) s s1 -> + ∃ s1', cexec s1 (dce c L) s1' /\ agree L s' s1' := by intro s c s' EXEC induction EXEC any_goals grind @@ -381,19 +381,19 @@ theorem dce_correct_terminating: have := live_while_charact b c1 L (live (com.WHILE b c1) L) (by grind) have : agree (live c1 (live (com.WHILE b c1) L)) s1 s4 := by apply agree_mon - . exact hyp - . grind + · exact hyp + · grind have ⟨ t1, ht1, ht2⟩ := a_ih (live (.WHILE b c1) L) s4 this have ⟨u1, hu1, hu2 ⟩ := a_ih2 L t1 ht2 exists u1 constructor rotate_right - . exact hu2 - . apply cexec.cexec_while_loop - . have := beval_agree (live (com.WHILE b c1) L) s1 s4 hyp b (by grind) + · exact hu2 + · apply cexec.cexec_while_loop + · have := beval_agree (live (com.WHILE b c1) L) s1 s4 hyp b (by grind) grind - . exact ht1 - . grind + · exact ht1 + · grind case cexec_assign s2 x a=> intro L s3 AG simp [live] at AG @@ -401,19 +401,19 @@ theorem dce_correct_terminating: case neg notIn => exists s3 constructor - . grind [dce] - . simp [notIn] at AG + · grind [dce] + · simp [notIn] at AG exact @agree_update_dead s2 s3 L x (aeval s2 a) (by grind) notIn case pos isIn => simp [isIn] at AG exists (update x (aeval s3 a) s3) constructor - . simp [dce, isIn] + · simp [dce, isIn] grind - . have subgoal : aeval s2 a = aeval s3 a := by + · have subgoal : aeval s2 a = aeval s3 a := by apply aeval_agree - . exact AG - . intro y mem + · exact AG + · intro y mem grind rw [subgoal] apply @agree_update_live @@ -423,8 +423,8 @@ theorem dce_correct_terminating: simp [dce] have EQ : beval s2 b = beval s4 b := by apply beval_agree - . apply AG - . simp [live] + · apply AG + · simp [live] intro y mem grind by_cases beval s2 b = true @@ -436,9 +436,9 @@ theorem dce_correct_terminating: have ⟨s5 , EX', AG' ⟩ := ih (by grind) exists s5 constructor - . apply cexec.cexec_ifthenelse + · apply cexec.cexec_ifthenelse grind - . exact AG' + · exact AG' case neg isFalse => simp [isFalse] at EXEC specialize ih L s4 @@ -447,16 +447,16 @@ theorem dce_correct_terminating: have ⟨s5 , EX', AG' ⟩ := ih (by grind) exists s5 constructor - . apply cexec.cexec_ifthenelse + · apply cexec.cexec_ifthenelse grind - . exact AG' + · exact AG' case cexec_while_done s2 b c isFalse => intro L s1 AG have ⟨ h1 , h2 , h3 ⟩ := live_while_charact b c L (live (com.WHILE b c) L) (by grind) have EQ : beval s2 b = beval s1 b := by apply beval_agree - . apply AG - . intro y mem + · apply AG + · intro y mem specialize h1 y mem exact h1 exists s1 diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean index e9a7758..7607267 100644 --- a/LeroyCompilerVerificationCourse/Fixpoints.lean +++ b/LeroyCompilerVerificationCourse/Fixpoints.lean @@ -39,7 +39,7 @@ variable (α : Sort u) (F : α → α) [OrderWithBot α] open OrderStruct OrderWithBot theorem fixpoint_exists_1 [Monotone α F] : ∃ x : α, eq x (F x) := by - have REC : forall x : α, le x (F x) -> exists y : α , eq y (F y) := by + have REC : ∀ x : α, le x (F x) -> ∃ y : α , eq y (F y) := by intro x induction x using @WellFounded.induction α gt gt_wf case h x ih => @@ -50,11 +50,11 @@ theorem fixpoint_exists_1 [Monotone α F] : ∃ x : α, eq x (F x) := by grind [beq_true'] case neg isFalse => apply ih (F x) - . constructor - . exact h - . apply beq_false' + · constructor + · exact h + · apply beq_false' grind - . exact F_mon h + · exact F_mon h specialize REC apply REC apply bot_smallest @@ -71,19 +71,19 @@ instance : WellFoundedRelation α where rel := gt wf := gt_wf -@[grind] def iterate (x : α) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z) : α := +@[grind] def iterate (x : α) (PRE: le x (F x)) (SMALL: ∀ z, le (F z) z -> le x z) : α := if beq x (F x) then x else iterate (F x) (by apply F_mon; exact PRE) (by intro z hyp; specialize SMALL z hyp; apply le_trans; apply F_mon; exact SMALL; exact hyp) termination_by x decreasing_by grind [beq_false'] -@[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 +@[grind] theorem iterate_correct (x : α) (PRE: le x (F x)) (SMALL: ∀ 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 => constructor - . rw [←heq] at PRE + · rw [←heq] at PRE grind [beq_true'] - . intro z hyp + · intro z hyp specialize SMALL z hyp grind case case2 ih => @@ -103,10 +103,10 @@ theorem fixpoint_correct : unfold fixpoint' apply iterate_correct rotate_left - . exact bot - . apply bot_smallest - . grind [bot_smallest] - . rfl + · exact bot + · apply bot_smallest + · grind [bot_smallest] + · rfl end Fixpoint section Constprop @@ -142,11 +142,11 @@ theorem hash_set_incl_size_leq (S1 S2 : Store) : Le S2 S1 → List.Subperm (S1.t intro LE unfold Le at LE apply List.subperm_of_subset - . apply List.Pairwise.imp + · apply List.Pairwise.imp rotate_left - . exact distinct_keys_toList - . grind - . intro (k,v) mem + · exact distinct_keys_toList + · grind + · intro (k,v) mem specialize LE k v (by grind) grind @@ -168,7 +168,7 @@ theorem hash_set_incl_size_leq (S1 S2 : Store) : Le S2 S1 → List.Subperm (S1.t grind @[grind] theorem Gt_cardinal: - forall S S', Gt S S' -> S.size < S'.size := by + ∀ S S', Gt S S' -> S.size < S'.size := by intro S S' hyp unfold Gt at hyp have ⟨ t₁, t₂ ⟩ := @Le_cardinal S S' (hyp.1) @@ -220,8 +220,8 @@ instance : Monotone Store (fun x => Join Init (F x)) where have ⟨ h1, h2 ⟩:= (Join_characterization Init (F y) z n).1 isSome apply (Join_characterization (Init) (F x) z n).2 constructor - . exact h1 - . apply @F_mon _ _ _ _ _ y le + · exact h1 + · apply @F_mon _ _ _ _ _ y le exact h2 noncomputable def fixpoint_join : Store := by @@ -242,65 +242,65 @@ theorem fixpoint_join_eq: Eq' (Join Init (F (fixpoint_join Init F) )) (fixpoint_ simp [fixpoint_join] at * have := (@iterate_correct Store _ (fun x => Join Init (F x)) _ ?_ ?_ ?_ ?_ ?_ ).1 unfold Eq' - . exact this - . exact Init - . dsimp + · exact this + · exact Init + · dsimp apply Le_Join_l - . intro z hyp + · intro z hyp unfold le instOrderStructStore dsimp unfold Le intro x n hyp2 specialize hyp x n hyp2 grind - . rw [heq1] + · rw [heq1] theorem fixpoint_join_sound : Le Init (fixpoint_join Init F) /\ Le (F (fixpoint_join Init F)) (fixpoint_join Init F) := by have LE : Le (Join Init (F (fixpoint_join Init F))) (fixpoint_join Init F) := by apply Eq_Le apply fixpoint_join_eq constructor - . apply Le_trans + · apply Le_trans rotate_left - . exact LE - . apply Le_Join_l - . apply Le_trans + · exact LE + · apply Le_Join_l + · apply Le_trans rotate_left - . exact LE - . apply Le_Join_r + · exact LE + · apply Le_Join_r theorem fixpoint_join_smallest: - forall S, Le (Join Init (F S)) S -> Le (fixpoint_join Init F) S := by + ∀ S, Le (Join Init (F S)) S -> Le (fixpoint_join Init F) S := by intro S LE unfold fixpoint_join dsimp have := (@iterate_correct Store _ (fun x => Join Init (F x)) _ (fixpoint_join Init F) Init (?_) ?_ ?_).2 S LE exact this - . dsimp + · dsimp apply Le_Join_l - . intro z hyp + · intro z hyp unfold le instOrderStructStore dsimp unfold Le intro x n hyp2 specialize hyp x n hyp2 grind - . unfold fixpoint_join + · unfold fixpoint_join dsimp @[grind] theorem Join_increasing: - forall S1 S2 S3 S4, + ∀ S1 S2 S3 S4, Le S1 S2 -> Le S3 S4 -> Le (Join S1 S3) (Join S2 S4) := by intros grind @[grind] theorem Aeval_increasing: ∀ S1 S2, Le S1 S2 -> - forall a n, Aeval S2 a = .some n -> Aeval S1 a =.some n := by + ∀ a n, Aeval S2 a = .some n -> Aeval S1 a =.some n := by intro S1 S2 LE a induction a <;> grind @[grind] theorem Beval_increasing : ∀ S1 S2, Le S1 S2 -> - forall b n, Beval S2 b = .some n -> Beval S1 b = .some n := by + ∀ b n, Beval S2 b = .some n -> Beval S1 b = .some n := by intro S1 S2 LE b induction b any_goals grind @@ -310,7 +310,7 @@ theorem fixpoint_join_smallest: grind theorem Update_increasing: - forall S1 S2 x a, + ∀ S1 S2 x a, Le S1 S2 -> Le (Update x (Aeval S1 a) S1) (Update x (Aeval S2 a) S2) := by intros; grind @@ -330,15 +330,15 @@ theorem fixpoint_join_increasing (_ : Store) (F: Store → Store) (F_mon : ∀ x generalize heq : fixpoint_join' S2 F F_mon = fix2 have : (Le (Join S2 (F fix2)) fix2) := by apply Eq_Le - . have := @fixpoint_join_eq S2 F (by grind [wrapper]) + · have := @fixpoint_join_eq S2 F (by grind [wrapper]) rw [←heq] apply this apply Le_trans rotate_left - . apply this - . apply Join_increasing - . exact hyp - . grind + · apply this + · apply Join_increasing + · exact hyp + · grind noncomputable def Cexec' : (c : com) → {F : Store → Store // ∀ x y, le x y → le (F x) (F y)} | .SKIP => ⟨(fun S => S), by grind⟩ @@ -346,7 +346,7 @@ noncomputable def Cexec' : (c : com) → {F : Store → Store // ∀ x y, le x intro x y hyp simp apply Update_increasing - . exact hyp ⟩ + · exact hyp ⟩ | .SEQ c1 c2 => let ⟨ f₁, mon₁ ⟩ := Cexec' c1 let ⟨ f₂, mon₂ ⟩ := Cexec' c2 @@ -368,13 +368,13 @@ noncomputable def Cexec' : (c : com) → {F : Store → Store // ∀ x y, le x simp apply le_trans rotate_right - . exact Join (f₁ x) (f₂ x) + · exact Join (f₁ x) (f₂ x) rotate_left - . apply Join_increasing - . apply mon₁ - . exact hyp - . apply mon₂ - . exact hyp + · apply Join_increasing + · apply mon₁ + · exact hyp + · apply mon₂ + · exact hyp intro id val hyp2 have := (Join_characterization (f₁ x) (f₂ x) id val).1 hyp2 split <;> grind @@ -387,8 +387,8 @@ noncomputable def Cexec' : (c : com) → {F : Store → Store // ∀ x y, le x simp intro x y hyp apply fixpoint_join_increasing - . exact x - . exact hyp ⟩ + · exact x + · exact hyp ⟩ noncomputable def Cexec_Constprop (c : com) : Store → Store := (Cexec' c).val instance (c : com) : Monotone Store (Cexec_Constprop c) where diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean index 2d92ba6..f3f0974 100644 --- a/LeroyCompilerVerificationCourse/Imp.lean +++ b/LeroyCompilerVerificationCourse/Imp.lean @@ -42,7 +42,7 @@ theorem aeval_free : (∀ 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 <;> grind + fun_induction aeval s1 a with grind inductive bexp : Type where | TRUE @@ -348,15 +348,15 @@ def goes_wrong (c: com) (s: store) : Prop := ∃ c', ∃ s', star red (c, s) (c' grind case star_step x y _ a₁ a₂ a_ih => apply star.star_step - . apply red.red_seq_step + · apply red.red_seq_step rotate_left - . exact y.1 - . exact y.2 - . rw [h₁] + · exact y.1 + · exact y.2 + · rw [h₁] exact a₁ - . apply a_ih - . rfl - . exact h₂ + · apply a_ih + · rfl + · exact h₂ theorem cexec_to_reds (s s' : store) (c : com) : cexec s c s' → star red (c, s) (.SKIP, s') := by intro h @@ -364,23 +364,23 @@ theorem cexec_to_reds (s s' : store) (c : com) : cexec s c s' → star red (c, s any_goals grind case cexec_seq ih1 ih2 => apply star_trans - . apply red_seq_steps + · apply red_seq_steps exact ih1 - . apply star.star_step + · apply star.star_step apply red.red_seq_done exact ih2 case cexec_while_loop ih1 ih2 => apply star_trans - . apply star_one - . apply red.red_while_loop - . grind - . apply star_trans - . apply red_seq_steps - . exact ih1 - . apply star_trans + · apply star_one + · apply red.red_while_loop + · grind + · apply star_trans + · apply red_seq_steps + · exact ih1 + · apply star_trans rotate_left - . apply ih2 - . grind + · apply ih2 + · grind @[grind] theorem red_append_cexec (c1 c2 : com) (s1 s2 : store) : red (c1, s1) (c2, s2) → @@ -395,9 +395,9 @@ theorem cexec_to_reds (s s' : store) (c : com) : cexec s c s' → star red (c, s 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 + · -- Could be good to have an error about a metavariable in here apply cexec.cexec_skip - . exact h2 + · exact h2 all_goals grind theorem reds_to_cexec (s s' : store) (c : com) : @@ -411,9 +411,9 @@ theorem reds_to_cexec (s s' : store) (c : com) : grind case star_step r _ a_ih => apply red_append_cexec - . rw [←heq1] at r + · rw [←heq1] at r exact r - . apply a_ih + · apply a_ih all_goals grind @[grind] inductive cont where @@ -429,25 +429,25 @@ theorem reds_to_cexec (s s' : store) (c : com) : inductive step: com × cont × store -> com × cont × store -> Prop where - | step_assign: forall x a k s, + | step_assign: ∀ x a k s, step (.ASSIGN x a, k, s) (.SKIP, k, update x (aeval s a) s) - | step_seq: forall c1 c2 s k, + | step_seq: ∀ c1 c2 s k, step (.SEQ c1 c2, k, s) (c1, .Kseq c2 k, s) - | step_ifthenelse: forall b c1 c2 k s, + | step_ifthenelse: ∀ b c1 c2 k s, step (.IFTHENELSE b c1 c2, k, s) ((if beval s b then c1 else c2), k, s) - | step_while_done: forall b c k s, + | step_while_done: ∀ b c k s, beval s b = false -> step (.WHILE b c, k, s) (.SKIP, k, s) - | step_while_true: forall b c k s, + | step_while_true: ∀ b c k s, beval s b = true -> step (.WHILE b c, k, s) (c, .Kwhile b c k, s) - | step_skip_seq: forall c k s, + | step_skip_seq: ∀ c k s, step (.SKIP, .Kseq c k, s) (c, k, s) - | step_skip_while: forall b c k s, + | step_skip_while: ∀ b c k s, step (.SKIP, .Kwhile b c k, s) (.WHILE b c, k, s) diff --git a/LeroyCompilerVerificationCourse/Sequences.lean b/LeroyCompilerVerificationCourse/Sequences.lean index c26379d..d101c4b 100644 --- a/LeroyCompilerVerificationCourse/Sequences.lean +++ b/LeroyCompilerVerificationCourse/Sequences.lean @@ -76,7 +76,7 @@ theorem plus_one : ∀ a b, R a b → plus R a b := by grind theorem star_plus_trans: - forall a b c, star R a b -> plus R b c -> plus R a c := by + ∀ a b c, star R a b -> plus R b c -> plus R a c := by intro a b c H0 H1 cases H0 case star_refl => @@ -87,7 +87,7 @@ theorem star_plus_trans: · grind theorem plus_right: - forall a b c, star R a b -> R b c -> plus R a c := by + ∀ 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] @@ -102,8 +102,8 @@ def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → intro y Rxy exists y constructor - . exact Rxy - . intro y' Ryy' + · exact Rxy + · intro y' Ryy' unfold all_seq_inf at H apply H grind @@ -118,4 +118,4 @@ theorem infseq_coinduction_principle_2: case x => grind case y => grind [cases plus] -@[grind] def irred (R : α → α → Prop) (a : α) : Prop := forall b, ¬(R a b) +@[grind] def irred (R : α → α → Prop) (a : α) : Prop := ∀ b, ¬(R a b)