Parameterized computation core for the Bareiss elimination #

A computable model of a ring packages the representation the untrusted producer computes with: a value type V, its arithmetic (RingOps V), and the encoding between entry syntax and values. mkProducer assembles a Producer from a model's parts, and the tactic selects a model through the bareiss_ext extension registry.

Main definitions #

RingOps: the arithmetic of a model's value type.
bareissDecomp: fraction-free Gaussian elimination over a model's values.
mkProducer: assemble a producer from a model's parts.
bareiss_ext: the attribute registering a BareissExt 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

source

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

Type

Arithmetic of a model's value type.

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: total on the quotients of the elimination
isZero : V → Bool
The pivot zero test.

Instances For

source

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

Type

Decomposition data with entries in V: the values of the elimination, or the ring expressions constructed (V := Expr).

L : Array (Array V)
The lower-triangular transform.
swaps : Array (Nat × Nat)
The row swaps, in order. Stores the swaps instead of row re-indexing, since in common cases swaps are infrequent and therefore produce a smaller term to be checked by the kernel. The row permutation σ is later constructed by their product.
pivot : Array Nat
The pivot columns. The k-th entry is the column of the pivot in row k of the final echelon form.

Instances For

source

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

Mathlib.Tactic.Echelon.BareissData.mapM f d = do let __do_lift ← Array.mapM (fun (x : Array V) => Array.mapM f x) d.L pure { L := __do_lift, swaps := d.swaps, pivot := d.pivot }

Instances For

source

def Mathlib.Tactic.Echelon.Producer :

Type

A producer: run the elimination on the entries of a matrix literal, returning the decomposition constructed.

Equations

Mathlib.Tactic.Echelon.Producer = (Array (Array Lean.Expr) → Lean.MetaM (Mathlib.Tactic.Echelon.BareissData Lean.Expr))

Instances For

source

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.

Instances For

source

def Mathlib.Tactic.Echelon.mkProducer {V : Type} (ops : RingOps V) (prepare : Array (Array Lean.Expr) → Lean.MetaM (Array (Array V) × (BareissData V → BareissData V))) (mkEntry : V → Lean.MetaM Lean.Expr) :

Producer

Assemble a producer from a computation model's parts. ops describes the ring operation structure; prepare reifies the entries into the values the elimination runs on, plus a function restoring the resulting decomposition to one of the original matrix; mkEntry constructs the value back in the ring.

Equations