Proving product of two matrices

Stream: maths

[Anirudh Suresh]

What are tactics to use to prove that the product of simple matrices are equal to another matrix?

import Mathlib
open scoped Matrix


theorem t1:![![1, 0, 0, 0],
             ![0, 1, 0, 0],
             ![0, 0, 0, 1],
             ![0, 0, 1, 0]] *


           ![![1, 0, 0, 0],
             ![0, 0, 0, 1],
             ![0, 0, 1, 0],
             ![0, 1, 0, 0]] *


           ![![1, 0, 0, 0],
             ![0, 1, 0, 0],
             ![0, 0, 0, 1],
             ![0, 0, 1, 0]] =


          ![![1, 0, 0, 0],
            ![0, 0, 1, 0],
            ![0, 1, 0, 0],
            ![0, 0, 0, 1]]:=
  by {
    sorry
  }

[Aaron Liu]

import Mathlib
open scoped Matrix


example : ![![1, 0, 0, 0],
            ![0, 1, 0, 0],
            ![0, 0, 0, 1],
            ![0, 0, 1, 0]] *


          ![![1, 0, 0, 0],
            ![0, 0, 0, 1],
            ![0, 0, 1, 0],
            ![0, 1, 0, 0]] *


          ![![1, 0, 0, 0],
            ![0, 1, 0, 0],
            ![0, 0, 0, 1],
            ![0, 0, 1, 0]] =


          ![![1, 0, 0, 0],
            ![0, 0, 1, 0],
            ![0, 1, 0, 0],
            ![0, 0, 0, 1]] := by
  -- tactic 'decide' proved that the proposition ... is false
  decide

[Eric Wieser]

Matrices are !![...] not ![![...]]

[Eric Wieser]

If you picked up the ![![ from documentation somewhere, can you say where so that we can fix it?

[Anirudh Suresh]

I tried to define it as a vector of vectors which is why I made that mistake. The type checker did not give me any error so I assumed it was right.

[Eric Wieser]

What you got was a vector of vectors, which has elementwise multiplication

[Anirudh Suresh]

import Mathlib
open scoped Matrix

def A : Matrix (Fin 4) (Fin 4) ℂ :=
  ![ ![1, 0, 0, 0],
     ![0, 0, 0, 1],
     ![0, 0, 1, 0],
     ![0, 1, 0, 0] ]

Why is the type checker not showing any error for this though when they are clearly different types in terms of how the operations work on them

[Eric Wieser]

Ah, this is indeed unfortunate. The problem is that the types are equal at semireducible equality

[Eric Wieser]

Adding a Matrix.of to explicit convert from that representation to a Matrix is the right thing to do, but I agree it's not very discoverable

[Yakov Pechersky]

import Mathlib
open scoped Matrix


example : Matrix.of ![![1, 0, 0, 0],
            ![0, 1, 0, 0],
            ![0, 0, 0, 1],
            ![0, 0, 1, 0]] *


          Matrix.of ![![1, 0, 0, 0],
            ![0, 0, 0, 1],
            ![0, 0, 1, 0],
            ![0, 1, 0, 0]] *


          Matrix.of ![![1, 0, 0, 0],
            ![0, 1, 0, 0],
            ![0, 0, 0, 1],
            ![0, 0, 1, 0]] =


          Matrix.of ![![1, 0, 0, 0],
            ![0, 0, 1, 0],
            ![0, 1, 0, 0],
            ![0, 0, 0, 1]] := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp

[Yakov Pechersky]

decide also works, but that's because of no free vars. fin_cases followed by simp will work in a situation where there are variables in the matrices.

[Anirudh Suresh]

ahh I see. Thanks!