λ-calculus

The simply typed λ-calculus, with a locally nameless representation of syntax.

References

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

inductive LambdaCalculus.LocallyNameless.Stlc.Ty (Base : Type v) : Type v

Types of the simply typed lambda calculus.

• base {Base : Type v} : Base → Ty Base

  A base type, from a typing context.

• arrow {Base : Type v} : Ty Base → Ty Base → Ty Base

  A function type.

def LambdaCalculus.LocallyNameless.Stlc.«term_⤳_» : Lean.TrailingParserDescr

Equations

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

inductive LambdaCalculus.LocallyNameless.Stlc.Typing {Var : Type u} {Base : Type v} : Context Var (Ty Base) → Untyped.Term Var → Ty Base → Prop

An extrinsic typing derivation for locally nameless terms.

• var {Var : Type u} {Base : Type v} {Γ : Context Var (Ty Base)} {x : Var} {σ : Ty Base} : Γ✓ → ⟨x, σ⟩ ∈ Γ → Typing Γ (Untyped.Term.fvar x) σ

  Free variables, from a context judgement.

• abs {Var : Type u} {Base : Type v} {σ : Ty Base} {Γ : List ((_ : Var) × Ty Base)} {t : Untyped.Term Var} {τ : Ty Base} (L : Finset Var) : (∀ x ∉ L, Typing (⟨x, σ⟩ :: Γ) (t.open' (Untyped.Term.fvar x)) τ) → Typing Γ t.abs (σ.arrow τ)

  Lambda abstraction.

• app {Var : Type u} {Base : Type v} {Γ : Context Var (Ty Base)} {t : Untyped.Term Var} {σ τ : Ty Base} {t' : Untyped.Term Var} : Typing Γ t (σ.arrow τ) → Typing Γ t' σ → Typing Γ (t.app t') τ

  Function application.

def LambdaCalculus.LocallyNameless.Stlc.«term_⊢_∶_» : Lean.TrailingParserDescr

Equations

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

theorem LambdaCalculus.LocallyNameless.Stlc.Typing.perm {Var : Type u} {Base : Type v} {Γ Δ : Context Var (Ty Base)} {t : Untyped.Term Var} {τ : Ty Base} (ht : Typing Γ t τ) (hperm : List.Perm Γ Δ) : Typing Δ t τ

Typing is preserved on permuting a context.

theorem LambdaCalculus.LocallyNameless.Stlc.Typing.weaken_aux {Var : Type u} {Base : Type v} [DecidableEq Var] {Γ Δ Θ : Context Var (Ty Base)} {t : Untyped.Term Var} {τ : Ty Base} (der : Typing (Γ ++ Δ) t τ) : (Γ ++ Θ ++ Δ)✓ → Typing (Γ ++ Θ ++ Δ) t τ

Weakening of a typing derivation with an appended context.

theorem LambdaCalculus.LocallyNameless.Stlc.Typing.weaken {Var : Type u} {Base : Type v} [DecidableEq Var] {Γ Δ : Context Var (Ty Base)} {t : Untyped.Term Var} {τ : Ty Base} (der : Typing Γ t τ) (ok : (Γ ++ Δ)✓) : Typing (Γ ++ Δ) t τ

Weakening of a typing derivation by an additional context.

theorem LambdaCalculus.LocallyNameless.Stlc.Typing.lc {Var : Type u} {Base : Type v} {Γ : Context Var (Ty Base)} {t : Untyped.Term Var} {τ : Ty Base} (der : Typing Γ t τ) : t.LC

Typing derivations exist only for locally closed terms.

theorem LambdaCalculus.LocallyNameless.Stlc.Typing.subst_aux {Var : Type u} {Base : Type v} [DecidableEq Var] {Γ Δ : Context Var (Ty Base)} [HasFresh Var] {x : Var} {σ : Ty Base} {t : Untyped.Term Var} {τ : Ty Base} {s : Untyped.Term Var} (h : Typing (Δ ++ ⟨x, σ⟩ :: Γ) t τ) (der : Typing Γ s σ) : Typing (Δ ++ Γ) (t[x:=s]) τ

Substitution for a context weakened by a single type between appended contexts.

theorem LambdaCalculus.LocallyNameless.Stlc.Typing.typing_subst_head {Var : Type u} {Base : Type v} [DecidableEq Var] {Γ : Context Var (Ty Base)} [HasFresh Var] {x : Var} {σ : Ty Base} {t : Untyped.Term Var} {τ : Ty Base} {s : Untyped.Term Var} (weak : Typing (⟨x, σ⟩ :: Γ) t τ) (der : Typing Γ s σ) : Typing Γ (t[x:=s]) τ

Substitution for a context weakened by a single type.

theorem LambdaCalculus.LocallyNameless.Stlc.Typing.preservation_open {Var : Type u} {Base : Type v} [DecidableEq Var] {Γ : Context Var (Ty Base)} [HasFresh Var] {σ : Ty Base} {m : Untyped.Term Var} {τ : Ty Base} {n : Untyped.Term Var} {xs : Finset Var} (cofin : ∀ x ∉ xs, Typing (⟨x, σ⟩ :: Γ) (m.open' (Untyped.Term.fvar x)) τ) (der : Typing Γ n σ) : Typing Γ (m.open' n) τ

Typing preservation for opening.