Expansion of products of list matrices

proveMul rewrites ListMatrix.mul l m n A B for list literals A and B to a literal whose entries are the sums of products of the entries, with the proof constructed manually instead of asking the kernel to perform reduction.

The entries are obtained by unfolding equations of ListMatrix.dotProduct one term at a time, instead of leaving the unfolding to the kernel, which can trigger evaluation of arithmetic prematurely.

def Mathlib.Tactic.Matrix.mkListCongr {u : Lean.Level} {α : Q(Type u)} : List ((a : Q(«$α»)) × (b : Q(«$α»)) × Q(«$a» = «$b»)) → (l₁ : Q(List «$α»)) × (l₂ : Q(List «$α»)) × Q(«$l₁» = «$l₂»)

Construct a proof term that [a₀, …] = [b₀, …] in List α from proofs of aᵢ = bᵢ. MVarId.congrN also works, but is much slower to elaborate.

Equations

• Mathlib.Tactic.Matrix.mkListCongr [] = ⟨q([]), ⟨q([]), q(⋯)⟩⟩
• Mathlib.Tactic.Matrix.mkListCongr (⟨a, ⟨b, h⟩⟩ :: es) = match Mathlib.Tactic.Matrix.mkListCongr es with | ⟨l₁, ⟨l₂, hl⟩⟩ => ⟨q(«$a» :: «$l₁»), ⟨q(«$b» :: «$l₂»), q(⋯)⟩⟩

structure Mathlib.Tactic.Matrix.DotProductEq {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (aα : Q(Add «$α»)) (mα : Q(Mul «$α»)) : Type

A dot product of two lists of entries, ListMatrix.dotProduct n l₁ l₂ = expr, with its proof.

• n : Q(Nat)

  The number of terms.

• l₁ : Q(List «$α»)

  The first list.

• l₂ : Q(List «$α»)

  The second list.

• expr : Q(«$α»)

  The right-hand side.

• proof : Q(ListMatrix.dotProduct unknown_1 unknown_2 unknown_3 = unknown_4)

  The proof.

def Mathlib.Tactic.Matrix.proveDotProduct {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (aα : Q(Add «$α»)) (mα : Q(Mul «$α»)) (m : Nat) (l₁ l₂ : Q(List «$α»)) : DotProductEq zα aα mα

The dot product of the first m entries of the list literals l₁ and l₂, ListMatrix.dotProduct m l₁ l₂ = fold, with m a numeral and fold the sum of the products a₀ * b₀ + (a₁ * b₁ + (… + 0)), unfolded by the equations of ListMatrix.dotProduct. The function takes the pre-built Expr for list literals instead of taking the list of entry literals and build it here, to avoid reconstructing the expressions multiple times.

Equations

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

structure Mathlib.Tactic.Matrix.MulEq {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (aα : Q(Add «$α»)) (mα : Q(Mul «$α»)) (l m n : Nat) : Type

The expansion of the product ListMatrix.mul l m n A B of two list literals with the associated proof term. The input matrices are put as fields of the structure to avoid over-long dependent type signatures downstream.

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

  The list literal of the first factor.

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

  The list literal of the second factor.

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

  The rows of the product, each entry the sum of the products of the entries.

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

  The list literal of rows.

• proof : Q(ListMatrix.mul «$l» «$m» «$n» unknown_1 unknown_2 = unknown_3)

  The proof.

def Mathlib.Tactic.Matrix.proveMul {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (aα : Q(Add «$α»)) (mα : Q(Mul «$α»)) (l m n : Nat) (listA listB : List (List Q(«$α»))) : MulEq zα aα mα l m n

Rewrite ListMatrix.mul l m n A B to the literal whose entries are the sums of products of the entries. listA/listB are the rows of the l × m and m × n matrix respectively. The rows are not checked against l, m and n.

Equations

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