Certificate construction for the Bareiss decomposition

The certificate constructor from the decomposition data, and the default certifier mkCertificate, which currently proves the certificate conditions by decide +kernel.

This will eventually be generalised to a general certificate constructor that is parametric on a leaf normaliser.

Main definitions

• mkCertificate: build the Echelon.Decomposition certificate of a matrix literal.
• checkKernelDecide: check that equality in a ring reduces in the kernel.
• mkPerm, mkPivotLit, mkMatrixLit: elaborate the row permutation, the pivot function, and a matrix literal.

Implementation notes

The elimination records its echelon form U, making the product a certificate obligation of its own, L * A_σ = U, decided separately from the pivot condition on U.

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.mkMatrixLit {u : Lean.Level} (α : Q(Type u)) (m n : ℕ) (rows : Array (Array Lean.Expr)) : Q(Matrix (Fin «$m») (Fin «$n») «$α»)

Build the matrix literal of the row-major entries rows.

Equations

• Mathlib.Tactic.Echelon.mkMatrixLit α m n rows = (Matrix.of fun (i : Fin m) (j : Fin n) => rows[i]![j]!).mkLiteralQ

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.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») «$α»)) (entries : Array (Array Lean.Expr)) (data : BareissData Lean.Expr) : Lean.MetaM Q(Echelon.Decomposition «$A»)

Build the Echelon.Decomposition certificate of A from the decomposition data and entries, the parsed entries of A.

Equations

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