def Hex.Matrix.Lists.all (p : Nat → Bool) : Nat → Bool

Check a predicate at every index below a natural bound.

Equations

• Hex.Matrix.Lists.all p 0 = true
• Hex.Matrix.Lists.all p n.succ = (Hex.Matrix.Lists.all p n && p n)

def Hex.Matrix.Lists.entry {α : Type u_1} (zero : α) : List α → Nat → α

List lookup with an explicit default and structural recursion.

Equations

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

def Hex.Matrix.Lists.get (rows : List (List Int)) (i j : Nat) : Int

Integer entry of a row list, padded with zeros.

Equations

• Hex.Matrix.Lists.get rows i j = Hex.Matrix.Lists.entry 0 (Hex.Matrix.Lists.entry [] rows i) j

def Hex.Matrix.Lists.shape (n m : Nat) (rows : List (List Int)) : Bool

Exact rectangular dimensions, including empty rows.

Equations

• Hex.Matrix.Lists.shape n m rows = (rows.length.beq n && rows.all fun (row : List Int) => row.length.beq m)

def Hex.Matrix.Lists.dot : List Int → List Int → Int

A structurally recursive integer dot product.

Equations

• Hex.Matrix.Lists.dot (a :: as) (b :: bs) = (a.mul b).add (Hex.Matrix.Lists.dot as bs)
• Hex.Matrix.Lists.dot x✝¹ x✝ = 0

def Hex.Matrix.Lists.column (j : Nat) : List (List Int) → List Int

A column of a row list.

Equations

• Hex.Matrix.Lists.column j [] = []
• Hex.Matrix.Lists.column j (row :: rows) = Hex.Matrix.Lists.entry 0 row j :: Hex.Matrix.Lists.column j rows

def Hex.Matrix.Lists.product (n m : Nat) (a b : List (List Int)) (c : Nat → Nat → Int) : Bool

Check a matrix product against a supplied entry function. Shapes are checked separately by the caller.

Equations

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

def Hex.Matrix.Lists.identity (i j : Nat) : Int

The entry function for an identity matrix.

Equations

• Hex.Matrix.Lists.identity i j = if i.beq j = true then 1 else 0

def Hex.Matrix.Lists.diagonal (d : List Int) (i j : Nat) : Int

The entry function for a rectangular diagonal matrix.

Equations

• Hex.Matrix.Lists.diagonal d i j = if i.beq j = true then Hex.Matrix.Lists.entry 0 d i else 0

theorem Hex.Matrix.Lists.all_iff (p : Nat → Bool) (n : Nat) : all p n = true ↔ ∀ (i : Nat), i < n → p i = true

theorem Hex.Matrix.Lists.entry_eq_getD {α : Type u_1} (zero : α) (xs : List α) (i : Nat) : entry zero xs i = xs.getD i zero

def Hex.Matrix.Lists.add : List Int → List Int → List Int

Exact unnormalized integer coefficient addition.

Equations

• Hex.Matrix.Lists.add [] x✝ = x✝
• Hex.Matrix.Lists.add x✝ [] = x✝
• Hex.Matrix.Lists.add (x_2 :: xs) (y :: ys) = x_2.add y :: Hex.Matrix.Lists.add xs ys

def Hex.Matrix.Lists.scale (a : Int) (xs : List Int) : List Int

Integer coefficient scaling.

Equations

• Hex.Matrix.Lists.scale a xs = List.map a.mul xs

def Hex.Matrix.Lists.mul : List Int → List Int → List Int

Structural integer coefficient convolution.

Equations

• Hex.Matrix.Lists.mul [] x✝ = []
• Hex.Matrix.Lists.mul (x_2 :: xs) x✝ = Hex.Matrix.Lists.add (Hex.Matrix.Lists.scale x_2 x✝) (0 :: Hex.Matrix.Lists.mul xs x✝)

def Hex.Matrix.rowLists {R : Type u_1} {n m : Nat} (A : Matrix R n m) : List (List R)

The row-major list observation used in matrix denotation proofs.

Equations

• A.rowLists = List.map Vector.toList A.rows.toList

theorem Hex.Matrix.length_rowLists {R : Type u_1} {n m : Nat} (A : Matrix R n m) : A.rowLists.length = n

theorem Hex.Matrix.entry_rowLists {R : Type u_1} {n m : Nat} (A : Matrix R n m) (i : Fin n) : Lists.entry [] A.rowLists ↑i = A[i].toList

theorem Hex.Matrix.get_rowLists {R : Type u_1} {n m : Nat} [Zero R] (A : Matrix R n m) (i : Fin n) (j : Fin m) : Lists.entry 0 (Lists.entry [] A.rowLists ↑i) ↑j = A[i][j]