The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Sun, Feb 19, 2006 at 10:39:48PM +0100, Ron wrote:
> 2006/2/19, Lionel Elie Mamane 
>Â <lionel AT mamane.lu>:
>> On Sun, Feb 19, 2006 at 04:57:21PM +0100, Ron wrote:

>>> Coq seems to be a well developed theorem prover, however, I read in
>>> Chapter 1 of Coq'Art that Coq can't prove theorems about all
>>> computable functions(in particular those that not terminate).

>>> More on the limitations of Coq. I have been taught that predicate
>>> calculus can represent programs, so this would imply Coq can't do
>>> this.

>> Err... I'm not sure what you mean exactly. What is the relationship
>> between the two claims you are making in that sentence alone?

> In predicate logic you can state that a certain program, which will
> never terminate, will never produce output FOO, and there exists
> theorem provers which can handle predicate logic that can
> semi-decide this. And Coq couldn't handle all computable functions
> (as in Chapter 1). So, if you can use Coq to do all of predicate
> logic, then there must be something wrong in one of the above
> statements.

OK, I see. What you cannot do in Coq is, given two types A and B,
construct an object of type "A -> B" (a function that takes an A and
returns a B) that doesn't terminate on all a's. Even more strongly,
Coq must _see_ that it terminates; the exact condition is documented
in the manual. These are the Coq-native functions that Coq will
automatically compute for you; meaning if f is defined in this way and
for a particular a and b the computation of (f a) gives b, then these
two terms are equal at the lowest level in Coq (they are
_convertible_). They are indistinguishable in the Coq logic. This is
called the Poincaré principle.

This being said, there are ways to speak about partial functions, for
example the Bove-Capretta method: Basically, you add an additional
argument to your function which is the proof that it terminates on
this particular input (a trace of the computation, actually). Your
constructed function then artificially always terminates, because if
the original function doesn't terminate on input a, then you won't be
able to construct the second argument.


That's in Coq's native logic. But if you encode predicate logic (as an
object logic) in Coq, then obviously you get exactly the power of that
predicate logic. You'd loose the Poincaré principle, I think.


This maps to the two ways to use Coq:

 - Construct / prove something in Coq's logic itself.

 - Construct another logic as an object logic in Coq and do things in
   this logic.

-- 
Lionel