λ-calculus

The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. This file defines a call-by-value reduction.

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.Term.body {Var : Type u_1} (t : Term Var) : Prop

Existential predicate for being a locally closed body of an abstraction.

Equations

• t.body = ∃ (L : Finset Var), ∀ x ∉ L, (t.open_tm (Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.fvar x)).LC

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.body_let {Var : Type u_1} {t₁ t₂ : Term Var} [DecidableEq Var] : (t₁.let' t₂).LC ↔ t₁.LC ∧ t₂.body

Locally closed let bindings have a locally closed body.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.body_case {Var : Type u_1} {t₁ t₂ t₃ : Term Var} [DecidableEq Var] : (t₁.case t₂ t₃).LC ↔ t₁.LC ∧ t₂.body ∧ t₃.body

Locally closed case bindings have a locally closed bodies.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_tm_body {Var : Type u_1} {t₁ t₂ : Term Var} [DecidableEq Var] [HasFresh Var] (body : t₁.body) (lc : t₂.LC) : (t₁.open_tm t₂).LC

Opening a body preserves local closure.

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

Values are irreducible terms.

• abs {Var : Type u_1} {σ : Ty Var} {t₁ : Term Var} : (Term.abs σ t₁).LC → (Term.abs σ t₁).Value
• tabs {Var : Type u_1} {σ : Ty Var} {t₁ : Term Var} : (Term.tabs σ t₁).LC → (Term.tabs σ t₁).Value
• inl {Var : Type u_1} {t₁ : Term Var} : t₁.Value → t₁.inl.Value
• inr {Var : Type u_1} {t₁ : Term Var} : t₁.Value → t₁.inr.Value

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Value.lc {Var : Type u_1} {t : Term Var} (val : t.Value) : t.LC

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

The call-by-value reduction relation.

• appₗ {Var : Type u_1} {t₂ t₁ t₁' : Term Var} : t₂.LC → t₁.Red t₁' → (t₁.app t₂).Red (t₁'.app t₂)
• appᵣ {Var : Type u_1} {t₁ t₂ t₂' : Term Var} : t₁.Value → t₂.Red t₂' → (t₁.app t₂).Red (t₁.app t₂')
• tapp {Var : Type u_1} {t₁ t₁' : Term Var} {σ : Ty Var} : σ.LC → t₁.Red t₁' → (t₁.tapp σ).Red (t₁'.tapp σ)
• abs {Var : Type u_1} {σ : Ty Var} {t₁ t₂ : Term Var} : (Term.abs σ t₁).LC → t₂.Value → ((Term.abs σ t₁).app t₂).Red (t₁.open_tm t₂)
• tabs {Var : Type u_1} {σ : Ty Var} {t₁ : Term Var} {τ : Ty Var} : (Term.tabs σ t₁).LC → τ.LC → ((Term.tabs σ t₁).tapp τ).Red (t₁.open_ty τ)
• let_bind {Var : Type u_1} {t₁ t₁' t₂ : Term Var} : t₁.Red t₁' → t₂.body → (t₁.let' t₂).Red (t₁'.let' t₂)
• let_body {Var : Type u_1} {t₁ t₂ : Term Var} : t₁.Value → t₂.body → (t₁.let' t₂).Red (t₂.open_tm t₁)
• inl {Var : Type u_1} {t₁ t₁' : Term Var} : t₁.Red t₁' → t₁.inl.Red t₁'.inl
• inr {Var : Type u_1} {t₁ t₁' : Term Var} : t₁.Red t₁' → t₁.inr.Red t₁'.inr
• case {Var : Type u_1} {t₁ t₁' t₂ t₃ : Term Var} : t₁.Red t₁' → t₂.body → t₃.body → (t₁.case t₂ t₃).Red (t₁'.case t₂ t₃)
• case_inl {Var : Type u_1} {t₁ t₂ t₃ : Term Var} : t₁.Value → t₂.body → t₃.body → (t₁.inl.case t₂ t₃).Red (t₂.open_tm t₁)
• case_inr {Var : Type u_1} {t₁ t₂ t₃ : Term Var} : t₁.Value → t₂.body → t₃.body → (t₁.inr.case t₂ t₃).Red (t₃.open_tm t₁)

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.«term_⭢βᵛ_» : Lean.TrailingParserDescr

Equations

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

def Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.«term_↠βᵛ_» : Lean.TrailingParserDescr

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.Red.lc {Var : Type u_1} [HasFresh Var] [DecidableEq Var] {t t' : Term Var} (red : rs.Red t t') : t.LC ∧ t'.LC

Terms of a reduction are locally closed.