wierd rewrite fail

Stream: general

[MohanadAhmed]

Hello everyone,
In the following code when trying to rewrite using rank_eq_count_non_zero_eigs I get a very wierd error. The error is

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  rank (Aᴴ ⬝ A)

While the goal is
rank (Aᴴ ⬝ A) = Fintype.card { i // IsHermitian.eigenvalues (_ : IsHermitian (Aᴴ ⬝ A)) i ≠ 0 }

Note the case with the Complex Matrix (A: Matrix m n ℂ) works, while the case of (A: Matrix m n R where R: IsROrC does not! Any thoughts appreciated!

import Mathlib

open Matrix

lemma rank_eq_count_non_zero_eigs {n R: Type}[Fintype n][DecidableEq n]
  [IsROrC R][DecidableEq R]
  (A: Matrix n n R)(hA: A.IsHermitian) :
  A.rank =  (Fintype.card {i // hA.eigenvalues i ≠ 0}) := sorry


open ComplexOrder

lemma GOOD_rank_eq_card_pos_eigs_conj_transpose_mul_self {m n R: Type}
  [Fintype m][Fintype n][DecidableEq m][DecidableEq n]
  [IsROrC R][DecidableEq R][PartialOrder R][StarOrderedRing R]
  (A: Matrix m n ℂ):
  A.rank =  (Fintype.card {i // (Matrix.isHermitian_transpose_mul_self A).eigenvalues i ≠ 0}) := by
  rw [← rank_conjTranspose_mul_self]
  rw [rank_eq_count_non_zero_eigs (Aᴴ⬝A) (Matrix.isHermitian_transpose_mul_self A)] -- NO ERROR

lemma BAD_rank_eq_card_pos_eigs_conj_transpose_mul_self {m n R: Type}
  [Fintype m][Fintype n][DecidableEq m][DecidableEq n]
  [IsROrC R][DecidableEq R][PartialOrder R][StarOrderedRing R]
  (A: Matrix m n R):
  A.rank =  (Fintype.card {i // (Matrix.isHermitian_transpose_mul_self A).eigenvalues i ≠ 0}) := by
  rw [← rank_conjTranspose_mul_self]
  rw [rank_eq_count_non_zero_eigs (Aᴴ⬝A) (Matrix.isHermitian_transpose_mul_self A)] --Error Here!!

[Kevin Buzzard]

  ...
  rw [← rank_conjTranspose_mul_self]
  convert rank_eq_count_non_zero_eigs (Aᴴ⬝A) (Matrix.isHermitian_transpose_mul_self A)
  -- ⊢ StarOrderedRing.toStarRing = IsROrC.toStarRing

So that's what's stopping the rewrite working: two star ring structures on R. And now you can look at how you've set things up, and indeed you have a hypothesis IsROrC R (which gives R a star ring structure) and StarOrderedRing R (which gives it another, perhaps different, one). I don't know enough about the typeclasses here to suggest a fix though.

[MohanadAhmed]

Thanks. I added the StarOrderedRing because rank_conjTranspose_mul_self requires a StarOrderedRing? So what is the proper way to add StarOrderedRing here?

[MohanadAhmed]

Wierdly enough a rewrite the other way round works i.e.:

lemma BAD_rank_eq_card_pos_eigs_conj_transpose_mul_self {m n R: Type}
  [Fintype m][Fintype n][DecidableEq m][DecidableEq n]
  [IsROrC R][DecidableEq R][PartialOrder R][StarOrderedRing R]
  (A: Matrix m n R):
  A.rank =  (Fintype.card {i // (Matrix.isHermitian_transpose_mul_self A).eigenvalues i ≠ 0}) := by
  rw [← rank_conjTranspose_mul_self]
  rw [← rank_eq_count_non_zero_eigs (Aᴴ⬝A) (Matrix.isHermitian_transpose_mul_self A)]
  sorry

The goal state before the sorry is rank (Aᴴ ⬝ A) = rank (Aᴴ ⬝ A) which should have been closed by rfl in the rw . The doc for rw says:

rw is like rewrite, but also tries to close the goal by "cheap" (reducible) rfl afterwards.

Is this also related to the two Star Rings I placed or R?

[Kevin Buzzard]

If rfl doesn't work then try congr or congr' or convert rfl -- tactics (not all of which might exist in Lean 4, but some will) which will just reduce the goals to precisely the parts which aren't rfl, and I conjecture that you'll be left with ⊢ StarOrderedRing.toStarRing = IsROrC.toStarRing again (which is not provable because it's not true).

[MohanadAhmed]

So If I understand correctly, I cannot just add a StarOrderedRing instance on IsROrC, I need to bake it inside the IsROrC class. Looking at the Complex.Basic file there is a partialOrder definition. If I do something similar on IsROrC would that allow me to place a StarOrderedRing on IsROrC?

[MohanadAhmed]

Kevin Buzzard said:

If rfl doesn't work then try congr or congr' or convert rfl -- tactics (not all of which might exist in Lean 4, but some will) which will just reduce the goals to precisely the parts which aren't rfl, and I conjecture that you'll be left with ⊢ StarOrderedRing.toStarRing = IsROrC.toStarRing again (which is not provable because it's not true).

And just for future reference what you said is correct. convert rfl shows that I am now required to prove IsROrC.toStarRing = StarOrderedRing.toStarRing