feat: helper lemmas for use in the planned strong norm proof#381
feat: helper lemmas for use in the planned strong norm proof#381WegmannDavid wants to merge 12 commits intoleanprover:mainfrom
Conversation
chenson2018
changed the title
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
These are mostly suggestions about style and generality. Please ask if you have questions about anything!
| exact subst_lc (LC.abs xs m mem) h_lc | ||
| case abs => grind [abs <| free_union Var] | ||
| all_goals grind | ||
|
|
There was a problem hiding this comment.
Please only leave one newline between each theorem.
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
Outdated
Show resolved
Hide resolved
| case abs => grind [abs <| free_union Var] | ||
| all_goals grind | ||
|
|
||
| /-- Substitution respects a single reduction step. -/ |
There was a problem hiding this comment.
This is now more general than the above, so we should have
/-- Substitution of a locally closed term respects a single reduction step. -/
lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) :
s [ x := t ] ⭢βᶠ s' [ x := t ] := ... -- proof omitted
/-- Substitution respects a single reduction step of a free variable. -/
lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] := by
grind [redex_subst_cong_lc]Please note that I tweaked the docstrings a bit.
(The redex_subst_cong name should probably change, but these earliest modules have bad naming in general so I'll come back and do that myself.)
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
Outdated
Show resolved
Hide resolved
| rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_] | ||
| all_goals grind [redex_abs_close] | ||
|
|
||
| theorem redex_abs_fvar_finset_exists (xs : Finset Var) |
There was a problem hiding this comment.
I'm not sure I'd add this as a theorem, because it is exactly the definition of the constructor. Anywhere (like below in steps_open_l_abs) you would use this, you can just do cases on the M.abs ⭢βᶠ M'.abs and get the same result.
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
Outdated
Show resolved
Hide resolved
| · apply ih_l | ||
| · grind[Term.subst_lc, FullBeta.step_lc_r] | ||
|
|
||
| lemma steps_subst_cong2 {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) : |
There was a problem hiding this comment.
A better name without a number?
There was a problem hiding this comment.
steps_subst_cong_r? I was not sure how to name many of these, I did not yet figure out the naming algorithm behind the existing lemmas.
There was a problem hiding this comment.
This seems fine. (As I think I mentioned elsewhere I need to overhaul the naming for these modules, so any difficultly picking names is probably my fault!)
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
Outdated
Show resolved
Hide resolved
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
Outdated
Show resolved
Hide resolved
| LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by | ||
| induction M generalizing i <;> try grind | ||
|
|
||
| lemma open_abs_lc [HasFresh Var] : forall {M N : Term Var}, |
There was a problem hiding this comment.
Please use named hypotheses here.
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
|
Please also add a short description to the PR. |
2 participants
No description provided.