The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Zhoulai FU@Gmail 
>>>>> <zhoulai.fu AT gmail.com>
>>>>>  writes:

> Let P denote a predicate over natural numbers. Suppose that I have a coq
> proof for "forall n:nat, P(n)”. Then, can I establish a mapping A from
> natural numbers to {true, false}, so that for any natural number n, A(n) is
> true if and only if P(n) can be proved?

You can if P is "decidable".  If it is decidable, then you switch back and
forth between True and true freely.  Take a look at Coq.Logic.Decidable.

John