From 73f2b4d84509acefa5f0e02636f17abbb15b383f Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Mon, 24 Aug 2026 09:47:22 +0800
Subject: [PATCH] feat: generalize lcAt_openRec_iff_lcAt
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Generalized the theorem `lcAt_openRec_fvar_iff_lcAt` → `lcAt_openRec_iff_lcAt`
It now works for opening with an arbitrary term N (that is itself LcAt i), not just a free variable fvar x.
---
 .../LocallyNameless/Untyped/LcAt.lean         | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index 754eb41817..b1442b7bd6 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -64,15 +64,21 @@ lemma depth_openRec_fvar_eq_depth (M : Term Var) (x : Var) (i : ℕ) :
 theorem depth_open_fvar_eq_depth (M : Term Var) (x : Var) : depth (M ^ fvar x) = depth M :=
   depth_openRec_fvar_eq_depth M x 0
 
-/-- Opening for some free variable at i-th bound variable, increments `LcAt`. -/
+lemma lcAt_le (M : Term Var) (i j : ℕ) (h : i ≤ j) (lc : LcAt i M) : LcAt j M := by
+  induction M generalizing i j <;> grind
+
 @[simp, scoped grind =]
-theorem lcAt_openRec_fvar_iff_lcAt (M : Term Var) (x : Var) (i : ℕ) :
-    LcAt i (M⟦i ↝ fvar x⟧) = LcAt (i + 1) M := by
-  induction M generalizing i <;> grind
+theorem lcAt_openRec_iff_lcAt (M N : Term Var) (i : ℕ) (h : LcAt i N) :
+    LcAt i (M⟦i ↝ N⟧) = LcAt (i + 1) M := by
+  induction M generalizing i with
+  | bvar _ => grind
+  | fvar _ => grind
+  | app _ _ _ _ => grind
+  | abs _ ih => exact ih _ (lcAt_le _ _ _ (by omega) h)
 
 /-- Opening for some free variable is locally closed if and only if `M` is `LcAt 1`. -/
 theorem lcAt_open_fvar_iff_lcAt (M : Term Var) (x : Var) : LcAt 0 (M ^ fvar x) = LcAt 1 M :=
-  lcAt_openRec_fvar_iff_lcAt M x 0
+  lcAt_openRec_iff_lcAt M (fvar x) 0 (lcAt_le _ 0 0 (by omega) (by grind))
 
 /-- Locally closed terms. -/
 inductive LC : Term Var → Prop
@@ -135,7 +141,4 @@ lemma lcAt_openRec_above_lcAt (M N : Term Var) (i j : ℕ) (h : i ≤ j) (lc : L
     M⟦j ↝ N⟧ = M := by
   induction M generalizing i j <;> grind
 
-lemma lcAt_le (M : Term Var) (i j : ℕ) (h : i ≤ j) (lc : LcAt i M) : LcAt j M := by
-  induction M generalizing i j <;> grind
-
 end Cslib.LambdaCalculus.LocallyNameless.Untyped.Term