Topic: deriving decidable
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?
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.
Mario Carneiro (Sep 22 2020 at 00:05):
The usual approach is to use a Prop valued function and a proof it is decidable
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