The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Nov 8, 2018 at 5:04 AM Théo Zimmermann 
<theo.zimmi AT gmail.com>
 wrote:
> You may or may not be aware of the existence of a project to design a
> new standard library (without backward compatibility):
> https://github.com/coq/stdlib2

I took a look at the project; however, I found the current layout
confusing and I'm not sure where I would submit a "possible feature
discussion" request.  Of course, maybe a bug tracker might not be the
best place for such discussions.

Anyway, something I've been thinking of for a while that would be
useful would be if the standard library (either as an extension to the
current one, or in the new one) had an integrated "decidable
proposition" typeclass, something like:

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

And then wherever a proposition should be decidable, the library would
declare an instance of Decision for it - with dependencies on
decidability for subpropositions as needed, of course.

It could also be nice to then add a "decide" tactic which simply tries
to find a decidability instance for the current goal and then evaluate
to either extract a proof, or give an error that the decision
procedure gave a false result.

I've also thought that this could be greatly enhanced by a
"combinatorics" type of functionality.  So, for example, if it were
asked to decide "forall x y : bool, andb x (orb x y) = x" then it
would first search for an "exhaustive listing" instance for bool, then
use that to test all possible values of x and y against a decision
instance for @eq bool.  And possibly, if it were asked to decide
something like "forall n : N, n < 100 -> P n" or "exists n : Z, -100 <
n /\ n < 100 /\ P n" then it could first search through the
proposition for an a priori bound on the values which need to be
tested.

Then, of course, decidability could feed back into combinatorics - for
example, it could do a brute force calculation of # { n : N | n < 100
/\ Prime n } using an a priori bound search and then a decision
instance for Prime to list out the elements of the sigma-type
internally and then count the length of the list.  (Though this last
one would depend on whether a new standard library would use setoids
widely or not, in the way that e.g. MathClasses does...)

(I'm not insistent on using sumbool, though it tends to be my personal
preference.  I would also be OK with
Class Decision (P : Prop) : Type :=
decide : bool.
Arguments decide P [Decision].
Class DecisionCorrect (P : Prop) `{!Decision P} : Prop :=
decision_correct : P <-> (decide P = true).
if it helps with efficiency of evaluating decision procedures, and/or
we want maximal abstraction of the proof resulting from the "decide"
tactic to "match (decision_correct P) with | conj _ H => H (eq_refl
true) end" as opposed to a proof constructed piece by piece along the
decidability call chain.)
-- 
Daniel Schepler