## Stream: new members

### Topic: Trouble with instance resolution

#### Yury G. Kudryashov (Jul 08 2019 at 18:31):

Hi, I'm trying to prove some simple facts about End and Aut, see https://github.com/urkud/mathlib/blob/22ceb7d817a0f772a4ad9bb72eb3f282b4ebc920/src/category_theory/endomorphism.lean#L72
Could you please explain why Lean fails to find instances for monoid (End X) and monoid (End (f.obj X)) here? It tries End.monoid but says that is_defeq failed.

#### Kevin Buzzard (Jul 08 2019 at 19:04):

instance foo : @is_monoid_hom (End X) (End (f.obj X)) _ _ (@functor.map _ _ _ _ f X X : End X → End (f.obj X))


works.

What I think is going on is that Lean is actually looking for instances for monoid (X ⟶ X) and monoid (f.obj X ⟶ f.obj X). You tell Lean explicitly that you want the output of functor.map to have type End X → End (f.obj X) but I don't think Lean listens. It checks that the type is defeq to that but for some reason when the type class algorithm is running it has already decided that monoid (X ⟶ X) is what it should be looking for.

#### Kevin Buzzard (Jul 08 2019 at 19:09):

instance : monoid (X ⟶ X) := by apply_instance


fails, but

instance : monoid (X ⟶ X) := by {show monoid (End X), by apply_instance}


works and starts to solve the issues. There might also be some clever way of getting Lean to do elaboration in some different way.

#### Yury G. Kudryashov (Jul 08 2019 at 19:16):

Thanks @Kevin Buzzard! Indeed it was looking for monoid (X ⟶ X) instead of monoid (End X). I wonder why End.monoid fails defeq anyway but at least now I have a workaround.

#### Floris van Doorn (Jul 08 2019 at 19:20):

Type class inference does not do full definitional equality checking, for performance reasons. It should work if you make End reducible.

local attribute [reducible] End


#### Kevin Buzzard (Jul 08 2019 at 19:23):

But (@functor.map _ _ _ _ f X X : End X → End (f.obj X)) is supposed to have type End X → End (f.obj X) and that is what is fed to is_monoid_hom. I still don't quite understand what is going on here. Elaboration of that term is still spitting out something of type (X ⟶ X) → (f.obj X ⟶ f.obj X) despite Yury's pleas to do something else.

Is it possible to avoid at least one of the two @? I mean, @is_monoid_hom (End X) (End $f.obj X) _ _ f.map doesn't work because term f.map has type Π {X Y : C}, (X ⟶ Y) → (f.obj X ⟶ f.obj Y) : Type (max u v v') but is expected to have type End X → End (f.obj X) : Type (max v v') Is it about extra arguments, or about End not marked as reducible? #### Floris van Doorn (Jul 08 2019 at 19:45): But (@functor.map _ _ _ _ f X X : End X → End (f.obj X)) is supposed to have type End X → End (f.obj X) and that is what is fed to is_monoid_hom. I still don't quite understand what is going on here. Elaboration of that term is still spitting out something of type (X ⟶ X) → (f.obj X ⟶ f.obj X) despite Yury's pleas to do something else. The notation (t : T) asks Lean to check (and enforce) that the type of t is definitionally equal to T. After Lean has done that, Lean will happily forget that you ever asked, and just continue with what it thought was the type of t. To enforce that Lean uses the type T for t, use show T, from t. This works: instance foo : is_monoid_hom (show End X → End (f.obj X), from functor.map f) := sorry  #### Floris van Doorn (Jul 08 2019 at 19:46): Alternatively, if you don't like show and want to give implicit arguments, give them to is_monoid_hom: instance foo : @is_monoid_hom (End X) (End (f.obj X)) _ _ (functor.map f) := sorry  #### Floris van Doorn (Jul 08 2019 at 19:49): f.map This is a bug with the projection notation: the first argument of functor.map after the explicit argument is implicit, and the projection notation cannot deal with that if you don't apply it to another argument. In this case you just have to write functor.map f. #### Yury G. Kudryashov (Jul 08 2019 at 19:52): @Floris van Doorn Thank you for the explanation! #### Johan Commelin (Jul 08 2019 at 20:13): I do recall vaguely that show in data can cause little troubles down the road. #### Johan Commelin (Jul 08 2019 at 20:14): So even if it is more readable this way, I think that in practice the @is_monoid_hom version might be better for applications... #### Johan Commelin (Jul 08 2019 at 20:14): But I might very well be mistaken. #### Floris van Doorn (Jul 08 2019 at 20:21): I do recall vaguely that show in data can cause little troubles down the road. yeah, I wouldn't be surprised if the instance is_monoid_hom (show End X → End (f.obj X), from functor.map f) does not always apply when @is_monoid_hom ... (functor.map f) does. The form @is_monoid_hom ... (functor.map f) feels safer indeed. #### Mario Carneiro (Jul 08 2019 at 20:29): There is a tactic to fix this, I think it's called clean #### Mario Carneiro (Jul 08 2019 at 20:32): import tactic.basic def foo := 1 @[simp] theorem foo_eq : (show ℕ, from foo) = 1 := rfl #print foo_eq -- theorem foo_eq : (show ℕ, from foo) = 1 example : foo = 1 := by simp -- fails @[simp] theorem foo_eq' : (by clean show ℕ, from foo) = 1 := rfl #print foo_eq' -- theorem foo_eq' : foo = 1 example : foo = 1 := by simp -- works  #### Kevin Buzzard (Jul 08 2019 at 20:34): Aah -- a secret tactic! Not mentioned in any docs at all? #### Mario Carneiro (Jul 08 2019 at 20:35): It's pretty specialized, to basically this exact situation #### Kevin Buzzard (Jul 08 2019 at 20:35): At least it has a docstring. #### Mario Carneiro (Jul 08 2019 at 20:35): it removes a bunch of things that are identity functions used for annotation #### Mario Carneiro (Jul 08 2019 at 20:35): like show #### Mario Carneiro (Jul 08 2019 at 20:36): hm, this fails, but it looks like a lean bug: @[simp] theorem foo_eq'' : by clean (show ℕ, from foo) = 1 := rfl #print foo_eq'' -- theorem foo_eq'' : foo = 1 example : foo = 1 := by simp -- fails  #### Mario Carneiro (Jul 08 2019 at 20:37): rw foo_eq'' also fails with "can't find foo" which makes no sense since that's literally the statement #### Mario Carneiro (Jul 08 2019 at 20:43): Oh, these are not the same, but pp.all isn't enough to show the difference. (I changed 1 to nat.zero to make the super-pp-all not so big) def foo := nat.zero theorem foo_eq₁ : foo = nat.zero := rfl theorem foo_eq₂ : by clean (show ℕ, from foo) = nat.zero := rfl set_option pp.all true #print foo_eq₁ -- theorem foo_eq₁ : @eq.{1} nat foo nat.zero #print foo_eq₂ -- theorem foo_eq₂ : @eq.{1} nat foo nat.zero run_cmd do d ← tactic.get_decl foo_eq₁, tactic.trace d.type.to_raw_fmt -- (app (app (app (const eq [1]) (const nat [])) (const foo [])) (const nat.zero [])) run_cmd do d ← tactic.get_decl foo_eq₂, tactic.trace d.type.to_raw_fmt -- (app (app (app (const eq [1]) (const nat [])) [macro annotation (const foo [])]) (const nat.zero []))  #### Mario Carneiro (Jul 08 2019 at 20:43): damn you macro annotation #### Kevin Buzzard (Jul 08 2019 at 20:44): that's not particularly well-documented either, as far as I know #### Floris van Doorn (Jul 08 2019 at 20:45): Where is the "understatement" emoji? #### Mario Carneiro (Jul 08 2019 at 20:51): by sheer luck, there is an API function expr.is_annotation that will allow us to destructure an annotation #### Mario Carneiro (Jul 08 2019 at 20:51): so clean can be fixed #### Yury G. Kudryashov (Jul 08 2019 at 20:54): I'll rewrite #1195 to use @is_*_hom #### Mario Carneiro (Jul 08 2019 at 21:01): import tactic.basic open tactic interactive expr interactive.types meta def clean_aux : expr → option expr | (app (app (const n _) _) e') := guard (n ∈ interactive.clean_ids) >> (clean_aux e').get_or_else e' | (app (lam _ _ _ (var 0)) e') := (clean_aux e').get_or_else e' | e := do e' ← prod.snd <$> expr.is_annotation e,
(clean_aux e').get_or_else e'

meta def tactic.interactive.clean' (q : parse texpr) : tactic unit :=
do tgt : expr ← target,
e ← i_to_expr_strict (%%q : %%tgt),
tactic.exact \$ e.replace (λ e n, clean_aux e)

def foo := nat.zero

@[simp] theorem foo_eq₃ : by clean' (show ℕ, from foo) = nat.zero := rfl
run_cmd do
d ← tactic.get_decl foo_eq₃,
tactic.trace d.type.to_raw_fmt
-- (app (app (app (const eq [1]) (const nat [])) (const foo [])) (const nat.zero []))

example : foo = nat.zero := by simp -- works
`

Last updated: May 11 2021 at 22:14 UTC