Prove that a matrix is Hermitian

Stream: new members

[Yunong Shi]

Hi I am very new to Lean. I am trying to prove that a concrete matrix to be Hermitian. Here are the definitions and my proof so far:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Hermitian
def PauliX : Matrix (Fin 2) (Fin 2) ℂ :=
  ![![0, 1], ![1, 0]]

example paulix_is_hermitian: (∀ i j: Fin 2, star (PauliX j i) = PauliX i j) := by
  intros i j
  fin_cases i; fin_cases j
  all_goals simp [PauliX, star, Matrix.vecCons]
  rfl
  rfl
  ext
  simp

Currently, my first goal is:

j: Fin 2
⊢ (Fin.cons (Fin.cons 0 (Fin.cons 1 ![])) (Fin.cons (Fin.cons 1 (Fin.cons 0 ![])) ![]) j 1).re =
  (Fin.cons 1 (Fin.cons 0 ![]) j).re

I admit that I used the help of chatGPT to get here. I am confused that:

1. I used fin_cases i; fin_cases j, but why there is still j in the goal?
2. How do I proceed?
   Thanks!

[Kyle Miller]

fin_cases i; fin_cases j should be fin_cases i <;> fin_cases j. Maybe ChatGPT is confused about Lean 3 vs Lean 4.

The ; ends up meaning "do fin_cases j on the first goal produced by fin_cases i"

[Yunong Shi]

Got it. Thanks very much!

Here is my new proof:

example paulix_is_hermitian: (∀ i j: Fin 2, star (PauliX j i) = PauliX i j) := by
  intros i j
  fin_cases i <;> fin_cases j
  all_goals simp [PauliX, star, Matrix.vecCons]
  rfl
  rfl
  rfl
  rfl

However, I still get the error:

failed to infer binder type when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

I find all types are clear in the proof, what is wrong?

[Eric Wieser]

Note that ![![0, 1], ![1, 0]] is not a matrix, and some lemmas won't fire as a result

[Eric Wieser]

The correct notation is !![0, 1; 1, 0]

[Eric Wieser]

Your issue here is that the syntax for example is wrong. example foo : True := sorry means example (foo : _) : true := sorry

[Eric Wieser]

Which is to say: examples don't have names. If you want to give it a name, you should use theorem

[Eric Wieser]

It's unfortunate that lean parses this in such a confusing way

[Yunong Shi]

Thanks! @Eric Wieser It resolves all the problem!

[Yunong Shi]

Now I am trying to prove a 2nd version of the theorem, which leverages the "IsHermitian" in mathlib.

theorem PauliX_is_still_hermitian: PauliX.IsHermitian := by
  ext
  all_goals simp

Currently, I am having this goal:

i✝x✝: Fin 2
⊢ (PauliX x✝ i✝).re = (PauliX i✝ x✝).re

Since i✝, x✝ are Fin 2, I want to fin_cases them. However, I cannot type them in the editor (the editor won't recognize them). How do I proceed?

[llllvvuu]

i didn't test, but most likely you want to ext i x or something

[Jireh Loreaux]

I'm curious. Does just rfl alone (no ext) work?

[Kyle Miller]

Or avoid unfolding the definition and start by rewriting with docs#Matrix.IsHermitian.ext_iff

[Yunong Shi]

Jireh Loreaux said:

I'm curious. Does just rfl alone (no ext) work?

unfortunately, it doesn't. It says type not match.

[Jireh Loreaux]

Sorry, what I asked before was nonsense. Thanks for checking though!

[Jireh Loreaux]

You may want to write some simp lemmas for PauliX, like this:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Hermitian

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

@[simp] lemma PauliX₁₁ : PauliX 0 0 = 0 := rfl
@[simp] lemma PauliX₁₂ : PauliX 0 1 = 1 := rfl
@[simp] lemma PauliX₂₁ : PauliX 1 0 = 1 := rfl
@[simp] lemma PauliX₂₂ : PauliX 1 1 = 0 := rfl

example : PauliX.IsHermitian := by
  apply Matrix.IsHermitian.ext
  intro i j
  fin_cases i <;> fin_cases j <;> simp

which makes the proof quite simple.

[Kyle Miller]

You can also pass PauliX as a simp lemma rather than writing those four lemmas:

example : PauliX.IsHermitian := by
  apply Matrix.IsHermitian.ext
  intro i j
  fin_cases i <;> fin_cases j <;> simp [PauliX]

[Yunong Shi]

Those are very helpful. Thanks! @Jireh Loreaux @Kyle Miller