Parameterized computation core for the Bareiss elimination

bareissDecomp computes the transform L, the echelon form U, the row swaps and the pivot columns of an echelon decomposition by fraction-free elimination on a carrier of values.

As an optimisation, rows are scaled to clear their denominators (when applicable) before the elimination with the scales folded back into L afterwards.

A computation model supplies the carrier, its arithmetic operations (RingOps) and the encoding between entry syntax and values, and the tactic selects a model through the bareiss_ext extension registry.

Main definitions

• RingOps: the arithmetic of a model's carrier.
• Model: the computation model of a ring, including the encode/decode between the ring element and the carrier representation, and an optional entry certifier.
• EntryCertifier: the functions that prove the ring arithmetic facts about single entries that a certificate needs.
• bareissDecomp: runs fraction-free elimination over a model's carrier.
• BareissData: raw data of the computed decomposition.
• bareiss_ext: the attribute registering a computation model.

Implementation notes

The elimination in bareissDecomp maintains the invariant L * A_σ = W, where A_σ := A.submatrix σ id is the input with its rows in the arrangement σ accumulated so far and W is the working matrix. When the pivot search swaps the rows at positions r < p, the invariant must be restored against the new A_σ' = S * A_σ, where S is the permutation matrix of the transposition τ = (r, p):

S * W = S * L * (S⁻¹ * S) * A_σ = (S * L * S⁻¹) * A_σ'

so L is conjugated by the matrix of τ, as in LU factorisation with partial pivoting.

References

• [Bareiss, Sylvester's identity and multistep integer-preserving Gaussian elimination][bareiss1968]

structure Mathlib.Tactic.Echelon.RingOps (V : Type) : Type

Arithmetics on values of V.

• zero : V

  The zero value.

• one : V

  The one value.

• mul : V → V → V

  Multiplication.

• sub : V → V → V

  Subtraction.

• divExact : V → V → V

  Exact division.

• isZero : V → Bool

  The pivot zero test.

def Mathlib.Tactic.Echelon.RingOps.lift {V : Type} (ops : RingOps V) (decode : Lean.Expr → Option V) (encode : V → Lean.Expr) : RingOps Lean.Expr

The arithmetic of V on its literals with a decode-encode roundtrip per operation. This is less efficient than performing the elimination directly on V, but is a workaround for a restriction in the registry (see Carrier). Certificate construction is the bottleneck so this does not lead to much overall performance degradation. A literal decode rejects is read as 0 (should never happen for the literals provided by encode).

Equations

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

structure Mathlib.Tactic.Echelon.BareissData (V : Type) : Type

Decomposition data with entries in V, the carrier of the elimination or Expr once the entries are encoded.

• L : Array (Array V)

  The lower-triangular transform.

• U : Array (Array V)

  The echelon form, the final working matrix L * A_σ of the elimination.

• swaps : Array (Nat × Nat)

  The row swaps, in order. Swaps are infrequent in common cases, so their product is a smaller term for the kernel than a row permutation.

• pivot : Array Nat

  The pivot columns. The k-th entry is the column of the pivot in row k of the final echelon form.

def Mathlib.Tactic.Echelon.BareissData.mapM {V W : Type} (f : V → Lean.MetaM W) (d : BareissData V) : Lean.MetaM (BareissData W)

Map over the entries of the transform.

Equations

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

def Mathlib.Tactic.Echelon.BareissData.rowOrder {V : Type} (d : BareissData V) : Array Nat

The row arrangement of the swaps: the entry at position i is the original row index that the swaps move to position i, that is, σ i.

Equations

• d.rowOrder = Array.foldl (fun (ord : Array Nat) (x : Nat × Nat) => match x with | (a, b) => ord.swapIfInBounds a b) (Array.range d.L.size) d.swaps

def Mathlib.Tactic.Echelon.bareissDecomp {V : Type} (ops : RingOps V) (A : Array (Array V)) : Lean.MetaM (BareissData V)

Core algorithm of fraction-free Gaussian elimination, with the arithmetic supplied by the model.

A single sweep accumulates the transform L alongside the working matrix W, maintaining L * (A.submatrix σ id) = W for the row arrangement σ so far. The divisions are exact by Sylvester's identity, although the data-only computation does not prove that.

Equations

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

inductive Mathlib.Tactic.Echelon.Carrier : Type

The carriers a model computes on, the integers or expressions of the ring. The most direct method is for a model to name the carrier type directly as a field of the extension, but that puts the model in a higher universe level, and the registry can only store Type 0 elements.

• int : Carrier
• expr : Carrier

@[reducible, inline]

abbrev Mathlib.Tactic.Echelon.Carrier.type : Carrier → Type

The type of the values of a carrier.

Equations

• Mathlib.Tactic.Echelon.Carrier.int.type = Int
• Mathlib.Tactic.Echelon.Carrier.expr.type = Lean.Expr

structure Mathlib.Tactic.Echelon.EntryCertifier {u : Lean.Level} (α : Q(Type u)) : Type

An entry certifier proves arithmetic facts about expressions of the ring α that the certificates need. eq proves an equation a = b, such as an unreduced entry of a matrix product equal to its computed value, and neZero proves a ≠ 0, such as for a pivot entry.

eq is typically built on a normalizer, while neZero may depend on bespoke methods if a normalizer cannot provide a disequality proof.

• eq (a b : Q(«$α»)) : Lean.MetaM Q(«$a» = «$b»)

  Prove a = b.

• neZero (zα : Q(Zero «$α»)) (a : Q(«$α»)) : Lean.MetaM Q(«$a» ≠ 0)

  Prove a ≠ 0, stated with the caller's Zero instance zα.

structure Mathlib.Tactic.Echelon.Model {u : Lean.Level} (α : Q(Type u)) (V : Type) : Type

A computation model of the ring α on the carrier V.

• ops : RingOps V

  The arithmetic of the carrier.

• evalEntry : Q(«$α») → Lean.MetaM (V × Option V)

  Evaluate an entry to a value with an optional denominator for the row scaling. (n, some d) denotes n / d with d nonzero, and (n, none) denotes n.

• commonMultiple : V → V → V

  A nonzero common multiple for eliminating the denominators (ops.mul by default). A carrier type with a cheap lcm could supply it as an optimisation to keep the scaled entries small.

• mkEntry : V → Lean.MetaM Q(«$α»)

  The expression of the ring denoting a value.

• entryCertifier? : Option (EntryCertifier α)

  An optional certifier for the ring, or none to leave the conditions to the kernel. With none, the kernel checks the decomposition product L * A_σ = U by evaluating the list-based form as a whole without assembling it from per-entry proofs, which is faster than applying decideCertifier on every entry. As a result this field is optional rather than taking a default value, so that certifyProductEq can perform this optimization.

def Mathlib.Tactic.Echelon.scaleRows {V : Type} (ops : RingOps V) (commonMultiple : V → V → V) (rows : Array (Array (V × Option V))) : Array (Array V) × Array (Option V)

Clear the denominators of the rows before the decomposition algorithm.

Equations

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

def Mathlib.Tactic.Echelon.restoreScaling {V : Type} (ops : RingOps V) (scales : Array (Option V)) (d : BareissData V) : BareissData V

Fold the row scales into the transform after the decomposition algorithm. Column j of L is multiplied by the scale of the row that ends up in position j after permutation.

Equations

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

structure Mathlib.Tactic.Echelon.BareissExt : Type

An extension of the Bareiss ring computation model.

• model? {u : Lean.Level} (α : Q(Type u)) : Lean.MetaM (Option ((c : Carrier) × Model α c.type))

  The model for the element type α and its carrier, or none if the extension does not handle α.

def Mathlib.Tactic.Echelon.mkBareissExt (n : Lean.Name) : Lean.ImportM BareissExt

Read a bareiss_ext extension from a declaration of the right type.

Equations

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

opaque Mathlib.Tactic.Echelon.bareissExt : Lean.ScopedEnvExtension Lean.Name (Lean.Name × BareissExt) (Array (Lean.Name × BareissExt))

Environment extension for the bareiss_ext computation models. Uses a simple array to store the name-extension pairs for now.