Certificate construction for the Bareiss decomposition

certifyDecomposition constructs a proof of Echelon.Decomposition A L σ pivot from the given decomposition data. It proves that L * A_σ has the given pivots (through the product L * A_σ = U), and that L is lower triangular with nonzero diagonal entries.

The certify* functions assemble these proofs from facts about single entries, including the arithmetic equalities for the product and the non-zeroness for the diagonal entries of L and the pivots of U, which are established by the model's certifier (or the kernel).

Main definitions

• certifyDecomposition: builds the Echelon.Decomposition certificate from decomposition data.
• DecompositionCert: the internal certificate structure that includes the decomposition data, U and the product equation for downstream tactics.
• ListMatrixLit: an ofLists matrix together with its list literal and its rows of entries.

Implementation notes

The elimination records its echelon form U, making the product L * A_σ = U a certificate obligation of its own.

The product is proved on the list representation which the kernel checks more cheaply.

structure Mathlib.Tactic.Echelon.ListMatrixLit {u : Lean.Level} (α : Q(Type u)) (m n : ℕ) : Type

Three forms of one list-based matrix literal. This makes the argument list more succinct when a cert construction function needs to use multiple representations.

• matrix : Q(Matrix (Fin «$m») (Fin «$n») «$α»)

  The matrix, the ofLists term on lit.

• lit : Q(List (List «$α»))

  The list literal of rows.

• rows : List (List Q(«$α»))

  The rows of the matrix.

def Mathlib.Tactic.Echelon.ListMatrixLit.ofArray {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (m n : ℕ) (rows : Array (Array Q(«$α»))) : ListMatrixLit α m n

The ListMatrixLit of the matrix with rows rows.

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

The certifier that leaves each fact to the kernel's decide.

Equations

• Mathlib.Tactic.Echelon.decideCertifier α = { eq := fun (a b : Q(«$α»)) => Qq.mkDecideProofQ q(«$a» = «$b»), neZero := fun (_zα : Q(Zero «$α»)) (a : Q(«$α»)) => Qq.mkDecideProofQ q(«$a» ≠ 0) }

def Mathlib.Tactic.Echelon.certifyLowerTriangularDiagList {u : Lean.Level} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (k c : ℕ) (kQ cQ : Q(ℕ)) (rows : Q(List (List «$α»))) : Lean.MetaM Q(IsLowerTriangularDiagList «$kQ» «$cQ» «$rows»)

Construct the list-based IsLowerTriangularDiagList k c rows cert.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Echelon.certifyLowerTriangularDiagList certifier zα k 0 kQ cQ rows = pure q(⋯)

def Mathlib.Tactic.Echelon.certifyLowerTriangularDiag {u : Lean.Level} {m : ℕ} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (L : ListMatrixLit α m m) : Lean.MetaM ((have a := L.matrix; Q(«$a».IsLowerTriangular)) × have a := L.matrix; Q(∀ (i : Fin «$m»), «$a».diag i ≠ 0))

Prove that L is lower triangular with a nonzero diagonal.

Equations

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

def Mathlib.Tactic.Echelon.certifyPivotedList {u : Lean.Level} {n : ℕ} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (cols : List ℕ) (pivots : Q(List (Fin «$n»))) (rows : Q(List (List «$α»))) : Lean.MetaM Q(IsPivotedList «$pivots» «$rows»)

Construct the list-based IsPivotedList pivots rows cert.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Echelon.certifyPivotedList certifier zα [] pivots rows = pure q(⋯)

def Mathlib.Tactic.Echelon.certifyPivotedBy {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (certifier : EntryCertifier α) (zα : Q(Zero «$α»)) (U : ListMatrixLit α m n) (cols : List ℕ) (pivots : Q(List (Fin «$n»))) : Lean.MetaM (have a := U.matrix; Q(«$a».IsPivotedBy fun (i : Fin «$m») => pivotOfList «$pivots» ↑i))

Prove that U is pivoted by pivotOfList pivots from the rows of U, with certifier proving the pivot entries nonzero.

Equations

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

def Mathlib.Tactic.Echelon.certifyPermEq {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (A Aσ : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) (σ : Q(Equiv.Perm (Fin «$m»))) : Q(«$A».submatrix (⇑«$σ») id = «$Aσ»)

Prove the row arrangement A.submatrix σ id = Aσ.

Equations

• Mathlib.Tactic.Echelon.certifyPermEq A Aσ σ = Lean.Meta.mkExpectedPropHint q(⋯) q(«$A».submatrix (⇑«$σ») id = «$Aσ»)

def Mathlib.Tactic.Echelon.certifyRowsEq {u : Lean.Level} {α : Q(Type u)} (certifier : EntryCertifier α) (rows₁ rows₂ : List (List Q(«$α»))) : Lean.MetaM ((l₁ : Q(List (List «$α»))) × (l₂ : Q(List (List «$α»))) × Q(«$l₁» = «$l₂»))

Prove the row literals of rows₁ and rows₂ equal from the entrywise equations a = b, each proved by certifier.

Equations

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

def Mathlib.Tactic.Echelon.certifyProductEq {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (certifier? : Option (EntryCertifier α)) (cα : Q(AddCommMonoid «$α»)) {zα : Q(Zero «$α»)} {aα : Q(Add «$α»)} {mα : Q(Mul «$α»)} (mulEq : Matrix.MulEq zα aα mα m m n) (U : ListMatrixLit α m n) : Lean.MetaM (have a := U.matrix; have a_1 := mulEq.B; have a_2 := mulEq.A; Q(Matrix.ofLists «$m» «$m» «$a_2» * Matrix.ofLists «$m» «$n» «$a_1» = «$a»))

Prove the product L * Aσ = U from the expansion mulEq of the product of the row lists of L and Aσ, whose literals are mulEq.A and mulEq.B.

Equations

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

structure Mathlib.Tactic.Echelon.DecompositionCert {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) : Type

An internal structure recording the Echelon.Decomposition certificate of A with its data, together with the intermediate certificates that downstream tactics reuse (the echelon form U and the product equation stated on it).

• L : ListMatrixLit α m m

  The transformation matrix.

• σ : Q(Equiv.Perm (Fin «$m»))

  The row permutation on the rows of A.

• pivot : Q(Fin «$m» → WithTop (Fin «$n»))

  The pivot of the resulting echelon form.

• decomp : let a := self.L.matrix; Q(Echelon.Decomposition «$A» unknown_1 unknown_2 unknown_3)

  The decomposition certificate from the theory.

• U : ListMatrixLit α m n

  The echelon form.

• mul_eq : let a := self.U.matrix; let a_1 := self.L.matrix; Q(unknown_1 * «$A».submatrix (⇑unknown_2) id = unknown_3)

  The product equation.

def Mathlib.Tactic.Echelon.certifyDecomposition {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (certifier? : Option (EntryCertifier α)) (rα : Q(CommRing «$α»)) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) (entries : Array (Array Q(«$α»))) (data : BareissData Q(«$α»)) : Lean.MetaM (DecompositionCert rα A)

Build the DecompositionCert of A from the decomposition data and the parsed entries of A.

Equations

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