figuring out why something isn't decidable

Stream: new members

[Julian Berman]

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]

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

[Julian Berman]

Aha, thanks, will give that a shot!

[Alex J. Best]

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]

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]

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

[Julian Berman]

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

[Julian Berman]

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