Langlib

Langlib.Automata.LinearBounded.RowNumeral

Synchronous finite-row numerals #

This file supplies small, reusable finite-state verifiers for counters stored across a row. Digits are written least significant first, so carry propagation is checked in one left-to-right sweep, exactly the direction used by CertifiedRowSystem.

The digit order is made explicit by a DigitCodec. This keeps the scanners independent of a particular order instance; orderedCodec supplies the canonical increasing codec for every finite linear order.

structure RowNumeral.DigitCodec (D : Type u_1) [Fintype D] :

Type u_1

A numbering of a finite digit type by 0, ..., card D - 1.

toFin : D ≃ Fin (Fintype.card D)

Instances For

def RowNumeral.orderedCodec (D : Type u_1) [Fintype D] [LinearOrder D] :

The canonical increasing numbering of a finite linearly ordered digit type.

Equations

RowNumeral.orderedCodec D = { toFin := (monoEquivOfFin D ⋯).symm.toEquiv }

Instances For

def RowNumeral.DigitCodec.radix {D : Type u_1} [Fintype D] (_E : DigitCodec D) :

The radix of a row numeral.

Equations

_E.radix = Fintype.card D

Instances For

theorem RowNumeral.DigitCodec.radix_pos {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) :

def RowNumeral.DigitCodec.digitValue {D : Type u_1} [Fintype D] (E : DigitCodec D) (d : D) :

Numeric value of one digit.

Equations

E.digitValue d = ↑(E.toFin d)

Instances For

theorem RowNumeral.DigitCodec.digitValue_lt {D : Type u_1} [Fintype D] (E : DigitCodec D) (d : D) :

E.digitValue d < E.radix

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

D

The zero digit.

Equations

E.zero = E.toFin.symm ⟨0, ⋯⟩

Instances For

@[simp]

theorem RowNumeral.DigitCodec.toFin_zero {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) :

E.toFin E.zero = ⟨0, ⋯⟩

@[simp]

theorem RowNumeral.DigitCodec.digitValue_zero {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) :

E.digitValue E.zero = 0

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

D

The greatest digit.

Equations

E.last = E.toFin.symm ⟨E.radix - 1, ⋯⟩

Instances For

@[simp]

theorem RowNumeral.DigitCodec.digitValue_last {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) :

E.digitValue E.last = E.radix - 1

theorem RowNumeral.DigitCodec.digitValue_injective {D : Type u_1} [Fintype D] (E : DigitCodec D) :

Function.Injective E.digitValue

def RowNumeral.DigitCodec.next {D : Type u_1} [Fintype D] (E : DigitCodec D) (d : D) :

The next digit, or none at the greatest digit.

Equations

E.next d = if h : E.digitValue d + 1 < E.radix then some (E.toFin.symm ⟨E.digitValue d + 1, h⟩) else none

Instances For

theorem RowNumeral.DigitCodec.next_eq_some_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) (d d' : D) :

E.next d = some d' ↔ E.digitValue d + 1 < E.radix ∧ E.digitValue d' = E.digitValue d + 1

theorem RowNumeral.DigitCodec.next_eq_none_iff {D : Type u_1} [Fintype D] (E : DigitCodec D) (d : D) :

E.next d = none ↔ E.digitValue d + 1 = E.radix

theorem RowNumeral.DigitCodec.next_eq_none_iff_eq_last {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (d : D) :

E.next d = none ↔ d = E.last

def RowNumeral.DigitCodec.one {D : Type u_1} [Fintype D] (E : DigitCodec D) (h : 1 < E.radix) :

D

The digit one, available when the radix is at least two.

Equations

E.one h = E.toFin.symm ⟨1, h⟩

Instances For

@[simp]

theorem RowNumeral.DigitCodec.digitValue_one {D : Type u_1} [Fintype D] (E : DigitCodec D) (h : 1 < E.radix) :

E.digitValue (E.one h) = 1

def RowNumeral.DigitCodec.value {D : Type u_1} [Fintype D] (E : DigitCodec D) :

List D → ℕ

Value of an LSD-first digit row.

Equations

E.value [] = 0
E.value (d :: ds) = E.digitValue d + E.radix * E.value ds

Instances For

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

The all-zero row of a given width.

Equations

E.zeroRow width = List.replicate width E.zero

Instances For

def RowNumeral.DigitCodec.oneRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (h : 1 < E.radix) :

ℕ → List D

The numeral one at a positive width. At width zero it is the empty row.

Equations

E.oneRow h 0 = []
E.oneRow h n.succ = E.one h :: E.zeroRow n

Instances For

@[simp]

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

(E.zeroRow width).length = width

@[simp]

theorem RowNumeral.DigitCodec.length_oneRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (h : 1 < E.radix) (width : ℕ) :

(E.oneRow h width).length = width

@[simp]

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

E.value (E.zeroRow width) = 0

@[simp]

theorem RowNumeral.DigitCodec.value_oneRow {D : Type u_1} [Fintype D] [Nonempty D] (E : DigitCodec D) (h : 1 < E.radix) {width : ℕ} (hw : 0 < width) :

E.value (E.oneRow h width) = 1

Cellwise zero and copy checks #

def RowNumeral.DigitCodec.zeroStep {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (ok : Bool) (d : D) :

One cell of an all-zero check. false is an absorbing failure state.

Equations

E.zeroStep ok d = (ok && decide (d = E.zero))

Instances For

def RowNumeral.DigitCodec.copyStep {D : Type u_1} [Fintype D] [DecidableEq D] (_E : DigitCodec D) (ok : Bool) (old new : D) :

One cell of a synchronous equality/copy check.

Equations

_E.copyStep ok old new = (ok && decide (new = old))

Instances For

inductive RowNumeral.OneState :

State of the one-row checker.

first : OneState
rest : OneState
bad : OneState

Instances For

instance RowNumeral.instDecidableEqOneState :

DecidableEq OneState

Equations

RowNumeral.instDecidableEqOneState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RowNumeral.instFintypeOneState :

Fintype OneState

Equations

RowNumeral.instFintypeOneState = { elems := { val := ↑RowNumeral.OneState.enumList, nodup := RowNumeral.OneState.enumList_nodup }, complete := RowNumeral.instFintypeOneState._proof_1 }

instance RowNumeral.instReprOneState :

Equations

RowNumeral.instReprOneState = { reprPrec := RowNumeral.instReprOneState.repr }

def RowNumeral.instReprOneState.repr :

OneState → ℕ → Std.Format

Equations

RowNumeral.instReprOneState.repr RowNumeral.OneState.first prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RowNumeral.OneState.first")).group prec✝
RowNumeral.instReprOneState.repr RowNumeral.OneState.rest prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RowNumeral.OneState.rest")).group prec✝
RowNumeral.instReprOneState.repr RowNumeral.OneState.bad prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RowNumeral.OneState.bad")).group prec✝

Instances For

def RowNumeral.DigitCodec.oneStep {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (h : 1 < E.radix) :

OneState → D → OneState

Check one digit of the canonical positive-width numeral one.

Equations

E.oneStep h RowNumeral.OneState.bad x✝ = RowNumeral.OneState.bad
E.oneStep h RowNumeral.OneState.first x✝ = if x✝ = E.one h then RowNumeral.OneState.rest else RowNumeral.OneState.bad
E.oneStep h RowNumeral.OneState.rest x✝ = if x✝ = E.zero then RowNumeral.OneState.rest else RowNumeral.OneState.bad

Instances For

def RowNumeral.DigitCodec.checkZero {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) :

List D → Bool

Run a zero checker over a whole row.

Equations

E.checkZero [] = true
E.checkZero (d :: ds) = (decide (d = E.zero) && E.checkZero ds)

Instances For

def RowNumeral.DigitCodec.checkCopy {D : Type u_1} [Fintype D] [DecidableEq D] (E : DigitCodec D) :

List D → List D → Bool

Run a copy/equality checker over two rows; a length mismatch rejects.

Equations

E.checkCopy [] [] = true
E.checkCopy (old :: olds) (new :: news) = (decide (new = old) && E.checkCopy olds news)
E.checkCopy x✝¹ x✝ = false

Instances For

def RowNumeral.DigitCodec.checkOne {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (h : 1 < E.radix) :

List D → Bool

Run the canonical-one checker. The empty row rejects.

Equations

E.checkOne h [] = false
E.checkOne h (d :: ds) = (decide (d = E.one h) && E.checkZero ds)

Instances For

@[simp]

theorem RowNumeral.DigitCodec.checkZero_eq_true_iff {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (row : List D) :

E.checkZero row = true ↔ row = E.zeroRow row.length

@[simp]

theorem RowNumeral.DigitCodec.checkCopy_eq_true_iff {D : Type u_1} [Fintype D] [DecidableEq D] (E : DigitCodec D) (old new : List D) :

E.checkCopy old new = true ↔ new = old

@[simp]

theorem RowNumeral.DigitCodec.checkOne_eq_true_iff {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (h : 1 < E.radix) (row : List D) :

E.checkOne h row = true ↔ 0 < row.length ∧ row = E.oneRow h row.length

Synchronous successor #

inductive RowNumeral.CarryState :

State of the one-pass successor verifier.

carry : CarryState
done : CarryState
bad : CarryState

Instances For

instance RowNumeral.instDecidableEqCarryState :

DecidableEq CarryState

Equations

RowNumeral.instDecidableEqCarryState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RowNumeral.instFintypeCarryState :

Fintype CarryState

Equations

RowNumeral.instFintypeCarryState = { elems := { val := ↑RowNumeral.CarryState.enumList, nodup := RowNumeral.CarryState.enumList_nodup }, complete := RowNumeral.instFintypeCarryState._proof_1 }

def RowNumeral.instReprCarryState.repr :

CarryState → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
RowNumeral.instReprCarryState.repr RowNumeral.CarryState.bad prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RowNumeral.CarryState.bad")).group prec✝

Instances For

instance RowNumeral.instReprCarryState :

Repr CarryState

Equations

RowNumeral.instReprCarryState = { reprPrec := RowNumeral.instReprCarryState.repr }

def RowNumeral.DigitCodec.succStep {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) :

CarryState → D → D → CarryState

Check one aligned pair of digits while propagating a carry from left to right.

Equations

One or more equations did not get rendered due to their size.
E.succStep RowNumeral.CarryState.bad x✝¹ x✝ = RowNumeral.CarryState.bad
E.succStep RowNumeral.CarryState.done x✝¹ x✝ = if x✝ = x✝¹ then RowNumeral.CarryState.done else RowNumeral.CarryState.bad

Instances For

def RowNumeral.DigitCodec.evalSucc {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) :

CarryState → List D → List D → Option CarryState

Run the synchronous successor verifier; a length mismatch rejects.

Equations

E.evalSucc x✝ [] [] = some x✝
E.evalSucc x✝ (old :: olds) (new :: news) = E.evalSucc (E.succStep x✝ old new) olds news
E.evalSucc x✝² x✝¹ x✝ = none

Instances For

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

List D → List D × Bool

Increment an LSD-first row, returning an overflow bit.

Equations

E.increment [] = ([], true )
E.increment (d :: ds) = match E.next d with | some d' => (d' :: ds, false ) | none => have tail := E.increment ds; (E.zero :: tail.1, tail.2)

Instances For

@[simp]

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

(E.increment row).1.length = row.length

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

(E.increment row).2 = true ↔ row = List.replicate row.length E.last

Overflow occurs exactly at the all-greatest digit row.

theorem RowNumeral.DigitCodec.increment_fst_of_overflow {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

On overflow, canonical increment wraps to the all-zero row.

theorem RowNumeral.DigitCodec.evalSucc_bad_eq_some_iff {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (old new : List D) (q : CarryState) :

E.evalSucc CarryState.bad old new = some q ↔ old.length = new.length ∧ q = CarryState.bad

theorem RowNumeral.DigitCodec.evalSucc_done_eq_some_iff {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (old new : List D) (q : CarryState) :

E.evalSucc CarryState.done old new = some q ∧ q ≠ CarryState.bad ↔ new = old ∧ q = CarryState.done

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

E.evalSucc CarryState.done old new = some CarryState.done ↔ new = old

theorem RowNumeral.DigitCodec.evalSucc_carry_iff {D : Type u_1} [Fintype D] [Nonempty D] [DecidableEq D] (E : DigitCodec D) (old new : List D) (q : CarryState) :

E.evalSucc CarryState.carry old new = some q ∧ q ≠ CarryState.bad ↔ new = (E.increment old).1 ∧ q = if (E.increment old).2 = true then CarryState.carry else CarryState.done

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

E.evalSucc CarryState.carry old new = some CarryState.done ↔ new = (E.increment old).1 ∧ (E.increment old).2 = false

A successful non-overflowing scan is exactly canonical row successor.

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

E.evalSucc CarryState.carry old new = some CarryState.carry ↔ new = (E.increment old).1 ∧ (E.increment old).2 = true

A carry remaining after the last cell is exactly canonical overflow.

Synchronous comparison #

The scan still runs from least to most significant digit. A newly read unequal digit is more significant than everything seen before, so it replaces the accumulated ordering.

def RowNumeral.DigitCodec.compareStep {D : Type u_1} [Fintype D] (E : DigitCodec D) (q : Ordering) (x y : D) :

Compare one aligned pair during an LSD-first scan.

Equations

E.compareStep q x y = match compare (E.digitValue x) (E.digitValue y) with | Ordering.eq => q | q' => q'

Instances For

def RowNumeral.DigitCodec.evalCompare {D : Type u_1} [Fintype D] (E : DigitCodec D) :

Ordering → List D → List D → Option Ordering

Run the synchronous comparison scan; a length mismatch rejects.

Equations

E.evalCompare x✝ [] [] = some x✝
E.evalCompare x✝ (x_3 :: xs) (y :: ys) = E.evalCompare (E.compareStep x✝ x_3 y) xs ys
E.evalCompare x✝² x✝¹ x✝ = none

Instances For

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

Option Ordering

Canonical LSD-first comparison of two rows.

Equations

E.compareRows xs ys = E.evalCompare Ordering.eq xs ys

Instances For

theorem RowNumeral.DigitCodec.evalCompare_eq_compareRows {D : Type u_1} [Fintype D] (E : DigitCodec D) (xs ys : List D) :

E.evalCompare Ordering.eq xs ys = E.compareRows xs ys

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

Equality result of the synchronous comparison.

Equations

E.rowsEqual xs ys = (E.compareRows xs ys = some Ordering.eq)

Instances For

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

Strict less-than result of the synchronous comparison.

Equations

E.rowsLess xs ys = (E.compareRows xs ys = some Ordering.lt)

Instances For