The presentation of Hoare logic in chapter Hoare could be described as "model-theoretic": the proof rules for each of the constructors were presented as theorems about the evaluation behavior of programs, and proofs of program correctness (validity of Hoare triples) were constructed by combining these theorems directly in Coq. Another way of presenting Hoare logic is to define a completely separate proof system -- a set of axioms and inference rules that talk about commands, Hoare triples, etc. -- and then say that a proof of a Hoare triple is a valid derivation in that logic. We can do this by giving an inductive definition of valid derivations in this new logic. This chapter is optional. Before reading it, you'll want to read the ProofObjects chapter in Logical Foundations (Software Foundations, volume 1).

Definitions

We don't need to include axioms corresponding to hoare_consequence_pre or hoare_consequence_post, because these can be proven easily from H_Consequence.

As an example, let's construct a proof object representing a derivation for the hoare triple
      {{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}
      X::=X+1 ;; X::=X+2
      {{X=3}}.

We can use Coq's tactics to help us construct the proof object.

Properties

Exercise: 2 stars, standard (hoare_proof_sound)

Prove that derivations constructed with hoare_proof correspond to valid Hoare triples. In other words, hoare_proof derivations are sound. Hint: We already proved the soundness of each individual proof rule in Hoare as theorems hoare_skip, hoare_asgn, etc.; leverage those proofs.

We can also use Coq's reasoning facilities to prove metatheorems about Hoare Logic. For example, here are the analogs of two theorems we saw in chapter Hoare -- this time expressed in terms of the syntax of Hoare Logic derivations (provability) rather than directly in terms of the semantics of Hoare triples. The first one says that, for every P and c, the assertion {{P}} c {{True}} is provable in Hoare Logic. Note that the proof is more complex than the semantic proof in Hoare: we actually need to perform an induction over the structure of the command c.

Similarly, we can show that {{False}} c {{Q}} is provable for any c and Q.

As a last step, we can show that the set of hoare_proof axioms is sufficient to prove any true fact about (partial) correctness. More precisely, any semantic Hoare triple that we can prove can also be proved from these axioms. Such a set of axioms is said to be relatively complete. That is, the axioms are complete relative to what we can prove in the underlying assertion language. If there are gaps in what can be proved in that language, then we blame it, not the Hoare logic axioms. Our proof is inspired by this one: https://www.ps.uni-saarland.de/courses/sem-ws₁₁/script/Hoare.html To carry out the proof, we need to invent some intermediate assertions using a technical device known as weakest preconditions (which are also discussed in Hoare2). Given a command c and a desired postcondition assertion Q, the weakest precondition wp c Q is an assertion P such that {{P}} c {{Q}} holds, and moreover, for any other assertion P', if {{P'}} c {{Q}} holds then P' → P. We can more directly define this as follows:

To get accustomed to this definition of wp, prove the next two simple theorems.

Exercise: 1 star, standard (wp_is_precondition)

Exercise: 1 star, standard (wp_is_weakest)

Exercise: 2 stars, standard (wp_invariant)

Prove that for any Q, assertion wp (WHILE b DO c END) Q is an invariant of WHILE b DO c END.

The following utility lemma will be useful in the next exercise.

Exercise: 4 stars, standard (hoare_proof_complete)

Complete the proof of the theorem. Hint for the WHILE case: you need to invent a loop invariant.

Finally, we might hope that our axiomatic Hoare logic is decidable; that is, that there is an (terminating) algorithm (a decision procedure) that can determine whether or not a given Hoare triple is valid (derivable). But such a decision procedure cannot exist! Consider the triple {{True}} c {{False}}. This triple is valid if and only if c is non-terminating. So any algorithm that could determine validity of arbitrary triples could solve the Halting Problem. Similarly, the triple {{True}} SKIP {{P}} is valid if and only if ∀ s, P s is valid, where P is an arbitrary assertion of Coq's logic. But it is known that there can be no decision procedure for this logic. Overall, this axiomatic style of presentation gives a clearer picture of what it means to "give a proof in Hoare logic." However, it is not entirely satisfactory from the point of view of writing down such proofs in practice: it is quite verbose. The section of chapter Hoare2 on formalizing decorated programs shows how we can do even better.