!4#2773 type mismatch

Stream: mathlib4

[Jeremy Tan]

!4#2773 I can't understand why refine' mul_dvd_mul _ ih in Lean 4 generates a type mismatch error but mathlib 3 refine mul_dvd_mul _ ih doesn't

[Eric Wieser]

Looks like a change in a lemma statement

[Eric Wieser]

The error is

has type
  ?m.2582 * ↑(p ^ (k + 1)) ∣ ?m.2583 * (a ^ p ^ k - b ^ p ^ k) : Prop
but is expected to have type
  ↑(p * p ^ (k + 1)) ∣ ...

[Eric Wieser]

Note the arrows are in different places

[Eric Wieser]

You should open the lean3 and work out where they are supposed to be

[Eric Wieser]

And track down where the proof diverges

[Jeremy Tan]

using the lean web editor I find that

• in mathlib3, after the last pow_succ in rw [pow_succ' p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ] the coercion distributes and the term ↑p * ↑p ^ k.succ appears
• but in mathlib4 at the same place the coercion doesn't distribute and ↑(p * p ^ (k + 1)) remains

[Jeremy Tan]

I need a way to distribute the coercion

[Jeremy Tan]

but as I have only barely scratched the surface of mathlib I don't know how to look for suitable rewriting theorems

[Floris van Doorn]

The norm_cast tactic is useful when having do move coercions around.

[Jeremy Tan]

Nat.mul_cast worked, but now I'm getting a whnf heartbeat error

[Jeremy Tan]

I pushed a partial fix. Now in the proof at

rw [← mem_span_singleton, ← eq_zero_iff_mem, RingHom.map_geom_sum₂, RingHom.map_pow,
    RingHom.map_pow, h, geom_sum₂_self, hp, zero_mul]

when Lean tries to rewrite using h it reaches the max number of heartbeats

[Jeremy Tan]

just before rw [... h] the goal state is

⊢ (Finset.sum (Finset.range p) fun i => (↑(mk (span {↑p})) a ^ p ^ k) ^ i * (↑(mk (span {↑p})) b ^ p ^ k) ^ (p - 1 - i)) =

and I have h: ↑(mk (span {↑p})) a = ↑(mk (span {↑p})) b

[Jeremy Tan]

the comment at !4#2757 should solve it though:

For instance, in a statement of an equality a = b... The solution in that case was to provide a type ascription to a to avoid the metavariables.

how would that be done in this case?

[Jeremy Tan]

@Jireh Loreaux how do I apply a type ascription here to solve the heartbeat problem without setting max heartbeats?

[Jireh Loreaux]

The issue I described there may not be the same thing occurring here.

[Jireh Loreaux]

In fact I doubt it is.

[Jeremy Tan]

should I just apply the max heartbeat adjustment suggested on the PR or is there a better way out?

[Jireh Loreaux]

There are generally other workarounds when dealing with lean4#2074. You can grep mathlib for 2074 to find some.

[Jireh Loreaux]

If you want to see if it is caused by 2074, you can do set_option synthInstance.etaExperiment true before the declaration. If that doesn't fix it then it's probably not 2074.

[Jeremy Tan]

like this?

set_option synthInstance.etaExperiment true
theorem ...

[Jeremy Tan]

but it doesn't seem to change anything

[Jireh Loreaux]

Okay, in that case I would move on to something else for now and come back to it. I don't have time to actually pull it up right now.

[Jeremy Tan]

I've adopted the heartbeat fix for now

[Jireh Loreaux]

Please add a porting note so it doesn't get merged that way.

[Jeremy Tan]

@Jireh Loreaux Note added. Now what?

[Jireh Loreaux]

If there are no other things to be done for the PR, just wait. If there are, keep fixing other things.

[Jeremy Tan]

@Johan Commelin I don't get what the two instances are

[Johan Commelin]

Did you search for "2074"?

[Jeremy Tan]

hold on

[Johan Commelin]

You will find things like

-- Porting note: TODO: workaround for lean4#2074
attribute [-instance] Ring.toNonAssocRing

[Jeremy Tan]

what does that line do?

[Johan Commelin]

It disables that instance, so that typeclass resolution can't use it.

[Jeremy Tan]

adding the two lines

attribute [-instance] Semiring.toNonAssocSemiring
attribute [-instance] NonAssocRing.toNonAssocSemiring

together (and only together) work, but then I get another error where I introduced Nat.cast_mul

• adding just one of the two lines still leads to heartbeat error

[Johan Commelin]

What kind of error?

[Jeremy Tan]

rewrite just fails; ↑(p * p ^ (k + 1)) is there where Nat.cast_mul expects ↑(m * n) = ↑m * ↑n

[Jeremy Tan]

in the code with the heartbeat expansion this rewrite went through, allowing mul_dvd_mul on the next line to work

[Johan Commelin]

Can you try

erw [Nat.cast_mul]

on a line on its own? (So remove it from the current rw)

[Jeremy Tan]

still fails

[Johan Commelin]

Crazy

[Johan Commelin]

I'll load it up in VScode

[Jeremy Tan]

(the code with the disabled instances has been pushed in place of the heartbeat expansion, by the way)

[Johan Commelin]

ok, I'll pull again

[Jeremy Tan]

Watching bors stage, compile and commit the approved PRs is almost hypnotic

[Johan Commelin]

The problem seems to be the rw [h] on the last line. But I don't understand why.

[Jeremy Tan]

I had a discussion with Jireh earlier in this narrow and he asked me to perform the eta-experiment. We determined that this was probably not a 2074 issue

[Jeremy Tan]

If you want to see if it is caused by 2074, you can do set_option synthInstance.etaExperiment true before the declaration. If that doesn't fix it then it's probably not 2074.

[Jeremy Tan]

Which was why I simply opted for the heartbeat expansion suggested by Lukas

[Johan Commelin]

I pushed a fix and golf

[Jeremy Tan]

hmm... this may contain a lot for me to learn

[Johan Commelin]

Yeah, I think that besides 2074, there might be some orthogonal issue with quotients. But I don't understand the details.

[Jireh Loreaux]

I've ported a few quotient files and they have been a royal pain.