Automation

Many of the proofs we have done so far with Hoare triples can be streamlined using the automation techniques that we introduced in the Auto chapter of Logical Foundations. Recall that the auto tactic can be told to unfold definitions as part of its proof search. Let's give it that hint for the definitions and coercions we're using:

Also recall that auto will search for a proof involving intros and apply. By default, the theorems that it will apply include any of the local hypotheses, as well as theorems in a core database. The proof of hoare_consequence_pre, repeated below, looks like an opportune place for such automation, because all it does is unfold, intros, and apply. (It uses assumption, too, but that's just application of a hypothesis.)

Merely using auto, though, doesn't complete the proof.

The problem is the apply Hhoare with... part of the proof. Coq isn't able to figure out how to instantiate st without some help from us. Recall, though, that there are versions of many tactics that will use existential variables to make progress even when the regular versions of those tactics would get stuck. Here, the eapply tactic will introduce an existential variable ?st as a placeholder for st, and eassumption will instantiate ?st with st when it discovers st in assumption Heval. By using eapply we are essentially telling Coq, "Be patient: The missing part is going to be filled in later in the proof."

The eauto tactic will use eapply as part of its proof search. So, the entire proof can actually be done in just one line.

Of course, it's hard to predict that eauto suffices here without having gone through the original proof of hoare_consequence_pre to see the tactics it used. But now that we know eauto worked there, it's a good bet that it will also work for hoare_consequence_post.

We can also use eapply to streamline a proof (hoare_asgn_example1), that we did earlier as an example of using the consequence rule:

The final bullet of that proof also looks like a candidate for automation.

Now we have quite a nice proof script: it simply identifies the Hoare rules that need to be used and leaves the remaining low-level details up to Coq to figure out. By now it might be apparent that the entire proof could be automated if we added hoare_consequence_pre and hoare_asgn to the hint database. We won't do that in this chapter, so that we can get a better understanding of when and how the Hoare rules are used. In the next chapter, Hoare2, we'll dive deeper into automating entire proofs of Hoare triples. The other example of using consequence that we did earlier, hoare_asgn_example2, requires a little more work to automate. We can streamline the first line with eapply, but we can't just use auto for the final bullet, since it needs lia.

Let's introduce our own tactic to handle both that bullet and the bullet from example 1:

Again, we have quite a nice proof script. All the low-level details of proofs about assertions have been taken care of automatically. Of course, assertion_auto isn't able to prove everything we could possibly want to know about assertions -- there's no magic here! But it's good enough so far.

Exercise: 1 star, standard (hoare_asgn_examples_2)

Prove this triple. Try to make your proof script nicely automated by following the examples above.

Sequencing + Assignment

Here's an example of a program involving both sequencing and assignment. Note the use of hoare_seq in conjunction with hoare_consequence_pre and the eapply tactic.

Informally, a nice way of displaying a proof using the sequencing rule is as a "decorated program" where the intermediate assertion Q is written between c₁ and c₂:
  {{ a = n }}
     X := a
              {{ X = n }}; <--- decoration for Q
     skip
  {{ X = n }} We'll come back to the idea of decorated programs in much more detail in the next chapter.

Exercise: 2 stars, standard, especially useful (hoare_asgn_example4)

Translate this "decorated program" into a formal proof:
                   {{ True }} ->>
                   {{ 1 = 1 }}
    X := 1
                   {{ X = 1 }} ->>
                   {{ X = 1 ∧ 2 = 2 }};
    Y := 2
                   {{ X = 1 ∧ Y = 2 }} Note the use of "->>" decorations, each marking a use of hoare_consequence_pre. We've started you off by providing a use of hoare_seq that explicitly identifies X = 1 as the intermediate assertion.

Exercise: 3 stars, standard, optional (swap_exercise)

Write an Imp program c that swaps the values of X and Y and show that it satisfies the following specification:
      {{X ≤ Y}} c {{Y ≤ X}} Your proof should not need to use unfold valid_hoare_triple. Hints:

• Remember that Imp commands need to be enclosed in <{...}> brackets.
• Remember that the assignment rule works best when it's applied "back to front," from the postcondition to the precondition. So your proof will want to start at the end and work back to the beginning of your program.
• Remember that eapply is your friend.)

Exercise: 4 stars, advanced, optional (invalid_triple)

Show that
    {{ a = n }} X := 3; Y := a {{ Y = n }} is not a valid Hoare triple for some choices of a and n. Conceptual hint: Invent a particular a and n for which the triple in invalid, then use those to complete the proof. Technical hint: Hypothesis H below begins ∀ a n, .... You'll want to instantiate that with the particular a and n you've invented. You can do that with assert and apply, but you may remember (from Tactics.v in Logical Foundations) that Coq offers an even easier tactic: specialize. If you write
       specialize H with (a := your_a) (n := your_n) the hypothesis will be instantiated on your_a and your_n. Having chosen your a and n, proceed as follows:

• Use the (assumed) validity of the given hoare triple to derive a state st' in which Y has some value y₁
• Use the evaluation rules (E_Seq and E_Asgn) to show that Y has a different value y₂ in the same final state st'
• Since y₁ and y₂ are both equal to st' Y, they are equal to each other. But we chose them to be different, so this is a contradiction, which finishes the proof.

Conditionals

What sort of rule do we want for reasoning about conditional commands? Certainly, if the same assertion Q holds after executing either of the branches, then it holds after the whole conditional. So we might be tempted to write:

{{P}} c1 {{Q}}
{{P}} c2 {{Q}}
{{P}} if b then c1 else c2 {{Q}}

However, this is rather weak. For example, using this rule, we cannot show
     {{ True }}
       if X = 0
         then Y := 2
         else Y := X + 1
       end
     {{ X ≤ Y }} since the rule tells us nothing about the state in which the assignments take place in the "then" and "else" branches. Fortunately, we can say something more precise. In the "then" branch, we know that the boolean expression b evaluates to true, and in the "else" branch, we know it evaluates to false. Making this information available in the premises of the rule gives us more information to work with when reasoning about the behavior of c₁ and c₂ (i.e., the reasons why they establish the postcondition Q).

{{P /\   b}} c1 {{Q}}
{{P /\ ~ b}} c2 {{Q}}	(hoare_if)
{{P}} if b then c1 else c2 end {{Q}}

To interpret this rule formally, we need to do a little work. Strictly speaking, the assertion we've written, P ∧ b, is the conjunction of an assertion and a boolean expression -- i.e., it doesn't typecheck. To fix this, we need a way of formally "lifting" any bexp b to an assertion. We'll write bassertion b for the assertion "the boolean expression b evaluates to true (in the given state)."

A useful fact about bassertion:

We mentioned the congruence tactic in passing in Auto when building the find_rwd tactic. Like find_rwd, congruence is able to automatically find that both beval st b = false and beval st b = true are being assumed, notice the contradiction, and discriminate to complete the proof. Now we can formalize the Hoare proof rule for conditionals and prove it correct.

That is (unwrapping the notations):
      Theorem hoare_if : ∀ P Q b c₁ c₂,
        {{fun st ⇒ P st ∧ bassertion b st}} c₁ {{Q}} →
        {{fun st ⇒ P st ∧ ¬(bassertion b st)}} c₂ {{Q}} →
        {{P}} if b then c₁ else c₂ end {{Q}}.

Example

Here is a formal proof that the program we used to motivate the rule satisfies the specification we gave.

As we did earlier, it would be nice to eliminate all the low-level proof script that isn't about the Hoare rules. Unfortunately, the assertion_auto tactic we wrote wasn't quite up to the job. Looking at the proof of if_example, we can see why. We had to unfold a definition (bassertion) and use a theorem (eqb_eq) that we didn't need in earlier proofs. So, let's add those into our tactic, and clean it up a little in the process.

Now the proof is quite streamlined.

We can even shorten it a little bit more.

For later proofs, it will help to extend assertion_auto' to handle inequalities, too.

Exercise: 2 stars, standard (if_minus_plus)

Prove the theorem below using hoare_if. Do not use unfold valid_hoare_triple. The assertion_auto'' tactic we just defined may be useful.

Exercise: One-sided conditionals

In this exercise we consider extending Imp with "one-sided conditionals" of the form if₁ b then c end. Here b is a boolean expression, and c is a command. If b evaluates to true, then command c is evaluated. If b evaluates to false, then if₁ b then c end does nothing. We recommend that you complete this exercise before attempting the ones that follow, as it should help solidify your understanding of the material. The first step is to extend the syntax of commands and introduce the usual notations. (We've done this for you. We use a separate module to prevent polluting the global name space.)

Exercise: 2 stars, standard, especially useful (if1_ceval)

Add two new evaluation rules to relation ceval, below, for if₁. Let the rules for if guide you.

The following unit tests should be provable simply by eauto if you have defined the rules for if₁ correctly.

Now we have to repeat the definition and notation of Hoare triples, so that they will use the updated com type.

Exercise: 2 stars, standard (hoare_if₁)

Invent a Hoare logic proof rule for if₁. State and prove a theorem named hoare_if₁ that shows the validity of your rule. Use hoare_if as a guide. Try to invent a rule that is complete, meaning it can be used to prove the correctness of as many one-sided conditionals as possible. Also try to keep your rule compositional, meaning that any Imp command that appears in a premise should syntactically be a part of the command in the conclusion. Hint: if you encounter difficulty getting Coq to parse part of your rule as an assertion, try manually indicating that it should be in the assertion scope. For example, if you want e to be parsed as an assertion, write it as (e)%assertion.

For full credit, prove formally (hoare_if1_good) that your rule is precise enough to show the following Hoare triple is valid:
  {{ X + Y = Z }}
    if₁ Y ≠ 0 then
      X := X + Y
    end
  {{ X = Z }}

Before the next exercise, we need to restate the Hoare rules of consequence (for preconditions) and assignment for the new com type.

Exercise: 2 stars, standard (hoare_if1_good)

Use your if₁ rule to prove the following (valid) Hoare triple. Hint: assertion_auto'' will once again get you most but not all the way to a completely automated proof. You can finish manually, or tweak the tactic further. Hint: If you see a message like Unable to unify "Imp.ceval Imp.CSkip st st'" with..., it probably means you are using a definition or theorem e.g., hoare_skip from above this exercise without re-proving it for the new version of Imp with if₁.

While Loops

The Hoare rule for while loops is based on the idea of a command invariant (or just invariant): an assertion whose truth is guaranteed after executing a command, assuming it is true before. That is, an assertion P is a command invariant of c if
      {{P}} c {{P}} holds. Note that the command invariant might temporarily become false in the middle of executing c, but by the end of c it must be restored. As a first attempt at a while rule, we could try:
             {{P}} c {{P}}
      ---------------------------
      {{P} while b do c end {{P}} That rule is valid: if P is a command invariant of c, as the premise requires, then no matter how many times the loop body executes, P is going to be true when the loop finally finishes. But the rule also omits two crucial pieces of information. First, the loop terminates when b becomes false. So we can strengthen the postcondition in the conclusion:
              {{P}} c {{P}}
      ---------------------------------
      {{P} while b do c end {{P ∧ ¬b}} Second, the loop body will be executed only if b is true. So we can also strengthen the precondition in the premise:
            {{P ∧ b}} c {{P}}
      --------------------------------- (hoare_while)
      {{P} while b do c end {{P ∧ ¬b}} That is the Hoare while rule. Note how it combines aspects of skip and conditionals:

• If the loop body executes zero times, the rule is like skip in that the precondition survives to become (part of) the postcondition.
• Like a conditional, we can assume guard b holds on entry to the subcommand.

We call P a loop invariant of while b do c end if
      {{P ∧ b}} c {{P}} is a valid Hoare triple. This means that P will be true at the end of the loop body whenever the loop body executes. If P contradicts b, this holds trivially since the precondition is false. For instance, X = 0 is a loop invariant of
      while X = 2 do X := 1 end since the program will never enter the loop. The program
    while Y > 10 do Y := Y - 1; Z := Z + 1 end admits an interesting loop invariant:
    X = Y + Z Note that this doesn't contradict the loop guard but neither is it a command invariant of
    Y := Y - 1; Z := Z + 1 since, if X = 5, Y = 0 and Z = 5, running the command will set Y + Z to 6. The loop guard Y > 10 guarantees that this will not be the case. We will see many such loop invariants in the following chapter.

If the loop never terminates, any postcondition will work.

Of course, this result is not surprising if we remember that the definition of valid_hoare_triple asserts that the postcondition must hold only when the command terminates. If the command doesn't terminate, we can prove anything we like about the post-condition. Hoare rules that specify what happens if commands terminate, without proving that they do, are said to describe a logic of partial correctness. It is also possible to give Hoare rules for total correctness, which additionally specifies that commands must terminate. Total correctness is out of the scope of this textbook.

Exercise: 3 stars, standard (hoare_add_loop)

Give a formal proof for the addition example from the lecture. Hint: you might find lemmas negb_true_iff and leb_gt useful.

Exercise: REPEAT

Exercise: 4 stars, advanced (hoare_repeat)

In this exercise, we'll add a new command to our language of commands: REPEAT c until b end. You will write the evaluation rule for REPEAT and add a new Hoare rule to the language for programs involving it. (You may recall that the evaluation rule is given in an example in the Auto chapter. Try to figure it out yourself here rather than peeking.)

REPEAT behaves like while, except that the loop guard is checked after each execution of the body, with the loop repeating as long as the guard stays false. Because of this, the body will always execute at least once.

Add new rules for REPEAT to ceval below. You can use the rules for while as a guide, but remember that the body of a REPEAT should always execute at least once, and that the loop ends when the guard becomes true.

A couple of definitions from above, copied here so they use the new ceval.

To make sure you've got the evaluation rules for repeat right, prove that ex1_repeat evaluates correctly.

Now state and prove a theorem, hoare_repeat, that expresses an appropriate proof rule for repeat commands. Use hoare_while as a model, and try to make your rule as precise as possible.

For full credit, argue (informally) that your rule can be used to prove the following valid Hoare triple:
  {{ X > 0 }}
    repeat
      Y := X;
      X := X - 1
    until X = 0 end
  {{ X = 0 ∧ Y > 0 }}

Summary

So far, we've introduced Hoare Logic as a tool for reasoning about Imp programs. The rules of Hoare Logic are:

	(hoare_asgn)
{{Q [X ⊢> a]}} X:=a {{Q}}

	(hoare_skip)
{{ P }} skip {{ P }}

{{ P }} c1 {{ Q }}
{{ Q }} c2 {{ R }}	(hoare_seq)
{{ P }} c1;c2 {{ R }}

{{P /\   b}} c1 {{Q}}
{{P /\ ~ b}} c2 {{Q}}	(hoare_if)
{{P}} if b then c1 else c2 end {{Q}}

{{P /\ b}} c {{P}}	(hoare_while)
{{P}} while b do c end {{P /\ ~ b}}

{{P'}} c {{Q'}}
P ->> P'
Q' ->> Q	(hoare_consequence)
{{P}} c {{Q}}

Our task in this chapter has been to define the rules of Hoare logic, and prove that the definitions are sound. Having done so, we can now work within Hoare logic to prove that particular programs satisfy particular Hoare triples. In the next chapter, we'll see how Hoare logic is can be used to prove that more interesting programs satisfy interesting specifications of their behavior. Crucially, we will do so without ever again unfolding the definition of Hoare triples -- i.e., we will take the rules of Hoare logic as a closed world for reasoning about programs.

Optional Additional Exercises

Havoc

In this exercise, we will derive proof rules for a HAVOC command, which is similar to the nondeterministic any expression from the the Imp chapter. First, we enclose this work in a separate module, and recall the syntax and big-step semantics of Himp commands.

The definition of Hoare triples is exactly as before.

And the precondition consequence rule is exactly as before.

Exercise: 3 stars, advanced, optional (hoare_havoc)

Complete the Hoare rule for HAVOC commands below by defining havoc_pre, and prove that the resulting rule is correct.

Exercise: 3 stars, advanced, optional (havoc_post)

Complete the following proof without changing any of the provided commands. If you find that it can't be completed, your definition of havoc_pre is probably too strong. Find a way to relax it so that havoc_post can be proved. Hint: the assertion_auto tactics we've built won't help you here. You need to proceed manually.

Assert and Assume

Exercise: 4 stars, standard, optional (assert_vs_assume)

In this exercise, we will extend IMP with two commands, assert and assume. Both commands are ways to indicate that a certain assertion should hold any time this part of the program is reached. However they differ as follows:

• If an assert statement fails, it causes the program to go into an error state and exit.
• If an assume statement fails, the program fails to evaluate at all. In other words, the program gets stuck and has no final state.

The new set of commands is:

To define the behavior of assert and assume, we need to add notation for an error, which indicates that an assertion has failed. We modify the ceval relation, therefore, so that it relates a start state to either an end state or to error. The result type indicates the end value of a program, either a state or an error:

Now we are ready to give you the ceval relation for the new language.

We redefine hoare triples: Now, {{P}} c {{Q}} means that, whenever c is started in a state satisfying P, and terminates with result r, then r is not an error and the state of r satisfies Q.

To test your understanding of this modification, give an example precondition and postcondition that are satisfied by the assume statement but not by the assert statement.

Then prove that any triple for an assert also works when assert is replaced by assume.

Next, here are proofs for the old hoare rules adapted to the new semantics. You don't need to do anything with these.

Here are the other proof rules (sanity check)