Index codings

An IndexCoding ι κ is an injection encode : ι → κ together with a decoder that is a left inverse on encoded values (mirroring Encodable, the codomain-ℕ special case). Codings are how an ι-indexed infinitary connective is expressed at a larger carrier κ, and how infinitary formulas are transported between carriers (Infinitary/Reindex.lean).

Main definitions

• IndexCoding.id, IndexCoding.trans: identity and forward composition, with id_trans, trans_id, trans_assoc.
• IndexCoding.sumInl, IndexCoding.sumInr: the canonical codings into a sum.
• IndexCoding.ofEncodable / ofEncodableWith: the coding of an encodable type into ℕ, by instance search or from an explicitly given Encodable value; no choice is involved.
• IndexCoding.ofEquiv: the coding induced by an equivalence; its decode is total.
• IndexCoding.pad: total extension of an ι-indexed family to a κ-indexed one, sending undecodable indices to a default. The laws pad_trans and comp_pad centralize all decoder analysis; consumers chain and commute pads through them.
• IndexCoding.toEmbedding: the underlying embedding (decode_encode forces injectivity).

structure FirstOrder.IndexCoding (ι : Type uι) (κ : Type uκ) : Type (max uι uκ)

A coding of the index type ι into κ: an injection encode together with a decoder that is a left inverse on encoded values. Values outside the range of encode may decode to none or to duplicate source branches; the padding semantics only ever relies on decode_encode.

• encode : ι → κ

  The injection.

• decode : κ → Option ι

  The decoder, a left inverse on encoded values.

• decode_encode (i : ι) : self.decode (self.encode i) = some i

  Decoding recovers every encoded index.

theorem FirstOrder.IndexCoding.ext {ι : Type uι} {κ : Type uκ} {c₁ c₂ : IndexCoding ι κ} (he : c₁.encode = c₂.encode) (hd : c₁.decode = c₂.decode) : c₁ = c₂

Two codings with the same encode and decode are equal; the coherence proof is irrelevant.

theorem FirstOrder.IndexCoding.ext_iff {ι : Type uι} {κ : Type uκ} {c₁ c₂ : IndexCoding ι κ} : c₁ = c₂ ↔ c₁.encode = c₂.encode ∧ c₁.decode = c₂.decode

theorem FirstOrder.IndexCoding.encode_injective {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) : Function.Injective c.encode

encode is injective: decode_encode already provides a retraction.

def FirstOrder.IndexCoding.id (ι : Type uι) : IndexCoding ι ι

The identity coding.

Equations

• FirstOrder.IndexCoding.id ι = { encode := fun (i : ι) => i, decode := some, decode_encode := ⋯ }

def FirstOrder.IndexCoding.trans {ι : Type uι} {κ : Type uκ} {μ : Type uμ} (c₁ : IndexCoding ι κ) (c₂ : IndexCoding κ μ) : IndexCoding ι μ

Forward composition of codings, in the Equiv.trans argument order: first c₁ : ι → κ, then c₂ : κ → μ.

Equations

• c₁.trans c₂ = { encode := c₂.encode ∘ c₁.encode, decode := fun (m : μ) => (c₂.decode m).bind c₁.decode, decode_encode := ⋯ }

def FirstOrder.IndexCoding.sumInl (ι : Type uι) (κ : Type uκ) : IndexCoding ι (ι ⊕ κ)

The canonical coding of the left summand into a sum.

Equations

• FirstOrder.IndexCoding.sumInl ι κ = { encode := Sum.inl, decode := Sum.getLeft?, decode_encode := ⋯ }

def FirstOrder.IndexCoding.sumInr (ι : Type uι) (κ : Type uκ) : IndexCoding κ (ι ⊕ κ)

The canonical coding of the right summand into a sum.

Equations

• FirstOrder.IndexCoding.sumInr ι κ = { encode := Sum.inr, decode := Sum.getRight?, decode_encode := ⋯ }

def FirstOrder.IndexCoding.ofEncodableWith {ι : Type uι} (e : Encodable ι) : IndexCoding ι ℕ

Explicit-data variant of ofEncodable: build the coding from a given encoding value rather than by instance search. Code that stores a particular Encodable as data (e.g. a coded-family presentation that must not consult ambient instances) uses this, so the compiler enforces that the resulting syntax depends on the stored encoding.

Equations

• FirstOrder.IndexCoding.ofEncodableWith e = { encode := Encodable.encode, decode := Encodable.decode, decode_encode := ⋯ }

def FirstOrder.IndexCoding.pad {ι : Type uι} {κ : Type uκ} {β : Sort u_1} (c : IndexCoding ι κ) (default : β) (f : ι → β) : κ → β

Total extension of a family along a coding: decoded indices select a branch, undecodable ones get the default.

Equations

• c.pad default f k = (c.decode k).elim default f

@[simp]

theorem FirstOrder.IndexCoding.pad_encode {ι : Type uι} {κ : Type uκ} {β : Sort u_1} (c : IndexCoding ι κ) (default : β) (f : ι → β) (i : ι) : c.pad default f (c.encode i) = f i

theorem FirstOrder.IndexCoding.pad_of_decode_none {ι : Type uι} {κ : Type uκ} {β : Sort u_1} (c : IndexCoding ι κ) {default : β} {f : ι → β} {k : κ} (h : c.decode k = none) : c.pad default f k = default

theorem FirstOrder.IndexCoding.pad_of_decode_some {ι : Type uι} {κ : Type uκ} {β : Sort u_1} (c : IndexCoding ι κ) {default : β} {f : ι → β} {k : κ} {i : ι} (h : c.decode k = some i) : c.pad default f k = f i