Algebra.Ring.Equiv help request

Stream: mathlib4

[Anatole Dedecker]

I'm currently working on Algebra.Ring.Basic (mathlib4#1077) and I could use a bit of help for the following things:

• do we have assert_not_exists in Lean4? It was here to prevent mathlib3 PRs from messing with imports, so should I just get rid of it?
• the linter complains that I added no doc to the map_add field of RingEquivClass. I could add a doc of course, but the fact that the linter complains suggest that it is treated as a def not a lemma. Is there a way to fix that?

class RingEquivClass (F : Type _) (R S : outParam (Type _)) [Mul R] [Add R] [Mul S] [Add S] extends
  MulEquivClass F R S where
  map_add : ∀ (f : F) (a b), f (a + b) = f a + f b
#align ring_equiv_class RingEquivClass

• lots of lemmas which used to be tagged simp now trigger the simpNF linter. I think this is because coercions are fully expanded, and this expanded form exhibits terms that aren't in simp normal form. But somehov it even feels wrong that simp gets to see these expanded terms, is that realy the optimal solution?

[Eric Wieser]

assert_not_exists wasn't created solely to support porting, it was created to mitigate a problem that was spotted as a side-effect of porting.

[Eric Wieser]

Someone should probably port the tactic, but it's probably fine to leave behind TODOs for now

[Eric Wieser]

Did you remove the shortcut CoeFun instance?

[Anatole Dedecker]

Eric Wieser said:

Did you remove the shortcut CoeFun instance?

I did because it was removed for MulEquiv (I think?)

[Kevin Buzzard]

Possibly related: https://github.com/leanprover-community/mathlib4/pull/931 .

[Scott Morrison]

Yes, please leave all assert_not_exists in place, commented out, with a -- Porting note: not implemented yet.

[Scott Morrison]

Answering your other questions:

• We've decided that doc-strings for fields of structures are valuable, whether they are defs or theorems, but yes, it would be nice if these were theorems.
• Re: coercions fully expanded: that ship has sailed. :-)

[Anatole Dedecker]

coercions fully expanded: that ship has sailed

Well, it would have been surprising if we didn't meet any problems during the port!
I think I have a potential solution, but I'd like to hear from experts before trying it further. Since simp doesn't go through definition, I would suggest that instances of the form

instance [SomeHomClass F α β] : CoeTC F (CorrespondingHomType α β) :=
  ⟨fun f =>
    { toFun := f,
      some := _,
      other := _,
      fields := _ }⟩

get replaced by

@[coe]
def SomeHomClass.toCorrespondingHomType [SomeHomClass F α β] (f : F) : CorrespondingHomType α β :=
{ toFun := f,
  some := _,
  other := _,
  fields := _ }

instance [SomeHomClass F α β] : CoeTC F (CorrespondingHomType α β) :=
  ⟨SomeHomClass.toCorrespondingHomType⟩

That way there is no problem anymore since simp doesn't unfold the new SomeHomClass.toCorrespondingHomType definition (which just gets printed as a coercion).

Incidentally, this also fix the @[norm_cast] problem I was experiencing there

Does it look wrong?

[Mario Carneiro]

simp does not know anything about the @[coe] attribute

[Anatole Dedecker]

Right it's just that it doesn't unfold the definition

[Mario Carneiro]

but your suggestion looks correct, in the sense that you should never have a complicated term in a Coe instance because it is unfolded at parse time and no one wants to see that stuff

[Mario Carneiro]

we should probably have a linter for this

[Anatole Dedecker]

So should I have a go at doing that for all of these instances? We already have quite a few, just type instCoeTC in the search bar and at least the ten first definitions follow this pattern

[Anatole Dedecker]

Maybe @Anne Baanen and @Eric Wieser want to be aware of this

[Eric Wieser]

Your suggestion looks like a reasonable way to translate what we have in mathlib3; I still dislike these instances for other reasons, but that's not something that makes sense to address while porting

[Anatole Dedecker]

Okay so I did all of these changes in mathlib4#1150. Now the linter complains that f.toFun (for f : α →+* β) is not in simp normal form (in docs4#RingHom.toFun_eq_coe) because it really means f.toMonoidHom.toOneHom.toFun and f.toMonoidHom can be simplified to MonoidHomClass.toMonoidHom f... I notice a lot of these toFun_eq_coe have been removed in other files (by @Winston Yin in particular), should I do the same here. That feels right to me in the sense that we know which of these lemmas are useful in Lean3, but it doesn't make any sense to bother about them if we aren't even sure they'll actually be used, but I don't want to take that kind of decision.

[Eric Wieser]

Anatole Dedecker said:

and f.toMonoidHom can be simplified to MonoidHomClass.toMonoidHom f

This is one of the things I don't like about these coercion instances...

[Eric Wieser]

I would caution against removing any lemma entirely, but we could remove simp and add a porting note

[Eric Wieser]

There's also the option of abandoning new-style classes for morphisms (ie, not using extends at all); then f.toFun would really mean f.toFun and there would be no f.toMonoidHom.

[Anatole Dedecker]

For now I'll remove the simp. I don't feel competent at all to make big design decisions here :sweat_smile:

[Anatole Dedecker]

mathlib4#1150 is now ready for review with the changes discussed above. The port of Algebra.Ring.Equiv mathlib4#1077 now depends on it

[Kevin Buzzard]

(mathlib4 not matrhlib4)