λ-calculus

Contexts as pairs of free variables and types.

@[reducible, inline]

abbrev LambdaCalculus.LocallyNameless.Context (Var : Type u) (Ty : Type v) : Type (max v u)

A typing context is a list of free variables and corresponding types.

Equations

• LambdaCalculus.LocallyNameless.Context Var Ty = List ((_ : Var) × Ty)

def LambdaCalculus.LocallyNameless.Context.dom {Var : Type u} {Ty : Type v} [DecidableEq Var] : Context Var Ty → Finset Var

The domain of a context is the finite set of free variables it uses.

Equations

• LambdaCalculus.LocallyNameless.Context.dom = List.toFinset ∘ List.keys

@[reducible, inline]

abbrev LambdaCalculus.LocallyNameless.Context.Ok {Var : Type u} {Ty : Type v} : Context Var Ty → Prop

A well-formed context.

Equations

• LambdaCalculus.LocallyNameless.Context.Ok = List.NodupKeys

instance LambdaCalculus.LocallyNameless.Context.instHasWellFormed {Var : Type u} {Ty : Type v} : HasWellFormed (Context Var Ty)

Equations

• LambdaCalculus.LocallyNameless.Context.instHasWellFormed = { wf := LambdaCalculus.LocallyNameless.Context.Ok }

theorem LambdaCalculus.LocallyNameless.Context.dom_perm_mem_iff {Var : Type u} {Ty : Type v} [DecidableEq Var] {Γ Δ : Context Var Ty} (h : List.Perm Γ Δ) {x : Var} : x ∈ Γ.dom ↔ x ∈ Δ.dom

Context membership is preserved on permuting a context.

theorem LambdaCalculus.LocallyNameless.Context.wf_perm {Var : Type u} {Ty : Type v} {Γ Δ : Context Var Ty} (h : List.Perm Γ Δ) : Γ✓ → Δ✓

Context well-formedness is preserved on permuting a context.

theorem LambdaCalculus.LocallyNameless.Context.wf_strengthen {Var : Type u} {Ty : Type v} {Γ Δ : Context Var Ty} {x : Var} {σ : Ty} (ok : (Δ ++ ⟨x, σ⟩ :: Γ)✓) : (Δ ++ Γ)✓

Context well-formedness is preserved on removing an element.