## Stream: new members

### Topic: figuring out why something isn't decidable

#### Julian Berman (Oct 19 2020 at 19:57):

I have a predicate and some structures I've defined, all finite -- and so one I expect to be decidable if I've not done something wrong, but lean is telling me it has failed to synthesize type class instance for ⊢ decidable <my long expression of state> -- is there any trick I can use to see where in my hierarchy of types and definitions am I losing decidability? What I've been doing so far (sprinkling around @[reducible] on definitions and [derive decidable_eq] on structures to make the message continually simpler) is both a bit tedious and also ended in a dead end.

#### Kevin Buzzard (Oct 19 2020 at 20:08):

You can try example : decidable <some subexpression> := by apply_instance

#### Julian Berman (Oct 19 2020 at 20:24):

Aha, thanks, will give that a shot!

#### Alex J. Best (Oct 19 2020 at 20:47):

Julian can you give an example? I had some ideas for tricks that might work, but i want to see if they do before recommending anything here!

#### Julian Berman (Oct 19 2020 at 20:56):

My diff is small but it's to a larger amount of code which I'd have to tear out to make self contained.. I can paste the error message but I suspect that's not helpful until I minimize my example. Just in case:

[lean] [E] failed to synthesize type class instance for
⊢ decidable
(∀ (i : fin 1.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ),
({start_board := starting_position,
elements := ![((2, 0), 0, 1), ((2, 2), 1, 0), ((0, 1), 2, 2), ((0, 2), 2, 1), ((0, 0), 1, 2), ((1, 2),
2,
0), ((2, 0), 0, 1), ((2, 1), 0, 0), ((0, 0), 1, 2), ((1, 0), 0, 2), ((0, 2), 2, 1), ((2, 2),
1,
0), ((1, 0), 0, 2), ((0, 1), 2, 2), ((2, 1), 0, 0), ((1, 2), 2, 0)],
all_occupied_start' := _,
all_unoccupied_end' := _}.moves
i).is_legal)
state:
⊢ ∀ (i : fin 1.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ),
({start_board := starting_position,
elements := ![((2, 0), 0, 1), ((2, 2), 1, 0), ((0, 1), 2, 2), ((0, 2), 2, 1), ((0, 0), 1, 2), ((1, 2), 2, 0), ((2,
0),
0,
1), ((2, 1), 0, 0), ((0, 0), 1, 2), ((1, 0), 0, 2), ((0, 2), 2, 1), ((2, 2), 1, 0), ((1, 0),
0,
2), ((0, 1), 2, 2), ((2, 1), 0, 0), ((1, 2), 2, 0)],
all_occupied_start' := _,
all_unoccupied_end' := _}.moves
i).is_legal


#### Julian Berman (Oct 19 2020 at 20:57):

Which I basically tried chipping away at by adding dsimp [10 defs that stack to make that big thing]

#### Julian Berman (Oct 19 2020 at 20:57):

But perhaps Kevin's suggestion to instead try "bottoms-up" with some subexpressions is a better idea

#### Julian Berman (Oct 19 2020 at 20:58):

If I hit a wall again will work on getting something self-contained together.

Last updated: May 15 2021 at 22:14 UTC