From 36b7bb6d7754167a29cadd67e476a372a79c0b4e Mon Sep 17 00:00:00 2001 From: lengyijun Date: Sun, 16 Aug 2026 18:31:13 +0800 Subject: [PATCH] feat: FullEta.steps_fv MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Show that multi-step full η-reduction preserves free variables, by induction on the single-step result. --- .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index a830d898f..9a55706aa 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -75,13 +75,15 @@ variable [HasFresh Var] [DecidableEq Var] /-- An η-reduction step does not introduce new free variables. -/ lemma step_not_fv (step : M ⭢ηᶠ M') : M.fv = M'.fv := by induction step with - | base => grind | abs => have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var have := open_close x grind [open_preserve_not_fvar] | _ => grind +lemma steps_fv (steps : M ↠ηᶠ M') : M.fv = M'.fv := by + induction steps with grind [step_not_fv] + /- `s ⭢ηᶠ s'` implies `s[x := N] ⭢ηᶠ s'[x := N]`. -/ lemma step_subst_cong_l {x : Var} (s s' N : Term Var) (step : s ⭢ηᶠ s') (lc_N : LC N) : s[x := N] ⭢ηᶠ s'[x := N] := by