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

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.

instance Mathlib.Tactic.Echelon.instNonemptyRingOps {V✝ : Type} [Nonempty V✝] : Nonempty (RingOps V✝)

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.

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.ModelAux {u : Lean.Level} (α : Q(Type u)) (V : Type) : Type

The underlying type of Model.

We want to allow the carrier type of this model to be any type. Unfortunately, making it a structure field causes the structure to live in Type 1, which doesn't work in IO/MetaM.

• 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 Mathlib.Tactic.Matrix.certifyProductEq can perform this optimization.

instance Mathlib.Tactic.Echelon.instNonemptyModelAux {u✝ : Lean.Level} {α✝ : Q(Type u✝)} {V✝ : Type} [Nonempty V✝] : Nonempty (ModelAux α✝ V✝)

def Mathlib.Tactic.Echelon.ModelType {u : Lean.Level} (α : Q(Type u)) : Type

An opaque model type that is used in place of the actual model type. We artificially add a parameter α to avoid mixing model types of different rings.

Equations

• Mathlib.Tactic.Echelon.ModelType α = (Mathlib.Tactic.Echelon.ModelValueTypeSpec✝ α).val

instance Mathlib.Tactic.Echelon.instNonemptyModelType {u : Lean.Level} (α : Q(Type u)) : Nonempty (ModelType α)

@[reducible, inline]

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

A computation model of a ring α. It should be constructed using Model.mk.

Equations

• Mathlib.Tactic.Echelon.Model α = Mathlib.Tactic.Echelon.ModelAux α (Mathlib.Tactic.Echelon.ModelType α)

def Mathlib.Tactic.Echelon.Model.mk {u : Lean.Level} {α : Q(Type u)} (V : Type) (model : ModelAux α V) : Model α

Construct a Model α from a ModelAux α V by replacing V with ModelType α using unsafeCast. This is safe if you use only one Model α at a time.

Equations

• Mathlib.Tactic.Echelon.Model.mk V model = Mathlib.Tactic.Echelon.Model.mk.unsafe_impl_2✝ V model

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 (Model α))

  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.