From 5a0079ab6f87e5d6333d783906d8e89238e56d1c Mon Sep 17 00:00:00 2001 From: lengyijun Date: Wed, 20 May 2026 07:47:51 +0800 Subject: [PATCH 1/2] feat(Eta): stronger step_not_fv --- .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 9907b11a2..20c078e26 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -63,7 +63,7 @@ lemma invert_step_app_fvar (step : (app M (fvar x)) ⭢ηᶠ N) : variable [HasFresh Var] [DecidableEq Var] /-- An η-reduction step does not introduce new free variables. -/ -lemma step_not_fv (step : M ⭢ηᶠ M') (hw : w ∉ M.fv) : w ∉ M'.fv := by +lemma step_not_fv (step : M ⭢ηᶠ M') : M.fv = M'.fv := by induction step with | base => grind | abs => From 6002d76cd793b8f30d32a0dffa791ee0fe2349be Mon Sep 17 00:00:00 2001 From: lengyijun Date: Wed, 20 May 2026 08:17:39 +0800 Subject: [PATCH 2/2] feat(FullBeta): generalize step_not_fv --- .../LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean | 2 +- .../LocallyNameless/Untyped/FullBetaEtaConfluence.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index 1b90ff1e6..2b485cfe1 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -98,7 +98,7 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') : redex_subst_cong_lc _ _ _ _ step (.fvar y) /-- An β-reduction step does not introduce new free variables. -/ -lemma step_not_fv (step : M ⭢βᶠ N) (hw : w ∉ M.fv) : w ∉ N.fv := by +lemma step_not_fv (step : M ⭢βᶠ N) : N.fv ⊆ M.fv := by induction step with | base h => cases h with | beta => grind [open_preserve_not_fvar] | abs => diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean index 24ae1c943..a300ed58c 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean @@ -77,9 +77,9 @@ lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by cases h_eta with | eta => have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var have st_beta_w : app y₁ (fvar w) ⭢βᶠ N ^ fvar w := by grind [st_body_beta w] - rcases invert_step_app_fvar st_beta_w with ⟨u', _, st_u⟩ | ⟨u1, _, _⟩ + rcases invert_step_app_fvar st_beta_w with ⟨u', h, st_u⟩ | ⟨u1, _, _⟩ · use u' - grind [open_eq_app ?_ (step_not_fv st_u ?_)] + apply open_eq_app at h <;> grind [FullBeta.step_not_fv st_u] · use abs u1 grind [open_injective w N u1] case abs S ys st_body_eta =>