Zulip Chat Archive

Stream: new members

Topic: figuring out why something isn't decidable


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 19 2020 at 20:08):

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

view this post on Zulip Julian Berman (Oct 19 2020 at 20:24):

Aha, thanks, will give that a shot!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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