Zulip Chat Archive

Stream: general

Topic: why can't Lean generate this instance?


view this post on Zulip Kenny Lau (Apr 08 2020 at 20:36):

universes u

example {α β : Type u} [discrete_linear_ordered_field α] (f : β  α) (x : α) :
  decidable_pred (λ i, x < f i) :=
by apply_instance

why does this fail?

error state:

tactic.mk_instance failed to generate instance for
  decidable_pred (λ (i : β), x < f i)
state:
α β : Type u,
_inst_1 : discrete_linear_ordered_field α,
f : β  α,
x : α
 decidable_pred (λ (i : β), x < f i)

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 20:45):

Did you try to look at the trace?

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:46):

yeah it keeps trying a billion things on the lambda thing

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:46):

actually it substituted in the lambda so it's trying to prove some (_ : \a) < _ is decidable

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:47):

but somehow it never finds the right instance

view this post on Zulip Chris Hughes (Apr 08 2020 at 20:47):

If you beta reduce it does it work?

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:48):

so you mean intro?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 20:48):

If I put decidable_linear_order instead of discrete*, it works.

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 20:49):

Doesn't work with decidable_linear_ordered_comm_group

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:53):

can this be solved with some priority hacking?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 20:55):

It tries has_lt.lt.decidable but for some reason defeq fails.

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 20:55):

@Gabriel Ebner ?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 20:55):

@Simon Hudon ?

view this post on Zulip Gabriel Ebner (Apr 08 2020 at 21:03):

The surprising thing is that the following works:

example {α β : Type u} [discrete_linear_ordered_field α] (f : β  α) (x : α) (i : β) :
  decidable (x < f i) :=
by apply_instance

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 21:13):

I don't know how to debug this...

view this post on Zulip Gabriel Ebner (Apr 08 2020 at 21:14):

Problem seems to be in unification, because the type-class search creates higher-order patterns like ?x_123 a:

-- also fails
example {α β : Type u} [discrete_linear_ordered_field α] (f : β  α) (x : α) :
   i, decidable (x < f i) :=
by apply_instance

view this post on Zulip Gabriel Ebner (Apr 08 2020 at 21:14):

I haven't got a good explanation either, but here's a workaround:

instance foo {α} [discrete_linear_ordered_field α] (a b : α) : decidable (a < b) :=
by apply_instance

Last updated: May 10 2021 at 18:22 UTC