## Stream: general

### Topic: why can't Lean generate this instance?

#### 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)


#### Yury G. Kudryashov (Apr 08 2020 at 20:45):

Did you try to look at the trace?

#### Kenny Lau (Apr 08 2020 at 20:46):

yeah it keeps trying a billion things on the lambda thing

#### Kenny Lau (Apr 08 2020 at 20:46):

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

#### Kenny Lau (Apr 08 2020 at 20:47):

but somehow it never finds the right instance

#### Chris Hughes (Apr 08 2020 at 20:47):

If you beta reduce it does it work?

#### Kenny Lau (Apr 08 2020 at 20:48):

so you mean intro?

#### Yury G. Kudryashov (Apr 08 2020 at 20:48):

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

#### Yury G. Kudryashov (Apr 08 2020 at 20:49):

Doesn't work with decidable_linear_ordered_comm_group

#### Kenny Lau (Apr 08 2020 at 20:53):

can this be solved with some priority hacking?

#### Yury G. Kudryashov (Apr 08 2020 at 20:55):

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

@Gabriel Ebner ?

@Simon Hudon ?

#### 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


#### Yury G. Kudryashov (Apr 08 2020 at 21:13):

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

#### 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


#### 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