feat(untyped): define CBN and Standard evaluation strategies#671
Conversation
|
Hi, I am doing something similar. I also have verified leftmost theorem in debruijn index. We are working on https://github.com/awesome-lambda-calculus/Fokker_challenge , normalization theorem is of most importance to us. |
|
Hi! Really cool project! |
|
Just read through your docs and I'm glad to see the project officially uses Locally Nameless. |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Looks straightforward, just a couple of small golfs:
| lemma cbn_lc_l (step : M ⭢ₙ N) : LC M := by | ||
| induction step | ||
| all_goals grind | ||
|
|
There was a problem hiding this comment.
| induction step with grind |
| induction step | ||
| case base beta_step => | ||
| cases beta_step | ||
| apply beta_lc <;> assumption | ||
| case app lc_z _ lc_n => exact LC.app lc_n lc_z |
There was a problem hiding this comment.
This seems reasonable:
| induction step | |
| case base beta_step => | |
| cases beta_step | |
| apply beta_lc <;> assumption | |
| case app lc_z _ lc_n => exact LC.app lc_n lc_z | |
| induction step with grind |
| variable {M N : Term Var} | ||
|
|
||
| /-- The left side of a standard reduction is locally closed. -/ | ||
| lemma stand_lc_l (step : M ⭢ₛ N) : LC M := by |
There was a problem hiding this comment.
I think for the other reduction strategies we namespace all these lemmas. Especially since you do so for Standard.lc_refl below this feels odd.
3 participants
This is the first step towards the Standardization Theorem.
Instead of the classic (and painful) Barendregt approach, I defined
Standardreductionrelying on
CBNto find the head redex, which makes the proofs much nicer.