The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 20/12/2013 23:25, троль wrote:

> My question is actually this: if {{ P }} WHILE b DO c END {{ Q }} is
> valid hoare triple, does it implies, that you can prove it with
> hoare_while? Since H_While is just a relation version of hoare_while.
> I suppose, that you can't prove such a thing with an arbitrary loop
> due to undecidability of loop's invariants inference. Am I right? Or
> maybe someone has a solution to hoare_proof_complete?

I can't tell about the version of Hoare logic described in Software 
Foundations (and as always, the devil is in the details), but what you 
are looking for is Cook's result about relative completeness. What he 
states is that, if your assertion language is rich enough to represent 
the sets of states of your program, then there exists an invariant such 
that you can prove '{p} while b ... {q}' by applying hoare_while.

The proof is straightforward: just use the assertion 'i' that represents 
all the pre-states of the while loop that lead to a state included in 
'q'. (By hypothesis on the expressiveness of the assertion language, it 
exists.) It is easy to check that 'i' is indeed an invariant of your 
loop (it holds at the start, during, and at the end of the loop) and 
that 'i /\ not b -> q' holds.

It might seem magical, but there is an important point to keep in mind 
here: Cook proves that Hoare logic is complete (which is the solution to 
hoare_proof_complete) but he does not give you a way to build the actual 
invariants, he just proves that they exist. That's when you try to build 
an invariant that you encounter issues with undecidability.

Best regards,

Guillaume