Alternative Definitions for LC:

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.

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt {Var : Type u} (k : ℕ) : Term Var → Bool

LcAt k M is satisfied when all bound indices of M are smaller than k.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt k (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.bvar i) = decide (i < k)
• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt k (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.fvar a) = true
• Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt k t.abs = Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LcAt (k + 1) t

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.depth {Var : Type u} : Term Var → ℕ

depth counts the maximum number of the lambdas that are enclosing variables.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.bvar i).depth = 0
• (Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.fvar a).depth = 0
• (t₁.app t₂).depth = max t₁.depth t₂.depth
• t.abs.depth = t.depth + 1

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ind_on_depth {Var : Type u} (P : Term Var → Prop) (bvar : ∀ (i : ℕ), P (bvar i)) (fvar : ∀ (x : Var), P (fvar x)) (app : ∀ (M N : Term Var), P M → P N → P (M.app N)) (abs : ∀ (M : Term Var), P M → (∀ (N : Term Var), N.depth ≤ M.depth → P N) → P M.abs) (M : Term Var) : P M

@[simp]

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.depth_openRec_fvar_eq_depth {Var : Type u} (M : Term Var) (x : Var) (i : ℕ) : (openRec i (fvar x) M).depth = M.depth

The depth of the lambda expression doesn't change by opening at i-th bound variable for some free variable.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.depth_open_fvar_eq_depth {Var : Type u} (M : Term Var) (x : Var) : (M.open' (fvar x)).depth = M.depth

The depth of the lambda expression doesn't change by opening for some free variable.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_le {Var : Type u} (M : Term Var) (i j : ℕ) (h : i ≤ j) (lc : LcAt i M = true) : LcAt j M = true

@[simp]

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_openRec_iff_lcAt {Var : Type u} (M N : Term Var) (i : ℕ) (h : LcAt i N = true) : LcAt i (openRec i N M) = LcAt (i + 1) M

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_open_fvar_iff_lcAt {Var : Type u} (M : Term Var) (x : Var) : LcAt 0 (M.open' (fvar x)) = LcAt 1 M

Opening for some free variable is locally closed if and only if M is LcAt 1.

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.LC {Var : Type u} : Term Var → Prop

Locally closed terms.

• fvar {Var : Type u} (x : Var) : (Term.fvar x).LC
• abs {Var : Type u} (L : Finset Var) (e : Term Var) : (∀ x ∉ L, (e.open' (Term.fvar x)).LC) → e.abs.LC
• app {Var : Type u} {l r : Term Var} : l.LC → r.LC → (l.app r).LC

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Value {Var : Type u} : Term Var → Prop

Values are irreducible terms.

• abs {Var : Type u} (e : Term Var) : e.abs.LC → e.abs.Value

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.IsAbs {Var : Type u} : Term Var → Prop

IsAbs m holds when m is an abstraction.

• abs {Var : Type u} (m : Term Var) : m.abs.IsAbs

@[instance_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.instDecidableIsAbs {Var : Type u} (m : Term Var) : Decidable m.IsAbs

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_iff_LC {Var : Type u} (M : Term Var) [HasFresh Var] : LcAt 0 M = true ↔ M.LC

M is LcAt 0 if and only if M is locally closed.

@[instance_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.instDecidableLCOfHasFresh {Var : Type u} [HasFresh Var] (t : Term Var) : Decidable t.LC

Equations

• t.instDecidableLCOfHasFresh = ⋯.mpr inferInstance

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_openRec_lcAt {Var : Type u} (M N : Term Var) (i : ℕ) : LcAt i (openRec i N M) = true → LcAt (i + 1) M = true

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_abs_lc {Var : Type u} [HasFresh Var] {M N : Term Var} (hlc : (M.open' N).LC) : M.abs.LC

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.lcAt_openRec_above_lcAt {Var : Type u} (M N : Term Var) (i j : ℕ) (h : i ≤ j) (lc : LcAt i M = true) : openRec j N M = M