Index codings

An IndexCoding ι κ consists of an injection into κ and a decoder recovering the encoded indices. Padding extends an ι-indexed family to κ with a chosen default. In particular, true padding preserves universal quantification and false padding preserves existence; these are the neutral extensions used for coded infinitary conjunctions and disjunctions.

The API provides identity and composition, codings from equivalences and explicit or inferred Encodable data, sum codings, the underlying embedding, and the padding composition laws.

Adapted from Cameron Freer's Mathlib/ModelTheory/Infinitary/IndexCoding.lean in cameronfreer/mathlib4.

structure TauCeti.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 TauCeti.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 TauCeti.IndexCoding.ext_iff {ι : Type uι} {κ : Type uκ} {c₁ c₂ : IndexCoding ι κ} : c₁ = c₂ ↔ c₁.encode = c₂.encode ∧ c₁.decode = c₂.decode

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

encode is injective: decode_encode already provides a retraction.

def TauCeti.IndexCoding.toEmbedding {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) : ι ↪ κ

The underlying embedding of a coding.

@[simp]

theorem TauCeti.IndexCoding.toEmbedding_apply {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) (i : ι) : c.toEmbedding i = c.encode i

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

The identity coding.

@[simp]

theorem TauCeti.IndexCoding.id_encode {ι : Type uι} (i : ι) : (IndexCoding.id ι).encode i = i

@[simp]

theorem TauCeti.IndexCoding.id_decode {ι : Type uι} (i : ι) : (IndexCoding.id ι).decode i = some i

def TauCeti.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₂ : κ → μ.

@[simp]

theorem TauCeti.IndexCoding.trans_encode {ι : Type uι} {κ : Type uκ} {μ : Type uμ} (c₁ : IndexCoding ι κ) (c₂ : IndexCoding κ μ) (i : ι) : (c₁.trans c₂).encode i = c₂.encode (c₁.encode i)

@[simp]

theorem TauCeti.IndexCoding.trans_decode {ι : Type uι} {κ : Type uκ} {μ : Type uμ} (c₁ : IndexCoding ι κ) (c₂ : IndexCoding κ μ) (m : μ) : (c₁.trans c₂).decode m = (c₂.decode m).bind c₁.decode

@[simp]

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

Composing the identity coding before a coding leaves it unchanged.

@[simp]

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

Composing a coding with the identity coding leaves it unchanged.

theorem TauCeti.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₃)

Composition of index codings is associative.

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

The canonical coding of the left summand into a sum.

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

The canonical coding of the right summand into a sum.

@[simp]

theorem TauCeti.IndexCoding.sumInl_encode {ι : Type uι} {κ : Type uκ} (i : ι) : (sumInl ι κ).encode i = Sum.inl i

@[simp]

theorem TauCeti.IndexCoding.sumInl_decode {ι : Type uι} {κ : Type uκ} (k : ι ⊕ κ) : (sumInl ι κ).decode k = k.getLeft?

@[simp]

theorem TauCeti.IndexCoding.sumInr_encode {ι : Type uι} {κ : Type uκ} (k : κ) : (sumInr ι κ).encode k = Sum.inr k

@[simp]

theorem TauCeti.IndexCoding.sumInr_decode {ι : Type uι} {κ : Type uκ} (k : ι ⊕ κ) : (sumInr ι κ).decode k = k.getRight?

def TauCeti.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.

def TauCeti.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.

@[simp]

theorem TauCeti.IndexCoding.ofEncodableWith_encode {ι : Type uι} (e : Encodable ι) (i : ι) : (ofEncodableWith e).encode i = Encodable.encode i

@[simp]

theorem TauCeti.IndexCoding.ofEncodableWith_decode {ι : Type uι} (e : Encodable ι) (n : ℕ) : (ofEncodableWith e).decode n = Encodable.decode n

@[simp]

theorem TauCeti.IndexCoding.ofEncodable_encode {ι : Type uι} [Encodable ι] (i : ι) : (ofEncodable ι).encode i = Encodable.encode i

@[simp]

theorem TauCeti.IndexCoding.ofEncodable_decode {ι : Type uι} [Encodable ι] (n : ℕ) : (ofEncodable ι).decode n = Encodable.decode n

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

The coding induced by an equivalence of carriers. Its decoder always returns the inverse image, so padding along it never selects the default branch.

@[simp]

theorem TauCeti.IndexCoding.ofEquiv_encode {ι : Type uι} {κ : Type uκ} (e : ι ≃ κ) (i : ι) : (ofEquiv e).encode i = e i

@[simp]

theorem TauCeti.IndexCoding.ofEquiv_decode {ι : Type uι} {κ : Type uκ} (e : ι ≃ κ) (k : κ) : (ofEquiv e).decode k = some (e.symm k)

@[simp]

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

The coding induced by the identity equivalence is the identity coding.

theorem TauCeti.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 TauCeti.IndexCoding.ofEquiv_trans_ofEquiv_symm {ι : Type uι} {κ : Type uκ} (e : ι ≃ κ) : (ofEquiv e).trans (ofEquiv e.symm) = IndexCoding.id ι

Composing the coding of an equivalence with the coding of its inverse gives the identity coding.

def TauCeti.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.

theorem TauCeti.IndexCoding.pad_apply {ι : Type uι} {κ : Type uκ} {β : Sort u_1} (c : IndexCoding ι κ) (default : β) (f : ι → β) (k : κ) : c.pad default f k = (c.decode k).elim default f

Evaluate padding using the decoder, without unfolding the coding or padding.

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

Padding at an encoded index recovers the original branch.

@[simp]

theorem TauCeti.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

@[simp]

theorem TauCeti.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 TauCeti.IndexCoding.id_pad {ι : Type uι} {β : Sort u_1} (default : β) (f : ι → β) : (IndexCoding.id ι).pad default f = f

Padding along the identity coding leaves the family unchanged.

theorem TauCeti.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 with the same default.

theorem TauCeti.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 a padded family maps its default and its original branches.

@[simp]

theorem TauCeti.IndexCoding.forall_pad_true_iff {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) (p : ι → Prop) : (∀ (k : κ), c.pad True p k) ↔ ∀ (i : ι), p i

Universal quantification is unchanged by padding with True.

@[simp]

theorem TauCeti.IndexCoding.exists_pad_false_iff {ι : Type uι} {κ : Type uκ} (c : IndexCoding ι κ) (p : ι → Prop) : (∃ (k : κ), c.pad False p k) ↔ ∃ (i : ι), p i

Existential quantification is unchanged by padding with False.

@[simp]

theorem TauCeti.IndexCoding.iUnion_pad_of_eq_empty {ι : Type uι} {κ : Type uκ} {β : Sort u_1} {γ : Type u_2} (c : IndexCoding ι κ) {g : β → Set γ} {d : β} (hd : g d = ∅) (f : ι → β) : ⋃ (k : κ), g (c.pad d f k) = ⋃ (i : ι), g (f i)

Taking the union of sets assigned to a padded family preserves the original union when the default is assigned the empty set.