deriving decidable

Stream: general

[Hunter Freyer]

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]

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]

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

[Mario Carneiro]

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