Certificates for list-based matrix literals

This file contains common utilities for tactics that certify a computation on matrix literals from proofs about the lists of their rows.

Main definitions

• certifyProductEq: certify that the product of two matrix literals equals a third, given the expansion of the product by MulExpand.
• certifyRowsEq: certify the equality of two row literals from the equations of their entries.
• certifyOfArray: certifies that the row-major array of a matrix literal is equal to the array of the matrix's entries.

structure Mathlib.Tactic.Matrix.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.Matrix.ListMatrixLit.ofRows {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (m n : ℕ) (rows : List (List 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.Matrix.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, given as an array of rows.

Equations

• Mathlib.Tactic.Matrix.ListMatrixLit.ofArray zα m n rows = Mathlib.Tactic.Matrix.ListMatrixLit.ofRows zα m n (List.map Array.toList rows.toList)

def Mathlib.Tactic.Matrix.certifyRowsEq {u : Lean.Level} {α : Q(Type u)} (proveEq : (a b : Q(«$α»)) → Lean.MetaM Q(«$a» = «$b»)) (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 proveEq.

Equations

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

def Mathlib.Tactic.Matrix.certifyProductEq {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (proveEq? : Option ((a b : Q(«$α»)) → Lean.MetaM Q(«$a» = «$b»))) (cα : Q(AddCommMonoid «$α»)) {zα : Q(Zero «$α»)} {aα : Q(Add «$α»)} {mα : Q(Mul «$α»)} (mulEq : 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(ofLists «$m» «$m» «$a_2» * ofLists «$m» «$n» «$a_1» = «$a»))

Prove the product ofLists mulEq.A * ofLists mulEq.B = U from the list-based expansion of mulEq.

Equations

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

def Mathlib.Tactic.Matrix.ListMatrixLit.array {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (L : ListMatrixLit α m n) : Q(Array «$α»)

The literal of the row-major array of the entries of the matrix literal L.

Equations

• L.array = let mkListLitQ_1 := Qq.mkListLitQ L.rows.flatten; q(«$mkListLitQ_1».toArray)

def Mathlib.Tactic.Matrix.certifyOfArray {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (zα : Q(Zero «$α»)) (L : ListMatrixLit α m n) : Lean.MetaM (have a := L.array; have a_1 := L.matrix; Q(«$a_1».toArray = «$a»))

Prove that the row-major array of the m × n matrix literal L is the literal L.array.

Equations

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