From 98b2996f7d4fbefada8412256552715c1ec5fcc5 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Fri, 14 Aug 2026 07:42:49 +0800 Subject: [PATCH 1/2] wip --- Cslib.lean | 1 + .../LocallyNameless/Untyped/Depth.lean | 62 +++++++++++++++++++ .../LocallyNameless/Untyped/LcAt.lean | 32 +--------- 3 files changed, 64 insertions(+), 31 deletions(-) create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Depth.lean diff --git a/Cslib.lean b/Cslib.lean index 73f87a580..2d4968057 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -149,6 +149,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Depth public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostReduction public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Depth.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Depth.lean new file mode 100644 index 000000000..eeb781743 --- /dev/null +++ b/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 diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean index 4a74cf41d..7eb8fcbb8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean @@ -7,6 +7,7 @@ Authors: Elimia (Sehun Kim) module public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Depth /-! @@ -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 : ℕ) : From cb2afb2cbc060f19c9ce36985872b62026c03fd5 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Fri, 14 Aug 2026 07:51:11 +0800 Subject: [PATCH 2/2] refactor(LocallyNameless): Extract depth into a dedicated module --- Cslib.lean | 2 +- .../LambdaCalculus/LocallyNameless/Untyped/LcAt.lean | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib.lean b/Cslib.lean index 2d4968057..5a56183d8 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -143,13 +143,13 @@ 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 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Depth public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostReduction public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean index 7eb8fcbb8..375094bcb 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean @@ -11,10 +11,10 @@ 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`. -/