simp-normal form for bundled hom conversion

Stream: general

[Eric Wieser]

Which of these should be the simp-normal forms for ring_equiv.to_ring_hom and ring_equiv.to_add_equiv?

[Eric Wieser]

\poll The simp-normal forms should be:

[Eric Wieser]

(deleted)

[Eric Wieser]

(deleted)

[Bryan Gin-ge Chen]

(deleted)

[Eric Wieser]

/poll The simp-normal forms should be:
(↑f : R →+* S) and (↑f : R ≃+ S)
f.to_ring_hom and f.to_add_equiv

[Eric Wieser]

This question is really about _all_ the simple bundled maps, as right now it's all over the place.

[Kevin Buzzard]

My choice is made purely for aesthetic reasons. What other reasons should come into play here?

[Eric Wieser]

If coercions are simp-normal, then sometimes you have to write (f : @a_really_nasty_type_that_doesnt_elaborate _ _ ≃+ S) instead of f.to_add_equiv

[Eric Wieser]

Essentially, the coercion will almost always look nicer in the goal view, but the to_* version will almost always be easier to write

[Adam Topaz]

Can you think of an exmaple where (f : _ ≃+ S) doesn't elaborate properly?

[Eric Wieser]

Sometimes S is also a mouthful

[Adam Topaz]

(f : _ ≃+ _)

[Eric Wieser]

That doesn't work for lots of cases

[Eric Wieser]

Try expressing docs#ring_equiv.to_ring_hom_comp_symm_to_ring_hom using that notation

[Adam Topaz]

I'm sure you're right, but I think we should have an example we can play around with

[Adam Topaz]

Ok, I'll try :)

[Eric Wieser]

lemma to_ring_hom_comp_symm_to_ring_hom {R S} [semiring R] [semiring S] (e : R ≃+* S) :
  (e : R →+* S).comp ↑e.symm = ring_hom.id _ :=
by { ext, simp }

[Adam Topaz]

import data.equiv.ring

variables {R S : Type*} [semiring R] [semiring S]

theorem foo (e : R ≃+* S) : (↑(e.symm) : _ →+* _).comp (e : R →+* S) = ring_hom.id _ := sorry

[Eric Wieser]

Right, but you still had to pass R and S explicitly

[Adam Topaz]

true

[Kevin Buzzard]

But I think that passing explicit type ascriptions often makes code easier to read!

[Floris van Doorn]

My first impression would also be (f : R →+* S), but after the discussion I'm not so sure anymore...

[Eric Wieser]

Added a third option to the poll, we could do something like

abbreviation ring_equiv.to_«≃+» (f : M ≃+* N) := f.to_add_equiv

[Scott Morrison]

Too many scary brackets!

[Eric Wieser]

I've done some initial cleanups of lemmas about coercions in #6268. Once that's in, I'll try a follow-up PR to change the simp-normal form to what the consensus seems to be in this thread