λ-calculus

The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. This file defines opening, local closure, and substitution.

References

• A. Chargueraud, The Locally Nameless Representation
• See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which this is adapted

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec {Var : Type u_1} (X : ℕ) (δ : Ty Var) : Ty Var → Ty Var

Variable opening (type opening to type) of the ith bound variable.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec X δ Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.top = Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.top
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.bvar Y) = if X = Y then δ else Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.bvar Y
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar X_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar X_1

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.«term_⟦_↝_⟧ᵞ» : Lean.TrailingParserDescr

Variable opening (type opening to type) of the ith bound variable.

Equations

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

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.open' {Var : Type u_1} (γ δ : Ty Var) : Ty Var

Variable opening (type opening to type) of the closest binding.

Equations

• γ.open' δ = Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec 0 δ γ

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.«term_^ᵞ_» : Lean.TrailingParserDescr

Variable opening (type opening to type) of the closest binding.

Equations

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

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.LC {Var : Type u_1} : Ty Var → Prop

Locally closed types.

• top {Var : Type u_1} : Ty.top.LC
• var {Var : Type u_1} {X : Var} : (fvar X).LC
• arrow {Var : Type u_1} {σ τ : Ty Var} : σ.LC → τ.LC → (σ.arrow τ).LC
• all {Var : Type u_1} {σ τ : Ty Var} (L : Finset Var) : σ.LC → (∀ X ∉ L, (τ.open' (fvar X)).LC) → (σ.all τ).LC
• sum {Var : Type u_1} {σ τ : Ty Var} : σ.LC → τ.LC → (σ.sum τ).LC

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst {Var : Type u_1} [DecidableEq Var] (X : Var) (δ : Ty Var) : Ty Var → Ty Var

Type substitution.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.top = Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.top
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.bvar Y) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.bvar Y
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar X_1) = if X_1 = X then δ else Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar X_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ (σ.arrow τ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ σ).arrow (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ τ)
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ (σ.all τ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ σ).all (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ τ)
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ (σ.sum τ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ σ).sum (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst X δ τ)

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.instHasSubstitution {Var : Type u_1} [DecidableEq Var] : HasSubstitution (Ty Var) Var (Ty Var)

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec_neq_eq {Var : Type u_1} {X Y : ℕ} {σ τ γ : Ty Var} (neq : X ≠ Y) (h : openRec Y τ σ = openRec X γ (openRec Y τ σ)) : σ = openRec X γ σ

An opening appearing in both sides of an equality of types can be removed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec_lc {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {X : ℕ} {σ τ : Ty Var} (lc : σ.LC) : σ = openRec X τ σ

A locally closed type is unchanged by opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst_def {Var : Type u_1} [DecidableEq Var] {δ γ : Ty Var} {X : Var} : subst X δ γ = γ[X:=δ]

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst_fresh {Var : Type u_1} [DecidableEq Var] {γ : Ty Var} {X : Var} (nmem : X ∉ γ.fv) (δ : Ty Var) : γ = γ[X:=δ]

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec_subst {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {δ : Ty Var} (Y : ℕ) (σ τ : Ty Var) (lc : δ.LC) (X : Var) : (openRec Y τ σ)[X:=δ] = openRec Y (τ[X:=δ]) (σ[X:=δ])

Substitution of a locally closed type distributes with opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.open_subst {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {δ : Ty Var} (σ τ : Ty Var) (lc : δ.LC) (X : Var) : (σ.open' τ)[X:=δ] = σ[X:=δ].open' (τ[X:=δ])

Specialize Ty.openRec_subst to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.open_subst_var {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {δ : Ty Var} {Y X : Var} (σ : Ty Var) (neq : Y ≠ X) (lc : δ.LC) : (σ.open' (fvar Y))[X:=δ] = σ[X:=δ].open' (fvar Y)

Specialize Ty.subst_open to free variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.openRec_subst_intro {Var : Type u_1} [DecidableEq Var] {γ : Ty Var} {X : Var} (Y : ℕ) (δ : Ty Var) (nmem : X ∉ γ.fv) : openRec Y δ γ = (openRec Y (fvar X) γ)[X:=δ]

Opening to a type is equivalent to opening to a free variable and substituting.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.open_subst_intro {Var : Type u_1} [DecidableEq Var] {γ : Ty Var} {X : Var} (δ : Ty Var) (nmem : X ∉ γ.fv) : γ.open' δ = (γ.open' (fvar X))[X:=δ]

Specialize Ty.openRec_subst_intro to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.subst_lc {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {σ τ : Ty Var} (σ_lc : σ.LC) (τ_lc : τ.LC) (X : Var) : σ[X:=τ].LC

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.nmem_fv_openRec {Var : Type u_1} [DecidableEq Var] {σ γ : Ty Var} {k : ℕ} {X : Var} (nmem : X ∉ (openRec k γ σ).fv) : X ∉ σ.fv

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.nmem_fv_open {Var : Type u_1} [DecidableEq Var] {σ γ : Ty Var} {X : Var} (nmem : X ∉ (σ.open' γ).fv) : X ∉ σ.fv

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy {Var : Type u_1} (X : ℕ) (δ : Ty Var) : Term Var → Term Var

Variable opening (term opening to type) of the ith bound variable.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy X δ t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy X δ t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy X δ t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy X δ t₂).inr

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.«term_⟦_↝_⟧ᵗᵞ» : Lean.TrailingParserDescr

Variable opening (term opening to type) of the ith bound variable.

Equations

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

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTy {Var : Type u_1} (t : Term Var) (δ : Ty Var) : Term Var

Variable opening (term opening to type) of the closest binding.

Equations

• t.openTy δ = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy 0 δ t

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.«term_^ᵗᵞ_» : Lean.TrailingParserDescr

Variable opening (term opening to type) of the closest binding.

Equations

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

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm {Var : Type u_1} (x : ℕ) (s : Term Var) : Term Var → Term Var

Variable opening (term opening to term) of the ith bound variable.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm x s (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_2) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_2
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm x s (t₁.tapp σ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm x s t₁).tapp σ
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm x s t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm x s t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm x s t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm x s t₂).inr

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.«term_⟦_↝_⟧ᵗᵗ» : Lean.TrailingParserDescr

Variable opening (term opening to term) of the ith bound variable.

Equations

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

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTm {Var : Type u_1} (t₁ t₂ : Term Var) : Term Var

Variable opening (term opening to term) of the closest binding.

Equations

• t₁.openTm t₂ = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm 0 t₂ t₁

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.«term_^ᵗᵗ_» : Lean.TrailingParserDescr

Variable opening (term opening to term) of the closest binding.

Equations

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

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.LC {Var : Type u_1} : Term Var → Prop

Locally closed terms.

• var {Var : Type u_1} {x : Var} : (fvar x).LC
• abs {Var : Type u_1} {t₁ : Term Var} {σ : Ty Var} (L : Finset Var) : σ.LC → (∀ x ∉ L, (t₁.openTm (fvar x)).LC) → (Term.abs σ t₁).LC
• app {Var : Type u_1} {t₁ t₂ : Term Var} : t₁.LC → t₂.LC → (t₁.app t₂).LC
• tabs {Var : Type u_1} {t₁ : Term Var} {σ : Ty Var} (L : Finset Var) : σ.LC → (∀ X ∉ L, (t₁.openTy (Ty.fvar X)).LC) → (Term.tabs σ t₁).LC
• tapp {Var : Type u_1} {t₁ : Term Var} {σ : Ty Var} : t₁.LC → σ.LC → (t₁.tapp σ).LC
• let' {Var : Type u_1} {t₁ t₂ : Term Var} (L : Finset Var) : t₁.LC → (∀ x ∉ L, (t₂.openTm (fvar x)).LC) → (t₁.let' t₂).LC
• inl {Var : Type u_1} {t₁ : Term Var} : t₁.LC → t₁.inl.LC
• inr {Var : Type u_1} {t₁ : Term Var} : t₁.LC → t₁.inr.LC
• case {Var : Type u_1} {t₁ t₂ t₃ : Term Var} (L : Finset Var) : t₁.LC → (∀ x ∉ L, (t₂.openTm (fvar x)).LC) → (∀ x ∉ L, (t₃.openTm (fvar x)).LC) → (t₁.case t₂ t₃).LC

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy_neq_eq {Var : Type u_1} {t : Term Var} {X Y : ℕ} {σ τ : Ty Var} (neq : X ≠ Y) (eq : openRecTy Y σ t = openRecTy X τ (openRecTy Y σ t)) : t = openRecTy X τ t

An opening (term to type) appearing in both sides of an equality of terms can be removed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm_ty_eq {Var : Type u_1} {t : Term Var} {δ : Ty Var} {x : ℕ} {s : Term Var} {y : ℕ} (eq : openRecTm x s t = openRecTy y δ (openRecTm x s t)) : t = openRecTy y δ t

Elimination of mixed term and type opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy_lc {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {X : ℕ} {σ : Ty Var} {t : Term Var} (lc : t.LC) : t = openRecTy X σ t

A locally closed term is unchanged by type opening.

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy {Var : Type u_1} [DecidableEq Var] (X : Var) (δ : Ty Var) : Term Var → Term Var

Substitution of a type within a term.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ (t₁.tapp σ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ t₁).tapp (σ[X:=δ])
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy X δ t₂).inr

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.instHasSubstitutionTy {Var : Type u_1} [DecidableEq Var] : HasSubstitution (Term Var) Var (Ty Var)

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy_def {Var : Type u_1} [DecidableEq Var] {t : Term Var} {δ : Ty Var} {X : Var} : substTy X δ t = t[X:=δ]

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy_fresh {Var : Type u_1} [DecidableEq Var] {t : Term Var} {X : Var} (nmem : X ∉ t.fvTy) (δ : Ty Var) : t = t[X:=δ]

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy_substTy {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {δ : Ty Var} (Y : ℕ) (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : (openRecTy Y σ t)[X:=δ] = openRecTy Y (σ[X:=δ]) (t[X:=δ])

Substitution of a locally closed type distributes with term opening to a type .

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTy_substTy {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {δ : Ty Var} (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : (t.openTy σ)[X:=δ] = t[X:=δ].openTy (σ[X:=δ])

Specialize Term.openRecTy_subst to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTy_substTy_var {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {δ : Ty Var} {Y X : Var} (t : Term Var) (neq : Y ≠ X) (lc : δ.LC) : (t.openTy (Ty.fvar Y))[X:=δ] = t[X:=δ].openTy (Ty.fvar Y)

Specialize Term.openTy_subst to free type variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy_substTy_intro {Var : Type u_1} [DecidableEq Var] {δ : Ty Var} {X : Var} (Y : ℕ) (t : Term Var) (nmem : X ∉ t.fvTy) : openRecTy Y δ t = (openRecTy Y (Ty.fvar X) t)[X:=δ]

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTy_substTy_intro {Var : Type u_1} [DecidableEq Var] {X : Var} (t : Term Var) (δ : Ty Var) (nmem : X ∉ t.fvTy) : t.openTy δ = (t.openTy (Ty.fvar X))[X:=δ]

Specialize Term.openRecTy_substTy_intro to the first opening.

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm {Var : Type u_1} [DecidableEq Var] (x : Var) (s : Term Var) : Term Var → Term Var

Substitution of a term within a term.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_2) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_2
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_2) = if x_2 = x then s else Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_2
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s (t₁.tapp σ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s t₁).tapp σ
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm x s t₂).inr

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.instHasSubstitution {Var : Type u_1} [DecidableEq Var] : HasSubstitution (Term Var) Var (Term Var)

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm_def {Var : Type u_1} [DecidableEq Var] {t : Term Var} {x : Var} {s : Term Var} : substTm x s t = t[x:=s]

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm_neq_eq {Var : Type u_1} {t : Term Var} {x y : ℕ} {s₁ s₂ : Term Var} (neq : x ≠ y) (eq : openRecTm y s₁ t = openRecTm x s₂ (openRecTm y s₁ t)) : t = openRecTm x s₂ t

An opening (term to term) appearing in both sides of an equality of terms can be removed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy_tm_eq {Var : Type u_1} {t : Term Var} {Y : ℕ} {σ : Ty Var} {x : ℕ} {s : Term Var} (eq : openRecTy Y σ t = openRecTm x s (openRecTy Y σ t)) : t = openRecTm x s t

Elimination of mixed term and type opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm_lc {Var : Type u_1} [DecidableEq Var] {t : Term Var} [HasFresh Var] {x : ℕ} {s : Term Var} (lc : t.LC) : t = openRecTm x s t

A locally closed term is unchanged by term opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm_fresh {Var : Type u_1} [DecidableEq Var] {t : Term Var} {x : Var} (nmem : x ∉ t.fvTm) (s : Term Var) : t = t[x:=s]

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm_substTm {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} (y : ℕ) (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : (openRecTm y t₂ t₁)[x:=s] = openRecTm y (t₂[x:=s]) (t₁[x:=s])

Substitution of a locally closed term distributes with term opening to a term.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTm_substTm {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : (t₁.openTm t₂)[x:=s] = t₁[x:=s].openTm (t₂[x:=s])

Specialize Term.openRecTm_substTm to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTm_substTm_var {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} {x y : Var} (t : Term Var) (neq : y ≠ x) (lc : s.LC) : (t.openTm (fvar y))[x:=s] = t[x:=s].openTm (fvar y)

Specialize Term.openRecTm_substTm to free term variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm_substTy {Var : Type u_1} [DecidableEq Var] [HasFresh Var] (y : ℕ) (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : (openRecTm y t₂ t₁)[X:=δ] = openRecTm y (t₂[X:=δ]) (t₁[X:=δ])

Substitution of a locally closed type distributes with term opening to a term.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTm_substTy {Var : Type u_1} [DecidableEq Var] [HasFresh Var] (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) : (t₁.openTm t₂)[X:=δ] = t₁[X:=δ].openTm (t₂[X:=δ])

Specialize Term.openRecTm_substTy to the first opening

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTm_substTy_var {Var : Type u_1} [DecidableEq Var] [HasFresh Var] (t₁ : Term Var) (δ : Ty Var) (X y : Var) : (t₁.openTm (fvar y))[X:=δ] = t₁[X:=δ].openTm (fvar y)

Specialize Term.openTm_substTy to free term variables

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTy_substTm {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} (Y : ℕ) (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : (openRecTy Y δ t)[x:=s] = openRecTy Y δ (t[x:=s])

Substitution of a locally closed term distributes with term opening to a type.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTy_substTm {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) : (t.openTy δ)[x:=s] = t[x:=s].openTy δ

Specialize Term.openRecTy_substTm to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTy_substTm_var {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} (t : Term Var) (lc : s.LC) (x Y : Var) : (t.openTy (Ty.fvar Y))[x:=s] = t[x:=s].openTy (Ty.fvar Y)

Specialize Term.openTy_substTm to free type variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRecTm_substTm_intro {Var : Type u_1} [DecidableEq Var] {x : Var} (y : ℕ) (t s : Term Var) (nmem : x ∉ t.fvTm) : openRecTm y s t = (openRecTm y (fvar x) t)[x:=s]

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openTm_substTm_intro {Var : Type u_1} [DecidableEq Var] {x : Var} (t s : Term Var) (nmem : x ∉ t.fvTm) : t.openTm s = (t.openTm (fvar x))[x:=s]

Specialize Term.openRecTm_substTm_intro to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTy_lc {Var : Type u_1} [DecidableEq Var] {t : Term Var} {δ : Ty Var} [HasFresh Var] (t_lc : t.LC) (δ_lc : δ.LC) (X : Var) : t[X:=δ].LC

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.substTm_lc {Var : Type u_1} [DecidableEq Var] {t s : Term Var} [HasFresh Var] (t_lc : t.LC) (s_lc : s.LC) (x : Var) : t[x:=s].LC

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.subst {Var : Type u_1} [DecidableEq Var] (X : Var) (δ : Ty Var) : Binding Var → Binding Var

Binding substitution of types.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.subst X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub γ) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub (γ[X:=δ])
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.subst X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty γ) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty (γ[X:=δ])

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.instHasSubstitutionTy {Var : Type u_1} [DecidableEq Var] : HasSubstitution (Binding Var) Var (Ty Var)

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.substSub {Var : Type u_1} [DecidableEq Var] {δ γ : Ty Var} {X : Var} : (sub γ)[X:=δ] = sub (γ[X:=δ])

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.substTy {Var : Type u_1} [DecidableEq Var] {δ γ : Ty Var} {X : Var} : (ty γ)[X:=δ] = ty (γ[X:=δ])

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.subst_fresh {Var : Type u_1} [DecidableEq Var] {X : Var} {γ : Binding Var} (nmem : X ∉ γ.fv) (δ : Ty Var) : γ = γ[X:=δ]

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