From 8f1adfa034240a612d4caf637de82d1c14f3e800 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Jul 2025 07:42:42 +0200 Subject: [PATCH] finish --- LeroyCompilerVerificationCourse/Compil.lean | 102 +++++++++--------- .../Constprop.lean | 96 ++++++++--------- LeroyCompilerVerificationCourse/Deadcode.lean | 36 +++---- .../Fixpoints.lean | 26 ++--- LeroyCompilerVerificationCourse/Imp.lean | 93 ++++++++-------- .../Sequences.lean | 6 +- 6 files changed, 176 insertions(+), 183 deletions(-) diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean index ba9eeb1..78a998e 100644 --- a/LeroyCompilerVerificationCourse/Compil.lean +++ b/LeroyCompilerVerificationCourse/Compil.lean @@ -7,18 +7,18 @@ Authors: Wojciech Różowski import LeroyCompilerVerificationCourse.Imp @[grind] inductive instr : Type where - | Iconst (n: Int) - | Ivar (x: ident) - | Isetvar (x: ident) + | Iconst (n : Int) + | Ivar (x : ident) + | Isetvar (x : ident) | Iadd | Iopp - | Ibranch (d: Int) - | Ibeq (d1: Int) (d0: Int) - | Ible (d1: Int) (d0: Int) + | Ibranch (d : Int) + | Ibeq (d1 : Int) (d0 : Int) + | Ible (d1 : Int) (d0 : Int) | Ihalt deriving Repr -@[grind] def codelen (c: List instr) : Int := c.length +@[grind] def codelen (c : List instr) : Int := c.length def stack : Type := List Int @@ -29,7 +29,7 @@ def config : Type := Int × stack × store | [] => .none | i :: C' => if pc = 0 then .some i else instr_at C' (pc - 1) -@[grind] inductive transition (C: List instr): config → config → Prop where +@[grind] inductive transition (C : List instr) : config → config → Prop where | trans_const : ∀ pc stk s n, instr_at C pc = .some (.Iconst n) → transition C (pc , stk , s) @@ -38,58 +38,58 @@ def config : Type := Int × stack × store instr_at C pc = .some (.Ivar x) -> transition C (pc , stk , s) (pc + 1, s x :: stk, s) - | trans_setvar: ∀ 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: ∀ 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: ∀ 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: ∀ 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: ∀ 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: ∀ 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) (pc', stk , s) -@[grind] def transitions (C: List instr) : config → config → Prop := +@[grind] def transitions (C : List instr) : config → config → Prop := star (transition C) -def machine_terminates (C: List instr) (s_init: store) (s_final: store) : Prop := +def machine_terminates (C : List instr) (s_init : store) (s_final : store) : Prop := ∃ 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 := +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 := +def machine_goes_wrong (C : List instr) (s_init : store) : Prop := ∃ pc stk s, transitions C (0, [], s_init) (pc, stk, s) ∧ irred (transition C) (pc, stk, s) ∧ (instr_at C pc ≠ .some .Ihalt ∨ stk ≠ []) -@[grind] def compile_aexp (a: aexp) : List instr := +@[grind] def compile_aexp (a : aexp) : List instr := match a with | .CONST n => .Iconst n :: [] | .VAR x => .Ivar x :: [] | .PLUS a1 a2 => (compile_aexp a1) ++ (compile_aexp a2) ++ (.Iadd :: []) | .MINUS a1 a2 => compile_aexp a1 ++ compile_aexp a2 ++ (.Iopp :: .Iadd :: []) -@[grind] def compile_bexp (b: bexp) (d1: Int) (d0: Int) : List instr := +@[grind] def compile_bexp (b : bexp) (d1 : Int) (d0 : Int) : List instr := match b with | .TRUE => if d1 = 0 then [] else .Ibranch d1 :: [] | .FALSE => if d0 = 0 then [] else .Ibranch d0 :: [] @@ -101,7 +101,7 @@ def machine_goes_wrong (C: List instr) (s_init: store) : Prop := let code1 := compile_bexp b1 0 (codelen code2 + d0) code1 ++ code2 -@[grind] def compile_com (c: com) : List instr:= +@[grind] def compile_com (c : com) : List instr := match c with | .SKIP => [] @@ -123,28 +123,28 @@ def machine_goes_wrong (C: List instr) (s_init: store) : Prop := ++ code_body ++ .Ibranch (- (codelen code_test + codelen code_body + 1)) :: [] -def compile_program (p: com) : List instr:= +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:= +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: ∀ C1 C2 C3 pc, +@[grind] inductive code_at : List instr -> Int -> List instr-> Prop where + | code_at_intro : ∀ C1 C2 C3 pc, pc = codelen C1 -> code_at (C1 ++ C2 ++ C3) pc C2 -@[grind] theorem codelen_cons: +@[grind] theorem codelen_cons : ∀ i c, codelen (i :: c) = codelen c + 1 := by grind @[grind] theorem codelen_singleton : codelen [i] = 1 := by dsimp [codelen] -@[grind] theorem codelen_app: +@[grind] theorem codelen_app : ∀ c1 c2, codelen (c1 ++ c2) = codelen c1 + codelen c2 := by intro c1 _ induction c1 with grind @@ -155,7 +155,7 @@ def smart_Ibranch (d: Int) : List instr:= intro i c2 c1 pc induction c1 generalizing pc with grind -@[grind] theorem instr_at_app: +@[grind] theorem instr_at_app : ∀ i c2 c1 pc, pc = codelen c1 -> instr_at (c1 ++ (i :: c2)) pc = .some i := by @@ -184,7 +184,7 @@ theorem code_at_head : have s : c1 ++ i :: C' ++ c3 = c1 ++ [i] ++ C' ++ c3 := by grind grind -@[grind] theorem code_at_app_left: +@[grind] theorem code_at_app_left : ∀ C pc C1 C2, code_at C pc (C1 ++ C2) -> code_at C pc C1 := by @@ -194,7 +194,7 @@ theorem code_at_head : have := code_at.code_at_intro c1 m1 (m2 ++ c3) pc a grind [List.append_assoc] -@[grind] theorem code_at_app_right: +@[grind] theorem code_at_app_right : ∀ C pc C1 C2, code_at C pc (C1 ++ C2) -> code_at C (pc + codelen C1) C2 := by @@ -531,35 +531,35 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s apply ih2 grind -inductive compile_cont (C: List instr) : cont -> Int -> Prop where - | ccont_stop: ∀ pc, +inductive compile_cont (C : List instr) : cont -> Int -> Prop where + | ccont_stop : ∀ pc, instr_at C pc = .some .Ihalt -> compile_cont C .Kstop pc - | ccont_seq: ∀ 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: ∀ 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: ∀ 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: ∀ c k st pc, +inductive match_config (C : List instr) : com × cont × store -> config -> Prop where + | 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) -def com_size (c: com) : Nat := +def com_size (c : com) : Nat := match c with | .SKIP => 1 | .ASSIGN _ _ => 1 @@ -568,21 +568,21 @@ def com_size (c: com) : Nat := | .WHILE _ c1 => (com_size c1 + 1) -theorem com_size_nonzero: ∀ c, (com_size c > 0) := by +theorem com_size_nonzero : ∀ c, (com_size c > 0) := by intro c fun_induction com_size with grind -def cont_size (k: cont) : Nat := +def cont_size (k : cont) : Nat := match k with | .Kstop => 0 | .Kseq c k' => (com_size c + cont_size k') | .Kwhile _ _ k' => cont_size k' -def measure' (impconf: com × cont × store) : Nat := +def measure' (impconf : com × cont × store) : Nat := match impconf with | (c, k, _) => (com_size c + cont_size k) -theorem compile_cont_Kstop_inv (C : List instr) (pc : Int) (s : store): +theorem compile_cont_Kstop_inv (C : List instr) (pc : Int) (s : store) : compile_cont C .Kstop pc → ∃ pc', star (transition C) (pc, [], s) (pc', [], s) @@ -593,7 +593,7 @@ theorem compile_cont_Kstop_inv (C : List instr) (pc : Int) (s : store): rw [h₁, h₂] at H induction H generalizing pc with grind -theorem compile_cont_Kseq_inv (C : List instr) (c : com) (k :cont) (pc : Int) (s : store) (H : compile_cont C (.Kseq c k) pc): +theorem compile_cont_Kseq_inv (C : List instr) (c : com) (k :cont) (pc : Int) (s : store) (H : compile_cont C (.Kseq c k) pc) : ∃ pc', star (transition C) (pc, [], s) (pc', [], s) ∧ code_at C pc' (compile_com c) @@ -603,7 +603,7 @@ theorem compile_cont_Kseq_inv (C : List instr) (c : com) (k :cont) (pc : Int) (s rw [h₁, h₂] at H induction H generalizing pc k with grind -theorem compile_cont_Kwhile_inv (C : List instr) (b : bexp) (c : com) (k : cont) (pc : Int) (s : store) (H : compile_cont C (.Kwhile b c k) pc): +theorem compile_cont_Kwhile_inv (C : List instr) (b : bexp) (c : com) (k : cont) (pc : Int) (s : store) (H : compile_cont C (.Kwhile b c k) pc) : ∃ pc', plus (transition C) (pc, [], s) (pc', [], s) ∧ code_at C pc' (compile_com (.WHILE b c)) @@ -640,13 +640,13 @@ theorem compile_cont_Kwhile_inv (C : List instr) (b : bexp) (c : com) (k : cont) · exact d any_goals grind -theorem match_config_skip (C : List instr) (k : cont) (s : store) (pc : Int) (H: compile_cont C k pc): +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 -theorem simulation_step: +theorem simulation_step : ∀ C impconf1 impconf2 machconf1, step impconf1 impconf2 -> match_config C impconf1 machconf1 -> @@ -817,7 +817,7 @@ theorem simulation_step: · exact w₂.1 · exact w₂.2 -theorem simulation_steps: +theorem simulation_steps : ∀ C impconf1 impconf2, star step impconf1 impconf2 -> ∀ machconf1, match_config C impconf1 machconf1 -> ∃ machconf2, @@ -851,7 +851,7 @@ theorem simulation_steps: theorem instr_at_len : instr_at (C ++ [i]) (codelen C) = .some i := by induction C with grind -theorem match_initial_configs: +theorem match_initial_configs : ∀ c s, match_config (compile_program c) (c, .Kstop, s) (0, [], s) := by intro c s @@ -864,7 +864,7 @@ theorem match_initial_configs: constructor grind -theorem compile_program_correct_terminating_2: +theorem compile_program_correct_terminating_2 : ∀ c s s', star step (c, .Kstop, s) (.SKIP, .Kstop, s') -> machine_terminates (compile_program c) s s' := by @@ -882,7 +882,7 @@ theorem compile_program_correct_terminating_2: exact D · exact E -theorem simulation_infseq_inv: +theorem simulation_infseq_inv : ∀ C n impconf1 machconf1, infseq step impconf1 -> match_config C impconf1 machconf1 -> (measure' impconf1 < n) -> @@ -915,7 +915,7 @@ theorem simulation_infseq_inv: · exact w.2.1 · exact w.2.2 -theorem compile_program_correct_diverging: +theorem compile_program_correct_diverging : ∀ c s, infseq step (c, .Kstop, s) -> machine_diverges (compile_program c) s := by diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean index 79439da..5b759b2 100644 --- a/LeroyCompilerVerificationCourse/Constprop.lean +++ b/LeroyCompilerVerificationCourse/Constprop.lean @@ -16,14 +16,14 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where | some v => if e.2 != v then return false return true -@[grind] def mk_PLUS_CONST (a: aexp) (n: Int) : aexp := +@[grind] def mk_PLUS_CONST (a : aexp) (n : Int) : aexp := if n = 0 then a else match a with | .CONST m => .CONST (m + n) | .PLUS a (.CONST m) => .PLUS a (.CONST (m + n)) | _ => .PLUS a (.CONST n) -@[grind] def mk_PLUS (a1 a2: aexp) : aexp := +@[grind] def mk_PLUS (a1 a2 : aexp) : aexp := match a1, a2 with | .CONST m, _ => mk_PLUS_CONST a2 m | _, .CONST m => mk_PLUS_CONST a1 m @@ -32,7 +32,7 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where | _, .PLUS a2 (.CONST m2) => mk_PLUS_CONST (.PLUS a1 a2) m2 | _, _ => .PLUS a1 a2 -@[grind] def mk_MINUS (a1 a2: aexp) : aexp := +@[grind] def mk_MINUS (a1 a2 : aexp) : aexp := match a1, a2 with | _, .CONST m => mk_PLUS_CONST a1 (-m) | .PLUS a1 (.CONST m1), .PLUS a2 (.CONST m2) => mk_PLUS_CONST (.MINUS a1 a2) (m1 - m2) @@ -40,7 +40,7 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where | _, .PLUS a2 (.CONST m2) => mk_PLUS_CONST (.MINUS a1 a2) (-m2) | _, _ => .MINUS a1 a2 -@[grind] def simplif_aexp (a: aexp) : aexp := +@[grind] def simplif_aexp (a : aexp) : aexp := match a with | .CONST n => .CONST n | .VAR x => .VAR x @@ -51,12 +51,12 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where #guard_msgs in #eval simplif_aexp (.MINUS (.PLUS (.VAR "x") (.CONST 1)) (.PLUS (.VAR "y") (.CONST 1))) -@[grind] theorem mk_PLUS_CONST_sound: +@[grind] theorem mk_PLUS_CONST_sound : ∀ 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: +theorem mk_PLUS_sound : ∀ 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 @@ -64,7 +64,7 @@ theorem mk_PLUS_sound: next m _ => grind -theorem mk_MINUS_sound: +theorem mk_MINUS_sound : ∀ 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) @@ -74,26 +74,26 @@ theorem simplif_aexp_sound : ∀ s a, aeval s (simplif_aexp a) = aeval s a := by induction a any_goals grind [mk_PLUS_sound, mk_MINUS_sound] -@[grind] def mk_EQUAL (a1 a2: aexp) : bexp := +@[grind] def mk_EQUAL (a1 a2 : aexp) : bexp := match a1, a2 with | .CONST n1, .CONST n2 => if n1 = n2 then .TRUE else .FALSE | .PLUS a1 (.CONST n1), .CONST n2 => .EQUAL a1 (.CONST (n2 - n1)) | _, _ => .EQUAL a1 a2 -@[grind] def mk_LESSEQUAL (a1 a2: aexp) : bexp := +@[grind] def mk_LESSEQUAL (a1 a2 : aexp) : bexp := match a1, a2 with | .CONST n1, .CONST n2 => if n1 <= n2 then .TRUE else .FALSE | .PLUS a1 (.CONST n1), .CONST n2 => .LESSEQUAL a1 (.CONST (n2 - n1)) | _, _ => .LESSEQUAL a1 a2 -@[grind] def mk_NOT (b: bexp) : bexp := +@[grind] def mk_NOT (b : bexp) : bexp := match b with | .TRUE => .FALSE | .FALSE => .TRUE | .NOT b => b | _ => .NOT b -@[grind] def mk_AND (b1 b2: bexp) : bexp := +@[grind] def mk_AND (b1 b2 : bexp) : bexp := match b1, b2 with | .TRUE, _ => b2 | _, .TRUE => b1 @@ -101,12 +101,12 @@ theorem simplif_aexp_sound : ∀ s a, aeval s (simplif_aexp a) = aeval s a := by | _, .FALSE => .FALSE | _, _ => .AND b1 b2 -theorem mk_EQUAL_sound: +theorem mk_EQUAL_sound : ∀ 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: +theorem mk_LESSEQUAL_sound : ∀ 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 @@ -116,69 +116,69 @@ theorem mk_NOT_sound : intros s b fun_cases (mk_NOT b) <;> grind -theorem mk_AND_sound: +theorem mk_AND_sound : ∀ 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 -@[grind] def mk_IFTHENELSE (b: bexp) (c1 c2: com) : com := +@[grind] def mk_IFTHENELSE (b : bexp) (c1 c2 : com) : com := match b with | .TRUE => c1 | .FALSE => c2 | _ => .IFTHENELSE b c1 c2 -@[grind] def mk_WHILE (b: bexp) (c: com) : com := +@[grind] def mk_WHILE (b : bexp) (c : com) : com := match b with | .FALSE => .SKIP | _ => .WHILE b c -theorem cexec_mk_IFTHENELSE: ∀ 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: ∀ 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: ∀ 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 fun_cases (mk_WHILE b c) <;> grind def Store := Std.HashMap ident Int -@[grind] def matches' (s: store) (S: Store): Prop := +@[grind] def matches' (s : store) (S : Store) : Prop := ∀ x n, S.get? x = .some n -> s x = n -@[grind] def Le (S1 S2: Store) : Prop := +@[grind] def Le (S1 S2 : Store) : Prop := ∀ x n, S2.get? x = .some n -> S1.get? x = .some n @[grind] def Top : Store := Std.HashMap.emptyWithCapacity -@[grind] def Join (S1 S2: Store) : Store := +@[grind] def Join (S1 S2 : Store) : Store := S1.filter (fun key _ => S2.get? key == S1.get? key) -- In leroy's course this is decidable -def Equal (S1 S2: Store) := Std.HashMap.Equiv S1 S2 +def Equal (S1 S2 : Store) := Std.HashMap.Equiv S1 S2 noncomputable instance : Decidable (Equal S' S) := Classical.propDecidable (Equal S' S) -theorem matches_Le: ∀ 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: ∀ S, Le S Top := by +theorem Le_Top : ∀ S, Le S Top := by unfold Le Top intros grind [Std.HashMap] -@[grind] theorem Join_characterization: +@[grind] theorem Join_characterization : ∀ S1 S2 x n, (Join S1 S2).get? x = .some n ↔ S1.get? x = .some n ∧ S2.get? x = .some n := by @@ -190,11 +190,11 @@ theorem Le_Top: ∀ S, Le S Top := by simp [Join] grind -theorem Le_Join_l: ∀ 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: ∀ 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: ∀ 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 @@ -202,23 +202,23 @@ theorem Equal_Le: ∀ S1 S2, Equal S1 S2 -> Le S1 S2 := by have := @Std.HashMap.Equiv.getElem?_eq _ _ _ _ S1 S2 _ _ x eq grind -@[grind] def lift1 {A B: Type} (f: A -> B) (o: Option A) : Option B := +@[grind] def lift1 {A B : Type} (f : A -> B) (o : Option A) : Option B := match o with | .some x => .some (f x) | .none => .none -@[grind] def lift2 {A B C: Type} (f: A -> B -> C) (o1: Option A) (o2: Option B) : Option C := +@[grind] def lift2 {A B C : Type} (f : A -> B -> C) (o1 : Option A) (o2 : Option B) : Option C := match o1, o2 with | .some x1, .some x2 => .some (f x1 x2) | _, _ => .none -@[grind] def Aeval (S: Store) (a: aexp) : Option Int := +@[grind] def Aeval (S : Store) (a : aexp) : Option Int := match a with | .CONST n => .some n | .VAR x => S.get? x | .PLUS a1 a2 => lift2 (Int.add) (Aeval S a1) (Aeval S a2) | .MINUS a1 a2 => lift2 (Int.sub) (Aeval S a1) (Aeval S a2) -@[grind] def Beval (S: Store) (b: bexp) : Option Bool := +@[grind] def Beval (S : Store) (b : bexp) : Option Bool := match b with | .TRUE => .some true | .FALSE => .some false @@ -227,7 +227,7 @@ theorem Equal_Le: ∀ S1 S2, Equal S1 S2 -> Le S1 S2 := by | .NOT b1 => lift1 (fun m => !m) (Beval S b1) | .AND b1 b2 => lift2 (fun m n => m && n) (Beval S b1) (Beval S b2) -@[grind] theorem Aeval_sound: +@[grind] theorem Aeval_sound : ∀ s S, matches' s S -> ∀ a n, Aeval S a = .some n -> aeval s a = n := by intro s S h1 a n h2 @@ -242,7 +242,7 @@ theorem Equal_Le: ∀ S1 S2, Equal S1 S2 -> Le S1 S2 := by unfold lift2 at h2 split at h2 <;> grind -theorem Beval_sound: +theorem Beval_sound : ∀ s S, matches' s S -> ∀ b n, Beval S b = .some n -> beval s b = n := by intro s S h1 b n h2 @@ -267,7 +267,7 @@ theorem Beval_sound: split at h2 <;> grind -@[grind] def Update (x: ident) (N: Option Int) (S: Store) : Store := +@[grind] def Update (x : ident) (N : Option Int) (S : Store) : Store := match N with | .none => S.erase x | .some n => S.insert x n @@ -287,14 +287,14 @@ theorem Beval_sound: unfold Update grind -theorem matches_update: ∀ s S x n N, +theorem matches_update : ∀ s S x n N, matches' s S -> (∀ 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 -@[grind] noncomputable def fixpoint_rec (F: Store -> Store) (fuel: Nat) (S: Store) : Store := +@[grind] noncomputable def fixpoint_rec (F : Store -> Store) (fuel : Nat) (S : Store) : Store := match fuel with | 0 => Top | fuel + 1 => @@ -303,7 +303,7 @@ theorem matches_update: ∀ s S x n N, @[grind] def num_iter : Nat := 20 -@[grind] noncomputable def fixpoint (F: Store -> Store) (init_S: Store) : Store := +@[grind] noncomputable def fixpoint (F : Store -> Store) (init_S : Store) : Store := fixpoint_rec F num_iter init_S theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint F init_S) : @@ -320,7 +320,7 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint cases E <;> grind [Equal_Le] -@[grind] noncomputable def Cexec (S: Store) (c: com) : Store := +@[grind] noncomputable def Cexec (S : Store) (c : com) : Store := match c with | .SKIP => S | .ASSIGN x a => Update x (Aeval S a) S @@ -333,7 +333,7 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint | .WHILE _ c1 => fixpoint (fun x => Join S (Cexec x c1)) S -@[grind] theorem Cexec_sound: +@[grind] theorem Cexec_sound : ∀ c s1 s2 S1, cexec s1 c s2 -> matches' s1 S1 -> matches' s2 (Cexec S1 c) := by intro c @@ -412,7 +412,7 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint · apply Le_Join_l · exact MATCHES -@[grind] def cp_aexp (S: Store) (a: aexp) : aexp := +@[grind] def cp_aexp (S : Store) (a : aexp) : aexp := match a with | .CONST n => .CONST n | .VAR x => match S.get? x with @@ -422,7 +422,7 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint | .MINUS a1 a2 => mk_MINUS (cp_aexp S a1) (cp_aexp S a2) -@[grind] def cp_bexp (S: Store) (b: bexp) : bexp := +@[grind] def cp_bexp (S : Store) (b : bexp) : bexp := match b with | .TRUE => .TRUE | .FALSE => .FALSE @@ -431,20 +431,20 @@ theorem fixpoint_sound (F : Store → Store) (init_S : Store) (h : S = fixpoint | .NOT b => mk_NOT (cp_bexp S b) | .AND b1 b2 => mk_AND (cp_bexp S b1) (cp_bexp S b2) -@[grind] theorem cp_aexp_sound: +@[grind] theorem cp_aexp_sound : ∀ 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: +theorem cp_bexp_sound : ∀ 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] -@[grind] noncomputable def cp_com (S: Store) (c: com) : com := +@[grind] noncomputable def cp_com (S : Store) (c : com) : com := match c with | .SKIP => .SKIP | .ASSIGN x a => @@ -457,7 +457,7 @@ theorem cp_bexp_sound: let sfix := Cexec S (.WHILE b c) mk_WHILE (cp_bexp sfix b) (cp_com sfix c) -theorem cp_com_correct_terminating: +theorem cp_com_correct_terminating : ∀ 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 @@ -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: ∀ s1 c1 s2, + have INNER : ∀ s1 c1 s2, cexec s1 c1 s2 -> c1 = .WHILE b c -> matches' s1 X -> diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean index 0ae5d85..db53083 100644 --- a/LeroyCompilerVerificationCourse/Deadcode.lean +++ b/LeroyCompilerVerificationCourse/Deadcode.lean @@ -16,7 +16,7 @@ open Classical in @[grind] noncomputable instance (a b : IdentSet) : Decidable (a ⊆ b) := Classical.propDecidable (a ⊆ b) -@[grind] instance (x : ident) (a: IdentSet) : Decidable (x ∈ a) := Std.HashSet.instDecidableMem +@[grind] instance (x : ident) (a : IdentSet) : Decidable (x ∈ a) := Std.HashSet.instDecidableMem @[grind] instance : EmptyCollection IdentSet where emptyCollection := Std.HashSet.emptyWithCapacity @@ -34,14 +34,14 @@ open Classical in @[grind] theorem insert_characterisation (a : IdentSet) (x : ident) : x ∈ a.insert x := by grind [Std.HashSet.contains_insert] -@[grind] def fv_aexp (a: aexp) : IdentSet := +@[grind] def fv_aexp (a : aexp) : IdentSet := match a with | .CONST _ => ∅ | .VAR v => Std.HashSet.instSingleton.singleton v | .PLUS a1 a2 => (fv_aexp a1) ∪ (fv_aexp a2) | .MINUS a1 a2 => (fv_aexp a1) ∪ (fv_aexp a2) -@[grind] def fv_bexp (b: bexp) : IdentSet := +@[grind] def fv_bexp (b : bexp) : IdentSet := match b with | .TRUE => ∅ | .FALSE => ∅ @@ -50,7 +50,7 @@ open Classical in | .NOT b1 => fv_bexp b1 | .AND b1 b2 => (fv_bexp b1) ∪ (fv_bexp b2) -@[grind] def fv_com (c: com) : IdentSet := +@[grind] def fv_com (c : com) : IdentSet := match c with | .SKIP => ∅ | .ASSIGN _ a => fv_aexp a @@ -58,24 +58,24 @@ open Classical in | .IFTHENELSE b c1 c2 => (fv_bexp b) ∪ ((fv_com c1) ∪ (fv_com c2)) | .WHILE b c => (fv_bexp b) ∪ (fv_com c) -@[grind] noncomputable def deadcode_fixpoint_rec (F : IdentSet → IdentSet) (default : IdentSet) (fuel: Nat) (x: IdentSet) : IdentSet := +@[grind] noncomputable def deadcode_fixpoint_rec (F : IdentSet → IdentSet) (default : IdentSet) (fuel : Nat) (x : IdentSet) : IdentSet := match fuel with | 0 => default | fuel + 1 => let x' := F x if x' ⊆ x then x else deadcode_fixpoint_rec F default fuel x' -@[grind] noncomputable def deadcode_fixpoint (F : IdentSet → IdentSet) (default : IdentSet): IdentSet := +@[grind] noncomputable def deadcode_fixpoint (F : IdentSet → IdentSet) (default : IdentSet) : IdentSet := deadcode_fixpoint_rec F default 20 ∅ -@[grind] theorem fixpoint_charact' (n : Nat) (x : IdentSet) (F : IdentSet → IdentSet) (default : IdentSet): +@[grind] theorem fixpoint_charact' (n : Nat) (x : IdentSet) (F : IdentSet → IdentSet) (default : IdentSet) : ((F (deadcode_fixpoint_rec F default n x)) ⊆ (deadcode_fixpoint_rec F default n x)) ∨ (deadcode_fixpoint_rec F default n x = default) := by induction n generalizing x <;> grind theorem fixpoint_charact (F : IdentSet → IdentSet) (default : IdentSet) : ((F (deadcode_fixpoint F default)) ⊆ (deadcode_fixpoint F default)) ∨ (deadcode_fixpoint F default = default) := by grind -theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F_stable : ∀ x , x ⊆ default -> (F x) ⊆ default): deadcode_fixpoint F default ⊆ default := by +theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F_stable : ∀ x , x ⊆ default -> (F x) ⊆ default) : deadcode_fixpoint F default ⊆ default := by have : ∀ n : Nat, ∀ x : IdentSet, x ⊆ default → (deadcode_fixpoint_rec F default n x) ⊆ default := by intro n induction n @@ -97,7 +97,7 @@ theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F unfold instHasSubsetIdentSet grind -@[grind] noncomputable def live (c: com) (L: IdentSet) : IdentSet := +@[grind] noncomputable def live (c : com) (L : IdentSet) : IdentSet := match c with | .SKIP => L | .ASSIGN x a => @@ -113,7 +113,7 @@ theorem fixpoint_upper_bound (F : IdentSet → IdentSet) (default : IdentSet) (F let default := (fv_com (.WHILE b c)) ∪ L deadcode_fixpoint (fun x => L' ∪ (live c x)) default -theorem live_upper_bound: +theorem live_upper_bound : ∀ c L, (live c L) ⊆ ((fv_com c) ∪ L) := by intro c @@ -216,7 +216,7 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet) have := live_upper_bound c L' y mem grind -@[grind] noncomputable def dce (c: com) (L: IdentSet): com := +@[grind] noncomputable def dce (c : com) (L : IdentSet) : com := match c with | .SKIP => .SKIP | .ASSIGN x a => if x ∈ L then .ASSIGN x a else .SKIP @@ -224,10 +224,10 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet) | .IFTHENELSE b c1 c2 => .IFTHENELSE b (dce c1 L) (dce c2 L) | .WHILE b c => .WHILE b (dce c (live (.WHILE b c) L)) -@[grind] def agree (L: IdentSet) (s1 s2: store) : Prop := +@[grind] def agree (L : IdentSet) (s1 s2 : store) : Prop := ∀ x, x ∈ L -> s1 x = s2 x -@[grind] theorem agree_mon: +@[grind] theorem agree_mon : ∀ L L' s1 s2, agree L' s1 s2 -> L ⊆ L' -> agree L s1 s2 := by intro L L' s1 s2 AG sub @@ -237,7 +237,7 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet) specialize AG x sub exact AG -@[grind] theorem aeval_agree: +@[grind] theorem aeval_agree : ∀ 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 @@ -287,7 +287,7 @@ theorem live_while_charact (b : bexp) (c : com) (L L' : IdentSet) specialize contained y (by grind) exact contained -theorem beval_agree: +theorem beval_agree : ∀ L s1 s2, agree L s1 s2 -> ∀ b, (fv_bexp b) ⊆ L -> beval s1 b = beval s2 b := by intro L s1 s2 AG b @@ -342,7 +342,7 @@ theorem beval_agree: specialize b2_ih (by grind) grind -theorem agree_update_live: +theorem agree_update_live : ∀ s1 s2 L x v, agree (L.erase x) s1 s2 -> agree L (update x v s1) (update x v s2) := by @@ -358,7 +358,7 @@ theorem agree_update_live: case pos isEq => grind -theorem agree_update_dead: +theorem agree_update_dead : ∀ s1 s2 L x v, agree L s1 s2 -> ¬x ∈ L -> agree L (update x v s1) s2 := by @@ -369,7 +369,7 @@ theorem agree_update_dead: simp [update] by_cases x=y <;> grind -theorem dce_correct_terminating: +theorem dce_correct_terminating : ∀ 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 diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean index 7607267..c8ffa70 100644 --- a/LeroyCompilerVerificationCourse/Fixpoints.lean +++ b/LeroyCompilerVerificationCourse/Fixpoints.lean @@ -14,7 +14,7 @@ universe u eq : α → α → Prop le : α → α → Prop beq : α → α → Bool - le_trans: ∀ x y z, le x y -> le y z -> le x z + le_trans : ∀ x y z, le x y -> le y z -> le x z beq_true' : ∀ x y : α, beq x y = true → eq x y beq_false' : ∀ x y : α, beq x y = false → ¬ eq x y gt_wf : WellFounded (fun x y : α => le y x ∧ ¬eq y x) @@ -71,13 +71,13 @@ instance : WellFoundedRelation α where rel := gt wf := gt_wf -@[grind] def iterate (x : α) (PRE: le x (F x)) (SMALL: ∀ 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: ∀ 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 @@ -150,7 +150,7 @@ theorem hash_set_incl_size_leq (S1 S2 : Store) : Le S2 S1 → List.Subperm (S1.t specialize LE k v (by grind) grind -@[grind] theorem Le_cardinal: +@[grind] theorem Le_cardinal : ∀ S T : Store, Le T S -> S.size <= T.size ∧ (S.size = T.size → Equal S T) := by @@ -167,7 +167,7 @@ theorem hash_set_incl_size_leq (S1 S2 : Store) : Le S2 S1 → List.Subperm (S1.t apply List.Subperm.perm_of_length_le (hash_set_incl_size_leq S T hyp) grind -@[grind] theorem Gt_cardinal: +@[grind] theorem Gt_cardinal : ∀ S S', Gt S S' -> S.size < S'.size := by intro S S' hyp unfold Gt at hyp @@ -217,7 +217,7 @@ instance : Monotone Store (fun x => Join Init (F x)) where simp at * unfold Le at * intro z n isSome - have ⟨ h1, h2 ⟩:= (Join_characterization Init (F y) z n).1 isSome + have ⟨h1, h2⟩ := (Join_characterization Init (F y) z n).1 isSome apply (Join_characterization (Init) (F x) z n).2 constructor · exact h1 @@ -236,7 +236,7 @@ noncomputable def fixpoint_join : Store := by specialize hyp x n hyp2 grind -theorem fixpoint_join_eq: Eq' (Join Init (F (fixpoint_join Init F) )) (fixpoint_join Init F) := by +theorem fixpoint_join_eq : Eq' (Join Init (F (fixpoint_join Init F) )) (fixpoint_join Init F) := by generalize heq1 : fixpoint_join Init F = t apply Eq'_sym simp [fixpoint_join] at * @@ -269,7 +269,7 @@ theorem fixpoint_join_sound : Le Init (fixpoint_join Init F) /\ Le (F (fixpoint_ · exact LE · apply Le_Join_r -theorem fixpoint_join_smallest: +theorem fixpoint_join_smallest : ∀ S, Le (Join Init (F S)) S -> Le (fixpoint_join Init F) S := by intro S LE unfold fixpoint_join @@ -288,13 +288,13 @@ theorem fixpoint_join_smallest: · unfold fixpoint_join dsimp -@[grind] theorem Join_increasing: +@[grind] theorem Join_increasing : ∀ 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 -> +@[grind] theorem Aeval_increasing : ∀ S1 S2, Le S1 S2 -> ∀ a n, Aeval S2 a = .some n -> Aeval S1 a =.some n := by intro S1 S2 LE a induction a <;> grind @@ -309,7 +309,7 @@ theorem fixpoint_join_smallest: simp [Beval, lift1] at ev grind -theorem Update_increasing: +theorem Update_increasing : ∀ S1 S2 x a, Le S1 S2 -> Le (Update x (Aeval S1 a) S1) (Update x (Aeval S2 a) S2) := by @@ -320,11 +320,11 @@ end FixpointJoin noncomputable instance wrapper (F : Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) : Monotone Store F where F_mon := by grind -noncomputable def fixpoint_join' (S : Store) (F: Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) := by +noncomputable def fixpoint_join' (S : Store) (F : Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) := by have := wrapper F (by grind) exact fixpoint_join S F -theorem fixpoint_join_increasing (_ : Store) (F: Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) (S1 S2: Store) : le S1 S2 → le (fixpoint_join' S1 F F_mon) (fixpoint_join' S2 F F_mon) := by +theorem fixpoint_join_increasing (_ : Store) (F : Store → Store) (F_mon : ∀ x y, le x y → le (F x) (F y)) (S1 S2 : Store) : le S1 S2 → le (fixpoint_join' S1 F F_mon) (fixpoint_join' S2 F F_mon) := by intro hyp apply @fixpoint_join_smallest S1 F (by grind [wrapper]) (fixpoint_join' S2 F F_mon) generalize heq : fixpoint_join' S2 F F_mon = fix2 diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean index f3f0974..f588561 100644 --- a/LeroyCompilerVerificationCourse/Imp.lean +++ b/LeroyCompilerVerificationCourse/Imp.lean @@ -47,22 +47,22 @@ theorem aeval_free : inductive bexp : Type where | TRUE | FALSE - | EQUAL (a1: aexp) (a2: aexp) - | LESSEQUAL (a1: aexp) (a2: aexp) - | NOT (b1: bexp) - | AND (b1: bexp) (b2: bexp) + | EQUAL (a1 : aexp) (a2 : aexp) + | LESSEQUAL (a1 : aexp) (a2 : aexp) + | NOT (b1 : bexp) + | AND (b1 : bexp) (b2 : bexp) -def NOTEQUAL (a1 a2: aexp) : bexp := .NOT (.EQUAL a1 a2) +def NOTEQUAL (a1 a2 : aexp) : bexp := .NOT (.EQUAL a1 a2) -def GREATEREQUAL (a1 a2: aexp) : bexp := .LESSEQUAL a2 a1 +def GREATEREQUAL (a1 a2 : aexp) : bexp := .LESSEQUAL a2 a1 -def GREATER (a1 a2: aexp) : bexp := .NOT (.LESSEQUAL a1 a2) +def GREATER (a1 a2 : aexp) : bexp := .NOT (.LESSEQUAL a1 a2) -def LESS (a1 a2: aexp) : bexp := GREATER a2 a1 +def LESS (a1 a2 : aexp) : bexp := GREATER a2 a1 -@[grind] def OR (b1 b2: bexp) : bexp := .NOT (.AND (.NOT b1) (.NOT b2)) +@[grind] def OR (b1 b2 : bexp) : bexp := .NOT (.AND (.NOT b1) (.NOT b2)) -@[grind] def beval (s: store) (b: bexp) : Bool := +@[grind] def beval (s : store) (b : bexp) : Bool := match b with | .TRUE => true | .FALSE => false @@ -71,15 +71,15 @@ 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: +theorem beval_OR : ∀ s b1 b2, beval s (OR b1 b2) = beval s b1 ∨ beval s b2 := by grind -inductive com: Type where +inductive com : Type where | SKIP - | ASSIGN (x : ident) (a: aexp) - | SEQ (c1: com) (c2: com) - | IFTHENELSE (b: bexp) (c1: com) (c2: com) - | WHILE (b: bexp) (c1: com) + | ASSIGN (x : ident) (a : aexp) + | SEQ (c1 : com) (c2 : com) + | IFTHENELSE (b : bexp) (c1 : com) (c2 : com) + | WHILE (b : bexp) (c1 : com) notation:10 l:10 " ;; " r:11 => com.SEQ l r @@ -90,28 +90,28 @@ def Euclidean_division := (.ASSIGN "r" (.MINUS (.VAR "r") (.VAR "b")) ;; .ASSIGN "q" (.PLUS (.VAR "q") (.CONST 1))) -@[grind] def update (x: ident) (v: Int) (s: store) : store := +@[grind] def update (x : ident) (v : Int) (s : store) : store := fun y => if x == y then v else s y -@[grind] inductive cexec: store → com → store → Prop where - | cexec_skip: +@[grind] inductive cexec : store → com → store → Prop where + | cexec_skip : cexec s .SKIP s - | cexec_assign: + | cexec_assign : cexec s (.ASSIGN x a) (update x (aeval s a) s) - | cexec_seq: + | cexec_seq : cexec s c1 s' -> cexec s' c2 s'' -> cexec s (.SEQ c1 c2) s'' - | cexec_ifthenelse: + | cexec_ifthenelse : cexec s (if beval s b then c1 else c2) s' -> cexec s (.IFTHENELSE b c1 c2) s' - | cexec_while_done: + | cexec_while_done : beval s b = false -> cexec s (.WHILE b c) s - | cexec_while_loop: + | cexec_while_loop : beval s b = true -> cexec s c s' -> cexec s' (.WHILE b c) s'' -> cexec s (.WHILE b c) s'' -theorem cexec_infinite_loop: +theorem cexec_infinite_loop : ∀ s, ¬ ∃ s', cexec s (.WHILE .TRUE .SKIP) s' := by intro _ h apply Exists.elim h @@ -152,7 +152,7 @@ theorem cexec_bounded_sound : ∀ fuel s c s', all_goals grind all_goals grind -theorem cexec_bounded_complete (s s' : store) (c : com): +theorem cexec_bounded_complete (s s' : store) (c : com) : cexec s c s' → ∃ fuel1, ∀ fuel, (fuel ≥ fuel1) → cexec_bounded fuel s c = .some s' := by intro h @@ -247,23 +247,23 @@ theorem cexec_bounded_complete (s s' : store) (c : com): grind @[grind] inductive red : com × store → com × store → Prop where - | red_assign: ∀ x a s, + | red_assign : ∀ x a s, red (.ASSIGN x a, s) (.SKIP, update x (aeval s a) s) - | red_seq_done: ∀ c s, + | red_seq_done : ∀ c s, red (.SEQ .SKIP c, s) (c, s) - | red_seq_step: ∀ c1 c s1 c2 s2, + | red_seq_step : ∀ c1 c s1 c2 s2, red (c1, s1) (c2, s2) → red (.SEQ c1 c, s1) (.SEQ c2 c, s2) - | red_ifthenelse: ∀ b c1 c2 s, + | red_ifthenelse : ∀ b c1 c2 s, red (.IFTHENELSE b c1 c2, s) ((if beval s b then c1 else c2), s) - | red_while_done: ∀ b c s, + | red_while_done : ∀ b c s, beval s b = false → red (.WHILE b c, s) (.SKIP, s) - | red_while_loop: ∀ b c s, + | red_while_loop : ∀ b c s, beval s b = true → red (.WHILE b c, s) (.SEQ c (.WHILE b c), s) -theorem red_progress: +theorem red_progress : ∀ c s, c = .SKIP ∨ ∃ c', ∃ s', red (c, s) (c', s') := by intro c induction c @@ -336,7 +336,7 @@ theorem red_progress: exists s grind -def goes_wrong (c: com) (s: store) : Prop := ∃ c', ∃ s', star red (c, s) (c', s') ∧ irred red (c', s') ∧ c' ≠ .SKIP +def goes_wrong (c : com) (s : store) : Prop := ∃ c', ∃ s', star red (c, s) (c', s') ∧ irred red (c', s') ∧ c' ≠ .SKIP @[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 @@ -421,33 +421,26 @@ theorem reds_to_cexec (s s' : store) (c : com) : | Kseq (c : com) (k : cont) | Kwhile (b : bexp) (c : com) (k : cont) -@[grind] def apply_cont (k: cont) (c: com) : com := +@[grind] def apply_cont (k : cont) (c : com) : com := match k with | .Kstop => c | .Kseq c1 k1 => apply_cont k1 (.SEQ c c1) | .Kwhile b1 c1 k1 => apply_cont k1 (.SEQ c (.WHILE b1 c1)) -inductive step: com × cont × store -> com × cont × store -> Prop where - - | step_assign: ∀ x a k s, +inductive step : com × cont × store -> com × cont × store -> Prop where + | step_assign : ∀ x a k s, step (.ASSIGN x a, k, s) (.SKIP, k, update x (aeval s a) s) - - | step_seq: ∀ c1 c2 s k, + | step_seq : ∀ c1 c2 s k, step (.SEQ c1 c2, k, s) (c1, .Kseq c2 k, s) - - | step_ifthenelse: ∀ 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: ∀ 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: ∀ 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: ∀ c k s, + | step_skip_seq : ∀ c k s, step (.SKIP, .Kseq c k, s) (c, k, s) - - | step_skip_while: ∀ 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 d101c4b..069be2a 100644 --- a/LeroyCompilerVerificationCourse/Sequences.lean +++ b/LeroyCompilerVerificationCourse/Sequences.lean @@ -75,7 +75,7 @@ theorem plus_one : ∀ a b, R a b → plus R a b := by exact rel grind -theorem star_plus_trans: +theorem star_plus_trans : ∀ a b c, star R a b -> plus R b c -> plus R a c := by intro a b c H0 H1 cases H0 @@ -86,7 +86,7 @@ theorem star_plus_trans: · exact a1 · grind -theorem plus_right: +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] @@ -108,7 +108,7 @@ def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → apply H grind -theorem infseq_coinduction_principle_2: +theorem infseq_coinduction_principle_2 : ∀ (x : α → Prop), (∀ (a : α), x a → ∃ b, plus R a b ∧ x b) → ∀ (a : α), x a → infseq R a := by