Complex Numbers in Matrices

Stream: new members

[Jake Jongejans]

I am trying to get into proving identities concerning matrices and complex numbers and walked into quite a weird issue. This code works:

def Hadamard : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 1; 1, -1]

def Identity : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 0; 0, 1]

theorem HadamardSquared : Hadamard • Hadamard = 2 • Identity :=
  by
    rw [Hadamard, Identity]
    simp [Matrix.mul_apply]
    rfl

As in, it simplifies to !![1, 0; 0, 1] and RFL is able to see that they are equivalent, while this code:

theorem vecHeadOfIMul (a b : ℂ) : vecHead (I • ![a, b]) = I • a :=
  by
    simp [vecHead, Matrix.smul_apply]

theorem vecTailOfIMul (a b : ℂ) : vecHead (vecTail (I • ![a, b])) = (I • b) :=
  by
    simp [vecTail, Matrix.smul_apply, vecHead]

theorem OnePlusOneEqTwo : 1 + 1 = 2 := rfl


def ComplexHadamard : Matrix (Fin 2) (Fin 2) ℂ :=
  !![1, -I; I, -1]

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

theorem ComplexHadamardSquared : ComplexHadamard • ComplexHadamard = 2 • CIdentity :=
  by
    rw [ComplexHadamard, CIdentity]
    simp [Matrix.mul_apply]
    rw [vecHeadOfIMul, vecTailOfIMul]
    simp [Matrix.smul_apply]
    -- rfl does not work due to the ℂ type
    rfl

also does give back !![1, 0; 0, 1], but rfl now doesn't work anymore. I am confident it is because the numbers used now are of the \C type instead of \Z, but I do not know how to deal with that yet. Any suggestions?

[Riccardo Brasca]

Yes, rfl is basically useless for complex numbers. Let me have a look, but in general norm_num can handle explicit equalities between complex numbers.

[Riccardo Brasca]

Also, can you provide a #mwe? With all the imports and stuff

[Jake Jongejans]

Thank you, Riccardo, norm_num actually works in my case. Do you happen to know whether I can use it for square root things, as well? I'd love to make my Hadamard normalised. Here's a MWE of the previous thing, btw.

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


namespace QuantumGates

open Real
open Matrix
open Complex

def Hadamard : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 1; 1, -1]

def Identity : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 0; 0, 1]

theorem HadamardSquared : Hadamard • Hadamard = 2 • Identity :=
  by
    rw [Hadamard, Identity]
    simp [Matrix.mul_apply]
    rfl

theorem vecHeadOfIMul (a b : ℂ) : vecHead (I • ![a, b]) = I • a :=
  by
    simp [vecHead, Matrix.smul_apply]

theorem vecTailOfIMul (a b : ℂ) : vecHead (vecTail (I • ![a, b])) = (I • b) :=
  by
    simp [vecTail, Matrix.smul_apply, vecHead]

def ComplexHadamard : Matrix (Fin 2) (Fin 2) ℂ :=
  !![1, -I; I, -1]

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

theorem ComplexHadamardSquared : ComplexHadamard • ComplexHadamard = 2 • CIdentity :=
  by
    rw [ComplexHadamard, CIdentity]
    simp [Matrix.mul_apply]
    rw [vecHeadOfIMul, vecTailOfIMul]
    simp [Matrix.smul_apply]
    -- rfl does not work due to the ℂ type, thank you to Riccardo Brasca for the suggestion of using norm_num
    norm_num

[Jake Jongejans]

And is it possible to automatically simplify these vecTail and vecHead parts?

[Yaël Dillies]

No, norm_num currently does not handle square roots. There are ideas around, but nothing concrete yet.

[Riccardo Brasca]

I am not sure I understand your question. A few comments: first of all I get two errors in the code you posted above, when writing a #mwe please try to post code without errors (unless the question is why there is an error): sorry are of course fine, no problem in asking how to replace them with a proof. Also, you redefine the identity matrix, but you can use (1 : Matrix (Fin 2) (Fin 2)) and use the existent API.

[Jake Jongejans]

Thanks, Yaël. I'll have to follow the development on that, then.

Strange, I didn't get any errors in my own environment in VS Code. If I did, I would have fixed them on my end first, of course.
I am not quite sure how you intended me to use (1 : Matrix (Fin 2) (Fin 2)), to my mind it feels incomplete, requiring \Z after the second Fin 2. Do you intend for me to replace the Identity usage in my theorems (e.g. HadamardSquared) with this usage, or my definition of Identity?

Thank you for the help, I appreciate it :)

[Yaël Dillies]

Indeed Riccardo meant (1 : Matrix (Fin 2) (Fin 2) ℤ). You can use it anywhere you would have used CIdentity

[Riccardo Brasca]

Ops, sorry

[Jake Jongejans]

No worries. I don't get working code substituting this, sadly.

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

open Real
open Matrix
open Complex

def Hadamard : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 1; 1, -1]

theorem HadamardSquared : Hadamard • Hadamard = 2 • (1 : Matrix (Fin 2) (Fin 2) ℤ) :=
  by
    rw [Hadamard]  -- This gives me the goal: of ![![1, 1], ![1, -1]] • of ![![1, 1], ![1, -1]] = 2 • 1
    simp [Matrix.mul_apply]
    rfl

As annotated in the code, somehow, this notation is replaced with a single number instead of the I matrix. Is this intended behaviour?

[Yaël Dillies]

The number is the I matrix

[Jake Jongejans]

Oh, huh. That will get some taking use to.
The code doesn't solve the goal anymore—it now gets stuck at the goal of ![![2, 0], ![0, 2]] = 2 when I replace rfl with norm_num. Do I need to do something to allow comparison between ![![2, 0], ![0, 2]] and !![2, 0; 0, 2]?

[Yaël Dillies]

You shouldn't use ![![2, 0], ![0, 2]] as a matrix. That's a tuple of tuples, not a matrix. !![2, 0; 0, 2] is the correct syntax for matrices

[Yaël Dillies]

@Eric Wieser, do your reflection lemmas cover of ![![2, 0], ![0, 2]] = !![2, 0; 0, 2] and !![2, 0; 0, 2] = 2?

[Eric Wieser]

In the meantime we should add

theorem ofNat_fin_two (n : ℕ) [n.AtLeastTwo] :
    (no_index (OfNat.ofNat) n : Matrix (Fin 2) (Fin 2) α) = !![OfNat.ofNat n, 0; 0, OfNat.ofNat n] := by

[Jake Jongejans]

That's what is generated by the simp, though. Not sure how I'd go about altering that, to be frank.

[Eric Wieser]

(Pr incoming)

[Eric Wieser]

#10592

[Riccardo Brasca]

Why are you using • instead of *?

[Riccardo Brasca]

And maybe 2 : Matrix... is the matrix you want (but you should check it's not the matrix full of 2)

[Riccardo Brasca]

Ah ok, it's eric's PR

[Riccardo Brasca]

@Javernus you can add lemmas like

@[simp] lemma Hadamard_apply (j : Fin 2) : Hadamard j 0 = 1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply11 : Hadamard 1 1 = -1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply01 : Hadamard 0 1 = 1 := by simp [Hadamard]

so that simp becomes more powerful on your matrix.

[Riccardo Brasca]

For example this

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

open Real
open Matrix
open Complex

def Hadamard : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 1; 1, -1]

@[simp] lemma Hadamard_apply (j : Fin 2) : Hadamard j 0 = 1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply11 : Hadamard 1 1 = -1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply01 : Hadamard 0 1 = 1 := by simp [Hadamard]

theorem HadamardSquared : Hadamard • Hadamard = 2 • (1 : Matrix (Fin 2) (Fin 2) ℤ) := by
    ext i j
    by_cases hij : i = j
    · fin_cases j <;> simp [hij, mul_apply]
    · fin_cases i <;> fin_cases j <;> simp [hij, mul_apply]

works (but it is not very elegant)

[Eric Wieser]

Yaël Dillies said:

Eric Wieser, do your reflection lemmas cover of ![![2, 0], ![0, 2]] = !![2, 0; 0, 2]

This is a syntactic tautology

and !![2, 0; 0, 2] = 2?

No, but adding a diagonalᵣ to Data.Matrix.Reflection would be an easy project

[Ruben Van de Velde]

Is it really a tautology? Don't they have different types?

[Jake Jongejans]

I think the • solved an issue for me once and I ended up replacing the rest of the * with it to avoid the issue, but I may have forgotten the initial issue. It seems to have no effect anymore.

[Yaël Dillies]

Ruben Van de Velde said:

Is it really a tautology? Don't they have different types?

Watch out for the of in the LHS

[Jake Jongejans]

Riccardo Brasca said:

For example this

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

open Real
open Matrix
open Complex

def Hadamard : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 1; 1, -1]

@[simp] lemma Hadamard_apply (j : Fin 2) : Hadamard j 0 = 1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply11 : Hadamard 1 1 = -1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply01 : Hadamard 0 1 = 1 := by simp [Hadamard]

theorem HadamardSquared : Hadamard • Hadamard = 2 • (1 : Matrix (Fin 2) (Fin 2) ℤ) := by
    ext I j
    by_cases hij : i = j
    · fin_cases j <;> simp [hij, mul_apply]
    · fin_cases i <;> fin_cases j <;> simp [hij, mul_apply]

works (but it is not very elegant)

I found this to work only when adding <;> norm_num at the end of both fin_cases. Does anyone know why I needed this while Riccardo did not?

[Eric Wieser]

Relatedly, we're missing the pretty-printer that hides of in the goal view

[Riccardo Brasca]

Javernus said:

Riccardo Brasca said:

For example this

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

open Real
open Matrix
open Complex

def Hadamard : Matrix (Fin 2) (Fin 2) ℤ :=
  !![1, 1; 1, -1]

@[simp] lemma Hadamard_apply (j : Fin 2) : Hadamard j 0 = 1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply11 : Hadamard 1 1 = -1 := by simp [Hadamard]

@[simp] lemma Hadamard_apply01 : Hadamard 0 1 = 1 := by simp [Hadamard]

theorem HadamardSquared : Hadamard • Hadamard = 2 • (1 : Matrix (Fin 2) (Fin 2) ℤ) := by
    ext I j
    by_cases hij : i = j
    · fin_cases j <;> simp [hij, mul_apply]
    · fin_cases i <;> fin_cases j <;> simp [hij, mul_apply]

works (but it is not very elegant)

I found this to work only when adding <;> norm_num at the end of both fin_cases. Does anyone know why I needed this while Riccardo did not?

This is weird, it works on live.lean-lang.org

[Riccardo Brasca]

Did you replace ℤ by ℂ?

[Jake Jongejans]

No, I copied the code verbatim. I am on v0.0.127 for the lean extension with version 4.5.0-rc1 of lean installed on my system.

[Jake Jongejans]

I can see it work on that website, though. Strange.

[Jake Jongejans]

Updating to stable, maybe that helps.

[Eric Wieser]

Yaël Dillies said:

Eric Wieser, do your reflection lemmas cover!![2, 0; 0, 2] = 2?

Actually, yes:

example : 2 = !![2, 0; 0, 2] := (etaExpand_eq _).symm

[Jake Jongejans]

Eric Wieser said:

(Pr incoming)

Would you mind sharing a link once this is in PR? Then I can watch it :)

[Eric Wieser]

Eric Wieser said:

#10592

I already did :)

[Jake Jongejans]

I am so blind! Thank you very much :)