Canonical enumeration of fixed-width finite rows

RowNumeral implements least-significant-digit-first counters and their synchronous finite-state verifiers. This file supplies their arithmetic semantics. A row of length n over a finite alphabet A has a unique rank below |A| ^ n; starting at the zero row and repeatedly applying fixed-width increment visits every such row exactly once before overflowing.

The final section chooses a codec for Option A. Its radix is |A| + 1, so on every positive-width input it has room for the endpoint |A| ^ n as well as all smaller row ranks. These are the fuel and depth counters used by the linear-space inductive-counting verifier.

noncomputable def RowNumeral.fintypeCodec (D : Type u_1) [Fintype D] : DigitCodec D

A choice-free-at-use-site digit codec for any finite type. Unlike orderedCodec, this does not require the caller to install a LinearOrder; the noncomputable choice is made once when the verifier is constructed.

Equations

• RowNumeral.fintypeCodec D = { toFin := Fintype.equivFin D }

Rank bounds and uniqueness

theorem RowNumeral.DigitCodec.value_lt_pow_length {D : Type u_1} [Fintype D] (E : DigitCodec D) (row : List D) : E.value row < E.radix ^ row.length

The numeric value of a row is below the number of rows of that length.

theorem RowNumeral.DigitCodec.value_injective_of_length_eq {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) {xs ys : List D} (hlen : xs.length = ys.length) (hvalue : E.value xs = E.value ys) : xs = ys

Equal-length rows with equal numeric values are equal.

theorem RowNumeral.DigitCodec.value_injective_on_length {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (n : ℕ) : Set.InjOn E.value {row : List D | row.length = n}

On rows of one fixed length, value is injective.

Greatest row and increment arithmetic

def RowNumeral.DigitCodec.lastRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : List D

The all-greatest-digit row of a fixed width.

Equations

• E.lastRow width = List.replicate width E.last

@[simp]

theorem RowNumeral.DigitCodec.length_lastRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : (E.lastRow width).length = width

theorem RowNumeral.DigitCodec.value_lastRow_add_one {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : E.value (E.lastRow width) + 1 = E.radix ^ width

The greatest row has rank radix ^ width - 1, stated without subtraction.

theorem RowNumeral.DigitCodec.increment_overflow_iff_value {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (row : List D) : (E.increment row).2 = true ↔ E.value row + 1 = E.radix ^ row.length

Overflow is equivalent to the old rank being the greatest possible rank.

theorem RowNumeral.DigitCodec.value_increment_of_not_overflow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (row : List D) (hno : (E.increment row).2 = false) : E.value (E.increment row).1 = E.value row + 1

A nonoverflowing increment raises the rank by exactly one.

theorem RowNumeral.DigitCodec.value_increment {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (row : List D) : E.value (E.increment row).1 = if (E.increment row).2 = true then 0 else E.value row + 1

The rank of fixed-width increment: on overflow it wraps to zero, otherwise it is the old rank plus one.

theorem RowNumeral.DigitCodec.increment_overflow_result {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (row : List D) (h : (E.increment row).2 = true) : (E.increment row).1 = E.zeroRow row.length

Fixed-width increment wraps to zero precisely after the greatest row.

def RowNumeral.DigitCodec.nextRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (row : List D) : List D

The row-only fixed-width successor.

Equations

• E.nextRow row = (E.increment row).1

@[simp]

theorem RowNumeral.DigitCodec.nextRow_length {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (row : List D) : (E.nextRow row).length = row.length

@[simp]

theorem RowNumeral.DigitCodec.iterate_nextRow_length {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (k : ℕ) (row : List D) : (E.nextRow^[k] row).length = row.length

Canonical fixed-width enumeration

theorem RowNumeral.DigitCodec.value_iterate_nextRow_zeroRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) {width k : ℕ} (hk : k < E.radix ^ width) : E.value (E.nextRow^[k] (E.zeroRow width)) = k

Before overflow, the rank of the kth row reached from zero is exactly k.

theorem RowNumeral.DigitCodec.exists_row_of_value {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) {width value : ℕ} (hvalue : value < E.radix ^ width) : ∃ (row : List D), row.length = width ∧ E.value row = value

Every value below radix ^ width is represented by the corresponding iterate of fixed-width successor from zero.

theorem RowNumeral.DigitCodec.iterate_nextRow_value_eq {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (row : List D) : E.nextRow^[E.value row] (E.zeroRow row.length) = row

Every fixed-width row occurs in the canonical successor enumeration, at its numeric rank.

theorem RowNumeral.DigitCodec.eq_of_iterate_nextRow_eq {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) {width i j : ℕ} (hi : i < E.radix ^ width) (hj : j < E.radix ^ width) (hrows : E.nextRow^[i] (E.zeroRow width) = E.nextRow^[j] (E.zeroRow width)) : i = j

Equality of two in-range enumeration positions forces equality of their ranks.

theorem RowNumeral.DigitCodec.existsUnique_iterate_nextRow_eq {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) {width : ℕ} (row : List D) (hlen : row.length = width) : ∃! k : ℕ, k < E.radix ^ width ∧ E.nextRow^[k] (E.zeroRow width) = row

A fixed-width row occurs at a unique in-range enumeration position.

theorem RowNumeral.DigitCodec.increment_iterate_nextRow_overflow_iff {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) {width k : ℕ} (hk : k < E.radix ^ width) : (E.increment (E.nextRow^[k] (E.zeroRow width))).2 = true ↔ k + 1 = E.radix ^ width

At an in-range enumeration position, the following increment overflows exactly when that position is the final rank.

theorem RowNumeral.DigitCodec.increment_iterate_nextRow_not_overflow_iff {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) {width k : ℕ} (hk : k < E.radix ^ width) : (E.increment (E.nextRow^[k] (E.zeroRow width))).2 = false ↔ k + 1 < E.radix ^ width

Equivalently, another nonoverflowing enumeration step exists exactly before the last rank.

@[simp]

theorem RowNumeral.DigitCodec.nextRow_lastRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : E.nextRow (E.lastRow width) = E.zeroRow width

Incrementing the greatest row wraps to the zero row.

theorem RowNumeral.DigitCodec.iterate_nextRow_capacity {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : E.nextRow^[E.radix ^ width] (E.zeroRow width) = E.zeroRow width

After exactly radix ^ width successors the enumeration has wrapped back to the zero row.

def RowNumeral.DigitCodec.rowEnumeration {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : List (List D)

The canonical list of every row of one width, in increasing numeric rank.

Equations

• E.rowEnumeration width = List.map (fun (k : ℕ) => E.nextRow^[k] (E.zeroRow width)) (List.range (E.radix ^ width))

@[simp]

theorem RowNumeral.DigitCodec.length_rowEnumeration {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : (E.rowEnumeration width).length = E.radix ^ width

theorem RowNumeral.DigitCodec.rowEnumeration_nodup {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) : (E.rowEnumeration width).Nodup

The canonical enumeration has no duplicate rows.

theorem RowNumeral.DigitCodec.mem_rowEnumeration_iff {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (width : ℕ) (row : List D) : row ∈ E.rowEnumeration width ↔ row.length = width

Membership in the canonical enumeration is exactly having the specified length.

Correctness of synchronous row comparison

theorem RowNumeral.DigitCodec.compareStep_eq_lt_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) (q : Ordering) (x y : D) : E.compareStep q x y = Ordering.lt ↔ E.digitValue x < E.digitValue y ∨ E.digitValue x = E.digitValue y ∧ q = Ordering.lt

theorem RowNumeral.DigitCodec.compareStep_eq_eq_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) (q : Ordering) (x y : D) : E.compareStep q x y = Ordering.eq ↔ E.digitValue x = E.digitValue y ∧ q = Ordering.eq

theorem RowNumeral.DigitCodec.evalCompare_eq_lt_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) (q : Ordering) {xs ys : List D} (hlen : xs.length = ys.length) : E.evalCompare q xs ys = some Ordering.lt ↔ E.value xs < E.value ys ∨ E.value xs = E.value ys ∧ q = Ordering.lt

General comparison invariant: the already-scanned ordering matters exactly when the remaining (more-significant) suffixes have equal value.

theorem RowNumeral.DigitCodec.evalCompare_eq_eq_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) (q : Ordering) {xs ys : List D} (hlen : xs.length = ys.length) : E.evalCompare q xs ys = some Ordering.eq ↔ E.value xs = E.value ys ∧ q = Ordering.eq

Equality variant of the general comparison invariant.

theorem RowNumeral.DigitCodec.compareRows_eq_lt_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) {xs ys : List D} (hlen : xs.length = ys.length) : E.compareRows xs ys = some Ordering.lt ↔ E.value xs < E.value ys

The synchronous comparison reports strict inequality exactly when the numeric ranks are strictly ordered.

theorem RowNumeral.DigitCodec.compareRows_eq_eq_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) {xs ys : List D} (hlen : xs.length = ys.length) : E.compareRows xs ys = some Ordering.eq ↔ E.value xs = E.value ys

The synchronous comparison reports equality exactly when the numeric ranks are equal (for equal-length rows).

Boolean scanner acceptance predicates

def RowNumeral.DigitCodec.checkSucc {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (old new : List D) : Bool

Boolean acceptance predicate for a nonoverflowing synchronous successor scan.

Equations

• E.checkSucc old new = decide (E.evalSucc RowNumeral.CarryState.carry old new = some RowNumeral.CarryState.done)

@[simp]

theorem RowNumeral.DigitCodec.checkSucc_eq_true_iff {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (old new : List D) : E.checkSucc old new = true ↔ new = (E.increment old).1 ∧ (E.increment old).2 = false

def RowNumeral.DigitCodec.checkLE {D : Type u_1} [Fintype D] (E : DigitCodec D) (xs ys : List D) : Bool

Boolean acceptance predicate for value xs ≤ value ys. A length mismatch is rejected because neither comparison result can be produced.

Equations

• E.checkLE xs ys = decide (E.compareRows xs ys = some Ordering.lt ∨ E.compareRows xs ys = some Ordering.eq)

@[simp]

theorem RowNumeral.DigitCodec.checkLE_eq_true_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) {xs ys : List D} (hlen : xs.length = ys.length) : E.checkLE xs ys = true ↔ E.value xs ≤ E.value ys

The base-Option A fuel counter

noncomputable def RowNumeral.fuelCodec (A : Type u_2) [inst : Fintype A] : DigitCodec (Option A)

The canonical fuel codec. The extra none digit raises its radix from |A| to |A| + 1, independently of how the Fintype instance orders the digits.

Equations

• RowNumeral.fuelCodec A = RowNumeral.fintypeCodec (Option A)

@[simp]

theorem RowNumeral.fuelCodec_radix (A : Type u_2) [Fintype A] : (fuelCodec A).radix = Fintype.card A + 1

theorem RowNumeral.card_pow_lt_succ_card_pow (A : Type u_2) [Fintype A] {width : ℕ} (hwidth : 0 < width) : Fintype.card A ^ width < (Fintype.card A + 1) ^ width

Pure cardinal-arithmetic form of the fuel-capacity bound.

theorem RowNumeral.rowCapacity_lt_fuelCapacity (A : Type u_2) [Fintype A] {width : ℕ} (hwidth : 0 < width) : Fintype.card A ^ width < (fuelCodec A).radix ^ width

On every positive width, an Option A counter has strictly more values than there are width-n rows over A.

theorem RowNumeral.exists_fuelRow_of_le_rowCapacity (A : Type u_2) [Fintype A] {width value : ℕ} (hwidth : 0 < width) (hvalue : value ≤ Fintype.card A ^ width) : ∃ (row : List (Option A)), row.length = width ∧ (fuelCodec A).value row = value

Every number up to and including the number of width-n rows over A fits in the width-n base-Option A fuel counter.

def RowNumeral.countDigitCodec (A : Type u_2) [Fintype A] : DigitCodec (Fin (Fintype.card A + 1))

A concrete Fin (|A| + 1) codec, useful when a construction wants the count digits themselves rather than the equivalent Option A representation.

Equations

• RowNumeral.countDigitCodec A = { toFin := finCongr ⋯ }

@[simp]

theorem RowNumeral.countDigitCodec_radix (A : Type u_2) [Fintype A] : (countDigitCodec A).radix = Fintype.card A + 1

theorem RowNumeral.exists_countRow_of_le_rowCapacity (A : Type u_2) [Fintype A] {width value : ℕ} (hwidth : 0 < width) (hvalue : value ≤ Fintype.card A ^ width) : ∃ (row : List (Fin (Fintype.card A + 1))), row.length = width ∧ (countDigitCodec A).value row = value

Concrete count-row form of exists_fuelRow_of_le_rowCapacity.