Rewrite failed (!4#4087 Algebra.MonoidAlgebra.ToDirectSum)

Stream: mathlib4

[Pim Otte]

In https://github.com/leanprover-community/mathlib4/pull/4087 I'm stuck on this line. I've compared the types, and I think the rewrite should work. The only thing I can spot is the x y/f g difference, but I'm pretty sure that they're alpha-equivalent. Anyone got a pointer?

[Eric Wieser]

The rewrite fails because the instance further up the file fails

[Eric Wieser]

If you can't get a definition to work, all the failures about it below are nonsense

[Pim Otte]

Ah, thank!

[Eric Wieser]

I reverted your fix commit, it changed the meaning of your results and made some of them false

[Pim Otte]

That would've been hard to prove then:') I'll study to see if I grasp it better now:)

[Eric Wieser]

The underlying problem here is that a huge pile of lemmas about Finsupp addition no longer work on AddMonoidAlgebra

[Pim Otte]

Do you have any advice for a particular angle how to fix that? (Adding Coe instances sort of intuitively makes sense, but I have no clue if that's actually a valid path)

[Eric Wieser]

Adding coe instances sounds like the wrong approach to me

[Eric Wieser]

I on't have a good answer though; so far it seems we've just duplicate every bit of API for finsupp that we need; see near docs4#AddMonoidAlgebra.single. There are 10 or so lemmas which are just copied

[Pim Otte]

I guess that would work, so I'll give that a shot. Thanks a lot:)

[Eric Wieser]

Replacing simp and rw with erw sometimes works too

[Pim Otte]

I did end up adding a type class instance to fix most of it, I'm not sure if what I has any unintended side-effects, but the whole thing does compile, so I'm guessing it's at least a good starting point?

[Kevin Buzzard]

I would say the converse -- changing mathlib whilst porting is a high-risk strategy and it's better to understand what's going on than just making random changes in order to get one file compiling locally.

[Pim Otte]

Well, the fact that I'm winging it a little bit is the reason I'm picking files without dependents to learn:)

Is there a particular reason adding an instance is more risky than duplicating API?

[Kevin Buzzard]

As long as we understand that why the instance is necessary in Lean 4 and not in Lean 3 it's fine.

[Pim Otte]

Well, I don't understand yet, but I added a comment, so a reviewer won't overlook it:)

[Eric Wieser]

What was the instance?

[Pim Otte]

noncomputable instance [AddMonoid ι] [Semiring M] :
  NonUnitalNonAssocSemiring (ι →₀ M) := AddMonoidAlgebra.nonUnitalNonAssocSemiring

[Eric Wieser]

That instance is bad, it conflicts with the pointwise instance

[Pim Otte]

And what about if I made it a local instance?

[Eric Wieser]

It's still very much a hack, and it would be better to find the right solution

[Pim Otte]

This is what @Chris Hughes ended up doing: https://github.com/leanprover-community/mathlib4/pull/4087/commits/ba111775b57a5c957749b7b99c53269c2a0f8d80

Thanks all for the pointers:)

[Eric Wieser]

That's probably the least hacky way to use the instance. It would still be good to understand the failure, because we don't want to have to use this hack every time

[Chris Hughes]

It sounds like the problem is that we're using Finsupp lemmas on AddMonoudAlgebra, so sometimes AddMonoidAlgebra gets unfolded which is bad because we can't synthesise instances for it. We should properly transfer the lemmas we need about Finsupp.

[Eric Wieser]

It's not just the lemmas, but the defs too