Zulip Chat Archive

Stream: general

Topic: deriving decidable


view this post on Zulip Hunter Freyer (Sep 22 2020 at 00:01):

What's the best practice for modeling decidable relations? I could have a function from A -> A -> bool, but then I don't get a proof object I can do induction over. The only other thing I can think of is writing an inductive to model the proof, and then also implement the decision procedure, but it seems like I'll be essentially writing the same code twice. Thoughts?

view this post on Zulip Hunter Freyer (Sep 22 2020 at 00:02):

The topic gives away what I'd magically love to have happen: just a @[derive decidable] tag that for a subset of types could come up with a decision procedure based on the type signature. But I don't think that's a thing.

view this post on Zulip Mario Carneiro (Sep 22 2020 at 00:05):

The usual approach is to use a Prop valued function and a proof it is decidable

view this post on Zulip Mario Carneiro (Sep 22 2020 at 00:08):

If you have a recursive function, it's pretty simple to build the decision procedure (and you might even consider using bool for this if you are worried about code duplication). But for inductive types it's not at all simple to come up with a decision procedure in general


Last updated: May 16 2021 at 21:11 UTC