HoareAsLogicHoare Logic as a Logic

The presentation of Hoare logic in Hoare.v 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.

For example, let's construct a proof object representing a derivation for the hoare triple We can use Coq's tactics to help us construct the proof object.

Exercise: 2 stars

Prove that such proof objects represent true claims.

☐ 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 Hoare.v — 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.v: 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.

This 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. FormalDec.v shows how we can do even better.