From e1386e7bd953bf4f65a5e13ea08ab816f4598ec6 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Mon, 22 Jun 2026 06:53:43 +0800 Subject: [PATCH] refactor(LocallyNameless/Untyped): Rename redex_abs_close to steps_abs_close --- .../LocallyNameless/Untyped/FullBetaEtaConfluence.lean | 2 +- .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean index 2412f2c10..6968b0099 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean @@ -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. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index f6b55c08c..f5f1f40c4 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -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)) @@ -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) :