motive type not correct??

Stream: general

[MohanadAhmed]

In the following code rw commented out next to the sorry generates an error of motive type not correct. I have read a few of the cases in the chat stream where motive not correct error are reported but couldn't figure out a usable fix. Any thought?

import Mathlib

variable {m n: Type _}[Fintype n][Fintype m]
variable {K : Type _}[IsROrC K]

open Matrix BigOperators

lemma dot_product_star_self_eq_zero_iff_R_or_C
    (v : n → K) : Matrix.dotProduct (star v) v = 0 ↔  v = 0 := by sorry

@[simp]
lemma ker_mulVecLin_conjTranspose_mul_self_R_or_C (A : Matrix m n K) :
    LinearMap.ker (Aᴴ ⬝ A).mulVecLin = LinearMap.ker (mulVecLin A) := by sorry

open FiniteDimensional

theorem rank_conjTranspose_mul_self_R_or_C (A : Matrix m n K) : (Aᴴ ⬝ A).rank = A.rank := by
  dsimp only [rank]
  refine' add_left_injective (finrank K (LinearMap.ker (mulVecLin A))) _
  dsimp only
  trans finrank K { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
    finrank K { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) }
  · sorry -- rw [← ker_mulVecLin_conjTranspose_mul_self_R_or_C] -- motive type is not correct
  · simp only [LinearMap.finrank_range_add_finrank_ker]

[MohanadAhmed]

Note this is just an adaptation of the proof of rank_conjTranspose_mul_self where the rw is working nicely.

[Kevin Buzzard]

I'm not at a computer right now but -- try simp only? Or find a trick with convert?

[Yury G. Kudryashov]

This error usually happens when you try to rewrite rw [(h : a = b)] in a goal, where the type of some part of the expression depends on a. E.g., in your case finrank K M takes instance-implicit arguments [AddCommGroup M] [Module K M], so you can't rewrite on (h : M = N) without noticing that the instances on M and N agree.

[MohanadAhmed]

Yury G. Kudryashov said:

This error usually happens when you try to rewrite rw [(h : a = b)] in a goal, where the type of some part of the expression depends on a. E.g., in your case finrank K M takes instance-implicit arguments [AddCommGroup M] [Module K M], so you can't rewrite on (h : M = N) without noticing that the instances on M and N agree.

What is the difference between the case above and the case already in mathlib for docs#rank_conjTranspose_mul_self which looks identical to me? What trips up rewrite here and not in the mathlib proof

[MohanadAhmed]

Kevin Buzzard said:

I'm not at a computer right now but -- try simp only? Or find a trick with convert?

• I tried just simp onlyand 'dsimp` and then using rewrite did not work.
• I also tried makeing ker_mulVecLin_conjTranspose_mul_self_R_or_C a simp lemma and simping with it. Not useful.
• I tried using simp_rw and erw.

From reading around this "motive" thing seems to be like a replace template. So I tried taking that from the working example inside mathlib. It says that the rw produces the term:

Eq.mpr
  (id
    (ker_mulVecLin_conjTranspose_mul_self A ▸
      Eq.refl
        (finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
            finrank R { x // x ∈ LinearMap.ker (mulVecLin A) } =
          finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
            finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) })))
  (Eq.refl
    (finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } + finrank R { x // x ∈ LinearMap.ker (mulVecLin A) }))

So I tried that while replacing ker_mulVecLin_conjTranspose_mul_self with ker_mulVecLin_conjTranspose_mul_self_R_or_C with no use also

[MohanadAhmed]

I have no idea how to use convert and from looking around it seems to have so many forms some with using some without using (my random attempts were not useful)

[Mario Carneiro]

The usual pattern is to write convert e and then if you get goals which are unprovable because they went too deep (e.g. if e is a proof of P (b + a) and your goal is P (a + b) then convert e will give you subgoals a = b and b = a but probably you wanted a + b = b + a instead) then use using 1, using 2, etc, increase the number until you get the goals you expect

[MohanadAhmed]

I am not sure what is going but it works "inside mathlib"!!

• On a clean project the rw gives motive is not type correct. The project is just one file which you can find here on github dotProd_outside_math. When I copy the code of the lemma docs#rank_conjTranspose_mul_self outside of mathlib (and rename it) gives the same error!!!

• I moved the lemma into mathlib and the rewrite works. No complaints about motive is not type correct. This is on the branch MohanadAhmed/IsROrC_AHA_rank_workaround

In the form of MWE:

import Mathlib


variable {m n: Type _}[Fintype n][Fintype m]
variable {K: Type}[IsROrC K]

open Matrix BigOperators


@[simp]
theorem IsROrC.re_sum (f : α → K) : IsROrC.re (∑ i in s, f i) = ∑ i in s, IsROrC.re (f i) := by
  apply map_sum _ _

@[simp]
theorem IsROrC.im_sum (f : α → K) : IsROrC.im (∑ i in s, f i) = ∑ i in s, IsROrC.im (f i) := by
  apply map_sum _ _

lemma dot_product_star_self_eq_zero_iff_R_or_C
    (v : n → K) : Matrix.dotProduct (star v) v = 0 ↔  v = 0 := by sorry

theorem ker_mulVecLin_conjTranspose_mul_self_R_or_C (A : Matrix m n K) :
    LinearMap.ker (Aᴴ ⬝ A).mulVecLin = LinearMap.ker (mulVecLin A) := by sorry
open FiniteDimensional Matrix

theorem rank_conjTranspose_mul_self_R_or_C (A : Matrix m n K) : (Aᴴ ⬝ A).rank = A.rank := by
  dsimp only [Matrix.rank]
  refine' add_left_injective (finrank K (LinearMap.ker (mulVecLin A))) _
  dsimp only
  trans finrank K { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
    finrank K { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) }
  · rw [ker_mulVecLin_conjTranspose_mul_self_R_or_C] -- Error
  · simp only [LinearMap.finrank_range_add_finrank_ker]

variable {R: Type}[Field R][PartialOrder R][StarOrderedRing R]
theorem NotInMathlib_rank_conjTranspose_mul_self (A : Matrix m n R) : (Aᴴ ⬝ A).rank = A.rank := by
  dsimp only [rank]
  refine' add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) _
  dsimp only
  trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) }
  · rw [ker_mulVecLin_conjTranspose_mul_self] -- Error
  · simp only [LinearMap.finrank_range_add_finrank_ker]

[Yury G. Kudryashov]

I don't know why the proof in Mathlib works.

[MohanadAhmed]

@Yury G. Kudryashov
So far the error is the same

1. On my local machine with the lemmas "outside mathlib"
2. In Lean4 Playground

image.png

[MohanadAhmed]

So I don't think I am doing anything particularly wrong (I mean in setting up the project and mathlib dependency)!

[MohanadAhmed]

Yury G. Kudryashov said:

I don't know why the proof in Mathlib works.

Any random ideas I can try?

[Yury G. Kudryashov]

This works:

import Mathlib.Data.Matrix.Rank


variable {m n: Type _}[Fintype n][Fintype m]

open Matrix BigOperators
open FiniteDimensional Matrix

variable {R: Type}[Field R][PartialOrder R][StarOrderedRing R]
theorem NotInMathlib_rank_conjTranspose_mul_self (A : Matrix m n R) : (Aᴴ ⬝ A).rank = A.rank := by
  dsimp only [rank]
  refine' add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) _
  dsimp only
  trans finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ ⬝ A)) } +
    finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ ⬝ A)) }
  · rw [ker_mulVecLin_conjTranspose_mul_self] -- Error
  · simp only [LinearMap.finrank_range_add_finrank_ker]

[Yury G. Kudryashov]

The same proof with import Mathlib fails

[MohanadAhmed]

So is the behavior of rw affected by the imports one has at the top of the file?

[MohanadAhmed]

Just for clarity at a future time:
I can confirm what you said: the reduced imports makes the rw work.
In my case I need

import Mathlib.Data.Matrix.Rank
import Mathlib.Data.IsROrC.Basic

since the example depends on IsROrC fields

[Yury G. Kudryashov]

The imports affect the instances Lean uses behind the scene.

[Yury G. Kudryashov]

It looks like docs#AddCommGroup.ofSubgroupOnRing is the offending instance

[Yury G. Kudryashov]

It looks like a bad instance to me.

[MohanadAhmed]

Nice! How did you get to that? Like what debugging steps?

[Yury G. Kudryashov]

This:

import Mathlib

variable {m n: Type _}[Fintype n][Fintype m]

open Matrix BigOperators
open FiniteDimensional Matrix

variable {R: Type}[Field R][PartialOrder R][StarOrderedRing R]

theorem NotInMathlib_rank_conjTranspose_mul_self (A : Matrix m n R) : (Aᴴ ⬝ A).rank = A.rank :=
  add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) <|
   calc (Aᴴ ⬝ A).rank + finrank R (LinearMap.ker (mulVecLin A))
       = (Aᴴ ⬝ A).rank + finrank R (LinearMap.ker (mulVecLin (Aᴴ ⬝ A))) := by
         congr
     _ = _ := by simp only [rank, LinearMap.finrank_range_add_finrank_ker]

shows some HEq about this instance after congr.

[Yury G. Kudryashov]

Could you please try to compile Mathlib without docs#AddCommGroup.ofSubgroupOnRing and other similar instances in that file (just delete them and push to github so that CI runs lake build)?

[MohanadAhmed]

OK
It is in this branch MohanadAhmed/mathlib_without_AddCommGroup_blah_inst

[MohanadAhmed]

The build failed

[MohanadAhmed]

details here https://github.com/leanprover-community/mathlib4/actions/runs/5703006908/job/15455182227

[MohanadAhmed]

The errors are timeouts in some file ././Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.leanwith large maxHeartbeat values like 400000

[Eric Wieser]

Yury G. Kudryashov said:

It looks like a bad instance to me.

Can an instance be bad if it's implementation is inferInstance?

[Eric Wieser]

Oh, I guess maybe the trouble is that it consumes A as a family

[MohanadAhmed]

Yury G. Kudryashov said:

Could you please try to compile Mathlib without docs#AddCommGroup.ofSubgroupOnRing and other similar instances in that file (just delete them and push to github so that CI runs lake build)?

I just noticed that you said other similar instances.
Which ones would those be?
I only removed the one you mentioned?

[Yury G. Kudryashov]

Eric Wieser said:

Oh, I guess maybe the trouble is that it consumes A as a family

Yes, it is written for a family but applies in any case. I don't know if it can cause troubles.

[Eric Wieser]

The instance in question was a workaround for a bug in Lean3 TC inference