Numbering a structured index

The index types of Dinur's construction are built from a few formers: a pair of indices, a choice between two, an optional one, a tuple. Fintype numbers such a type too, but by an enumeration no algorithm can follow. This module numbers them explicitly instead: a pair is numbered by mixed radix, a choice by offsetting the second summand, a tuple by its digits.

The decoding is partial — a number out of range names nothing — which is what makes the numbering compose without needing any type to be inhabited.

Main definitions

• Complexity.NumEnc — an explicit numbering of a finite type

Main results

• the instances for Fin, Bool, Unit, products, sums, options and tuples

class Complexity.NumEnc (α : Type) : Type

An explicit numbering of a finite type: every value has a number below card, and every number below card names a value.

• card : ℕ

  How many values there are.

• enc : α → ℕ

  The number of a value.

• dec : ℕ → Option α

  The value a number names, if any.

• enc_lt (a : α) : enc a < card α

  Numbers are below the count.

• dec_enc (a : α) : dec (enc a) = some a

  Decoding a number back gives the value.

• enc_dec (i : ℕ) (a : α) : dec i = some a → enc a = i

  And a number in range is the number of what it names.

• dec_isSome (i : ℕ) : i < card α → (dec i).isSome = true

  Every number below the count names something.

theorem Complexity.NumEnc.enc_injective {α : Type} [NumEnc α] : Function.Injective enc

theorem Complexity.NumEnc.dec_eq_none_of_le {α : Type} [NumEnc α] {i : ℕ} (h : card α ≤ i) : dec i = none

def Complexity.NumEnc.get {α : Type} [NumEnc α] {i : ℕ} (h : i < card α) : α

The value a number in range names.

Equations

• Complexity.NumEnc.get h = (Complexity.NumEnc.dec i).get ⋯

@[simp]

theorem Complexity.NumEnc.dec_get {α : Type} [NumEnc α] {i : ℕ} (h : i < card α) : dec i = some (get h)

@[simp]

theorem Complexity.NumEnc.enc_get {α : Type} [NumEnc α] {i : ℕ} (h : i < card α) : enc (get h) = i

@[simp]

theorem Complexity.NumEnc.get_enc {α : Type} [NumEnc α] (a : α) : get ⋯ = a

theorem Complexity.NumEnc.card_eq_fintype_card (α : Type) [Fintype α] [NumEnc α] : card α = Fintype.card α

The count is the number of values.

def Complexity.NumEnc.equivFin (α : Type) [NumEnc α] : α ≃ Fin (card α)

The numbering, as an equivalence with an initial segment.

Equations

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

noncomputable def Complexity.NumEnc.equivFinCard (α : Type) [Fintype α] [NumEnc α] : α ≃ Fin (Fintype.card α)

The numbering, as an equivalence with Fin of the type's own cardinality — a drop-in replacement for Fintype.equivFin that an algorithm can follow.

Equations

• Complexity.NumEnc.equivFinCard α = (Complexity.NumEnc.equivFin α).trans (finCongr ⋯)

@[simp]

theorem Complexity.NumEnc.val_equivFinCard (α : Type) [Fintype α] [NumEnc α] (a : α) : ↑((equivFinCard α) a) = enc a

The formers

@[instance_reducible]

instance Complexity.NumEnc.instFin (n : ℕ) : NumEnc (Fin n)

Equations

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

@[instance_reducible]

instance Complexity.NumEnc.instBool : NumEnc Bool

Equations

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

@[instance_reducible]

instance Complexity.NumEnc.instUnit : NumEnc Unit

Equations

• Complexity.NumEnc.instUnit = { card := 1, enc := fun (x : Unit) => 0, dec := fun (i : ℕ) => if i = 0 then some () else none, enc_lt := ⋯, dec_enc := ⋯, enc_dec := ⋯, dec_isSome := ⋯ }

theorem Complexity.NumEnc.prod_lt {α β : Type} [NumEnc α] [NumEnc β] (a : α) (b : β) : enc a * card β + enc b < card α * card β

theorem Complexity.NumEnc.prod_div {α β : Type} [NumEnc α] [NumEnc β] (a : α) (b : β) : (enc a * card β + enc b) / card β = enc a

theorem Complexity.NumEnc.prod_mod {α β : Type} [NumEnc α] [NumEnc β] (a : α) (b : β) : (enc a * card β + enc b) % card β = enc b

@[instance_reducible]

instance Complexity.NumEnc.instProd {α β : Type} [NumEnc α] [NumEnc β] : NumEnc (α × β)

Equations

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

@[instance_reducible]

instance Complexity.NumEnc.instSum {α β : Type} [NumEnc α] [NumEnc β] : NumEnc (α ⊕ β)

Equations

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

@[instance_reducible]

instance Complexity.NumEnc.instOption {α : Type} [NumEnc α] : NumEnc (Option α)

Equations

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

@[reducible]

noncomputable def Complexity.NumEnc.ofFintype (α : Type) [Fintype α] : NumEnc α

Any finite type is numbered by its own enumeration. For a type whose size is a constant, that is all an algorithm needs: the numbering is a lookup on a bounded key.

Equations

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