what the heq, PosSemidef

Stream: new members

[Alex Meiburg]

So I'm trying to prove some things about PSD matrices and I ran into issues where sqrt requires a proof that the matrix is PSD, which meant I got HEq issues because PosSemidef A and PosSemidef B are different types even if A = B. A minimized chunk of my proof looks like this:

import Mathlib

variable {m n R : Type*} [Fintype m] [Fintype n]
variable [RCLike R] [DecidableEq n] [DecidableEq m]

namespace Matrix
open scoped ComplexOrder

theorem sqrt_neg (A : Matrix m n R) : (Matrix.posSemidef_conjTranspose_mul_self (-A)).sqrt =
    (Matrix.posSemidef_conjTranspose_mul_self A).sqrt := by
  have : (-A)ᴴ * -A = (A)ᴴ * A := by
    rw [Matrix.conjTranspose_neg, Matrix.neg_mul, Matrix.mul_neg]
    exact neg_neg _
  apply congr_heq
  rw [this]
  exact heq_prop _ _

so I was eventually able to get it with

  apply congr_heq
  rw [this]
  exact heq_prop _ _

but what I really "meant" was just rw [this]. Is there a better way to handle these types of things ... ?

[Alex Meiburg]

If I just cared about sqrt, I could just write a lemma like

lemma sqrt_eq {A B : Matrix m m R} (h : A = B) (hA : A.PosSemidef) (hB : B.PosSemidef) :
    hA.sqrt = hB.sqrt := by
  apply congr_heq
  rw [h]
  exact heq_prop _ _

and rely on that. But there are many such matrix functions, like IsHermitian.eigenvalues, IsHermitian..eigenvectorMatrix, IsHermitian.eigenvectorMatrixInv, and it feels wrong to have to write so many similar "casting" lemmas.

[Jireh Loreaux]

Note: @Jon Bannon is currently in the process of refactoring Matrix.IsHermitian.eigen* stuff, so expect some things around that to change very soon. I think there's a PR, but it's not in an appropriate state yet, so I won't link it.

[Jireh Loreaux]

Moreover, note that some of this will be fixed by using the continuous functional calculus. There will be an instance of that for hermitian and positive semidefinite matrices soon (but it needs the refactor first). And I have material about sqrt for the cfc waiting in another repo which I'll PR soonish.

[Jireh Loreaux]

Also, I would bet that using the term constructor congr (or the tactic congrm) can help you here, but I haven't tested it.

[Jireh Loreaux]

Can you share what you're working on concerning positive semidefinite matrices?

Note that there's currently lots of defeq abuse in those files, which is part of the thing that Jon is cleaning up.

[Alex Meiburg]

I'm trying to write up some things from quantum information theory. Just basic stuff right now. :)

[Jireh Loreaux]

@Kyle Miller I know this is kind of cursed, but do you understand why the congrm tactic succeeds here but the declaration fails because the kernel says it still has free variables? Seems like a bug in congr, which I know you're currently working on.

import Mathlib

variable {m n R : Type*} [Fintype m] [Fintype n]
variable [RCLike R] [DecidableEq n] [DecidableEq m]

namespace Matrix
open scoped ComplexOrder

lemma sqrt_eq {A B : Matrix m m R} (h : A = B) (hA : A.PosSemidef) (hB : B.PosSemidef) :
    hA.sqrt = hB.sqrt := by
  congrm(Matrix.PosSemidef.sqrt (A := $(h)) ‹_›)

[Kyle Miller]

congr! works here:

lemma sqrt_eq {A B : Matrix m m R} (h : A = B) (hA : A.PosSemidef) (hB : B.PosSemidef) :
    hA.sqrt = hB.sqrt := by
  congr!

That tactic is "goal directed" vs congrm and congr(...) which are "term directed" (the former can use whatever it finds in the goal, the latter needs to synthesize what it needs). The issue appears to be ‹_›, which doesn't seem to play nice with congrm/congr(...), though I'm not sure what the issue is exactly.

[Kyle Miller]

@Jireh Loreaux Thanks for that example. There was a bad bug deep within congr(...): #12253

[Jireh Loreaux]

Lol, I can't believe I didn't think of congr! in this case. Thanks for the bug fix Kyle!

[Kyle Miller]

It's neat to see that congrm/congr(...) actually works with ‹_›. (That didn't turn out to be the problem by the way. The real issue was that congr(...) was building a term that used Subsingleton instances to automatically handle discrepancies between arguments, but it wasn't substituting it in everywhere, leaving a stray fvar in the term.)

[Jireh Loreaux]

Yeah, I didn't know if it would work with ‹_› either, and was a bit surprised to see that it did. I also realized you can postpone goals with metavariable holes like ?_. I tried that first, found it was very cool that it worked, then tried with ‹_›. Unsurprisingly, given what the issue ended up being, the fvar error also occurred with ?_.