Algebra.Periodic !4#1963

Stream: mathlib4

[Yury G. Kudryashov]

In !4#1963, Lean fails to find [Module α α] in many lemmas. Why can it happen? How can I debug it?

[Eric Wieser]

My guess is that it's looking for @Module α α Ring.toSemiring _ but finds @Module α α CommSemiring.toSemiring _ or a more complex version thereof. What α causes the issue?

[Yury G. Kudryashov]

It's a DivisionRing

[Yury G. Kudryashov]

The following works:

  @Periodic.const_inv_smul₀ α β α f c _ _ Semiring.toModule h a

[Yury G. Kudryashov]

But it's a workaround

[Eric Wieser]

Does example [DivisionRing a] : Module a a := inferInstance at least work?

[Yury G. Kudryashov]

No, it doesn't

[Yury G. Kudryashov]

example {α} [DivisionRing α] : Module α α := inferInstance -- fails
example {α} [DivisionRing α] : Module α α := Semiring.toModule -- works

[Yury G. Kudryashov]

(deleted)

[Eric Wieser]

Ouch

[Eric Wieser]

I think this confirms my "new-style structure" hunch

[Eric Wieser]

import Mathlib.Algebra.Module.Basic

example {α} [Ring α] : Module α α := inferInstance -- fails, needs
/-
@Module α α (@Ring.toSemiring α inst✝)
  (@NonUnitalNonAssocSemiring.toAddCommMonoid α
    (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring α
      (@NonAssocRing.toNonUnitalNonAssocRing α (@Ring.toNonAssocRing α inst✝))))
-/
example {α} [CommSemiring α] : Module α α := inferInstance -- works, needs
/-
@Module α α (@CommSemiring.toSemiring α inst✝)
  (@NonUnitalNonAssocSemiring.toAddCommMonoid α
    (@NonAssocSemiring.toNonUnitalNonAssocSemiring α
      (@Semiring.toNonAssocSemiring α (@CommSemiring.toSemiring α inst✝))))
-/
#check Semiring.toModule
/-
Semiring.toModule.{u_1} {R : Type u_1} [inst✝ : Semiring R] :
  @Module R R inst✝
    (@NonUnitalNonAssocSemiring.toAddCommMonoid R
      (@NonAssocSemiring.toNonUnitalNonAssocSemiring R (@Semiring.toNonAssocSemiring R inst✝)))
-/

[Eric Wieser]

The one that works is a syntactic match, the one that fails is only a match after unfolding

[Kevin Buzzard]

This could be related to lean4#2074

[Kevin Buzzard]

That also involved failure of a defeq equality which wasn't syntactic in ring theory

[Eric Wieser]

That looks almost certainly related

[Kevin Buzzard]

yeah, if you do

set_option pp.all true
set_option pp.universes false
set_option trace.Meta.synthInstance true
set_option trace.Meta.isDefEq true

then you can see the failure in the first example boils down to this failure :

        [] ❌ @NonUnitalNonAssocSemiring.toAddCommMonoid α
              (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring α
                (@NonAssocRing.toNonUnitalNonAssocRing α
                  (@Ring.toNonAssocRing α
                    inst✝))) =?= @NonUnitalNonAssocSemiring.toAddCommMonoid α
              (@NonAssocSemiring.toNonUnitalNonAssocSemiring α
                (@Semiring.toNonAssocSemiring α (@Ring.toSemiring α inst✝))) ▼

and this is true by rfl.

[Reid Barton]

I added a comment on the issue.

[Reid Barton]

It seems like new-style structures would indeed have had the same issue in Lean 3

[Yury G. Kudryashov]

It seems that replacing DivisionRing with DivisionSemiring solves the problem.

[Yury G. Kudryashov]

It compiles.

[Eric Wieser]

While that change is reasonable in isolation, I think porting the rest of mathlib3 with workarounds for this issue in the remaining 70% of files would be a mistake. A lot of linear algebra and analysis is going to become very unpleasant, and removing the hacks later will likely be more work that just making problems like this as blocking and porting other things in the meantime

[Yury G. Kudryashov]

In this case, I generalized these lemmas, so while it's a workaround, it won't backfire later.

[Reid Barton]

You might have pushed off the problem to the users (if any) of whatever you changed, but I agree you probably didn't make anything worse.

[Eric Wieser]

I think writing Semiring.toModule in a bunch of places would be a step too far

[Yury G. Kudryashov]

I think that generalizing these lemmas is the right thing to do anyway.

[Eric Wieser]

I think we should either backport that or wait till after the port though

[Yury G. Kudryashov]

Why? The new lemmas are backward compatible with the old ones.