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.toEmbedding {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) : ι ↪ κ

The underlying embedding of a coding.

Equations

• c.toEmbedding = { toFun := c.encode, inj' := ⋯ }

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 := ⋯ }

@[simp]

theorem FirstOrder.IndexCoding.id_trans {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) : (IndexCoding.id ι).trans c = c

@[simp]

theorem FirstOrder.IndexCoding.trans_id {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) : c.trans (IndexCoding.id κ) = c

theorem FirstOrder.IndexCoding.trans_assoc {ι : Type uι} {κ : Type uκ} {μ : Type uμ} {ν : Type uν} (c₁ : IndexCoding ι κ) (c₂ : IndexCoding κ μ) (c₃ : IndexCoding μ ν) : (c₁.trans c₂).trans c₃ = c₁.trans (c₂.trans c₃)

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.ofEncodable (ι : Type uι) [Encodable ι] : IndexCoding ι ℕ

The canonical coding of an encodable type into ℕ. No choice is involved; a Countable carrier can be upgraded noncomputably via Encodable.ofCountable at the call site.

Equations

• FirstOrder.IndexCoding.ofEncodable ι = FirstOrder.IndexCoding.ofEncodableWith inferInstance

def FirstOrder.IndexCoding.ofEquiv {ι : Type uι} {κ : Type uκ} (e : ι ≃ κ) : IndexCoding ι κ

The coding induced by an equivalence of carriers. Its decode is total, so reindexing along it introduces no padding: this is the case of genuine syntactic transport (in particular the ULift universe adjustment), as opposed to an arbitrary coding, which preserves semantics but pads.

Equations

• FirstOrder.IndexCoding.ofEquiv e = { encode := ⇑e, decode := fun (k : κ) => some (e.symm k), decode_encode := ⋯ }

@[simp]

theorem FirstOrder.IndexCoding.ofEquiv_refl {ι : Type uι} : ofEquiv (Equiv.refl ι) = IndexCoding.id ι

theorem FirstOrder.IndexCoding.ofEquiv_trans {ι : Type uι} {κ : Type uκ} {μ : Type uμ} (e₁ : ι ≃ κ) (e₂ : κ ≃ μ) : ofEquiv (e₁.trans e₂) = (ofEquiv e₁).trans (ofEquiv e₂)

ofEquiv turns equivalence composition into coding composition.

@[simp]

theorem FirstOrder.IndexCoding.ofEquiv_trans_ofEquiv_symm {ι : Type uι} {κ : Type uκ} (e : ι ≃ κ) : (ofEquiv e).trans (ofEquiv e.symm) = IndexCoding.id ι

The two codings of an equivalence compose to the identity coding.

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

@[simp]

theorem FirstOrder.IndexCoding.id_pad {ι : Type uι} {β : Sort u_1} (default : β) (f : ι → β) : (IndexCoding.id ι).pad default f = f

theorem FirstOrder.IndexCoding.pad_trans {ι : Type uι} {κ : Type uκ} {μ : Type uμ} {β : Sort u_1} (c₁ : IndexCoding ι κ) (c₂ : IndexCoding κ μ) (default : β) (f : ι → β) : (c₁.trans c₂).pad default f = c₂.pad default (c₁.pad default f)

Padding along a composite coding is iterated padding: the decode analysis for a chain of codings happens HERE, once, not at every consumer.

theorem FirstOrder.IndexCoding.comp_pad {ι : Type uι} {κ : Type uκ} {β : Sort u_1} {γ : Sort u_2} (c : IndexCoding ι κ) (g : β → γ) (default : β) (f : ι → β) : g ∘ c.pad default f = c.pad (g default) (g ∘ f)

Mapping commutes with padding: the other half of the transport-coherence engine.