Skip to content

refactor(LocallyNameless/Untyped): Rename redex_abs_close to steps_abs_close #672

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

Open
lengyijun wants to merge 1 commit into
base: main
Choose a base branch
from
+3 −3
Open

refactor(LocallyNameless/Untyped): Rename redex_abs_close to steps_abs_close #672

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 1 deletion Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by
| refl => grind [open_close]
| single => exact .single (Xi.abs {w} (by grind [FullBeta.redex_subst_cong]))
· rw [open_close w N 0 (by grind)]
exact FullEta.redex_abs_close h_eta (FullBeta.step_lc_r (st_body_beta w (by grind)))
exact FullEta.steps_abs_close h_eta (FullBeta.step_lc_r (st_body_beta w (by grind)))

open Commute in
/-- βη-reduction is confluent. -/
Expand Down
4 changes: 2 additions & 2 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ lemma step_abs_close {x} (step : M ⭢ηᶠ M') (lc_M : LC M) : (M ^* x).abs ⭢
grind [step_subst_cong_l]

/-- Abstracting then closing preserves multiple reductions. -/
lemma redex_abs_close {x} (steps : M ↠ηᶠ M') (lc_M : LC M) : (M ^* x).abs ↠ηᶠ (M' ^* x).abs := by
lemma steps_abs_close {x} (steps : M ↠ηᶠ M') (lc_M : LC M) : (M ^* x).abs ↠ηᶠ (M' ^* x).abs := by
induction steps using Relation.ReflTransGen.head_induction_on
case refl => exact .refl
case head b c st_bc _ ih => exact .head (step_abs_close st_bc lc_M) (ih (step_lc_r st_bc))
Expand All @@ -115,7 +115,7 @@ theorem redex_abs_cong {M M' : Term Var} (xs : Finset Var)
case abs L hL =>
have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
rw [open_close x M 0, open_close x M' 0]
all_goals grind [redex_abs_close (x := x) (cofin x ?_) (hL x ?_)]
all_goals grind [steps_abs_close (x := x) (cofin x ?_) (hL x ?_)]

/- `t ⭢ηᶠ t'` implies `s [ x := t ] ↠ηᶠ s [ x := t' ]`. -/
lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (st : t ⭢ηᶠ t') (lc_s : LC s) (lc_t : LC t) :
Expand Down
Loading