λ-calculus

The λ-calculus with polymorphism and subtyping, 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 adapted

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty (Var : Type u_2) : Type u_2

Types of the polymorphic lambda calculus.

• top {Var : Type u_2} : Ty Var

  The type ⊤, with a single inhabitant.

• bvar {Var : Type u_2} : ℕ → Ty Var

  Bound variables that appear in a type, using a de-Bruijn index.

• fvar {Var : Type u_2} : Var → Ty Var

  Free type variables.

• arrow {Var : Type u_2} : Ty Var → Ty Var → Ty Var

  A function type.

• all {Var : Type u_2} : Ty Var → Ty Var → Ty Var

  A universal quantification.

• sum {Var : Type u_2} : Ty Var → Ty Var → Ty Var

  A sum type.

def Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy.default {a✝ : Type u_2} : Ty a✝

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy.default = Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.top

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy {a✝ : Type u_2} : Inhabited (Ty a✝)

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy = { default := Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedTy.default }

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Term (Var : Type u_2) : Type u_2

Syntax of locally nameless lambda terms, with free variables over Var.

• bvar {Var : Type u_2} : ℕ → Term Var

  Bound term variables that appear under a lambda abstraction, using a de-Bruijn index.

• fvar {Var : Type u_2} : Var → Term Var

  Free term variables.

• abs {Var : Type u_2} : Ty Var → Term Var → Term Var

  Lambda abstraction, introducing a new bound term variable.

• app {Var : Type u_2} : Term Var → Term Var → Term Var

  Function application.

• tabs {Var : Type u_2} : Ty Var → Term Var → Term Var

  Type abstraction, introducing a new bound type variable.

• tapp {Var : Type u_2} : Term Var → Ty Var → Term Var

  Type application.

• let' {Var : Type u_2} : Term Var → Term Var → Term Var

  Binding of a term.

• inl {Var : Type u_2} : Term Var → Term Var

  Left constructor of a sum.

• inr {Var : Type u_2} : Term Var → Term Var

  Right constructor of a sum.

• case {Var : Type u_2} : Term Var → Term Var → Term Var → Term Var

  Case matching on a sum.

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding (Var : Type u_2) : Type u_2

A context binding.

• sub {Var : Type u_2} : Ty Var → Binding Var

  Subtype binding.

• ty {Var : Type u_2} : Ty Var → Binding Var

  Type binding.

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding {a✝ : Type u_2} : Inhabited (Binding a✝)

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding = { default := Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding.default }

def Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding.default {a✝ : Type u_2} : Binding a✝

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.instInhabitedBinding.default = Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub default

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fv {Var : Type u_1} [DecidableEq Var] : Ty Var → Finset Var

Free variables of a type.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.top.fv = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.bvar a).fv = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.fvar X).fv = {X}
• (σ.arrow τ).fv = σ.fv ∪ τ.fv
• (σ.all τ).fv = σ.fv ∪ τ.fv
• (σ.sum τ).fv = σ.fv ∪ τ.fv

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.fv {Var : Type u_1} [DecidableEq Var] : Binding Var → Finset Var

Free variables of a binding.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.sub σ).fv = σ.fv
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding.ty σ).fv = σ.fv

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fv_ty {Var : Type u_1} [DecidableEq Var] : Term Var → Finset Var

Free type variables of a term.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar a).fv_ty = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar a).fv_ty = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.abs σ t₁).fv_ty = σ.fv ∪ t₁.fv_ty
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.tabs σ t₁).fv_ty = σ.fv ∪ t₁.fv_ty
• (t₁.tapp σ).fv_ty = σ.fv ∪ t₁.fv_ty
• t₁.inl.fv_ty = t₁.fv_ty
• t₁.inr.fv_ty = t₁.fv_ty
• (t₁.app t₂).fv_ty = t₁.fv_ty ∪ t₂.fv_ty
• (t₁.let' t₂).fv_ty = t₁.fv_ty ∪ t₂.fv_ty
• (t₁.case t₂ t₃).fv_ty = t₁.fv_ty ∪ t₂.fv_ty ∪ t₃.fv_ty

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fv_tm {Var : Type u_1} [DecidableEq Var] : Term Var → Finset Var

Free term variables of a term.

Equations

• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.bvar a).fv_tm = ∅
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar a).fv_tm = {a}
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.abs σ t₁).fv_tm = t₁.fv_tm
• (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.tabs σ t₁).fv_tm = t₁.fv_tm
• (t₁.tapp σ).fv_tm = t₁.fv_tm
• t₁.inl.fv_tm = t₁.fv_tm
• t₁.inr.fv_tm = t₁.fv_tm
• (t₁.app t₂).fv_tm = t₁.fv_tm ∪ t₂.fv_tm
• (t₁.let' t₂).fv_tm = t₁.fv_tm ∪ t₂.fv_tm
• (t₁.case t₂ t₃).fv_tm = t₁.fv_tm ∪ t₂.fv_tm ∪ t₃.fv_tm

@[reducible, inline]

abbrev Cslib.LambdaCalculus.LocallyNameless.Fsub.Env (Var : Type u_2) : Type u_2

A context of bindings.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.Env Var = Cslib.LambdaCalculus.LocallyNameless.Context Var (Cslib.LambdaCalculus.LocallyNameless.Fsub.Binding Var)