hom classes and coercion

Stream: general

[Yury G. Kudryashov]

In #11091 I add some new *_hom_class instances and now Lean fails to simplify some coercion in data.polynomial.basic. I suggest that we define something like this (probably, with some out_params):

class fun_like.has_forgetful_coe (F G : Type*) {α : Type*} {β : α → Type*} [fun_like F α β] [fun_like G α β]
  extends has_coe_t F G :=
(coe_coe : ∀ f : F, ((f : G) : Π a, β a) = f)

Then we automatically get all coercions like (M ≃* N) → (M →* N). Currently, I'm not sure how to rewrite (((e : R ≃+* S) : R →+* S) : R →* S) to e : R →* S`.

[Anne Baanen]

The class looks good to me. Looks like α and β have to be out_params so the extends has_coe_t F G doesn't become a dangerous instance.

[Yury G. Kudryashov]

Do you have any ideas about the norm_cast lemma squashing two coes? Should we add a reducible non-instance fun_like.has_forgetful_coe.trans?

[Yury G. Kudryashov]

I don't want to make it an instance because Lean should find has_forgetful_coe F (M →* N) from monoid_hom_class F M N.

[Yury G. Kudryashov]

But it should be defeq to the instance coming from monoid_hom_class.

[Anne Baanen]

Agreed, let's not make trans an instance. The alternative is to unbundle the data (coe) from the class forgetful_coe, then we can be sure there's no non-instance appearing in the simp-normal form. But that has its own (term size) issues...

[Anne Baanen]

So I'm thinking along the lines of:

class fun_like.has_forgetful_coe (F G : Type*) {α : Type*} {β : α → Type*} [fun_like F α β] [fun_like G α β]
  [has_coe_t F G] :=
(coe_fn_coe : ∀ f : F, ((f : G) : Π a, β a) = f)

and then you should be able to prove

lemma coe_coe [has_forgetful_coe F G] [has_forgetful_coe G H] [has_forgetful_coe F H] (f : F) :
  ((f : G) : H) = (f : H) :=
coe_fn_injective (by simp only [coe_fn_coe]) -- or something like that

[Anne Baanen]

Then the monoid_hom_class.has_forgetful_coe would provide the F → H and G → H instances, and ring_hom_class.has_forgetful_coe the F → G instance.

[Anne Baanen]

Or actually, coe_coe should be provable without unbundling has_coe_t.