The Bareiss decomposition driver

Given a matrix literal A over a commutative domain, the entry point mkBareissDecomposition selects a computation model for the element type, runs the elimination, and elaborates a certificate ⟨L, σ, pivot, …⟩ : Echelon.Decomposition A, with the certificate conditions checked by the kernel via decide. The elimination itself is the model-parameterized bareissDecomp in Mathlib.Tactic.Echelon.Core.

Main definitions

• mkBareissDecomposition: produce and elaborate the decomposition of a matrix literal.
• BareissResult: the elaborated certificate together with the computed decomposition data.
• checkBareissApplicable: the applicability check of the Bareiss method.
• producerFor: select the computation model for a ring.

def Mathlib.Tactic.Echelon.mkFinNumeral (n i : ℕ) : Lean.MetaM Q(Fin «$n»)

Build the numeral of i in Fin $n.

Equations

• Mathlib.Tactic.Echelon.mkFinNumeral n i = Lean.Meta.mkNumeral q(Fin «$n») i

def Mathlib.Tactic.Echelon.mkPivotLit (m n : ℕ) (pivots : Array ℕ) : Lean.MetaM Q(Fin «$m» → WithTop (Fin «$n»))

Build the pivot literal ![↑c₀, …, ⊤, …] : Fin m → WithTop (Fin n), sending the first rows to their pivot columns and the remaining rows to ⊤.

Equations

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

def Mathlib.Tactic.Echelon.mkPerm (m : ℕ) (swaps : Array (ℕ × ℕ)) : Lean.MetaM Q(Equiv.Perm (Fin «$m»))

Build the permutation σ = swap a₀ b₀ * swap a₁ b₁ * ⋯ from the recorded swaps.

Equations

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

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

Check that equality with zero in α reduces to a verdict in the kernel, as the certificate conditions will be decided by kernel reduction. This needs to be changed when the cert-checking tactic is updated.

Equations

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

def Mathlib.Tactic.Echelon.checkBareissApplicable (R : Lean.Expr) : Lean.MetaM (Except Lean.MessageData Unit)

The applicability check of the Bareiss method, which requires a commutative domain with kernel-decidable equality.

Equations

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

def Mathlib.Tactic.Echelon.certifyCondition (name : String) (c : Q(Prop)) : Lean.MetaM Q(«$c»)

Prove the certificate condition c by a kernel-checked decide, with name naming the condition in errors.

Equations

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

def Mathlib.Tactic.Echelon.mkCertificate {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (_cr : Q(CommRing «$α»)) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) (L : Q(Matrix (Fin «$m») (Fin «$m») «$α»)) (σ : Q(Equiv.Perm (Fin «$m»))) (pivot : Q(Fin «$m» → WithTop (Fin «$n»))) : Lean.MetaM Q(Echelon.Decomposition «$A»)

Build the Echelon.Decomposition certificate of A from its constructed components, with the certificate conditions proven by kernel-checked decide.

Equations

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

def Mathlib.Tactic.Echelon.producerFor (R : Lean.Expr) : Lean.MetaM Producer

Select the computation model for the ring expression R: the first registered bareiss_ext extension that handles R, or the default rational model.

Equations

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

structure Mathlib.Tactic.Echelon.BareissResult : Type

The result of producing a decomposition by Bareiss.

• cert : Lean.Expr

  The elaborated Echelon.Decomposition certificate term.

• data : BareissData Lean.Expr

  The decomposition data underlying the certificate.

def Mathlib.Tactic.Echelon.mkBareissDecomposition {u : Lean.Level} (A : Lean.Expr) (m n : ℕ) (α : Q(Type u)) (entries : Array (Array Lean.Expr)) : Lean.MetaM BareissResult

Produce and elaborate the Echelon.Decomposition certificate of the matrix literal A.

Equations

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