λ-calculus

The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax. This file defines the well-formedness condition for types and contexts.

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

A type is well-formed when it is locally closed and all free variables appear in a context.

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

inductive Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf {Var : Type u_1} [DecidableEq Var] : Env Var → Prop

An environment is well-formed if it binds each variable exactly once to a well-formed type.

• empty {Var : Type u_1} [DecidableEq Var] : Wf []
• sub {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {X : Var} {τ : Ty Var} : Γ.Wf → Ty.Wf Γ τ → X ∉ Context.dom Γ → Wf (⟨X, Binding.sub τ⟩ :: Γ)
• ty {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {x : Var} {τ : Ty Var} : Γ.Wf → Ty.Wf Γ τ → x ∉ Context.dom Γ → Wf (⟨x, Binding.ty τ⟩ :: Γ)

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.to_ok {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} (wf : Γ.Wf) : Γ✓

A well-formed context contains no duplicate keys.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.lc {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ : Ty Var} (wf : Wf Γ σ) : σ.LC

A well-formed type is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.perm_env {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {σ : Ty Var} (wf : Wf Γ σ) (perm : List.Perm Γ Δ) (ok_Γ : Γ✓) (ok_Δ : Δ✓) : Wf Δ σ

A type remains well-formed under context permutation.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.weaken {Var : Type u_1} [DecidableEq Var] {Γ Δ Θ : Env Var} {σ : Ty Var} (wf_ΓΘ : Wf (Γ ++ Θ) σ) (ok_ΓΔΘ : (Γ ++ Δ ++ Θ)✓) : Wf (Γ ++ Δ ++ Θ) σ

A type remains well-formed under context weakening (in the middle).

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

A type remains well-formed under context weakening (at the front).

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.weaken_cons {Var : Type u_1} [DecidableEq Var] {Δ : Env Var} {σ : Ty Var} {X : Var} {b : Binding Var} (wf : Wf Δ σ) (ok : (⟨X, b⟩ :: Δ)✓) : Wf (⟨X, b⟩ :: Δ) σ

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

A type remains well-formed under context narrowing.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.narrow_cons {Var : Type u_1} [DecidableEq Var] {Δ : Env Var} {σ τ τ' : Ty Var} {X : Var} (wf : Wf (⟨X, Binding.sub τ⟩ :: Δ) σ) (ok : (⟨X, Binding.sub τ'⟩ :: Δ)✓) : Wf (⟨X, Binding.sub τ'⟩ :: Δ) σ

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

A type remains well-formed under context strengthening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.map_subst {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {σ τ τ' : Ty Var} [HasFresh Var] {X : Var} (wf_σ : Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ) σ) (wf_τ' : Wf Δ τ') (ok : (Context.map_val (fun (x : Binding Var) => x[X:=τ']) Γ ++ Δ)✓) : Wf (Context.map_val (fun (x : Binding Var) => x[X:=τ']) Γ ++ Δ) (σ[X:=τ'])

A type remains well-formed under context substitution (of a well-formed type).

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.open_lc {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ τ δ : Ty Var} [HasFresh Var] (ok_Γ : Γ✓) (wf_all : Wf Γ (σ.all τ)) (wf_δ : Wf Γ δ) : Wf Γ (τ.open' δ)

A type remains well-formed under opening (to a well-formed type).

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.of_bind_ty {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ : Ty Var} {X : Var} (wf : Γ.Wf) (bind : Binding.ty σ ∈ List.dlookup X Γ) : Wf Γ σ

A type bound in a context is well formed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.of_env_ty {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ : Ty Var} {X : Var} (wf : Env.Wf (⟨X, Binding.ty σ⟩ :: Γ)) : Wf Γ σ

A type at the head of a well-formed context is well-formed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.of_env_sub {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} {σ : Ty Var} {X : Var} (wf : Env.Wf (⟨X, Binding.sub σ⟩ :: Γ)) : Wf Γ σ

A subtype at the head of a well-formed context is well-formed.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Ty.Wf.nmem_fv {Var : Type u_1} [DecidableEq Var] {Γ : Env Var} [HasFresh Var] {X : Var} {σ : Ty Var} (wf : Wf Γ σ) (nmem : X ∉ Context.dom Γ) : X ∉ σ.fv

A variable not appearing in a context does not appear in its well-formed types.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.narrow {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {τ τ' : Ty Var} {X : Var} (wf_env : (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ).Wf) (wf_τ' : Ty.Wf Δ τ') : (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ).Wf

A context remains well-formed under narrowing (of a well-formed subtype).

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

A context remains well-formed under strengthening.

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst {Var : Type u_1} [DecidableEq Var] {Γ Δ : Env Var} {τ τ' : Ty Var} [HasFresh Var] {X : Var} (wf_env : (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ).Wf) (wf_τ' : Ty.Wf Δ τ') : Wf (Context.map_val (fun (x : Binding Var) => x[X:=τ']) Γ ++ Δ)

A context remains well-formed under substitution (of a well-formed type).

theorem Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.map_subst_nmem {Var : Type u_1} [DecidableEq Var] [HasFresh Var] (Γ : Env Var) (X : Var) (σ : Ty Var) (wf : Γ.Wf) (nmem : X ∉ Context.dom Γ) : Γ = Context.map_val (fun (x : Binding Var) => x[X:=σ]) Γ

A well-formed context is unchaged by substituting for a free key.