refactor(LocallyNameless): Extract depth into a dedicated module

Cslib.lean

@@ -143,6 +143,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.BetaAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Depth
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Depth.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Elimia (Sehun Kim). All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Elimia (Sehun Kim)
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+
+/-!
+Depth of locally nameless terms
+
+This module defines the `depth` of an untyped lambda term in the locally nameless representation.
+`depth` measures the maximum nesting of abstractions surrounding any variable.
+
+We also provide a custom induction principle `ind_on_depth` that is convenient when reasoning by
+induction on depth, together with basic lemmas showing that opening a term with a free variable
+does not change its depth.
+-/
+
+
+@[expose] public section
+
+namespace Cslib.LambdaCalculus.LocallyNameless.Untyped.Term
+
+universe u
+
+variable {Var : Type u}
+
+/-- `depth` counts the maximum number of the lambdas that are enclosing variables. -/
+@[simp, scoped grind =]
+def depth : Term Var → ℕ
+| bvar _ => 0
+| fvar _ => 0
+| app t₁ t₂ => max (depth t₁) (depth t₂)
+| abs t => depth t + 1
+
+set_option linter.tacticAnalysis.verifyGrindOnly false in
+@[elab_as_elim]
+protected lemma ind_on_depth (P : Term Var → Prop) (bvar : ∀ i, P (bvar i)) (fvar : ∀ x, P (fvar x))
+    (app : ∀ M N, P M → P N → P (app M N))
+    (abs : ∀ M, P M → (∀ N, N.depth ≤ M.depth → P N) → P M.abs)
+    (M : Term Var) : P M := by
+  induction h : M.depth using Nat.strong_induction_on generalizing M with | _ n ih
+  induction M with
+  | abs M' => apply abs M' <;> grind
+  | bvar | fvar => grind
+  | app => apply app <;> grind only [depth, = max_def]
+
+/-- The depth of the lambda expression doesn't change by opening at i-th bound variable
+ for some free variable. -/
+ @[simp, scoped grind =]
+lemma depth_openRec_fvar_eq_depth (M : Term Var) (x : Var) (i : ℕ) :
+    (M⟦i ↝ fvar x⟧).depth = M.depth := by
+  induction M generalizing i <;> grind
+
+/-- The depth of the lambda expression doesn't change by opening for some free variable. -/
+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
+
+end Cslib.LambdaCalculus.LocallyNameless.Untyped.Term

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean

@@ -7,13 +7,14 @@ Authors: Elimia (Sehun Kim)
 module
 
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Depth
 
 /-!
 
-Alternative Definitions for LC:
+Definitions for LC and `LcAt`:
 
-This module defines `LcAt k M`, a more general definition of local closure. When k = 0, this is
-equivalent to `LC`, as shown in `lcAt_iff_LC`.
+`LcAt k M` is a more general definition of local closure. When k = 0, this is equivalent to `LC`,
+as shown in `lcAt_iff_LC`.
 
 -/
 
@@ -33,37 +34,6 @@ def LcAt (k : ℕ) : Term Var → Bool
 | app t₁ t₂ => LcAt k t₁ && LcAt k t₂
 | abs t => LcAt (k + 1) t
 
-/-- `depth` counts the maximum number of the lambdas that are enclosing variables. -/
-@[simp, scoped grind =]
-def depth : Term Var → ℕ
-| bvar _ => 0
-| fvar _ => 0
-| app t₁ t₂ => max (depth t₁) (depth t₂)
-| abs t => depth t + 1
-
-set_option linter.tacticAnalysis.verifyGrindOnly false in
-@[elab_as_elim]
-protected lemma ind_on_depth (P : Term Var → Prop) (bvar : ∀ i, P (bvar i)) (fvar : ∀ x, P (fvar x))
-    (app : ∀ M N, P M → P N → P (app M N))
-    (abs : ∀ M, P M → (∀ N, N.depth ≤ M.depth → P N) → P M.abs)
-    (M : Term Var) : P M := by
-  induction h : M.depth using Nat.strong_induction_on generalizing M with | _ n ih
-  induction M with
-  | abs M' => apply abs M' <;> grind
-  | bvar | fvar => grind
-  | app => apply app <;> grind only [depth, = max_def]
-
-/-- The depth of the lambda expression doesn't change by opening at i-th bound variable
- for some free variable. -/
- @[simp, scoped grind =]
-lemma depth_openRec_fvar_eq_depth (M : Term Var) (x : Var) (i : ℕ) :
-    (M⟦i ↝ fvar x⟧).depth = M.depth := by
-  induction M generalizing i <;> grind
-
-/-- The depth of the lambda expression doesn't change by opening for some free variable. -/
-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`. -/
 @[simp, scoped grind =]
 theorem lcAt_openRec_fvar_iff_lcAt (M : Term Var) (x : Var) (i : ℕ) :