The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

While there isn't a free lunch I think the first alternative has the
advantage that you have to do solve the problem only once while if you
follow the 2nd approach and prove forall x : A, P x <-> f x = true you
have to do the same analysis in the program and in the proof.

On the other hand the 2nd alternative also works in classical predicate
logic which is why I use this one in my introductory logic course where I
use Coq but don't mention Type Theory :-)

Thorsten


On 01/10/2012 15:32, "Andrej Bauer" 
<andrej.bauer AT andrej.com>
 wrote:

>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

This message and any attachment are intended solely for the addressee and may 
contain confidential information. If you have received this message in error, 
please send it back to me, and immediately delete it.   Please do not use, 
copy or disclose the information contained in this message or in any 
attachment.  Any views or opinions expressed by the author of this email do 
not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.