resolving motive problem

Stream: mathlib4

[Suzuka Yu]

Greetings! I came across this "motive is not type correct" problem in the following code:

import Mathlib

open Polynomial

example {F : Type*} [Field F] (p : F[X]) (hp : p = 0) : Module.finrank F (AdjoinRoot p) = p.natDegree := by
  rw [hp]
  unfold AdjoinRoot
  convert_to Module.finrank F (F[X] ⧸ (⊥ : Ideal F[X])) = 0
  refine LinearEquiv.finrank_eq ?_
  · have := (Ideal.span_singleton_eq_bot (x := (0 : F[X]))).2 rfl
    rw [this]
    sorry
  convert_to Module.finrank F F[X] = 0
  exact LinearEquiv.finrank_eq <| (AlgEquiv.quotientBot F F[X]).toLinearEquiv
  exact Module.finrank_of_not_finite <| Polynomial.not_finite

The error message is

tactic 'rewrite' failed, motive is not type correct:
  fun _a ↦ (F[X] ⧸ _a) ≃ₗ[F] F[X] ⧸ ⊥
Error: application type mismatch
  @CommRing.toNonUnitalCommRing (F[X] ⧸ _a) (instCommRing 0)
argument
  instCommRing 0
has type
  CommRing (AdjoinRoot 0) : Type u_2
but is expected to have type
  CommRing (F[X] ⧸ _a) : Type u_2

Seems like it didn't unfold AdjoinRoot? How can I resolve it? simp_rw, erw doesn't work here

[Matt Diamond]

this seems to work (instead of rw [this]):

rw [← this]
exact LinearEquiv.refl _ _

[Matt Diamond]

I'm not sure why the rewrite works in one direction but not the other, but at least this should resolve it

[Suzuka Yu]

Ah, yes! Thanks! (I'm also curious whats happening behind the scene lol)

[Kevin Buzzard]

The goal ⊢ (F[X] ⧸ Ideal.span {0}) ≃ₗ[F] F[X] ⧸ ⊥ contains an explicit Ideal.span {0} but it also contains at least one "secret" one. The goal is an isomorphism of F-algebras so buried away in the goal there must be some kind of data which expresses how F[X] ⧸ Ideal.span {0} is an F-algebra: remember that what Lean prints is not all of what is going on; a lot of information in the terms printed on the screen is suppressed by the pretty-printer (for example all implicit inputs to functions, all typeclass information etc). When you attempt to change the visible Ideal.span {0} to ⊥ Lean makes the change, and now when it tries to make sense of the resulting expression it says "wait a minute, this is supposed to be the type of isomorphisms of F-algebras but the F-algebra on the left is F[X] ⧸ ⊥ and the data showing that it's an F-algebra is data showing that F[X] ⧸ Ideal.span {0} is an F-algebra, so this expression doesn't even make sense as a type any more". You hence get the error. By the way, you shouldn't be in tactic mode with your goal a Type, goals should always be Props in tactic mode.

You might ask "well why doesn't Lean just rewrite all of the Ideal.span {0}s, including the ones that the user can't see?". This is a fair question but it turns out that this is super-complicated in Lean's type theory and the rw tactic cannot do it in this case. The problem is that even if two ideals I and J are equal, but if the proof of this equality is not rfl (and in your case it's not rfl, it's Ideal.span_singleton_eq_bot), then the relationship between the types R/I and R/J is complicated, and Lean would rather say that they are isomorphic than equal (equality of types is a poorly-behaved concept in Lean's type theory, most questions about it are undecidable). So what you really want to do here is to say "I and J are equal, so R/I and R/J are isomorphic F-algebras, and I will apply this isomorphism to continue" but this is well beyond the remit of the rw tactic, which only deals in equalities not isomorphisms. You can see the point where rw gives up in the error message; it is confused about two types which you have proved are equal but the proof isn't rfl, so it is now muddled about how to get a ring structure on one type from a ring structure on the other one. Such a transfer of ring structures shoudl be done via a bijection, not an equality of types.

[Edison Xie]

Suzuka Yu said:

Greetings! I came across this "motive is not type correct" problem in the following code:

import Mathlib

open Polynomial

example {F : Type*} [Field F] (p : F[X]) (hp : p = 0) :
    Module.finrank F (AdjoinRoot p) = p.natDegree := by
  subst hp
  change Module.finrank F (F[X]⧸_) = 0
  have := ((Submodule.quotEquivOfEq _ _ <| Ideal.span_singleton_eq_bot (x := (0 : F[X]))|>.2 rfl)
    |>.restrictScalars F) ≪≫ₗ (AlgEquiv.quotientBot F F[X]).toLinearEquiv
  simpa [this.finrank_eq] using Module.finrank_of_not_finite <| Polynomial.not_finite

this would avoid rewriting theorems about Ideal.span {0}

[Aaron Liu]

Kevin Buzzard said:

The problem is that even if two ideals I and J are equal, but if the proof of this equality is not rfl (and in your case it's not rfl, it's Ideal.span_singleton_eq_bot), then the relationship between the types R/I and R/J is complicated, and Lean would rather say that they are isomorphic than equal (equality of types is a poorly-behaved concept in Lean's type theory, most questions about it are undecidable).

Really? I would've thought the you can just subst your way out

[Kevin Buzzard]

Unfortunately subst doesn't work here. What happens is that you have equal ideals $I$ and $J$, and then you can deduce that the types $R/I$ and $R/J$ are equal, however subst does not tell you that the CommRing instances match up.

[Yaël Dillies]

Also remember that subst only works if at least one of $I$ or $J$ is a free variable. Kevin's $I$ and $J$ are definitely not free variables.

[Aaron Liu]

You case just have two instances?? Also Eq.rec tells you the CommRing instances match up.

[Aaron Liu]

Yaël Dillies said:

Also remember that subst only works if at least one of $I$ or $J$ is a free variable. Kevin's $I$ and $J$ are definitely not free variables.

I didn't mean the tactic subst, but rather the general idea of substituting an equality. Sorry if that wasn't clear.

[Yaël Dillies]

Yes, so this general idea of substituting an equality incarnates itself here by "$I = J$, so $R/I$ and $R/J$ are isomorphic rings".

[Yaël Dillies]

This is definitely a rabbit hole, but you might want to learn a bit of homotopy type theory

[Aaron Liu]

I was thinking "I = J, so R ⧸ I = R ⧸ J and the two instances are HEq"

[Aaron Liu]

But that works too

[Yaël Dillies]

Aaron Liu said:

I was thinking "I = J, so R ⧸ I = R ⧸ J and the two instances are HEq"

With that view, docs#RingEquiv is a more general (and flexible!) version of your predicate "A = B and the two instances are HEq"

[Kyle Miller]

Aaron Liu said:

the general idea of substituting an equality

The general idea of substituting an equality is what rw does though, and it fails here.

@Kevin Buzzard rw rewrites all occurrences simultaneously, even the "secret" ones. I'm not sure what you're talking about with equality of types confusing rw, since rw doesn't distinguish whether a term is a value or a type or a proposition or a universe or what-have-you. I think the problem is simply that the LHS of the rewrite lemma doesn't literally appear inside one of the instance arguments. If it did, then it could rewrite and typecheck. However, the terms are really large (if you set `pp.explicit), and I didn't have the patience to try to verify this.

It's a fair caution that rewrites that involve equalities of types are best to be avoided (better to create an isomorphism and compose).

[Aaron Liu]

The secret one is hidden inside AdjoinRoot.instCommRing

[Aaron Liu]

rw does not unfold this instance so does not get to rewrite it

[Kyle Miller]

Yep, that's the one. It takes a few unfoldings, but then rw can see it:

example {F : Type*} [Field F] (p : F[X]) (hp : p = 0) : Module.finrank F (AdjoinRoot p) = p.natDegree := by
  rw [hp]
  unfold AdjoinRoot
  convert_to Module.finrank F (F[X] ⧸ (⊥ : Ideal F[X])) = 0
  refine LinearEquiv.finrank_eq ?_
  · have := (Ideal.span_singleton_eq_bot (x := (0 : F[X]))).2 rfl
    unfold AdjoinRoot.instCommRing AdjoinRoot.instAlgebra AdjoinRoot.mk._proof_1
    rw [this]
    sorry
  convert_to Module.finrank F F[X] = 0
  exact LinearEquiv.finrank_eq <| (AlgEquiv.quotientBot F F[X]).toLinearEquiv
  exact Module.finrank_of_not_finite <| Polynomial.not_finite

[Kyle Miller]

@Kevin Buzzard I think I misunderstood what you were saying in your post, sorry. When you said "secret" I thought you just meant implicit arguments, not that it might be buried deeper in an expression, or otherwise obscured.

[Kyle Miller]

It's not exactly the same, but I think the rw failure here could be regarded as being similar to why this doesn't work:

example (x : ℕ) (h : x + x = 2 * x) : x + (x + 1) = 2 * x + 1 := by
  rw [h]

[Kyle Miller]

Reiterating a point Kevin made, rewriting data like this is not the right approach (my unfold is just for illustration, it's not the solution!). It's better to work with isomorphisms.

I couldn't find it easily, but there ought to be an isomorphism somewhere in mathlib for R ⧸ I ≃+* R ⧸ J given I = J.

[Ruben Van de Velde]

docs#Ideal.quotEquivOfEq ?

[Ruben Van de Velde]

(First hit on loogle)

[Kyle Miller]

if only it were F-linear...

[Kyle Miller]

Ok, docs#Submodule.quotEquivOfEq was the answer.

import Mathlib

open Polynomial

example {F : Type*} [Field F] (p : F[X]) (hp : p = 0) : Module.finrank F (AdjoinRoot p) = p.natDegree := by
  rw [hp]
  unfold AdjoinRoot
  convert_to Module.finrank F (F[X] ⧸ (⊥ : Ideal F[X])) = 0
  refine LinearEquiv.finrank_eq ?_
  · have := (Ideal.span_singleton_eq_bot (x := (0 : F[X]))).2 rfl
    have := Submodule.quotEquivOfEq _ _ this
    exact this.restrictScalars (R := F)
  convert_to Module.finrank F F[X] = 0
  exact LinearEquiv.finrank_eq <| (AlgEquiv.quotientBot F F[X]).toLinearEquiv
  exact Module.finrank_of_not_finite <| Polynomial.not_finite

[Edison Xie]

docs#Submodule.quotEquivOfEqBot is a hack :)

[Edison Xie]

import Mathlib

open Polynomial in
example {F : Type*} [Field F] (p : F[X]) (hp : p = 0) :
    Module.finrank F (AdjoinRoot p) = p.natDegree := by
  subst hp
  change Module.finrank F (F[X]⧸_) = 0
  have := Submodule.quotEquivOfEqBot (Ideal.span {(0 : F[X])})
    (Ideal.span_singleton_eq_bot (x := (0 : F[X]))|>.2 rfl)|>.restrictScalars F |>.finrank_eq
  simpa [this] using Module.finrank_of_not_finite Polynomial.not_finite