From d93e41412d2ab57ccb2117e4cbb1d9143e445a14 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Tue, 19 May 2026 17:37:40 +0800 Subject: [PATCH] feat(LocallyNameless/Untyped): make `LcAt` and `LC` decidable --- .../LambdaCalculus/LocallyNameless/Untyped/LcAt.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean index 5a6529c1e..7222d84bb 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean @@ -27,10 +27,10 @@ variable {Var : Type u} /-- `LcAt k M` is satisfied when all bound indices of M are smaller than `k`. -/ @[simp, scoped grind =] -def LcAt (k : ℕ) : Term Var → Prop +def LcAt (k : ℕ) : Term Var → Bool | bvar i => i < k -| fvar _ => True -| app t₁ t₂ => LcAt k t₁ ∧ LcAt k t₂ +| fvar _ => true +| 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. -/ @@ -83,6 +83,10 @@ theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by grind [fresh_exists L] | _ => grind [cases LC] +instance [HasFresh Var] (t : Term Var) : Decidable t.LC := by + rw [← lcAt_iff_LC] + infer_instance + /- Opening for some term at i-th bound variable increments `LcAt` by one -/ lemma lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) : LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by