CoqEAL bareiss — a fraction-free determinant certified against Matrix.det

CoqEAL's bareiss computes an exact integer determinant by fraction-free elimination, never leaving ℤ. This file proves the refinement at the base sizes: a ℤ-only, #eval-computable determinant certified equal to Mathlib's Matrix.det. At 2×2 the formula is a*d - b*c; at 3×3 it is the Sarrus/Bareiss expansion. Both avoid division, and both equal Matrix.det (det_fin_two, det_fin_three) — computing the classical determinant in ℤ.

def Transfer.Examples.CoqEAL.Bareiss.det2 (M : Matrix (Fin 2) (Fin 2) ℤ) : ℤ

Fraction-free 2×2 determinant (the Bareiss base case).

Equations

• Transfer.Examples.CoqEAL.Bareiss.det2 M = M 0 0 * M 1 1 - M 0 1 * M 1 0

theorem Transfer.Examples.CoqEAL.Bareiss.det2_eq (M : Matrix (Fin 2) (Fin 2) ℤ) : det2 M = M.det

det2 refines Mathlib's Matrix.det at size 2.

def Transfer.Examples.CoqEAL.Bareiss.det3 (M : Matrix (Fin 3) (Fin 3) ℤ) : ℤ

Fraction-free 3×3 determinant (the Sarrus/Bareiss expansion).

Equations

• Transfer.Examples.CoqEAL.Bareiss.det3 M = M 0 0 * (M 1 1 * M 2 2 - M 1 2 * M 2 1) - M 0 1 * (M 1 0 * M 2 2 - M 1 2 * M 2 0) + M 0 2 * (M 1 0 * M 2 1 - M 1 1 * M 2 0)

theorem Transfer.Examples.CoqEAL.Bareiss.det3_eq (M : Matrix (Fin 3) (Fin 3) ℤ) : det3 M = M.det

det3 refines Mathlib's Matrix.det at size 3.

Compute a classical determinant in ℤ

def Transfer.Examples.CoqEAL.Bareiss.sample : Matrix (Fin 2) (Fin 2) ℤ

A concrete matrix.

Equations

• Transfer.Examples.CoqEAL.Bareiss.sample = !![1, 2; 3, 4]