The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

You could define a decision procedure for a predicate P : A -> Prop to
be a function f : A -> bool such that forall x : A, P x <-> f x =
true. While this avoids mentioning false or negation explicitly, I
suspect it won't really help you in showing that some compllicated P
has a decision procedure. You might be better off by starting with a
different definition of decidable predicates, i.e, instead of defining

Definition decidable {A : Type} (P : A -> Prop) (x : A) := {P x} + {not (P 
x)},

you simply notice that bool is a subtype of Prop and so

Definition decidable {A : Type} := A -> bool.

But again, I don't think there is any free lunch here and things will
be equally complicated.

With kind regards,

Andrej