Simplify matrix conjugate transpose

Stream: new members

[Yunong Shi]

I want to prove that the multiplication of a simple column vector and its conjugate transpose results in 1.

If I do:

def my_vec: Matrix (Fin 2) (Fin 1) ℂ := !![1; 0]

theorem my_vec_mul_one: my_vecᴴ * my_vec  = 1 := by
   ext i j
   fin_cases i <;> fin_cases j <;> simp [my_vec]

I will have 1 goal:

1 goal
case a.h.a.head.head
(((Matrix.of ![![1], ![0]])ᴴ * Matrix.of ![![1], ![0]]) 0 0).re = 1

Following the proof state, I naturally expand the definitions and extend the lastsimp [my_vec] with simp [my_vec, Matrix.conjTranspose, Matrix.map, Matrix.of, Equiv.refl] but it will give me more and more complicated proof state, and it ends up look like:

1 goal
case a.h.a.head.head
⊢ ((({ toFun := id, invFun := id, left_inv := _, right_inv := _ } fun i j ↦
          (starRingEnd ℂ) ({ toFun := id, invFun := id, left_inv := _, right_inv := _ } ![![1], ![0]] j i)) *
        { toFun := id, invFun := id, left_inv := _, right_inv := _ } ![![1], ![0]])
      0 0).re =
  1

I am wondering how to simplify matrix conjugate and matrix transpose and prove theorems like the above about them?

[Eric Wieser]

You should not simplify Matrix.of ever

[Eric Wieser]

Use of_apply instead, which is safer

[Yunong Shi]

Eric Wieser said:

Use of_apply instead, which is safer

Thanks. But it still doesn't help proceed with the proof.

With simp [my_vec, Matrix.conjTranspose, Matrix.map, Matrix.of_apply], I have the following proof state now.

1 goal
case a.h.a.head.head
⊢ (((Matrix.of fun i j ↦ (starRingEnd ℂ) (Matrix.vecCons 1 (fun i ↦ 0) j)) * Matrix.of ![![1], ![0]]) 0 0).re = 1

(Matrix.of_apply didn't seem to help proceed the proof..)

[Matt Diamond]

have you tried docs#Matrix.mul_apply? what about something like this?

theorem my_vec_mul_one: my_vecᴴ * my_vec = 1 := by
   ext i j
   rw [Matrix.mul_apply]
   simp [my_vec]
   sorry

[Matt Diamond]

that gets you to a goal of 1 = OfNat.ofNat 1 i j which seems pretty close

[Matt Diamond]

actually this should get you all the way:

theorem my_vec_mul_one: my_vecᴴ * my_vec = 1 := by
   ext i j
   rw [Subsingleton.elim i j, Matrix.mul_apply]
   simp [my_vec]

[Yunong Shi]

Matt Diamond said:

have you tried docs#Matrix.mul_apply? what about something like this?

theorem my_vec_mul_one: my_vecᴴ * my_vec = 1 := by
   ext i j
   rw [Matrix.mul_apply]
   simp [my_vec]
   sorry

Thanks! I indeed tried Matrix.mul_apply, but only after fin_cases i <;> fin_cases j. It reported a type error. But obviously I should do multiplication before break down to different cases.

[Yunong Shi]

Matt Diamond said:

actually this should get you all the way:

theorem my_vec_mul_one: my_vecᴴ * my_vec = 1 := by
   ext i j
   rw [Subsingleton.elim i j, Matrix.mul_apply]
   simp [my_vec]

Thank you! However, for me, I have to repeat it,

theorem my_vec_mul_one: my_vecᴴ * my_vec = 1 := by
   ext i j
   rw [Subsingleton.elim i j, Matrix.mul_apply]
   simp [my_vec]
   rw [Subsingleton.elim i j, Matrix.mul_apply]
   simp [my_vec]

[Matt Diamond]

Hmm, maybe I typed something wrong... this is what I was working with:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Notation

open Matrix

def my_vec: Matrix (Fin 2) (Fin 1) ℂ := !![1; 0]

theorem my_vec_mul_one: my_vecᴴ * my_vec = 1 := by
   ext i j
   rw [Subsingleton.elim i j, mul_apply]
   simp [my_vec]

[Matt Diamond]

I didn't need to repeat anything to close the goal

[Matt Diamond]

if that's not closing the goal for you, maybe your mathlib is out of date? I just put this together in the web editor

[Yunong Shi]

Matt Diamond said:

Hmm, maybe I typed something wrong... this is what I was working with:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Notation

open Matrix

def my_vec: Matrix (Fin 2) (Fin 1) ℂ := !![1; 0]

theorem my_vec_mul_one: my_vecᴴ * my_vec = 1 := by
   ext i j
   rw [Subsingleton.elim i j, mul_apply]
   simp [my_vec]

Interesting, I have the same set up except that I didn't import Notation. If I don't repeat it, I will still have the imaginary part left as a goal:

1 goal
ij: Fin 1
⊢ ((qubit_zeroᴴ * qubit_zero) i j).im = (OfNat.ofNat 1 i j).im

[Yunong Shi]

Ah, Matt Diamond it's about importing Notation. If I do that, I don't have to repeat.

[Matt Diamond]

that's interesting... if I leave out the Notation import I get an error around !![1;0]... must be a difference in mathlib versions

[Yunong Shi]

Actually, having Notation didn't solve it. It was just the Lean interpreter being slow. I still have to repeat.

[Yunong Shi]

Screenshot-2024-01-22-at-8.54.57-PM.png
And Lean playground gives a more unexpected error..

(Now it works!)

[Matt Diamond]

you just forgot open Matrix

[Yunong Shi]

Yes, now Lean playground works!

[Matt Diamond]

:+1:

[Yunong Shi]

Matt Diamond I have a bit trouble understanding the Subsingleton.elim tactic you used. Is it that for Fin 1, there should only be 1 element in it?

[Matt Diamond]

Yep, are you familiar with the concept of subsingletons? I means that the type has no more than 1 possible value (it could also be empty), so we can prove that every term of the type equals every other term. Fin 1 has a subsingleton instance because the only possible value is 0.

[Matt Diamond]

docs#Subsingleton