Zulip Chat Archive

Stream: new members

Topic: Motive Not Type Correct Nth

MohanadAhmed (Jun 03 2023 at 17:30):

In the code below the rewrite in rank_eq_rank_diagonal fails. Weirdly enough, if I replace the RHS side with the zero matrix it does not fail.
The error message says "motive is not type correct". In full the error message is below the code. Checking some threads here I found suggest ions to try using: simp_rw: it fails. I also tried erewrite: it also fails.

The error message for simp_rw after setting set_option trace.simp_lemmas true is
[simp_lemmas.invalid] LHS of rule derived from '[anonymous]' occurs in RHS

import data.complex.basic
import linear_algebra.matrix.hermitian
import linear_algebra.matrix.pos_def
import linear_algebra.matrix.determinant
import linear_algebra.matrix.spectrum
import linear_algebra.matrix.nonsingular_inverse
import linear_algebra.matrix.diagonal
import data.matrix.basic
import data.matrix.rank
--import rank_surj_inv
import algebra.star.basic

open matrix complex
open_locale matrix big_operators

variables {m n R: Type*}
variables [fintype m][fintype n][decidable_eq m][decidable_eq n]
variables [field R][is_R_or_C R][partial_order R][star_ordered_ring R]

lemma modified_spectral_theorem (A: matrix n n )(hA: A.is_hermitian) :
  A = (hA.eigenvector_matrix) 
    (matrix.diagonal (coe  hA.eigenvalues))  hA.eigenvector_matrix_inv :=
  have h := hA.spectral_theorem,
  replace h := congr_arg (λ x, hA.eigenvector_matrix   x) h,
  simp only at h,
  rw [ matrix.mul_assoc, hA.eigenvector_matrix_mul_inv, matrix.one_mul] at h,
  rwa matrix.mul_assoc,

lemma rank_eq_rank_diagonal (A: matrix n n )(hA: A.is_hermitian) :
  A.rank = (matrix.diagonal ((coe  hA.eigenvalues): n  )).rank :=
    -- A.rank = (0: matrix n n ℂ).rank := -- This line makes rewrite work!!
  rw modified_spectral_theorem A hA,

rewrite tactic failed, motive is not type correct
  λ (_a : matrix n n ),
    A.rank = (diagonal (coe  hA.eigenvalues)).rank = (_a.rank = (diagonal (coe  hA.eigenvalues)).rank)
n : Type u_2,
_inst_2 : fintype n,
_inst_4 : decidable_eq n,
A : matrix n n ,
hA : A.is_hermitian
 A.rank = (diagonal (coe  hA.eigenvalues)).rank

MohanadAhmed (Jun 03 2023 at 17:50):

The trick suggested here to use nth_rewrite 0 also does not work. nth_rewrite_lhs 0 works.

MohanadAhmed (Jun 03 2023 at 17:51):

I guess this is because there is an A hiding inside hA.eigenvalues but what if I had another A on the lhs? Why is nth_rewrite not working but nth_rewrite_lhs working?

Last updated: Dec 20 2023 at 11:08 UTC