The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT sophia.inria.fr>]

George Herson wrote:
> 
> I'm fairly new to correctness proofs and formal methods and brand new to 
> Coq.
> My interests are in practical problem solving.
> 
> How broadly can these methodologies by used?
> 
> For example, i know it's sometimes hard to find but does there necessarily
> exist, for every loop, a loop invariant?
> 
> Let's say i have the following.  Is there a representation for the following
> algorithm for which Coq will help prove termination (or anything else 
> useful)?
> 
> input a positive number n
> while n is not equal to 1 do
>    if n is even then
>      n := n/2
>    else
>      n := 3*n+1
>    endif
>    print "Terminated".
> endwhile
> 
> merci
> george
> 

In Coq you have first of all to find a way to represent your program.
Since in Coq only terminating programs can be written and you don't know
yet whether your example is total or not, this is a problem.
Transform the algorithm in functional form, since this is closer to type
theory:

f: nat -> nat
f 1 = 1
f n = 1 + if (even n) then n/2 else 3n+1

(I changed the output, so, if the computation terminates, the result is
the number of steps of the computation.)

A method by Ana Bove allows you to define in type theory an inductive
predicate that is, in a certain sense, the most general invariant of the
algorithm:

Inductive Df : nat -> Set :=
  df1 : (Df 1)
| dfe : (n:nat)(even n)=true -> (Df n/2) -> (Df n)
| dfo : (n:nat)(even n)=false -> (Df 3n+1) -> (Df n).

(I am a bit sloppy with notation. This is not actual Coq code, but you
can change it to make it right.)

Then you can define f by recursion on the proof of Df:

f: (n:nat)(Df n)->nat
f 1 df1 = 1
f n (dfe n p h) = 1 + (f n/2 h)
f n (dfo n q k) = 1 + (f n/2 k)

So we use the proof of the predicate Df as an extra argument to the
function f. This can be done in Coq because it is based on type theory
and proofs can be used as ordinary mathematical objects.

Df can be seen as the most general invariant of the loop: it is defined
in such a way that an argument n satisfies it if and only if the
arguments of the recursive calls in the definition of (f n) satisfy it.

Now proving the totality of f is the same as proving that every n
satisfies Df. Of course, as Gerard Huet already remarked, there is no
hope for the proof tool to check this automatically, but there needs to
be some creative contribution from the user.

Bibliography:
Ana Bove, "Simple General Recursion in Type Theory", Nordic Journal of
Computing 8(2001),22-42

Ana Bove and Venanzio Capretta, "Nested General Recursion and Partiality
in Type Theory", Proceedings TPHOLs 2001, LNCS 2152, pg. 121-135

Ana Bove and Venanzio Capretta, Modelling General Recursion in Type
Theory,
   http://www-sop.inria.fr/lemme/Venanzio.Capretta/index.html

Venanzio