feat(untyped): standardization theorem for the lambda calculus#679
feat(untyped): standardization theorem for the lambda calculus#679m-ow wants to merge 3 commits into
Conversation
|
Looking for your next pr ! |
|
Could you share your next PR related to "leftmost reduction"? |
|
Hi! @lengyijun My branch is still a bit too messy to share right now, but I expect to open the PR very soon. |
m-ow
force-pushed
the
standardization-theorem
branch
from
7f7a6cd to
93dfbbb
Compare
|
opened #700 :) |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
This seems straightforward, just some style nitpicks.
|
|
||
| /-- A single Call-by-Name step is a full β-reduction. -/ | ||
| lemma CBN.step_to_redex (step : M ⭢ₙ N) : M ↠βᶠ N := by | ||
| induction step <;> grind [FullBeta.redex_app_l_cong, Relation.ReflTransGen.single] |
There was a problem hiding this comment.
Something I recently have been more strict about is trying not to not is golf proofs of the form
induction foo
· grind [bar]
· grind [baz]into a single induction foo <;> grind [bar, baz] for readability and performance reasons.
So I'd write at least
| induction step <;> grind [FullBeta.redex_app_l_cong, Relation.ReflTransGen.single] | |
| induction step with | |
| · grind [Relation.ReflTransGen.single] | |
| · grind [FullBeta.redex_app_l_cong] |
(or even be tempted to not use grind at all for such a short proof)
This same idea applies to other proofs in this file.
| cases h_beta | ||
| exact rdx (by assumption) (by assumption) .refl (lc_refl _ lc_N) | ||
| case app L _ _ lc_L _ ih => | ||
| exact app (ih (by cases lc_N; assumption)) (lc_refl L lc_L) |
There was a problem hiding this comment.
I'd at least do
| exact app (ih (by cases lc_N; assumption)) (lc_refl L lc_L) | |
| cases lc_N | |
| exact app (ih (by assumption)) (lc_refl L lc_L) |
for readability. It'd also be easy to make the assumption usages explicit if you'd like.
| | rdx _ lc_Z cbn_m std_body => | ||
| exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body |
There was a problem hiding this comment.
Fits on one line?
| | rdx _ lc_Z cbn_m std_body => | |
| exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body | |
| | rdx _ lc_Z cbn_m std_body => exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body |
| have h_neq : x ≠ y := by aesop | ||
| rw [← Term.subst_open_var y x N m h_neq lc_N, ← Term.subst_open_var y x N' m' h_neq lc_N'] | ||
| exact ih y (by aesop) hN lc_N lc_N' |
There was a problem hiding this comment.
We prefer grind to aesop
| have h_neq : x ≠ y := by aesop | |
| rw [← Term.subst_open_var y x N m h_neq lc_N, ← Term.subst_open_var y x N' m' h_neq lc_N'] | |
| exact ih y (by aesop) hN lc_N lc_N' | |
| have h_neq : x ≠ y := by grind | |
| rw [← Term.subst_open_var y x N m h_neq lc_N, ← Term.subst_open_var y x N' m' h_neq lc_N'] | |
| exact ih y (by grind) hN lc_N lc_N' |
| exact rdx (Term.subst_lc (x := x) lc_m lc_N) (Term.subst_lc (x := x) lc_n lc_N) | ||
| (CBN.steps_subst x cbn_m lc_N) std_p_subst |
There was a problem hiding this comment.
No need for the implicits here, can fit on one line:
| exact rdx (Term.subst_lc (x := x) lc_m lc_N) (Term.subst_lc (x := x) lc_n lc_N) | |
| (CBN.steps_subst x cbn_m lc_N) std_p_subst | |
| exact rdx (subst_lc lc_m lc_N) (subst_lc lc_n lc_N) (CBN.steps_subst x cbn_m lc_N) std_p_subst |
| case abs ih => | ||
| apply Standard.abs <| free_union [fv] Var | ||
| intro x hx | ||
| exact ih x (by aesop) (Term.beta_lc lc_M (by constructor)) |
There was a problem hiding this comment.
| exact ih x (by aesop) (Term.beta_lc lc_M (by constructor)) | |
| exact ih x (by grind) (Term.beta_lc lc_M (by constructor)) |
| have step2 : Term.app (Term.abs m') n ↠βᶠ (m' ^ n) := | ||
| .single (Xi.base (Beta.beta (CBN.steps_lc_r lc_m cbn_m) lc_n)) |
There was a problem hiding this comment.
In general, I think it'd be nicer to use the Term namespace to your advantage for formatting
| have step2 : Term.app (Term.abs m') n ↠βᶠ (m' ^ n) := | |
| .single (Xi.base (Beta.beta (CBN.steps_lc_r lc_m cbn_m) lc_n)) | |
| have step2 : m'.abs.app n ↠βᶠ m' ^ n := .single (.base (.beta (CBN.steps_lc_r lc_m cbn_m) lc_n)) |
| have h_subst := Standard.subst (h_body y (by aesop)) hN y lc_N lc_N' | ||
| rw [← Term.subst_intro y N M (by aesop), ← Term.subst_intro y N' M' (by aesop)] at h_subst |
There was a problem hiding this comment.
| have h_subst := Standard.subst (h_body y (by aesop)) hN y lc_N lc_N' | |
| rw [← Term.subst_intro y N M (by aesop), ← Term.subst_intro y N' M' (by aesop)] at h_subst | |
| have h_subst := Standard.subst (h_body y (by grind)) hN y lc_N lc_N' | |
| rw [← Term.subst_intro y N M (by grind), ← Term.subst_intro y N' M' (by grind)] at h_subst |
| case abs ih_beta => | ||
| apply Standard.abs <| free_union [fv] Var | ||
| intro y hy | ||
| exact ih y (by aesop) (ih_beta y (by aesop)) |
There was a problem hiding this comment.
| exact ih y (by aesop) (ih_beta y (by aesop)) | |
| exact ih y (by grind) (ih_beta y (by grind)) |
| exact h_subst | ||
|
|
||
| /-- A standard reduction followed by a full β-step is a standard reduction. -/ | ||
| lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := by |
There was a problem hiding this comment.
Maybe it would be useful to have instances for these like Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ⭢βᶠ ·) (· ⭢ₛ ·) in this case? Just a thought for later.
3 participants
This PR proves the standardization theorem: if
Mbeta-reduces toNin any number of steps, thenNis reachable fromMby a standard reduction.Builds on #671.