# Zulip Chat Archive

## Stream: maths

### Topic: Unification hints for hom

#### Chris Hughes (Feb 17 2019 at 20:21):

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 (Feb 17 2019 at 21:12):

where can I learn about unification hints?

#### Kevin Buzzard (Feb 17 2019 at 21:12):

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

#### Kevin Buzzard (Feb 17 2019 at 21:15):

There's this:

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 (Feb 27 2019 at 16:16):

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

#### Johan Commelin (Feb 27 2019 at 16:16):

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

#### Johan Commelin (Feb 27 2019 at 16:18):

@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 (Mar 01 2019 at 14:41):

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

#### Mario Carneiro (Mar 01 2019 at 20:59):

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 (Mar 01 2019 at 21:00):

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 (Mar 01 2019 at 21:02):

Does it work with `simp`

though. That's the main upside of bundling I think.

#### Johan Commelin (Mar 02 2019 at 10:09):

Right, if it doesn't work with `simp`

we are back to square 1.

Last updated: May 14 2021 at 19:21 UTC