Zulip Chat Archive

Stream: new members

Topic: Trouble with instance resolution


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

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

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

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

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

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

view this post on Zulip Yury G. Kudryashov (Jul 08 2019 at 19:32):

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?

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

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

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

view this post on Zulip Yury G. Kudryashov (Jul 08 2019 at 19:52):

@Floris van Doorn Thank you for the explanation!

view this post on Zulip Johan Commelin (Jul 08 2019 at 20:13):

I do recall vaguely that show in data can cause little troubles down the road.

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

view this post on Zulip Johan Commelin (Jul 08 2019 at 20:14):

But I might very well be mistaken.

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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 20:29):

There is a tactic to fix this, I think it's called clean

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

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 20:34):

Aah -- a secret tactic! Not mentioned in any docs at all?

view this post on Zulip Mario Carneiro (Jul 08 2019 at 20:35):

It's pretty specialized, to basically this exact situation

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 20:35):

At least it has a docstring.

view this post on Zulip Mario Carneiro (Jul 08 2019 at 20:35):

it removes a bunch of things that are identity functions used for annotation

view this post on Zulip Mario Carneiro (Jul 08 2019 at 20:35):

like show

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

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

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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 20:43):

damn you macro annotation

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 20:44):

that's not particularly well-documented either, as far as I know

view this post on Zulip Floris van Doorn (Jul 08 2019 at 20:45):

Where is the "understatement" emoji?

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

view this post on Zulip Mario Carneiro (Jul 08 2019 at 20:51):

so clean can be fixed

view this post on Zulip Yury G. Kudryashov (Jul 08 2019 at 20:54):

I'll rewrite #1195 to use @is_*_hom

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