failed to synthesize type class instance decidable_pred

Stream: new members

[Henning Dieterichs]

I have this function definition:

def test : list (nat × nat) → list (nat × nat)
| list := list.filter (λ ⟨ a, b ⟩, a > 10)

But I get the error

failed to synthesize type class instance for
test : _root_.list (ℕ × ℕ) → _root_.list (ℕ × ℕ),
list : _root_.list (ℕ × ℕ)
⊢ decidable_pred (λ (_x : ℕ × ℕ), test._match_1 _x)

This works though:

def test : list (nat × nat) → list (nat × nat)
| list := list.filter (λ x, x.fst > 10)

Seems like destructuring is not very compatible with automatic inference of decidability?

[Kevin Buzzard]

You can see exactly the problem which occurs. Using λ ⟨ a, b ⟩ is fine for proving theorems, but causes problems when making definitions because of the way Lean 3 takes this apart internally. Stick to the bottom one.

[Henning Dieterichs]

Thanks! I'd love to use destructuring though, as fst and snd are not very speaking

[Kevin Buzzard]

There's x.1 and x.2 but I totally agree.

[Jasmin Blanchette]

fst and snd are the traditional ML names, probably from the 80s if not earlier. We could always switch to Lisp-style car and cdr. :smiley:

[Kevin Lacker]

I wonder, why exactly doesn't this destructuring work in this situation? it would be a lot more readable to use inline functions of product types with destructuring syntax. I don't quite understand what the failed to synthesize type class instance error means here

[Kevin Buzzard]

You can see what happens from the error I guess. Lean can't see through the test._match_1 and I'm not sure if we can get to it to mark it reducible.

[Kevin Buzzard]

I was writing code for undergraduates last week and I did find this really annoying -- I defined a map on nat^2 by f(x)=something involving x.1 and x.2, and then I immediately wrote a lemma saying that f((a,b)) was the same thing but involving a and b. At the time I thought it looked clunky but this is what people have been doing in the past. Until January there were many requests from users for which the answer was "we can't do anything about it, it's in core" but now we have control of core we can do more things. I have no idea whether we can do something about this though. I can't remember whether have people have thought about it seriously since January -- I think a lot of us are just resigned to the x.1, x.2 thing.

[Kevin Lacker]

this sort of destructuring also semi-recently got into javascript and it has been nice there

[Mario Carneiro]

The issue is that there is no decidable instance defined for test._match_1

[Mario Carneiro]

marking it reducible won't help, it's defined by cases and there is no decidable instance for foo.cases_on either

[Kevin Lacker]

why is it any different from calling the pair _x and referring to the parts as _x.1 and _x.2? to me it seems like you'd be able to deduce the same thing about either syntax, since they are logically identical

[Mario Carneiro]

this is slightly different from the problem of definitional equalities that explains why we usually avoid pattern matching definitions

[Mario Carneiro]

They are logically identical, but that doesn't mean that they have the same instances

[Mario Carneiro]

even defeq things can have different instances

[Mario Carneiro]

Normally, you would make a definition and then prove it's decidable. If you made test._match_1 into a proper definition that's what you would do, and then there would be no issue

[Mario Carneiro]

but for these on the spot definitions it's usually not worth the effort compared to a slight reformulation

[Kevin Lacker]

so the problem is that lean sees the pair, and it's like well who knows if a lambda on a pair is decidable, and then it fails because it does not know that a lambda on a pair is decidable when the lambda is decidable on each of the parts

[Mario Carneiro]

It doesn't see lambda on a pair at all, it sees a new definition

[Reid Barton]

Even if it could see through all the equation compiler stuff, it would still face the term x.cases_on (\lam a b, a < 10) rather than the term x.fst < 10

[Mario Carneiro]

There is some parser magic that means that \lam <x, y>, e is equivalent to pausing the current elaboration, writing def foo | <x, y> := e just above, and then inserting foo at the point of use

[Mario Carneiro]

Conceivably, we could have instances that prove things about decidability of a cases_on expression

[Mario Carneiro]

but it still requires some unfolding

[Kevin Lacker]

if the parser magic is inserting foo everywhere, why does it work differently for a human to put foo.1 and foo.2 throughout the expression? because there's an extra def this way?

[Mario Carneiro]

foo.1 and foo.2 don't make new definitions

[Mario Carneiro]

it's also literally a different expression as reid says

[Mario Carneiro]

it's the difference between x.cases_on (\lam a b, a < 10) and x.cases_on (\lam a b, a) < 10

[Mario Carneiro]

the second one is obviously decidable even if you don't know what cases_on does