λ-calculus

The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. This file defines the typing relation.

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.Typing {Var : Type u_1} [DecidableEq Var] : Env Var → Term Var → Ty Var → Prop

The typing relation.

• var {Var : Type u_1} [DecidableEq Var] {σ : Ty Var} {Γ : Env Var} {x : Var} : Γ.Wf → Binding.ty σ ∈ List.dlookup x Γ → Typing Γ (Term.fvar x) σ
• abs {Var : Type u_1} [DecidableEq Var] {σ : Ty Var} {Γ : List ((_ : Var) × Binding Var)} {t₁ : Term Var} {τ : Ty Var} (L : Finset Var) : (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₁.open_tm (Term.fvar x)) τ) → Typing Γ (Term.abs σ t₁) (σ.arrow τ)
• app {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {t₁ : Term Var} {σ τ : Ty Var} {t₂ : Term Var} : Typing Γ t₁ (σ.arrow τ) → Typing Γ t₂ σ → Typing Γ (t₁.app t₂) τ
• tabs {Var : Type u_1} [DecidableEq Var] {σ : Ty Var} {Γ : List ((_ : Var) × Binding Var)} {t₁ : Term Var} {τ : Ty Var} (L : Finset Var) : (∀ X ∉ L, Typing (⟨X, Binding.sub σ⟩ :: Γ) (t₁.open_ty (Ty.fvar X)) (τ.open' (Ty.fvar X))) → Typing Γ (Term.tabs σ t₁) (σ.all τ)
• tapp {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {t₁ : Term Var} {σ τ σ' : Ty Var} : Typing Γ t₁ (σ.all τ) → Sub Γ σ' σ → Typing Γ (t₁.tapp σ') (τ.open' σ')
• sub {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {t : Term Var} {τ τ' : Ty Var} : Typing Γ t τ → Sub Γ τ τ' → Typing Γ t τ'
• let' {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {t₁ : Term Var} {σ : Ty Var} {t₂ : Term Var} {τ : Ty Var} (L : Finset Var) : Typing Γ t₁ σ → (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₂.open_tm (Term.fvar x)) τ) → Typing Γ (t₁.let' t₂) τ
• inl {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {t₁ : Term Var} {σ τ : Ty Var} : Typing Γ t₁ σ → Ty.Wf Γ τ → Typing Γ t₁.inl (σ.sum τ)
• inr {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {t₁ : Term Var} {τ σ : Ty Var} : Typing Γ t₁ τ → Ty.Wf Γ σ → Typing Γ t₁.inr (σ.sum τ)
• case {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {t₁ : Term Var} {σ τ : Ty Var} {t₂ : Term Var} {δ : Ty Var} {t₃ : Term Var} (L : Finset Var) : Typing Γ t₁ (σ.sum τ) → (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₂.open_tm (Term.fvar x)) δ) → (∀ x ∉ L, Typing (⟨x, Binding.ty τ⟩ :: Γ) (t₃.open_tm (Term.fvar x)) δ) → Typing Γ (t₁.case t₂ t₃) δ

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.wf {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ.Wf ∧ t.LC ∧ Ty.Wf Γ τ

Typings have well-formed contexts and types.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.weaken {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {Γ Δ Θ : Env Var} {τ : Ty Var} {t : Term Var} (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : Typing (Γ ++ Θ ++ Δ) t τ

Weakening of typings.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.weaken_head {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {Γ Δ : Env Var} {τ : Ty Var} {t : Term Var} (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) : Typing (Γ ++ Δ) t τ

Weakening of typings (at the front).

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.narrow {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {Γ Δ : Env Var} {τ δ δ' : Ty Var} {X : Var} {t : Term Var} (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) : Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ

Narrowing of typings.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.subst_tm {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {Γ Δ : Env Var} {σ τ : Ty Var} {X : Var} {t s : Term Var} (der : Typing (Γ ++ ⟨X, Binding.ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) : Typing (Γ ++ Δ) (t[X:=s]) τ

Term substitution within a typing.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.subst_ty {Var : Type u_1} [DecidableEq Var] [HasFresh Var] {Γ Δ : Env Var} {τ δ : Ty Var} {X : Var} {δ' : Ty Var} {t : Term Var} (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Δ δ δ') : Typing (Context.map_val (fun (x : Binding Var) => x[X:=δ]) Γ ++ Δ) (t[X:=δ]) (τ[X:=δ])

Type substitution within a typing.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.abs_inv {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {τ δ γ' : Ty Var} {t : Term Var} {γ : Ty Var} (der : Typing Γ (Term.abs γ' t) τ) (sub : Sub Γ τ (γ.arrow δ)) : Sub Γ γ γ' ∧ ∃ (δ' : Ty Var) (L : Finset Var), ∀ x ∉ L, Typing (⟨x, Binding.ty γ'⟩ :: Γ) (t.open_tm (Term.fvar x)) δ' ∧ Sub Γ δ' δ

Invert the typing of an abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.tabs_inv {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {τ δ : Ty Var} [HasFresh Var] {γ' : Ty Var} {t : Term Var} {γ : Ty Var} (der : Typing Γ (Term.tabs γ' t) τ) (sub : Sub Γ τ (γ.all δ)) : Sub Γ γ γ' ∧ ∃ (δ' : Ty Var) (L : Finset Var), ∀ X ∉ L, Typing (⟨X, Binding.sub γ⟩ :: Γ) (t.open_ty (Ty.fvar X)) (δ'.open' (Ty.fvar X)) ∧ Sub (⟨X, Binding.sub γ⟩ :: Γ) (δ'.open' (Ty.fvar X)) (δ.open' (Ty.fvar X))

Invert the typing of a type abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.inl_inv {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {τ δ : Ty Var} {t : Term Var} {γ : Ty Var} (der : Typing Γ t.inl τ) (sub : Sub Γ τ (γ.sum δ)) : ∃ (γ' : Ty Var), Typing Γ t γ' ∧ Sub Γ γ' γ

Invert the typing of a left case.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.inr_inv {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {δ : Ty Var} {t : Term Var} {T γ : Ty Var} (der : Typing Γ t.inr T) (sub : Sub Γ T (γ.sum δ)) : ∃ (δ' : Ty Var), Typing Γ t δ' ∧ Sub Γ δ' δ

Invert the typing of a right case.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.canonical_form_abs {Var : Type u_1} [DecidableEq Var] {σ τ : Ty Var} {t : Term Var} (val : t.Value) (der : Typing [] t (σ.arrow τ)) : ∃ (δ : Ty Var) (t' : Term Var), t = Term.abs δ t'

A value that types as a function is an abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.canonical_form_tabs {Var : Type u_1} [DecidableEq Var] {σ τ : Ty Var} {t : Term Var} (val : t.Value) (der : Typing [] t (σ.all τ)) : ∃ (δ : Ty Var) (t' : Term Var), t = Term.tabs δ t'

A value that types as a quantifier is a type abstraction.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.canonical_form_sum {Var : Type u_1} [DecidableEq Var] {σ τ : Ty Var} {t : Term Var} (val : t.Value) (der : Typing [] t (σ.sum τ)) : ∃ (t' : Term Var), t = t'.inl ∨ t = t'.inr

A value that types as a sum is a left or right case.