class TyDenote (β : Type) : Type 1

Typeclass for a baseType which is a Gödel code of Lean types.

Intuitively, each b : β represents a Lean Type, but using β instead of Type directly avoids a universe bump

• toType : β → Type

instance instTyDenoteUnit : TyDenote Unit

Equations

• instTyDenoteUnit = { toType := fun (x : Unit) => Unit }

def Ctxt (Ty : Type) : Type

Equations

• Ctxt Ty = List Ty

def Ctxt.empty {Ty : Type} : Ctxt Ty

Equations

• Ctxt.empty = []

instance Ctxt.instEmptyCollection {Ty : Type} : EmptyCollection (Ctxt Ty)

Equations

• Ctxt.instEmptyCollection = { emptyCollection := Ctxt.empty }

instance Ctxt.instInhabited {Ty : Type} : Inhabited (Ctxt Ty)

Equations

• Ctxt.instInhabited = { default := Ctxt.empty }

theorem Ctxt.empty_eq {Ty : Type} : ∅ = []

@[match_pattern]

def Ctxt.snoc {Ty : Type} : Ctxt Ty → Ty → Ctxt Ty

Equations

• tl.snoc hd = hd :: tl

def Ctxt.ofList {Ty : Type} : List Ty → Ctxt Ty

Turn a list of types into a context

Equations

• ↑Γ = Γ

def Ctxt.get? {Ty : Type} : Ctxt Ty → ℕ → Option Ty

Equations

• Ctxt.get? = List.get?

def Ctxt.map {Ty₁ : Type} {Ty₂ : Type} (f : Ty₁ → Ty₂) : Ctxt Ty₁ → Ctxt Ty₂

Map a function from one type universe to another over a context

Equations

• Ctxt.map f = List.map f

@[simp]

theorem Ctxt.map_nil {Ty : Type} {Ty' : Type} (f : Ty → Ty') : Ctxt.map f ∅ = ∅

@[simp]

theorem Ctxt.map_cons {Ty : Type} {Ty' : Type} (Γ : Ctxt Ty) (t : Ty) (f : Ty → Ty') : Ctxt.map f (t :: Γ) = f t :: Ctxt.map f Γ

theorem Ctxt.map_snoc {Ty : Type} {a : Ty} : ∀ {Ty_1 : Type} {f : Ty → Ty_1} (Γ : Ctxt Ty), Ctxt.map f (Γ.snoc a) = (Ctxt.map f Γ).snoc (f a)

instance Ctxt.instFunctor : Functor Ctxt

Equations

• Ctxt.instFunctor = { map := fun {α β : Type} => Ctxt.map, mapConst := fun {α β : Type} => Ctxt.map ∘ Function.const β }

instance Ctxt.instLawfulFunctor : LawfulFunctor Ctxt

Equations

• Ctxt.instLawfulFunctor = ⋯

def Ctxt.recOn {Ty : Type} {motive : Ctxt Ty → Sort u_1} (nil : motive Ctxt.empty) (snoc : (Γ : Ctxt Ty) → (t : Ty) → motive Γ → motive (Γ.snoc t)) (Γ : Ctxt Ty) : motive Γ

Recursion principle for contexts in terms of Ctxt.nil and Ctxt.snoc

Equations

• Ctxt.recOn nil snoc [] = nil
• Ctxt.recOn nil snoc (ty :: tys) = snoc tys ty (Ctxt.recOn nil snoc tys)

def Ctxt.Var {Ty : Type} (Γ : Ctxt Ty) (t : Ty) : Type

Equations

• Γ.Var t = { i : ℕ // Γ.get? i = some t }

def Ctxt.Var.mk {Ty : Type} (Γ : Ctxt Ty) (t : Ty) (i : ℕ) (hi : Γ.get? i = some t) : Γ.Var t

constructor for Var.

Equations

• Ctxt.Var.mk Γ t i hi = ⟨i, hi⟩

instance Ctxt.Var.instDecidableEq : {Ty : Type} → {Γ : Ctxt Ty} → {t : Ty} → DecidableEq (Γ.Var t)

Equations

• Ctxt.Var.instDecidableEq = id inferInstance

@[match_pattern]

def Ctxt.Var.last {Ty : Type} (Γ : Ctxt Ty) (t : Ty) : (Γ.snoc t).Var t

Equations

• Ctxt.Var.last Γ t = ⟨0, ⋯⟩

def Ctxt.Var.emptyElim {Ty : Type} {α : Sort u_1} {t : Ty} : Ctxt.Var [] t → α

Equations

• Ctxt.Var.emptyElim ⟨val, h⟩ = ⋯.elim

def Ctxt.Var.toSnoc {Ty : Type} {Γ : Ctxt Ty} {t : Ty} {t' : Ty} (var : Γ.Var t) : (Γ.snoc t').Var t

Take a variable in a context Γ and get the corresponding variable in context Γ.snoc t. This is marked as a coercion.

Equations

• ↑var = ⟨↑var + 1, ⋯⟩

@[simp]

theorem Ctxt.Var.zero_eq_last {Ty : Type} {Γ : Ctxt Ty} {t : Ty} (h : (Γ.snoc t).get? 0 = some t) : ⟨0, h⟩ = Ctxt.Var.last Γ t

@[simp]

theorem Ctxt.Var.succ_eq_toSnoc {Ty : Type} {t' : Ty} {Γ : Ctxt Ty} {t : Ty} {w : ℕ} (h : (Γ.snoc t).get? (w + 1) = some t') : ⟨w + 1, h⟩ = ↑⟨w, h⟩

def Ctxt.Var.toMap : {Ty : Type} → {Γ : Ctxt Ty} → {t : Ty} → {Ty_1 : Type} → {f : Ty → Ty_1} → Γ.Var t → (Ctxt.map f Γ).Var (f t)

Transport a variable from Γ to any mapped context Γ.map f

Equations

• Ctxt.Var.toMap ⟨i, h⟩ = ⟨i, ⋯⟩

def Ctxt.Var.cast {Op : Type} {ty₁ : Op} {ty₂ : Op} {Γ : Ctxt Op} (h_eq : ty₁ = ty₂) : Γ.Var ty₁ → Γ.Var ty₂

Equations

• Ctxt.Var.cast h_eq ⟨i, h⟩ = ⟨i, ⋯⟩

def Ctxt.Var.castCtxt {Op : Type} {Δ : Ctxt Op} {ty : Op} {Γ : Ctxt Op} (h_eq : Γ = Δ) : Γ.Var ty → Δ.Var ty

Equations

• Ctxt.Var.castCtxt h_eq ⟨i, h⟩ = ⟨i, ⋯⟩

@[simp]

theorem Ctxt.Var.cast_rfl : ∀ {Ty : Type} {Γ : Ctxt Ty} {t : Ty} (v : Γ.Var t) (h : t = t), Ctxt.Var.cast h v = v

@[simp]

theorem Ctxt.Var.castCtxt_rfl : ∀ {Ty : Type} {Γ : Ctxt Ty} {t : Ty} (v : Γ.Var t) (h : Γ = Γ), Ctxt.Var.castCtxt h v = v

@[simp]

theorem Ctxt.Var.castCtxt_castCtxt : ∀ {Ty : Type} {Γ : Ctxt Ty} {t : Ty} {Δ Ξ : Ctxt Ty} (v : Γ.Var t) (h₁ : Γ = Δ) (h₂ : Δ = Ξ), Ctxt.Var.castCtxt h₂ (Ctxt.Var.castCtxt h₁ v) = Ctxt.Var.castCtxt ⋯ v

@[simp]

theorem Ctxt.Var.toMap_last {Ty : Type} : ∀ {Ty_1 : Type} {f : Ty → Ty_1} {Γ : Ctxt Ty} {t : Ty}, (Ctxt.Var.last Γ t).toMap = Ctxt.Var.last (Ctxt.map f Γ) (f t)

@[simp]

theorem Ctxt.Var.toSnoc_toMap {Ty : Type} {t' : Ty} {Ty₂ : Type} {Γ : Ctxt Ty} {t : Ty} {var : Γ.Var t'} {f : Ty → Ty₂} : (↑var).toMap = ↑var.toMap

def Ctxt.Var.casesOn {Ty : Type} {motive : (Γ : Ctxt Ty) → (t t' : Ty) → (Γ.snoc t').Var t → Sort u_1} {Γ : Ctxt Ty} {t : Ty} {t' : Ty} (v : (Γ.snoc t').Var t) (toSnoc : {t t' : Ty} → {Γ : Ctxt Ty} → (v : Γ.Var t) → motive Γ t t' ↑v) (last : {Γ : Ctxt Ty} → {t : Ty} → motive Γ t t (Ctxt.Var.last Γ t)) : motive Γ t t' v

This is an induction principle that case splits on whether or not a variable is the last variable in a context.

Equations

• Ctxt.Var.casesOn ⟨0, h⟩ toSnoc last = cast ⋯ last
• Ctxt.Var.casesOn ⟨i.succ, h⟩ toSnoc last = toSnoc ⟨i, ⋯⟩

@[simp]

def Ctxt.Var.casesOn_last {Ty : Type} {motive : (Γ : Ctxt Ty) → (t t' : Ty) → (Γ.snoc t').Var t → Sort u_1} {Γ : Ctxt Ty} {t : Ty} (base : {t t' : Ty} → {Γ : Ctxt Ty} → (v : Γ.Var t) → motive Γ t t' ↑v) (last : {Γ : Ctxt Ty} → {t : Ty} → motive Γ t t (Ctxt.Var.last Γ t)) : (Ctxt.Var.casesOn (Ctxt.Var.last Γ t) (fun {t t' : Ty} {Γ : Ctxt Ty} => base) fun {Γ : Ctxt Ty} {t : Ty} => last) = last

Ctxt.Var.casesOn behaves in the expected way when applied to the last variable

Equations

• ⋯ = ⋯

@[simp]

def Ctxt.Var.casesOn_toSnoc {Ty : Type} {motive : (Γ : Ctxt Ty) → (t t' : Ty) → (Γ.snoc t').Var t → Sort u_1} {Γ : Ctxt Ty} {t : Ty} {t' : Ty} (v : Γ.Var t) (base : {t t' : Ty} → {Γ : Ctxt Ty} → (v : Γ.Var t) → motive Γ t t' ↑v) (last : {Γ : Ctxt Ty} → {t : Ty} → motive Γ t t (Ctxt.Var.last Γ t)) : (Ctxt.Var.casesOn (↑v) (fun {t t' : Ty} {Γ : Ctxt Ty} => base) fun {Γ : Ctxt Ty} {t : Ty} => last) = base v

Ctxt.Var.casesOn behaves in the expected way when applied to a previous variable, that is not the last one.

Equations

• ⋯ = ⋯

theorem Ctxt.toSnoc_injective {Ty : Type} {Γ : Ctxt Ty} {t : Ty} {t' : Ty} : Function.Injective Ctxt.Var.toSnoc

@[reducible, inline]

abbrev Ctxt.Hom {Ty : Type} (Γ : Ctxt Ty) (Γ' : Ctxt Ty) : Type

Equations

• Γ.Hom Γ' = (⦃t : Ty⦄ → Γ.Var t → Γ'.Var t)

@[reducible, inline]

abbrev Ctxt.Hom.id {Ty : Type} {Γ : Ctxt Ty} : Γ.Hom Γ

Equations

• Ctxt.Hom.id v = v

def Ctxt.Hom.comp {Ty : Type} {Γ : Ctxt Ty} {Γ' : Ctxt Ty} {Γ'' : Ctxt Ty} (self : Γ.Hom Γ') (rangeMap : Γ'.Hom Γ'') : Γ.Hom Γ''

f.comp g := g(f(x))

Equations

• self.comp rangeMap v = rangeMap (self v)

def Ctxt.Hom.with {Ty : Type} [DecidableEq Ty] {Γ₁ : Ctxt Ty} {Γ₂ : Ctxt Ty} (f : Γ₁.Hom Γ₂) {t : Ty} (v₁ : Γ₁.Var t) (v₂ : Γ₂.Var t) : Γ₁.Hom Γ₂

map.with v₁ v₂ adjusts a single variable of a Context map, so that in the resulting map

• v₁ now maps to v₂
• all other variables v still map to map v as in the original map

Equations

• f.with v₁ v₂ w = if h : ∃ (ty_eq : t = t'), ⋯ ▸ w = v₁ then Ctxt.Var.cast ⋯ v₂ else f w

def Ctxt.Hom.snocMap {Ty : Type} {Γ : Ctxt Ty} {Γ' : Ctxt Ty} (f : Γ.Hom Γ') {t : Ty} : (Γ.snoc t).Hom (Γ'.snoc t)

Equations

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

@[reducible, inline]

abbrev Ctxt.Hom.snocRight {Ty : Type} {Γ : Ctxt Ty} {Γ' : Ctxt Ty} (f : Γ.Hom Γ') {t : Ty} : Γ.Hom (Γ'.snoc t)

Equations

• f.snocRight v = ↑(f v)

def Ctxt.Hom.unSnoc : {Ty : Type} → {Δ Γ : Ctxt Ty} → {t : Ty} → (Γ.snoc t).Hom Δ → Γ.Hom Δ

Remove a type from the domain (left) context

Equations

• f.unSnoc v = f ↑v

@[simp]

theorem Ctxt.Hom.unSnoc_apply {Ty : Type} {t : Ty} {Δ : Ctxt Ty} {u : Ty} {Γ : Ctxt Ty} (f : (Γ.snoc t).Hom Δ) (v : Γ.Var u) : f.unSnoc v = f ↑v

instance Ctxt.instCoeVarSnoc {Ty : Type} {t : Ty} {t' : Ty} {Γ : Ctxt Ty} : Coe (Γ.Var t) ((Γ.snoc t').Var t)

Equations

• Ctxt.instCoeVarSnoc = { coe := Ctxt.Var.toSnoc }

def Ctxt.Valuation {Ty : Type} [TyDenote Ty] (Γ : Ctxt Ty) : Type

A valuation for a context. Provide a way to evaluate every variable in a context.

Equations

• Γ.Valuation = (⦃t : Ty⦄ → Γ.Var t → ⟦t⟧)

def Ctxt.Valuation.eval {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} (VAL : Γ.Valuation) ⦃t : Ty⦄ (v : Γ.Var t) : ⟦t⟧

A valuation for a context. Provide a way to evaluate every variable in a context.

Equations

• VAL.eval v = VAL v

def Ctxt.Valuation.nil {Ty : Type} [TyDenote Ty] : Ctxt.Valuation []

Make a valuation for the empty context.

Equations

• Ctxt.Valuation.nil v = v.emptyElim

instance Ctxt.instInhabitedValuationNil {Ty : Type} [TyDenote Ty] : Inhabited (Ctxt.Valuation [])

Equations

• Ctxt.instInhabitedValuationNil = { default := Ctxt.Valuation.nil }

def Ctxt.Valuation.snoc {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : ⟦t⟧) : (Γ.snoc t).Valuation

Make a valuation for Γ.snoc t from a valuation for Γ and an element of t.toType.

Equations

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

theorem Ctxt.Valuation.snoc_eq {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : ⟦t⟧) : (s::ᵥx) = fun (t_1 : Ty) (var : (Γ.snoc t).Var t_1) => match var with | ⟨0, hvar⟩ => ⋯ ▸ x | ⟨i.succ, hvar⟩ => s ⟨i, hvar⟩

Show the equivalence between the definition in terms of snoc and snoc'.

@[simp]

theorem Ctxt.Valuation.snoc_last {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {t : Ty} (s : Γ.Valuation) (x : ⟦t⟧) : (s::ᵥx) (Ctxt.Var.last Γ t) = x

@[simp]

theorem Ctxt.Valuation.snoc_zero {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {ty : Ty} (s : Γ.Valuation) (x : ⟦ty⟧) (h : (Γ.snoc ty).get? 0 = some ty) : (s::ᵥx) ⟨0, h⟩ = x

@[simp]

theorem Ctxt.Valuation.snoc_toSnoc {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {t : Ty} {t' : Ty} (s : Γ.Valuation) (x : ⟦t⟧) (v : Γ.Var t') : (s::ᵥx) ↑v = s v

Helper to simplify context manipulation with toSnoc and variable access.

@[simp]

theorem Ctxt.Valuation.snoc_eval {Ty : Type} [TyDenote Ty] {n : ℕ} {var_val : Ty} {ty : Ty} (Γ : Ctxt Ty) (V : Γ.Valuation) (v : ⟦ty⟧) (hvar : (Γ.snoc ty).get? (n + 1) = some var_val) : (V::ᵥv) ⟨n + 1, hvar⟩ = V ⟨n, hvar⟩

(ctx.snoc v₁) ⟨n+1, _⟩ = ctx ⟨n, _⟩

theorem Ctxt.Valuation.eq_nil {Ty : Type} [TyDenote Ty] (V : Ctxt.empty.Valuation) : V = Ctxt.Valuation.nil

There is only one distinct valuation for the empty context

@[simp]

theorem Ctxt.Valuation.snoc_toSnoc_last {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {t : Ty} (V : (Γ.snoc t).Valuation) : ((fun (t_1 : Ty) (v' : Γ.Var t_1) => V ↑v')::ᵥV (Ctxt.Var.last Γ t)) = V

def Ctxt.Valuation.singleton {Ty : Type} [TyDenote Ty] {t : Ty} (v : ⟦t⟧) : Ctxt.Valuation [t]

Make a a valuation for a singleton value

Equations

• Ctxt.Valuation.singleton v = (Ctxt.Valuation.nil::ᵥv)

def Ctxt.Valuation.ofHVector {Ty : Type} [TyDenote Ty] {types : List Ty} : HVector TyDenote.toType types → (↑types).Valuation

Build valuation from a vector of values of types types.

Equations

• Ctxt.Valuation.ofHVector HVector.nil = default
• Ctxt.Valuation.ofHVector (x_1::ₕxs) = (Ctxt.Valuation.ofHVector xs::ᵥx_1)

def Ctxt.Valuation.ofPair {Ty : Type} [TyDenote Ty] {t₁ : Ty} {t₂ : Ty} (v₁ : ⟦t₁⟧) (v₂ : ⟦t₂⟧) : (↑[t₁, t₂]).Valuation

Build valuation from a vector of values of types types.

Equations

• Ctxt.Valuation.ofPair v₁ v₂ = Ctxt.Valuation.ofHVector (v₁::ₕ(v₂::ₕHVector.nil))

@[simp]

theorem Ctxt.Valuation.ofPair_fst {Ty : Type} [TyDenote Ty] {t₁ : Ty} {t₂ : Ty} (v₁ : ⟦t₁⟧) (v₂ : ⟦t₂⟧) : Ctxt.Valuation.ofPair v₁ v₂ ⟨0, ⋯⟩ = v₁

@[simp]

theorem Ctxt.Valuation.ofPair_snd {Ty : Type} [TyDenote Ty] {t₁ : Ty} {t₂ : Ty} (v₁ : ⟦t₁⟧) (v₂ : ⟦t₂⟧) : Ctxt.Valuation.ofPair v₁ v₂ ⟨1, ⋯⟩ = v₂

def Ctxt.Valuation.comap {Ty : Type} [TyDenote Ty] {Γi : Ctxt Ty} {Γo : Ctxt Ty} (Γiv : Γi.Valuation) (hom : Γo.Hom Γi) : Γo.Valuation

transport/pullback a valuation along a context homomorphism.

Equations

• Γiv.comap hom vo = Γiv (hom vo)

@[simp]

theorem Ctxt.Valuation.comap_snoc_snocMap {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {Γ_out : Ctxt Ty} (V : Γ_out.Valuation) {t : Ty} (x : ⟦t⟧) (map : Γ.Hom Γ_out) : (V::ᵥx).comap map.snocMap = (V.comap map::ᵥx)

@[simp]

theorem Ctxt.Valuation.comap_id {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} (Γv : Γ.Valuation) : Γv.comap Ctxt.Hom.id = Γv

@[simp]

theorem Ctxt.Valuation.comap_snoc_snocRight {Ty : Type} [TyDenote Ty] : ∀ {a : Ty} {x : ⟦a⟧} {Γ Δ : Ctxt Ty} (Γv : Γ.Valuation) (f : Δ.Hom Γ), (Γv::ᵥx).comap f.snocRight = Γv.comap f

def Ctxt.Valuation.reassignVar {Ty : Type} [TyDenote Ty] [DecidableEq Ty] {t : Ty} {Γ : Ctxt Ty} (V : Γ.Valuation) (var : Γ.Var t) (val : ⟦t⟧) : Γ.Valuation

Reassign the variable var to value val in context ctxt

Equations

• V.reassignVar var val vneedle = if h : ∃ (h : t = tneedle), ⋯ ▸ vneedle = var then ⋯ ▸ val else V vneedle

@[simp]

theorem Ctxt.Valuation.comap_with {Ty : Type} [TyDenote Ty] {ty : Ty} [DecidableEq Ty] {Γ : Ctxt Ty} {Δ : Ctxt Ty} {Γv : Γ.Valuation} {map : Δ.Hom Γ} {v : Δ.Var ty} {w : Γ.Var ty} : Γv.comap (map.with v w) = (Γv.comap map).reassignVar v (Γv w)

def Ctxt.Valuation.recOn {Ty : Type} [TyDenote Ty] {motive : {Γ : Ctxt Ty} → Γ.Valuation → Sort u_1} (nil : motive Ctxt.Valuation.nil) (snoc : {Γ : Ctxt Ty} → {t : Ty} → (V : Γ.Valuation) → (v : ⟦t⟧) → motive V → motive (V::ᵥv)) {Γ : Ctxt Ty} (V : Γ.Valuation) : motive V

Recursion principle for valuations in terms of Valuation.nil and Valuation.snoc

Equations

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

def Ctxt.Valuation.cast {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} {Δ : Ctxt Ty} (h : Γ = Δ) (V : Γ.Valuation) : Δ.Valuation

Equations

• Ctxt.Valuation.cast h V v = V (Ctxt.Var.castCtxt ⋯ v)

@[simp]

theorem Ctxt.Valuation.cast_rfl {Ty : Type} [TyDenote Ty] {Γ : Ctxt Ty} (h : Γ = Γ) (V : Γ.Valuation) : Ctxt.Valuation.cast h V = V

theorem Ctxt.Valuation.reassignVar_eq_of_lookup {Ty : Type} [TyDenote Ty] {t : Ty} [DecidableEq Ty] {Γ : Ctxt Ty} {V : Γ.Valuation} {var : Γ.Var t} : V.reassignVar var (V var) = V

reassigning a variable to the same value that has been looked up is identity.

@[reducible, inline]

abbrev Ctxt.VarSet {Ty : Type} (Γ : Ctxt Ty) : Type

VarSet Γ is the type of sets of variables from context Γ

Equations

• Γ.VarSet = Finset ((t : Ty) × Γ.Var t)

def Ctxt.VarSet.ofVar {Ty : Type} {t : Ty} {Γ : Ctxt Ty} (v : Γ.Var t) : Γ.VarSet

A VarSet with exactly one variable v

Equations

• Ctxt.VarSet.ofVar v = {⟨t, v⟩}

@[simp]

theorem Ctxt.Var.val_last {Ty : Type} {Γ : Ctxt Ty} {t : Ty} : ↑(Ctxt.Var.last Γ t) = 0

@[simp]

theorem Ctxt.Var.val_toSnoc {Ty : Type} {Γ : Ctxt Ty} {t : Ty} {t' : Ty} (v : Γ.Var t) : ↑↑v = ↑v + 1

instance Ctxt.Var.instRepr : {Ty : Type} → {Γ : Ctxt Ty} → {t : Ty} → Repr (Γ.Var t)

Equations

• Ctxt.Var.instRepr = { reprPrec := fun (v : Γ.Var t) (x : ℕ) => Lean.format "%" ++ Lean.format (List.length Γ - ↑v - 1) ++ Lean.format "" }

@[reducible, inline]

abbrev Ctxt.Diff.Valid {Ty : Type} (Γ₁ : Ctxt Ty) (Γ₂ : Ctxt Ty) (d : ℕ) : Prop

Equations

• Ctxt.Diff.Valid Γ₁ Γ₂ d = ∀ {i : ℕ} {t : Ty}, Γ₁.get? i = some t → Γ₂.get? (i + d) = some t

def Ctxt.Diff {Ty : Type} (Γ₁ : Ctxt Ty) (Γ₂ : Ctxt Ty) : Type

If Γ₁ is a prefix of Γ₂, then d : Γ₁.Diff Γ₂ represents the number of elements that Γ₂ has more than Γ₁

Equations

• Γ₁.Diff Γ₂ = { d : ℕ // Ctxt.Diff.Valid Γ₁ Γ₂ d }

def Ctxt.Diff.zero {Ty : Type} (Γ : Ctxt Ty) : Γ.Diff Γ

The difference between any context and itself is 0

Equations

• Ctxt.Diff.zero Γ = ⟨0, ⋯⟩

def Ctxt.Diff.toSnoc : {Ty : Type} → {Γ₁ Γ₂ : Ctxt Ty} → {t : Ty} → Γ₁.Diff Γ₂ → Γ₁.Diff (Γ₂.snoc t)

Adding a new type to the right context corresponds to incrementing the difference by 1

Equations

• d.toSnoc = ⟨↑d + 1, ⋯⟩

def Ctxt.Diff.unSnoc : {Ty : Type} → {Γ₂ Γ₁ : Ctxt Ty} → {t : Ty} → (Γ₁.snoc t).Diff Γ₂ → Γ₁.Diff Γ₂

Removing a type from the left context corresponds to incrementing the difference by 1

Equations

• d.unSnoc = ⟨↑d + 1, ⋯⟩

toMap

def Ctxt.Diff.toMap : {Ty : Type} → {Γ₁ Γ₂ : Ctxt Ty} → {Ty_1 : Type} → {f : Ty → Ty_1} → Γ₁.Diff Γ₂ → (Ctxt.map f Γ₁).Diff (Ctxt.map f Γ₂)

Mapping over contexts does not change their difference

Equations

• ↑d = ⟨↑d, ⋯⟩

append

theorem Ctxt.Diff.append_valid {Ty : Type} {Γ₁ : Ctxt Ty} {Γ₂ : Ctxt Ty} {Γ₃ : Ctxt Ty} {d₁ : ℕ} {d₂ : ℕ} : Ctxt.Diff.Valid Γ₁ Γ₂ d₁ → Ctxt.Diff.Valid Γ₂ Γ₃ d₂ → Ctxt.Diff.Valid Γ₁ Γ₃ (d₁ + d₂)

def Ctxt.Diff.append : {Ty : Type} → {Γ₁ Γ₂ Γ₃ : Ctxt Ty} → Γ₁.Diff Γ₂ → Γ₂.Diff Γ₃ → Γ₁.Diff Γ₃

Addition of the differences of two contexts

Equations

• d₁.append d₂ = ⟨↑d₁ + ↑d₂, ⋯⟩

toHom

def Ctxt.Diff.toHom : {Ty : Type} → {Γ₁ Γ₂ : Ctxt Ty} → Γ₁.Diff Γ₂ → Γ₁.Hom Γ₂

Adding the difference of two contexts to variable indices is a context mapping

Equations

• d.toHom v = ⟨↑v + ↑d, ⋯⟩

theorem Ctxt.Diff.Valid.of_succ {Ty : Type} {t : Ty} {Γ₁ : Ctxt Ty} {Γ₂ : Ctxt Ty} {d : ℕ} (h_valid : Ctxt.Diff.Valid Γ₁ (Γ₂.snoc t) (d + 1)) : Ctxt.Diff.Valid Γ₁ Γ₂ d

theorem Ctxt.Diff.toHom_succ {Ty : Type} {t : Ty} {Γ₁ : Ctxt Ty} {Γ₂ : Ctxt Ty} {d : ℕ} (h : Ctxt.Diff.Valid Γ₁ (Γ₂.snoc t) (d + 1)) : Ctxt.Diff.toHom ⟨d + 1, ⋯⟩ = (Ctxt.Diff.toHom ⟨d, ⋯⟩).snocRight

@[simp]

theorem Ctxt.Diff.toHom_zero {Ty : Type} {Γ : Ctxt Ty} {h : Ctxt.Diff.Valid Γ Γ 0} : Ctxt.Diff.toHom ⟨0, ⋯⟩ = Ctxt.Hom.id

@[simp]

theorem Ctxt.Diff.toHom_unSnoc {Ty : Type} {t : Ty} {Γ₁ : Ctxt Ty} {Γ₂ : Ctxt Ty} (d : (Γ₁.snoc t).Diff Γ₂) : d.unSnoc.toHom = fun (x : Ty) (v : Γ₁.Var x) => d.toHom ↑v

add

def Ctxt.Diff.add : {Ty : Type} → {Γ₁ Γ₂ Γ₃ : Ctxt Ty} → Γ₁.Diff Γ₂ → Γ₂.Diff Γ₃ → Γ₁.Diff Γ₃

Equations

• Ctxt.Diff.add ⟨d₁, h₁⟩ ⟨d₂, h₂⟩ = ⟨d₁ + d₂, ⋯⟩

instance Ctxt.Diff.instHAdd : {Ty : Type} → {Γ₁ Γ₂ Γ₃ : Ctxt Ty} → HAdd (Γ₁.Diff Γ₂) (Γ₂.Diff Γ₃) (Γ₁.Diff Γ₃)

Equations

• Ctxt.Diff.instHAdd = { hAdd := Ctxt.Diff.add }

def Ctxt.Diff.cast : {Ty : Type} → {Γ Γ' Δ Δ' : Ctxt Ty} → Γ = Γ' → Δ = Δ' → Γ.Diff Δ → Γ'.Diff Δ'

Equations

• Ctxt.Diff.cast h₁ h₂ ⟨n, h⟩ = ⟨n, ⋯⟩

structure Ctxt.DerivedCtxt {Ty : Type} (Γ : Ctxt Ty) : Type

Δ : DerivedCtxt Γ means that Δ is a context obtained by adding elements to context Γ. That is, there exists a context difference diff : Γ.Diff Δ.

• ctxt : Ctxt Ty
• diff : Γ.Diff self.ctxt

@[reducible, inline]

abbrev Ctxt.DerivedCtxt.ofCtxt {Ty : Type} (Γ : Ctxt Ty) : Γ.DerivedCtxt

Every context is trivially derived from itself

Equations

• Ctxt.DerivedCtxt.ofCtxt Γ = { ctxt := Γ, diff := Ctxt.Diff.zero Γ }

@[simp]

theorem Ctxt.DerivedCtxt.ofCtxt_empty {Ty : Type} : Ctxt.DerivedCtxt.ofCtxt [] = { ctxt := [], diff := Ctxt.Diff.zero [] }

value of a dervied context from an empty context, is the empty context with a zero diff.

def Ctxt.DerivedCtxt.snoc {Ty : Type} {Γ : Ctxt Ty} : Γ.DerivedCtxt → Ty → Γ.DerivedCtxt

snoc of a derived context applies snoc to the underlying context, and updates the diff

Equations

• { ctxt := ctxt, diff := diff }.snoc x = { ctxt := x :: ctxt, diff := diff.toSnoc }

theorem Ctxt.DerivedCtxt.snoc_ctxt_eq_ctxt_snoc : ∀ {Ty : Type} {Γ : Ctxt Ty} {Γ_1 : Γ.DerivedCtxt} {ty : Ty}, (Γ_1.snoc ty).ctxt = Γ_1.ctxt.snoc ty

instance Ctxt.DerivedCtxt.instCoeHead {Ty : Type} {Γ : Ctxt Ty} : CoeHead Γ.DerivedCtxt (Ctxt Ty)

Equations

• Ctxt.DerivedCtxt.instCoeHead = { coe := fun (x : Γ.DerivedCtxt) => match x with | { ctxt := Γ', diff := diff } => Γ' }

instance Ctxt.DerivedCtxt.instCoeDep {Ty : Type} {Γ : Ctxt Ty} : CoeDep (Ctxt Ty) Γ Γ.DerivedCtxt

Equations

• Ctxt.DerivedCtxt.instCoeDep = { coe := { ctxt := Γ, diff := Ctxt.Diff.zero Γ } }

instance Ctxt.DerivedCtxt.instCoeHeadMatch_1 {Ty : Type} {Γ : Ctxt Ty} {Γ' : Γ.DerivedCtxt} : CoeHead (match Γ' with | { ctxt := Γ', diff := diff } => Γ').DerivedCtxt Γ.DerivedCtxt

Equations

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

instance Ctxt.DerivedCtxt.instCoeVar {Ty : Type} {Γ : Ctxt Ty} {t : Ty} {Γ' : Γ.DerivedCtxt} : Coe (Γ.Var t) ((match Γ' with | { ctxt := Γ', diff := diff } => Γ').Var t)

Equations

• Ctxt.DerivedCtxt.instCoeVar = { coe := fun (v : Γ.Var t) => { ctxt := Γ'_1, diff := diff }.diff.toHom v }

dropUntil

def Ctxt.dropUntil {Ty : Type} {ty : Ty} (Γ : Ctxt Ty) (v : Γ.Var ty) : Ctxt Ty

Γ.dropUntil v is the largest prefix of context Γ that no longer contains variable v

Equations

• Γ.dropUntil v = List.drop (↑v + 1) Γ

@[simp]

theorem Ctxt.dropUntil_last : ∀ {Ty : Type} {Γ : Ctxt Ty} {ty : Ty}, (Γ.snoc ty).dropUntil (Ctxt.Var.last Γ ty) = Γ

@[simp]

theorem Ctxt.dropUntil_toSnoc : ∀ {Ty : Type} {Γ : Ctxt Ty} {ty t : Ty} {v : Γ.Var t}, (Γ.snoc ty).dropUntil ↑v = Γ.dropUntil v

def Ctxt.dropUntilDiff {Ty : Type} {ty : Ty} {Γ : Ctxt Ty} {v : Γ.Var ty} : (Γ.dropUntil v).Diff Γ

The difference between Γ.dropUntil v and Γ is exactly v.val + 1

Equations

• Ctxt.dropUntilDiff = ⟨↑v + 1, ⋯⟩

@[reducible, inline]

abbrev Ctxt.dropUntilHom : {Ty : Type} → {Γ : Ctxt Ty} → {t : Ty} → {v : Γ.Var t} → (Γ.dropUntil v).Hom Γ

Context homomorphism from (Γ.dropUntil v) to Γ, see also dropUntilDiff

Equations

• Ctxt.dropUntilHom = Ctxt.dropUntilDiff.toHom

@[simp]

theorem Ctxt.dropUntilHom_last : ∀ {Ty : Type} {Γ : Ctxt Ty} {ty : Ty}, Ctxt.dropUntilHom = Ctxt.Hom.id.snocRight

@[simp]

theorem Ctxt.dropUntilHom_toSnoc : ∀ {Ty : Type} {Γ : Ctxt Ty} {t t' : Ty} {v : Γ.Var t}, Ctxt.dropUntilHom = Ctxt.dropUntilHom.snocRight