4.5. Worked example🔗

The block below builds the integer matrix with rows (2, 0, 1), (1, 3, 2), and (0, 1, 1), whose determinant is 3. The Bareiss route agrees with the Leibniz determinant on it, the identity has determinant one, and a matrix with a dependent row pair is singular.

open Hex Hex.Matrix

namespace HexBareissChapterExample

-- A = [[2, 0, 1], [1, 3, 2], [0, 1, 1]], det = 3.
private def A : Matrix Int 3 3 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 0 => 2 | 0, 1 => 0 | 0, 2 => 1
    | 1, 0 => 1 | 1, 1 => 3 | 1, 2 => 2
    | 2, 0 => 0 | 2, 1 => 1 | 2, 2 => 1
    | _, _ => 0

-- The Bareiss determinant is 3, agreeing with Leibniz.
#guard Matrix.bareiss A = 3
#guard Matrix.bareiss A = Matrix.det A

-- The packaged record reads off the same determinant.
#guard (Matrix.bareissData A).det = 3

-- The identity has determinant one.
#guard Matrix.bareiss (Matrix.identity (R := Int) 3) = 1

-- S = [[1, 2], [2, 4]]: dependent rows, so singular.
private def S : Matrix Int 2 2 :=
  Matrix.ofFn fun i j =>
    match i.val, j.val with
    | 0, 0 => 1 | 0, 1 => 2
    | 1, 0 => 2 | 1, 1 => 4
    | _, _ => 0

#guard Matrix.bareiss S = 0

end HexBareissChapterExample