The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Jun 19, 2017 at 3:45 PM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
> Like John, I use mostly Equivalence and Proper, the standard library does
> not define many more than those. Usually I have a variant of EquivDec as
> well for decidable equality tests.
> About John's issues, I find the second one quite interesting, I understand
> it's due to the high overlap allowed. One could imagine to have a warning
> when a user-introduced instance can be used to solve every goal of the
> class, and refine it to give warnings for overlap as well. I always
> refrained going into this direction because it quickly becomes heuristic in
> our setting to decide which instances overlap due to computation and
> dependencies. Maybe a simply minded syntactic check would help here though,
> providing part of a solution to problem 1 as well. I have no better solution
> to the diamond problem and would advocate the same fix.

More generally than EquivDec, I often end up adding a "Decision" typeclass:

Class Decision (P:Prop) : Type :=
decide : {P} + {~P}.
Arguments decide P [Decision].

And then it's very easy to add instances like:

Instance and_dec `{Decision P} `{Decision Q} : Decision (P /\ Q).
Instance nat_lt_dec (m n:nat) : Decision (m < n).
Instance Forall_dec `{!forall x:X, Decision (P x)} (l:list X) :
Decision (Forall P l).

etc.

(Although sometimes, I've found if I also define e.g. nat_le_dec,
nat_gt_dec, nat_ge_dec, it tends to resolve to nat_le_dec in every
case.  Probably not much of an issue, though, unless you want close
control over the extraction.)
-- 
Daniel Schepler