structure Hex.Matrix.DetOps (R : Type) : Type

Operations on the serialized entries of a determinant certificate. The companion supplies canonical polynomial lists and their denotation laws.

• zero : R
• one : R
• add : R → R → R
• mul : R → R → R
• neg : R → R
• beq : R → R → Bool
• valid : R → Bool

def Hex.Matrix.DetOps.entry {R : Type} (ops : DetOps R) : List R → Nat → R

A row entry, with zero beyond the end.

Equations

• ops.entry [] x✝ = ops.zero
• ops.entry (x_2 :: tail) 0 = x_2
• ops.entry (head :: xs) n.succ = ops.entry xs n

def Hex.Matrix.DetOps.dot {R : Type} (ops : DetOps R) : List R → List R → R

Dot product, stopping at the shorter list.

Equations

• ops.dot (x_2 :: xs) (y :: ys) = ops.add (ops.mul x_2 y) (ops.dot xs ys)
• ops.dot x✝¹ x✝ = ops.zero

def Hex.Matrix.DetOps.column {R : Type} (ops : DetOps R) (j : Nat) : List (List R) → List R

Column extraction uses only structural list recursion.

Equations

• ops.column j [] = []
• ops.column j (r :: rs) = ops.entry r j :: ops.column j rs

def Hex.Matrix.DetOps.columns {R : Type} (ops : DetOps R) (A : List (List R)) (start : Nat) : Nat → List (List R)

Consecutive columns, starting at the supplied index.

Equations

• ops.columns A start 0 = []
• ops.columns A start n.succ = ops.column start A :: ops.columns A (start + 1) n

def Hex.Matrix.DetOps.validRow {R : Type} (ops : DetOps R) : List R → Bool

Canonicality of every entry in a row.

Equations

• ops.validRow [] = true
• ops.validRow (x_1 :: xs) = (ops.valid x_1 && ops.validRow xs)

def Hex.Matrix.DetOps.validRows {R : Type} (ops : DetOps R) : List (List R) → Bool

Canonicality of every entry in every row.

Equations

• ops.validRows [] = true
• ops.validRows (r :: rs) = (ops.validRow r && ops.validRows rs)

def Hex.Matrix.DetOps.zeroDots {R : Type} (ops : DetOps R) (v : List R) : List (List R) → Bool

Orthogonality against each supplied column.

Equations

• ops.zeroDots v [] = true
• ops.zeroDots v (r :: rs) = (ops.beq (ops.dot v r) ops.zero && ops.zeroDots v rs)

def Hex.Matrix.DetOps.anyNonzero {R : Type} (ops : DetOps R) : List R → Bool

At least one entry is nonzero.

Equations

• ops.anyNonzero [] = false
• ops.anyNonzero (x_1 :: xs) = (!ops.beq x_1 ops.zero || ops.anyNonzero xs)

def Hex.Matrix.DetOps.signed {R : Type} (ops : DetOps R) : List (Nat × Nat) → R → R

Apply the sign of the row permutation without a coefficient cast.

Equations

• ops.signed [] x✝ = x✝
• ops.signed (head :: swaps) x✝ = ops.neg (ops.signed swaps x✝)

def Hex.Matrix.DetOps.triangular {R : Type} (ops : DetOps R) (d : R) (swaps : List (Nat × Nat)) : List (List R) → Nat → List (List R) → List (List R) → R → Bool

Check the transform and adjacent diagonals. The last computed diagonal is retained instead of multiplying all pivot polynomials.

Equations

• One or more equations did not get rendered due to their size.
• ops.triangular d swaps x✝² x✝¹ [] [] x✝ = ops.beq d (ops.signed swaps x✝)
• ops.triangular d swaps x✝⁴ x✝³ x✝² x✝¹ x✝ = false

def Hex.Matrix.DetWitness.map {R S : Type} (f : R → S) : DetWitness R → DetWitness S

Map all entries of a witness, for conversion from executable entries to their serialized representation.

Equations

• Hex.Matrix.DetWitness.map f (Hex.Matrix.DetWitness.triangular s t d) = Hex.Matrix.DetWitness.triangular s (List.map (List.map f) t) (f d)
• Hex.Matrix.DetWitness.map f (Hex.Matrix.DetWitness.singular v) = Hex.Matrix.DetWitness.singular (List.map f v)

def Hex.Matrix.DetWitness.row {R : Type u_1} : List (List R) → Nat → List R

A row of a serialized matrix, with the empty row beyond its end.

Equations

• Hex.Matrix.DetWitness.row [] x✝ = []
• Hex.Matrix.DetWitness.row (r :: tail) 0 = r
• Hex.Matrix.DetWitness.row (head :: rs) i.succ = Hex.Matrix.DetWitness.row rs i

def Hex.Matrix.DetWitness.replace {R : Type u_1} : List (List R) → Nat → List R → List (List R)

Replace a row, leaving out-of-range indices unchanged.

Equations

• Hex.Matrix.DetWitness.replace [] x✝¹ x✝ = []
• Hex.Matrix.DetWitness.replace (head :: rs) 0 x✝ = x✝ :: rs
• Hex.Matrix.DetWitness.replace (r :: rs) i.succ x✝ = r :: Hex.Matrix.DetWitness.replace rs i x✝

def Hex.Matrix.DetWitness.swap {R : Type u_1} (a b : Nat) (A : List (List R)) : List (List R)

Exchange two rows. Bounds and distinctness are checked separately.

Equations

• Hex.Matrix.DetWitness.swap a b A = Hex.Matrix.DetWitness.replace (Hex.Matrix.DetWitness.replace A a (Hex.Matrix.DetWitness.row A b)) b (Hex.Matrix.DetWitness.row A a)

def Hex.Matrix.DetWitness.permute {R : Type u_1} : List (Nat × Nat) → List (List R) → List (List R)

Apply row swaps in their recorded order.

Equations

• Hex.Matrix.DetWitness.permute [] x✝ = x✝
• Hex.Matrix.DetWitness.permute ((a, b) :: ss) x✝ = Hex.Matrix.DetWitness.permute ss (Hex.Matrix.DetWitness.swap a b x✝)

def Hex.Matrix.DetWitness.rowLengths {R : Type u_1} (n : Nat) : List (List R) → Bool

Verify the number of entries in every row.

Equations

• Hex.Matrix.DetWitness.rowLengths n [] = true
• Hex.Matrix.DetWitness.rowLengths n (r :: rs) = (r.length.beq n && Hex.Matrix.DetWitness.rowLengths n rs)

def Hex.Matrix.checkDetPolyList {R : Type} (ops : DetOps R) (n : Nat) (A : List (List R)) : DetWitness R → Bool

A determinant checker parameterized by serialized entry arithmetic. Canonicality, shapes and swap bounds are checked before the arithmetic. For nonempty triangular witnesses, the diagonal walk requires the first transform diagonal to be one and each later one to equal the preceding product diagonal. The empty case requires the value one.

Equations

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