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 := λ _, α → β,

@[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⟩] }

(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:

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 (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