From dc0b831e69d77271791b1f067605306ecf3d5a2f Mon Sep 17 00:00:00 2001 From: lengyijun Date: Thu, 21 May 2026 06:32:31 +0800 Subject: [PATCH] feat: precise `close_var_not_fvar` This PR: 1. Rename `close_preserve_not_fvar` to `close_rec_fv` : shorter name, easier to remember 2. Remove `close_var_not_fvar_rec`: `close_rec_fv` is stronger theorem 3. Refactor `close_var_not_fvar`: make it precise 4. Add `close_rec_fv` and `close_var_not_fvar` to grind Following #580 --- .../LocallyNameless/Untyped/FullBeta.lean | 2 +- .../LocallyNameless/Untyped/FullEta.lean | 2 +- .../LocallyNameless/Untyped/Properties.lean | 17 +++++++---------- 3 files changed, 9 insertions(+), 12 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index f9a5f00c8..f037e7536 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -104,7 +104,7 @@ lemma step_not_fv (step : M ⭢βᶠ N) (hw : w ∉ M.fv) : w ∉ N.fv := by | abs => have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var have := open_close x - grind [close_preserve_not_fvar, open_preserve_not_fvar] + grind [open_preserve_not_fvar] | _ => grind /-- Abstracting then closing preserves a single reduction. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 10d29d35e..f5bbcec33 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -69,7 +69,7 @@ lemma step_not_fv (step : M ⭢ηᶠ M') (hw : w ∉ M.fv) : w ∉ M'.fv := by | abs => have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var have := open_close x - grind [close_preserve_not_fvar, open_preserve_not_fvar] + grind [open_preserve_not_fvar] | _ => grind /-- Substitution of a fresh variable preserves an η-reduction step. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean index e79c4bb96..fa839e4f9 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean @@ -52,9 +52,14 @@ lemma swap_open_fvar_close (k n : ℕ) (x y : Var) (m : Term Var) (neq₁ : k induction m generalizing k n <;> grind /-- Closing preserves free variables. -/ -lemma close_preserve_not_fvar {k y} (m : Term Var) : (m⟦k ↜ y⟧).fv = m.fv.erase y := by +@[scoped grind =] +lemma close_rec_fv {k y} (m : Term Var) : (m⟦k ↜ y⟧).fv = m.fv.erase y := by induction m generalizing k <;> grind +/-- Specializes `close_var_not_fvar_rec` to first closing. -/ +@[scoped grind =] +lemma close_var_not_fvar (x) (t : Term Var) : (t ^* x).fv = t.fv.erase x := close_rec_fv t + /-- Opening preserves free variables. -/ lemma open_preserve_not_fvar {k x} (m n : Term Var) (nmem_m : x ∉ m.fv) (nmem_n : x ∉ n.fv) : x ∉ (m⟦k ↝ n⟧).fv := by @@ -65,14 +70,6 @@ lemma subst_preserve_not_fvar {x y : Var} (m n : Term Var) (nmem : x ∉ m.fv x ∉ (m [y := n]).fv := by induction m <;> grind -/-- Closing removes a free variable. -/ -@[scoped grind ←] -lemma close_var_not_fvar_rec (x) (k) (t : Term Var) : x ∉ (t⟦k ↜ x⟧).fv := by - induction t generalizing k <;> grind - -/-- Specializes `close_var_not_fvar_rec` to first closing. -/ -lemma close_var_not_fvar (x) (t : Term Var) : x ∉ (t ^* x).fv := close_var_not_fvar_rec x 0 t - variable [HasFresh Var] omit [DecidableEq Var] in @@ -139,7 +136,7 @@ lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) (m_lc : LC m) : grind [ swap_open, =_ swap_open_fvar_close, open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ fvar y⟧) 0, open_close x' (t[x := fvar y]) 0, - open_preserve_not_fvar, close_preserve_not_fvar, subst_preserve_not_fvar] + open_preserve_not_fvar, close_rec_fv, subst_preserve_not_fvar] | _ => grind /-- Closing and opening are inverses. -/