Zulip Chat Archive

Stream: general

Topic: Using unification hints to find bundled homs


Eric Wieser (Jan 23 2021 at 17:22):

I was hoping something like this would be possible, but it seems not to work:

import algebra.group.pi
import data.finset.basic
import algebra.big_operators.basic

def monoid_hom.coe_monoid_hom (α β : Type*) [monoid α] [comm_monoid β] : (α →* β) →* (α  β) :=
{ to_fun := λ g, g,
  map_one' := rfl,
  map_mul' := λ x y, rfl, }

/-- Tell the unifier where to find a monoid_hom that matches a coercion -/
@[unify] def monoid_hom.coe_hint {M N : Type*} [monoid M] [comm_monoid N]
  (f : M →* N) (coe_fn_hom : (M →* N) →* has_coe_to_fun.F f) : unification_hint :=
{ pattern     := f  coe_fn_hom f,
  constraints := [coe_fn_hom  monoid_hom.coe_monoid_hom M N] }

open_locale big_operators

example  {ι M N : Type*} [comm_monoid M] [comm_monoid N] (s : finset ι) (fs : ι  M →* N) :
  ( i in s, fs i) = ( i in s, fs i) := begin
    -- convert (monoid_hom.coe_monoid_hom M N).map_prod _ _, -- works
    convert monoid_hom.map_prod _ fs _, -- leaves unsolved goals, unifier can't guess the hom
  end

My understanding was that unification hints are for telling the elaborator how to fill in metavariables automatically - but despite the goal matching pattern exactly, it doesn't appear to use my hint.

Am I missing something here?


Last updated: Dec 20 2023 at 11:08 UTC