Simplifying transpose of a matrix

Stream: Is there code for X?

[Heather Macbeth]

@Eric Wieser Can you help with a matrix simp which your PR #14992 seems to have broken? I am comparing this commit (after) with this commit (before) since there are olean caches available for both of them. There are 7 commits between them and only #14992 relates to matrices.

Here is a code snippet which breaks:

import data.matrix.notation

variables {R : Type*} [comm_ring R] [star_ring R]
local notation `⋆` := @has_star.star (matrix (fin 2) (fin 2) R) _

example (a b c d : R) :
  matrix.vec_mul ![a, b] (⋆ ![![c, a], ![d, a]]) 0 = a * star c + b * star a :=
begin
  simp [matrix.vec_head, matrix.vec_tail],
end

The point seems to be that the simp-lemma docs#matrix.cons_vec_mul changed statement in #14992 and the new, more specific statement only applies to matrices of the form docs#matrix.of -- but ⋆ ![![c, a], ![d, a]] is not of this form.

[Heather Macbeth]

The !![c, a; d, a] notation is not available at the time of these commits, but if you jump to the commit a few days later where that notation is defined (#14991), the following variant also breaks:

example (a b c d : R) :
  matrix.vec_mul ![a, b] (star !![c, a; d, a]) 0 = a * star c + b * star a :=
begin
  simp [matrix.vec_head, matrix.vec_tail],
end

[Eric Wieser]

Can you squeeze the simp on the commit that works?

[Eric Wieser]

I need to wait for my laptop to cool down, but then will take a look

[Eric Wieser]

Note that in the brief period where !![] notation didn't exist, the intended spelling was of ![![]]

[Heather Macbeth]

Eric Wieser said:

Can you squeeze the simp on the commit that works?

Thanks!

simp only [matrix.vec_head, matrix.vec_tail, matrix.cons_vec_mul, function.comp_app, fin.succ_zero_eq_one, matrix.empty_vec_mul,
  add_zero, pi.add_apply, pi.smul_apply, matrix.star_apply, matrix.cons_val_zero, algebra.id.smul_eq_mul,
  matrix.cons_val_one]

[Eric Wieser]

Also, on matrices I think ᴴ is prefered to star as the former works on rectangular matrices too

[Eric Wieser]

This proves it:

example (a b c d : R) :
  matrix.vec_mul ![a, b] (!![c, a; d, a]ᴴ) 0 = a * star c + b * star a :=
begin
  simp [matrix.vec_mul_conj_transpose, mul_comm],
end

[Heather Macbeth]

I see. Should docs#matrix.vec_mul_conj_transpose be a simp-lemma then?

[Eric Wieser]

It's not obvious to me that we should necessarily expect simp to behave well on concrete matrices

[Eric Wieser]

The missing pieces in comparison to the original proof are the lemmas transpose_of and conj_transpose_of, which we should probably have, but don't obvious make sense as simp lemmas

[Eric Wieser]

Here's another trivial lemma that simp can't prove:

example (a b c d : R) :
  !![c, a; d, a].map (+ 1) = !![c + 1, a + 1; d + 1, a + 1] :=
by simp

[Eric Wieser]

Back to your original problem: my opinion is that we should be writing a tactic to generate the following proof:

import data.matrix.reflection

example (a b c d : R) :
  matrix.vec_mul ![a, b] (!![c, a; d, a]ᴴ) 0 = a * star c + b * star a :=
congr_fun (matrix.vec_mulᵣ_eq (_ : _ → R) _).symm 0

[Eric Wieser]

I had a mathlib3 PR that did this (though only for matrix.mul while I waited for feedback), but it drowned in the porting tide

[Eric Wieser]

The matrix.vec_mulᵣ_eq lemmas made it to mathlib though

[Heather Macbeth]

Eric Wieser said:

It's not obvious to me that we should necessarily expect simp to behave well on concrete matrices

Here's another trivial lemma that simp can't prove:

example (a b c d : R) :
  !![c, a; d, a].map (+ 1) = !![c + 1, a + 1; d + 1, a + 1] :=
by simp

I have generally expected simp to be able to behave well on element evaluations of concrete matrices. In your example,

ext i j; fin_cases i; fin_cases j; simp,

works.

[Eric Wieser]

If we want that to work I think we want a lemma of the form matrix.vec_mul (cons x xs) A i = x * A 0 i + matrix.vec_mul xs (A.submatrix fin.succ id)

[Eric Wieser]

In fact, I think such a lemma is defeq to the current docs#matrix.cons_vec_mul

[Eric Wieser]

Here's the solution that I think we want:

@[simp] lemma cons_vec_mul_apply
  {α} [semiring α] {n : ℕ} {o' : Type*} (x : α) (v : fin n → α) (B : matrix (fin n.succ) o' α)
    (i : o'):
  vec_mul (vec_cons x v) B i = x * B 0 i + vec_mul v (B.submatrix fin.succ id) i :=
congr_fun (cons_vec_mul x v B) i

example (a b c d : R) :
  matrix.vec_mul ![a, b] (!![c, a; d, a]ᴴ) 0 = a * star c + b * star a :=
by simp

[Joseph Myers]

Heather Macbeth said:

I have generally expected simp to be able to behave well on element evaluations of concrete matrices. In your example,

ext i j; fin_cases i; fin_cases j; simp,

works.

Note that we haven't worked out how to make that work in Lean 4, or at least haven't implemented it in mathlib4 (test/matrix.lean in mathlib4 thus has the relevant tests commented out).

[Eric Wieser]

I would guess it's easier in lean 4 as we can match against ofNat (succ n) instead of needing to deal with bit0

[Eric Wieser]

The tests in question are here, cc @Heather Macbeth

[Eric Wieser]

(nevermind)

[Eric Wieser]

My attempt at this was

@[simp]
lemma vecCons_ofNat_succ
  {α : Type _} {n : ℕ} [NeZero n] (x : α) (xs : Fin n → α) (m : ℕ) :
  Matrix.vecCons x xs (OfNat.ofNat (Nat.succ m)) = if Nat.succ m % Nat.succ n = 0 then x else xs (OfNat.ofNat (m % Nat.succ n)) := sorry

but this doesn't behave usefully

[Eric Wieser]

Hmm, actually my test was bad.Maybe it's ok...