General properties of opening and substitution in untyped lambda calculus terms.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_fresh {Var : Type u} [DecidableEq Var] (x : Var) (t sub : Term Var) (nmem : x ∉ t.fv) : t[x := sub] = t

Substitution of a free variable not present in a term leaves it unchanged.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_close {Var : Type u} [DecidableEq Var] (x : Var) (t : Term Var) (k : ℕ) (nmem : x ∉ t.fv) : t = closeRec k x (openRec k (fvar x) t)

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_close_var {Var : Type u} [DecidableEq Var] (x : Var) (t : Term Var) (nmem : x ∉ t.fv) : t = (t.open' (fvar x)).close x

Specializes open_close to the first closing.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_injective {Var : Type u} [DecidableEq Var] (x : Var) (M M' : Term Var) (free_M : x ∉ M.fv) (free_M' : x ∉ M'.fv) (eq : M.open' (fvar x) = M'.open' (fvar x)) : M = M'

Opening is injective.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.swap_open_fvar_close {Var : Type u} [DecidableEq Var] (k n : ℕ) (x y : Var) (m : Term Var) (neq₁ : k ≠ n) (neq₂ : x ≠ y) : closeRec k x (openRec n (fvar y) m) = openRec n (fvar y) (closeRec k x m)

Opening and closing are associative for nonclashing free variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.close_rec_fv {Var : Type u} [DecidableEq Var] {k : ℕ} {y : Var} (m : Term Var) : (closeRec k y m).fv = m.fv.erase y

Closing preserves free variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.close_var_not_fvar {Var : Type u} [DecidableEq Var] (x : Var) (t : Term Var) : (t.close x).fv = t.fv.erase x

Specializes close_var_not_fvar_rec to first closing.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_preserve_not_fvar {Var : Type u} [DecidableEq Var] (k : ℕ) (m n : Term Var) : (openRec k n m).fv = m.fv ∪ n.fv ∨ (openRec k n m).fv = m.fv

Opening preserves free variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_preserve_not_fvar {Var : Type u} [DecidableEq Var] {y : Var} (m n : Term Var) : m[y := n].fv = m.fv.erase y ∨ m[y := n].fv = m.fv.erase y ∪ n.fv

Substitution preserves free variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_refl {Var : Type u} [DecidableEq Var] (m : Term Var) (x : Var) : m[x := fvar x] = m

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro_openRec {Var : Type u} [DecidableEq Var] {x : Var} {t e : Term Var} (mem : x ∉ e.fv) {k : ℕ} : openRec k t e = (openRec k (fvar x) e)[x := t]

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro {Var : Type u} [DecidableEq Var] (x : Var) (t e : Term Var) (mem : x ∉ e.fv) : e.open' t = (e.open' (fvar x))[x := t]

Opening to a term t is equivalent to opening to a free variable and substituting for t.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_lc {Var : Type u} [HasFresh Var] (k : ℕ) (t e : Term Var) (e_lc : e.LC) : openRec k t e = e

A locally closed term is unchanged by opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.swap_open {Var : Type u} [HasFresh Var] (k n : ℕ) (t₁ t₂ m : Term Var) (neq : k ≠ n) (h1 : t₁.LC) (h2 : t₂.LC) : openRec k t₁ (openRec n t₂ m) = openRec n t₂ (openRec k t₁ m)

Opening is associative for nonclashing locally closed terms.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.open_eq_app {Var : Type u} [DecidableEq Var] [HasFresh Var] {x : Var} {m n : Term Var} (hw_n : x ∉ n.fv) (hw_m : x ∉ m.fv) (lc_m : m.LC) (h : n.open' (fvar x) = m.app (fvar x)) : n = m.app (bvar 0)

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_openRec {Var : Type u} [DecidableEq Var] [HasFresh Var] (x : Var) (t : Term Var) (k : ℕ) (u e : Term Var) (lc : t.LC) : (openRec k u e)[x := t] = openRec k u[x := t] e[x := t]

Substitution of a locally closed term distributes with opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_open {Var : Type u} [DecidableEq Var] [HasFresh Var] (x : Var) (t u e : Term Var) (lc : t.LC) : (e.open' u)[x := t] = e[x := t].open' u[x := t]

Specialize subst_openRec to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_open_var {Var : Type u} [DecidableEq Var] [HasFresh Var] (x y : Var) (u e : Term Var) (neq : y ≠ x) (u_lc : u.LC) : (e.open' (fvar x))[y := u] = e[y := u].open' (fvar x)

Specialize subst_open to the free variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_lc {Var : Type u} [DecidableEq Var] [HasFresh Var] {x : Var} {e u : Term Var} (e_lc : e.LC) (u_lc : u.LC) : e[x := u].LC

Substitution of locally closed terms is locally closed.

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

Opening of locally closed terms is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.close_openRec_to_subst {Var : Type u} [DecidableEq Var] [HasFresh Var] (m n : Term Var) (x : Var) (k : ℕ) (m_lc : m.LC) (n_lc : n.LC) : openRec k n (closeRec k x m) = m[x := n]

Closing then opening is equivalent to substitution.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.close_open_to_subst {Var : Type u} [DecidableEq Var] [HasFresh Var] (m n : Term Var) (x : Var) (m_lc : m.LC) (n_lc : n.LC) : (m.close x).open' n = m[x := n]

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.close_open {Var : Type u} [DecidableEq Var] [HasFresh Var] (x : Var) (t : Term Var) (k : ℕ) (t_lc : t.LC) : openRec k (fvar x) (closeRec k x t) = t

Closing and opening are inverses.