Unification hints for hom

Stream: maths

[Chris Hughes]

Can we use unification hints for bundled homs? This is my best attempt, but it doesn't work

import algebra.field
def is_ring_hom' {α β : Type*} (f : α → β) : Prop := sorry

structure ring_hom (α β : Type*) :=
(f : α → β)
(is_hom : is_ring_hom' f)

instance (α β : Type*) : has_coe_to_fun (ring_hom α β) :=
{ F := λ _, α → β,
  coe := ring_hom.f }

def is_monoid_hom' {α β : Type*} (f : α → β) : Prop := sorry

structure add_monoid_hom (α β : Type*) :=
(f : α → β)
(is_hom : is_monoid_hom' f)

instance I2 (α β : Type*) : has_coe_to_fun (add_monoid_hom α β) :=
{ F := λ _, α → β,
  coe := add_monoid_hom.f }

@[unify] def ring_hom_to_add_monoid_hom {α β : Type*}
  (g : add_monoid_hom α β) (f : ring_hom α β) : unification_hint :=
{ pattern := (f : α → β) ≟ g,
  constraints := [g ≟ ⟨f.1, sorry⟩] }

lemma add_group_hom_add {α β : Type*} [add_monoid α] [add_monoid β] (f : add_monoid_hom α β)
  (x y : α) : f (x + y) = f x + f y := sorry

example {α β : Type*} [semiring α] [semiring β] (f : ring_hom α β) (x y : α) :
  f (x + y) = f x + f y := by rw add_group_hom_add

[Kenny Lau]

where can I learn about unification hints?

[Kevin Buzzard]

Cyril and Assia talked about them in Amsterdam and their notes are available on the thread IIRC

[Kevin Buzzard]

There's this:

https://leanprover.zulipchat.com/#narrow/stream/179818-Lean-Together.202019/topic/Unification.20hints.20paper

but that wasn't what I was remembering. Someone put links to a lot of the pdfs used in the talks but I can't find it right now

[Johan Commelin]

Is this issue that Chris raised blocking our move to bundled homs?

[Johan Commelin]

Can we find a solution to this, or should we give up on bundled homs?

[Johan Commelin]

@Cyril Cohen gave links to the unification hints demo files from Lean Together:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unification.20hints/near/158613068

[Johan Commelin]

@Mario Carneiro @Cyril Cohen Do you have any thought on this issue/idea?

[Mario Carneiro]

I think this can be proven without unification hints as

instance (α β : Type*) : has_coe (ring_hom α β) (add_monoid_hom α β) :=
⟨λ f, ⟨f.1, sorry⟩⟩

example {α β : Type*} [semiring α] [semiring β] (f : ring_hom α β) (x y : α) :
  f (x + y) = f x + f y := add_group_hom_add (f : add_monoid_hom α β) x y

[Mario Carneiro]

it will be nice if unification hints can be made to work, but I don't see why they wouldn't in this case so they might just be broken

[Chris Hughes]

Does it work with simp though. That's the main upside of bundling I think.

[Johan Commelin]

Right, if it doesn't work with simp we are back to square 1.