Trouble with instance resolution

Stream: new members

[Yury G. Kudryashov]

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]

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]

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]

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]

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]

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.

[Yury G. Kudryashov]

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]

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]

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]

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]

@Floris van Doorn Thank you for the explanation!

[Johan Commelin]

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

[Johan Commelin]

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]

But I might very well be mistaken.

[Floris van Doorn]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

It's pretty specialized, to basically this exact situation

[Kevin Buzzard]

At least it has a docstring.

[Mario Carneiro]

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

[Mario Carneiro]

like show

[Mario Carneiro]

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]

rw foo_eq'' also fails with "can't find foo" which makes no sense since that's literally the statement

[Mario Carneiro]

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]

damn you macro annotation

[Kevin Buzzard]

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

[Floris van Doorn]

Where is the "understatement" emoji?

[Mario Carneiro]

by sheer luck, there is an API function expr.is_annotation that will allow us to destructure an annotation

[Mario Carneiro]

so clean can be fixed

[Yury G. Kudryashov]

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

[Mario Carneiro]

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