λ-calculus

The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. This file defines the subtyping 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.Sub {Var : Type u_1} [DecidableEq Var] : Env Var → Ty Var → Ty Var → Prop

The subtyping relation.

• top {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ : Ty Var} : Γ.Wf → Ty.Wf Γ σ → Sub Γ σ Ty.top
• refl_tvar {Var : Type u_1} [DecidableEq Var] {X : Var} {Γ : Env Var} : Γ.Wf → Ty.Wf Γ (Ty.fvar X) → Sub Γ (Ty.fvar X) (Ty.fvar X)
• trans_tvar {Var : Type u_1} [DecidableEq Var] {σ : Ty Var} {Γ : Env Var} {σ' : Ty Var} {X : Var} : Binding.sub σ ∈ List.dlookup X Γ → Sub Γ σ σ' → Sub Γ (Ty.fvar X) σ'
• arrow {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ σ' τ' τ : Ty Var} : Sub Γ σ σ' → Sub Γ τ' τ → Sub Γ (σ'.arrow τ') (σ.arrow τ)
• all {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ σ' τ' τ : Ty Var} (L : Finset Var) : Sub Γ σ σ' → (∀ X ∉ L, Sub (⟨X, Binding.sub σ⟩ :: Γ) (τ'.open' (Ty.fvar X)) (τ.open' (Ty.fvar X))) → Sub Γ (σ'.all τ') (σ.all τ)
• sum {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ' σ τ' τ : Ty Var} : Sub Γ σ' σ → Sub Γ τ' τ → Sub Γ (σ'.sum τ') (σ.sum τ)

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.wf {Var : Type u_1} [DecidableEq Var] (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ Ty.Wf Γ σ ∧ Ty.Wf Γ σ'

Subtypes have well-formed contexts and types.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.refl {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ : Ty Var} (wf_Γ : Γ.Wf) (wf_σ : Ty.Wf Γ σ) : Sub Γ σ σ

Subtypes are reflexive when well-formed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.weaken {Var : Type u_1} [DecidableEq Var] {Γ Δ Θ : Env Var} {σ σ' : Ty Var} (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ ++ Δ ++ Θ) σ σ'

Weakening of subtypes.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.weaken_head {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {σ σ' : Ty Var} (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ'

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.narrow_aux {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {σ τ δ : Ty Var} {X : Var} {δ' : Ty Var} (trans : ∀ (Γ : Env Var) (σ τ : Ty Var), Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ) (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ' δ) : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.trans {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ τ δ : Ty Var} : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ

@[instance_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.instTransTy {Var : Type u_1} [DecidableEq Var] (Γ : Env Var) : Trans (Sub Γ) (Sub Γ) (Sub Γ)

Equations

• Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.instTransTy Γ = { trans := ⋯ }

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

Narrowing of subtypes.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.map_subst {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {σ τ δ : Ty Var} [HasFresh Var] {X : Var} {δ' : Ty Var} (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ δ') : Sub (Context.mapVal (fun (x : Binding Var) => x[X := δ]) Γ ++ Δ) σ[X := δ] τ[X := δ]

Subtyping of substitutions.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.strengthen {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {σ τ δ : Ty Var} {X : Var} (sub : Sub (Γ ++ ⟨X, Binding.ty δ⟩ :: Δ) σ τ) : Sub (Γ ++ Δ) σ τ

Strengthening of subtypes.