Zulip Chat Archive

Stream: maths

Topic: Unification hints for hom


view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 17 2019 at 21:12):

where can I learn about unification hints?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 17 2019 at 21:15):

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

view this post on Zulip Johan Commelin (Feb 27 2019 at 16:16):

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

view this post on Zulip Johan Commelin (Feb 27 2019 at 16:16):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 01 2019 at 14:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Mar 01 2019 at 21:02):

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

view this post on Zulip 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