Simp and matrix multiplication

Stream: new members

[Yakov Pechersky]

I've been struggling to prove that a matrix multiplication does not commute. My ite matrix definitions kept simplifying wrong. I think I figured out that there is an issue with what simp does to matrix multiplication. It relies on pi.mul_apply when it doesn't make sense in the context. Seems to also depend on whether * or • is used as the operation. Here is a mwe comparing the different simp results depending on the precise statement to be proved:

import data.real.basic
import data.matrix.notation
import linear_algebra.matrix

example : ∃ (S : matrix (fin 2) (fin 2) ℝ) (T : matrix (fin 2) (fin 2) ℝ),
          S * T ≠ T * S :=
begin
  set X := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℝ),
  set Y := (![![0, 1], ![0, 0]] : matrix (fin 2) (fin 2) ℝ),
  have : X * Y ≠ Y * X,
    { have : (X • Y) (0 : fin 2) (0 : fin 2) ≠ (Y • X) (0 : fin 2) (0 : fin 2),
        intros hx,
        simp [matrix.mul_eq_mul] at hx, -- hx : (X * Y) 0 0 = (Y * X) 0 0
        sorry,
       -- the following example only works if linear_algebra.matrix is imported
      have : (X • Y) (0 : fin 2) (0 : fin 2) ≠ (Y • X) (0 : fin 2) (0 : fin 2),
        intros hx, -- we can try squeeze_simp, which suggests:
        simp only [algebra.id.smul_eq_mul] at hx, -- hx : (X * Y) 0 0 = (Y * X) 0 0
        sorry,
      have : (X * Y) (0 : fin 2) (0 : fin 2) ≠ (Y * X) (0 : fin 2) (0 : fin 2),
        intros hx, -- we can try squeeze_simp, which suggests instead
        simp only [pi.mul_apply] at hx, -- hx : X 0 0 * Y 0 0 = Y 0 0 * X 0 0
        sorry,
      have : (X * Y) (0 : fin 2) (0 : fin 2) ≠ (Y * X) (0 : fin 2) (0 : fin 2),
        intros hx, -- we can try simp, which uses pi.mul_apply
        simp at hx, -- hx : X 0 0 * Y 0 0 = Y 0 0 * X 0 0
        sorry,
    },
  sorry,
end

[Yakov Pechersky]

Even dsimp [matrix.mul] splits is into a X 0 1 * Y 0 1.

[Yakov Pechersky]

Is this an issue of a difference between \bu and \cdot?

[Yakov Pechersky]

I can't imagine that it is, since the latter two examples use * directly.

[Yakov Pechersky]

norm_num also expands it into a X 0 1 * Y 0 1

[Yakov Pechersky]

But for some reason, specifying matrix.mul works:

      have : matrix.mul X Y (0 : fin 2) (1 : fin 2) ≠ matrix.mul Y X (0 : fin 2) (1 : fin 2),
        intros hx, -- specifying matrix.mul works
        norm_num at hx -- solved

[Yakov Pechersky]

And on the top level, using * works fine too.

import data.real.basic
import data.matrix.notation

example : ∃ (S : matrix (fin 2) (fin 2) ℝ) (T : matrix (fin 2) (fin 2) ℝ),
          S * T ≠ T * S :=
begin
  set X := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℝ),
  set Y := (![![0, 1], ![0, 0]] : matrix (fin 2) (fin 2) ℝ),
  use [X, Y],
  intros h,
  rw <-matrix.ext_iff at h,
  specialize h 0 1,
  norm_num at h,
  exact h,
end

[Johan Commelin]

It seems that matrix.ext_iff is stated in the "wrong" direction compared to the rest of the library.

[Scott Morrison]

You can also just use congr_fun, rather than going via matrix.ext_iff and specialize:

import data.real.basic
import data.matrix.notation

variables {R : Type*} [ring R] [nonzero R]

example : ∃ (S : matrix (fin 2) (fin 2) R) (T : matrix (fin 2) (fin 2) R),
          S * T ≠ T * S :=
begin
  use [![![1, 0], ![0, 0]], ![![0, 1], ![0, 0]]],
  intro h,
  simpa using congr_fun (congr_fun h 0) 1,
end

[Anne Baanen]

Hmm, so simp lemmas are stated in terms of matrix.mul instead of *, but somehow matrix.mul_eq_mul doesn't fire to turn the * into matrix.mul

[Anne Baanen]

Aha, (X * Y) i j gets simplified to X i j * Y i j, because X : fin 2 → fin 2 → ℝ instead of X : matrix (fin 2) (fin 2) ℝ, so it picks up the pointwise multiplication instance.

[Anne Baanen]

But giving explicit types doesn't work:

  set X : matrix (fin 2) (fin 2) ℝ := ![![1, 0], ![0, 0]],
  set Y : matrix (fin 2) (fin 2) ℝ := ![![0, 1], ![0, 0]],

gives a tactic state:

X : fin 1.succ → fin 2 → ℝ := ![![1, 0], ![0, 0]],
Y : fin 1.succ → fin 2 → ℝ := ![![0, 1], ![0, 0]]
⊢ ∃ (S T : matrix (fin 2) (fin 2) ℝ), S * T ≠ T * S

[Anne Baanen]

This seems like a bug in the set tactic, because let results in matrix (fin 2) (fin 2) ℝ, after which simp is able to reduce hx to false, what we want.

[Anne Baanen]

Weirdly, change matrix (fin 2) (fin 2) ℝ at X fails:

match failed
state:
Y : fin 1.succ → fin 2 → ℝ := ![![0, 1], ![0, 0]]
⊢ let X : fin 1.succ → fin 2 → ℝ := ![![1, 0], ![0, 0]]
  in ∃ (S T : matrix (fin 2) (fin 2) ℝ), S * T ≠ T * S

[Bryan Gin-ge Chen]

Anne Baanen said:

This seems like a bug in the set tactic, because let results in matrix (fin 2) (fin 2) ℝ, after which simp is able to reduce hx to false, what we want.

Do you mind creating a tracking issue for this? I don't want this to get lost...

[Anne Baanen]

Done: #3111.