λ-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 δ τ)

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.openRec_ty {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.openRec_ty X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty X δ t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty X δ t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty X δ t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty 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.open_ty {Var : Type u_1} (t : Term Var) (δ : Ty Var) : Term Var

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

Equations

• t.open_ty δ = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty 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.openRec_tm {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.openRec_tm x s (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_2) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_2
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm x s (t₁.tapp σ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm x s t₁).tapp σ
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm x s t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm x s t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm x s t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm 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.open_tm {Var : Type u_1} (t₁ t₂ : Term Var) : Term Var

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

Equations

• t₁.open_tm t₂ = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm 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₁.open_tm (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₁.open_ty (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₂.open_tm (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₂.open_tm (fvar x)).LC) → (∀ x ∉ L, (t₃.open_tm (fvar x)).LC) → (t₁.case t₂ t₃).LC

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty_neq_eq {Var : Type u_1} {t : Term Var} {X Y : ℕ} {σ τ : Ty Var} (neq : X ≠ Y) (eq : openRec_ty Y σ t = openRec_ty X τ (openRec_ty Y σ t)) : t = openRec_ty 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.openRec_tm_ty_eq {Var : Type u_1} {t : Term Var} {δ : Ty Var} {x : ℕ} {s : Term Var} {y : ℕ} (eq : openRec_tm x s t = openRec_ty y δ (openRec_tm x s t)) : t = openRec_ty y δ t

Elimination of mixed term and type opening.

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

A locally closed term is unchanged by type opening.

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty {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.subst_ty X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty X δ (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x_1
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty X δ (t₁.tapp σ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty X δ t₁).tapp (σ[X:=δ])
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty X δ t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty X δ t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty X δ t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty X δ t₂).inr

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.subst_ty_def {Var : Type u_1} [DecidableEq Var] {t : Term Var} {δ : Ty Var} {X : Var} : subst_ty X δ t = t[X:=δ]

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty_fresh {Var : Type u_1} [DecidableEq Var] {t : Term Var} {X : Var} (nmem : X ∉ t.fv_ty) (δ : 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.openRec_ty_subst_ty {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {δ : Ty Var} (Y : ℕ) (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : (openRec_ty Y σ t)[X:=δ] = openRec_ty Y (σ[X:=δ]) (t[X:=δ])

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

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

Specialize Term.openRec_ty_subst to the first opening.

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

Specialize Term.open_ty_subst to free type variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_ty_subst_ty_intro {Var : Type u_1} [DecidableEq Var] {δ : Ty Var} {X : Var} (Y : ℕ) (t : Term Var) (nmem : X ∉ t.fv_ty) : openRec_ty Y δ t = (openRec_ty 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.open_ty_subst_ty_intro {Var : Type u_1} [DecidableEq Var] {X : Var} (t : Term Var) (δ : Ty Var) (nmem : X ∉ t.fv_ty) : t.open_ty δ = (t.open_ty (Ty.fvar X))[X:=δ]

Specialize Term.openRec_ty_subst_ty_intro to the first opening.

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm {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.subst_tm x s (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_2) = Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar x_2
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm x s (t₁.tapp σ) = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm x s t₁).tapp σ
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm x s t₁.inl = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm x s t₁).inl
• Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm x s t₂.inr = (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm x s t₂).inr

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.subst_tm_def {Var : Type u_1} [DecidableEq Var] {t : Term Var} {x : Var} {s : Term Var} : subst_tm x s t = t[x:=s]

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm_neq_eq {Var : Type u_1} {t : Term Var} {x y : ℕ} {s₁ s₂ : Term Var} (neq : x ≠ y) (eq : openRec_tm y s₁ t = openRec_tm x s₂ (openRec_tm y s₁ t)) : t = openRec_tm 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.openRec_ty_tm_eq {Var : Type u_1} {t : Term Var} {Y : ℕ} {σ : Ty Var} {x : ℕ} {s : Term Var} (eq : openRec_ty Y σ t = openRec_tm x s (openRec_ty Y σ t)) : t = openRec_tm x s t

Elimination of mixed term and type opening.

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

A locally closed term is unchanged by term opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_tm_fresh {Var : Type u_1} [DecidableEq Var] {t : Term Var} {x : Var} (nmem : x ∉ t.fv_tm) (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.openRec_tm_subst_tm {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} (y : ℕ) (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : (openRec_tm y t₂ t₁)[x:=s] = openRec_tm 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.open_tm_subst_tm {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {s : Term Var} (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) : (t₁.open_tm t₂)[x:=s] = t₁[x:=s].open_tm (t₂[x:=s])

Specialize Term.openRec_tm_subst_tm to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_tm_subst_tm_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.open_tm (fvar y))[x:=s] = t[x:=s].open_tm (fvar y)

Specialize Term.openRec_tm_subst_tm to free term variables.

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

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

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

Specialize Term.openRec_tm_subst_ty to the first opening

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

Specialize Term.open_tm_subst_ty to free term variables

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

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

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

Specialize Term.openRec_ty_subst_tm to the first opening.

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

Specialize Term.open_ty_subst_tm to free type variables.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.openRec_tm_subst_tm_intro {Var : Type u_1} [DecidableEq Var] {x : Var} (y : ℕ) (t s : Term Var) (nmem : x ∉ t.fv_tm) : openRec_tm y s t = (openRec_tm 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.open_tm_subst_tm_intro {Var : Type u_1} [DecidableEq Var] {x : Var} (t s : Term Var) (nmem : x ∉ t.fv_tm) : t.open_tm s = (t.open_tm (fvar x))[x:=s]

Specialize Term.openRec_tm_subst_tm_intro to the first opening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.subst_ty_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.subst_tm_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:=δ])

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.subst_sub {Var : Type u_1} [DecidableEq Var] {δ γ : Ty Var} {X : Var} : (sub γ)[X:=δ] = sub (γ[X:=δ])

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.subst_ty {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.