Skip to content

chore: more grinding #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wkrozowski merged 4 commits into from
Aug 25, 2025
Merged

chore: more grinding #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
679f27e
chore: bump toolchain to v4.23.0-rc2
kim-em Aug 22, 2025
b839a59
chore: more grinding
kim-em Aug 22, 2025
bdd91be
more grind
kim-em Aug 22, 2025
1809781
Merge branch 'main' into more_grind
wkrozowski Aug 25, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
140 changes: 33 additions & 107 deletions LeroyCompilerVerificationCourse/Compil.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,6 @@ theorem code_at_head :
rw [heq1] at H
induction H
case code_at_intro c1 c2 c3 oc a =>
unfold instr_at
induction c1 generalizing oc with grind

@[grind] theorem code_at_tail :
Expand Down Expand Up @@ -227,56 +226,37 @@ theorem code_at_head :
induction C generalizing pc i
case nil => grind
case cons f t t_ih =>
unfold instr_at at h
by_cases pc = 0
rotate_left
next nz =>
grind
next z =>
have := code_at.code_at_intro [] [] (f :: t) pc
grind
have := code_at.code_at_intro [] [] (f :: t) pc
grind

@[grind] theorem code_at_to_instr_at : code_at C pc (c1 ++ i :: c2) → instr_at C (pc + codelen c1) = .some i := by
intro h
cases h
next b e a =>
have := instr_at_app i (c2 ++ e) (b ++ c1) (pc + codelen c1) (by simp [codelen]; grind)
grind [List.append_eq]
grind

theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int) (stk : stack) :
code_at C pc (compile_aexp a) →
transitions C (pc, stk, s) (pc + codelen (compile_aexp a), aeval s a :: stk, s) := by
induction a generalizing C pc stk
next =>
simp [aeval, compile_aexp]
intro a
unfold transitions
apply star_one
apply transition.trans_const
cases a
next => grind
grind
next =>
simp [aeval, compile_aexp]
intro a
apply star_one
apply transition.trans_var
cases a
next => grind
grind
next a1 a2 a1_ih a2_ih =>
simp [aeval, compile_aexp]
intro a
apply star_trans
· apply a1_ih
grind
· apply star_trans
· specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk)
apply a2_ih
· apply a2_ih
grind
· 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)
have h2 := @transition.trans_add ((c1 ++ compile_aexp a1 ++ compile_aexp a2) ++ (instr.Iadd :: c3)) (pc + codelen (compile_aexp a1) + codelen (compile_aexp a2)) stk s (aeval s a1) (aeval s a2) (by grind)
have h1 := instr_a
have h2 := @transition.trans_add
grind
next a1 a2 a1_ih a2_ih =>
simp [aeval, compile_aexp]
Expand All @@ -285,17 +265,15 @@ theorem compile_aexp_correct (C : List instr) (s : store) (a : aexp) (pc : Int)
· apply a1_ih
grind
· apply star_trans
· specialize a2_ih C (pc + codelen (compile_aexp a1)) (aeval s a1 :: stk)
apply a2_ih
· 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 this
· apply transition.trans_opp
grind
· apply star_one
· have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp]) instr.Iadd [] (by grind)
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)
· have := @code_at_to_instr_at C pc (compile_aexp a1 ++ compile_aexp a2 ++ [instr.Iopp])
have := @transition.trans_add
grind
-- Miss 5
theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : Int) (pc : Int) (stk : stack) (h : code_at C pc (compile_bexp b d1 d0)) :
Expand All @@ -311,12 +289,7 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
apply star.star_refl
case neg is_not_zero =>
apply star_one
simp [is_not_zero, codelen]
apply transition.trans_branch _ _ _ d1
· simp [compile_bexp, is_not_zero] at h
have := @code_at_to_instr_at C pc [] (instr.Ibranch d1) [] (by grind)
grind
· grind
grind
next =>
simp [compile_bexp, beval]
by_cases d0 = 0
Expand All @@ -326,51 +299,27 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
case neg is_not_zero =>
apply star_one
simp [is_not_zero, codelen]
apply transition.trans_branch _ _ _ d0
· simp [compile_bexp, is_not_zero] at h
have := @code_at_to_instr_at C pc [] (instr.Ibranch d0) [] (by grind)
grind
· grind
grind
next a1 a2 =>
simp [compile_bexp, beval]
apply star_trans
· apply compile_aexp_correct
rotate_left
· exact a1
· grind
· apply compile_aexp_correct (a := a1)
grind
· apply star_trans
· apply compile_aexp_correct
rotate_right
· exact a2
· grind
· apply compile_aexp_correct (a := a2)
grind
· apply star_one
· apply transition.trans_beq
rotate_left; rotate_left
· exact d1
· exact d0
· simp [compile_bexp] at h
grind
· grind
· apply transition.trans_beq (d1 := d1) (d0 := d0) <;> grind
next a1 a2 =>
simp [compile_bexp, beval]
apply star_trans
· apply compile_aexp_correct
rotate_left
· exact a1
· grind
· apply compile_aexp_correct (a := a1)
grind
· apply star_trans
· apply compile_aexp_correct
rotate_right
· exact a2
· grind
· apply compile_aexp_correct (a := a2)
grind
· apply star_one
· apply transition.trans_ble
rotate_left; rotate_left
· exact d1
· exact d0
· simp [compile_bexp] at h
grind
· grind
· apply transition.trans_ble (d1 := d1) (d0 := d0) <;> grind
next b1 ih =>
grind
next b1 b2 b1_ih b2_ih =>
Expand All @@ -379,11 +328,8 @@ 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
rotate_left
· exact 0
· exact (codelen code2 + d0)
· grind
· apply b1_ih (d1 := 0) (d0 := codelen code2 + d0)
grind
· by_cases beval s b1 = true
case pos isTrue =>
simp [isTrue]
Expand All @@ -397,9 +343,6 @@ theorem compile_bexp_correct (C : List instr) (s : store) (b : bexp) (d1 d0 : In
simp [Int.add_assoc] at *
exact b2_ih
case neg isFalse =>
simp [beval, isFalse]
rw [heq2]
simp [codelen_app]
grind

theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s c s') :
Expand All @@ -418,24 +361,16 @@ 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
rotate_left
· exact a
· unfold compile_com at h
grind
· apply compile_aexp_correct (a := a)
grind
· 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
· have := @transition.trans_setvar C
grind
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
unfold compile_com at h
apply code_at_app_left
exact h
grind
· specialize c2_ih C (pc + codelen (compile_com c1)) stk
simp [compile_com, codelen_app]
simp [Int.add_assoc] at c2_ih
Expand All @@ -459,11 +394,7 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
· apply ih
grind
· apply star_one
· apply transition.trans_branch
rotate_right
· exact codelen code2
· grind
· grind
· apply transition.trans_branch (d := codelen code2) <;> grind
case neg isFalse =>
simp [isFalse]
rw [heq3]
Expand Down Expand Up @@ -499,17 +430,13 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
apply star_trans
· 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
· apply ih1
grind
· apply star_trans
· apply star_one
apply transition.trans_branch
apply transition.trans_branch (d := d)
rotate_left
rotate_left
· exact d
· exact (pc + codelen code_branch + codelen code_body + 1 + d)
· grind
· grind
Expand All @@ -520,7 +447,6 @@ theorem compile_com_correct_terminating (s s' : store) (c : com) (h₁ : cexec s
rw [heq1, heq2, heq3] at ih2
simp [codelen_app]
simp [codelen_app] at ih2

have : (pc + codelen code_branch + codelen code_body + 1 + d +
(codelen code_branch + (codelen code_body + codelen [instr.Ibranch d])) ) = (pc + (codelen code_branch + (codelen code_body + codelen [instr.Ibranch d]))) := by grind
rw [←this]
Expand Down
4 changes: 1 addition & 3 deletions LeroyCompilerVerificationCourse/Constprop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -444,8 +444,7 @@ 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]
induction b with grind [mk_EQUAL_sound, mk_LESSEQUAL_sound, mk_AND_sound, mk_NOT_sound]

@[grind] noncomputable def cp_com (S : Store) (c : com) : com :=
match c with
Expand All @@ -469,7 +468,6 @@ theorem cp_com_correct_terminating :
case ASSIGN x a =>
cases EXEC
next =>
simp [cp_com]
have := @cexec.cexec_assign s1 x (cp_aexp S1 a)
grind
case IFTHENELSE b c1 c2 c1_ih c2_ih =>
Expand Down
Loading