Some general advice for the homework

• We've tried to make sure that most of the Coq proofs we ask you to do are similar to proofs that we've provided. Before starting to work on the homework problems, take the time to work through our proofs (both informally, on paper, and in Coq) and make sure you understand them in detail. This will save you a lot of time.
• Here's another thing that will save a lot of time. The Coq proofs we're doing now are sufficiently complicated that it is more or less impossible to complete them simply by "following your nose" or random hacking. You need to start with an idea about why the property is true and how the proof is going to go. The best way to do this is to write out at least a sketch of an informal proof on paper -- one that intuitively convinces you of the truth of the theorem -- before starting to work on the formal one.
• Use automation to save work! Some of the proofs in this chapter's exercises are pretty long if you try to write out all the cases explicitly.

Behavioral Equivalence

In the last chapter, we investigated the correctness of a very simple program transformation: the optimize_0plus function. The programming language we were considering was the first version of the language of arithmetic expressions -- with no variables -- so it was very easy to define what it means for a program transformation to be correct: it should always yield a program that evaluates to the same number as the original. To talk about the correctness of program transformations in the full Imp language, we need to think about the role of variables and the state.

Definitions

For aexps and bexps, the definition we want is clear. We say that two aexps or bexps are behaviorally equivalent if they evaluate to the same result in every state.

For commands, the situation is a little more subtle. We can't simply say "two commands are behaviorally equivalent if they evaluate to the same ending state whenever they are run in the same initial state," because some commands (in some starting states) don't terminate in any final state at all! What we need instead is this: two commands are behaviorally equivalent if, for any given starting state, they either both diverge or both terminate in the same final state.

Examples

For examples of command equivalence, let's start by looking at trivial transformations involving SKIP:

Exercise: 2 stars

☐ We can also explore transformations that simplify IFB commands:

Of course, few programmers would be tempted to write a while loop whose guard is literally BTrue. A more interesting case is when the guard is equivalent to true... Theorem: forall b c1 c2, if b is equivalent to BTrue, then IFB b THEN c1 ELSE c2 FI is equivalent to c1. Proof:

• (--->) We must show, for all st and st', that if IFB b THEN c1 ELSE c2 FI / st ==> st' then c1 / st ==> st'.
  There are two rules that could have been used to show IFB b THEN c1 ELSE c2 FI / st ==> st': E_IfTrue and E_IfFalse.
  • Suppose the rule used to show IFB b THEN c1 ELSE c2 FI / st ==> st' was E_IfTrue. We then have, by the premises of E_IfTrue, that c1 / st ==> st'. This is exactly what we set out to prove.
  • Suppose the rule used to show IFB b THEN c1 ELSE c2 FI / st ==> st' was E_IfFalse. We then know that beval st b = false and c2 / st ==> st'.
    Recall that b is equivalent to BTrue, i.e. forall st, beval st b = beval st BTrue. In particular, this means that beval st b = true, since beval st BTrue = true. But this is a contradiction, since E_IfFalse requires that beval st b = false. We therefore conclude that the final rule could not have been E_IfFalse.
• (<---) We must show, for all st and st', that if c1 / st ==> st' then IFB b THEN c1 ELSE c2 FI / st ==> st'.
  Since b is equivalent to BTrue, we know that beval st b = beval st BTrue = true. Together with the assumption that c1 / st ==> st', we can apply E_IfTrue to derive IFB b THEN c1 ELSE c2 FI / st ==> st'. ☐

Here is the formal version of this proof:

Similarly:

Exercise: 2 stars

☐

Exercise: 3 stars

☐ For while loops, there is a similar pair of theorems: a loop whose guard is equivalent to BFalse is equivalent to SKIP, while a loop whose guard is equivalent to BTrue is equivalent to WHILE BTrue DO SKIP END (or any other non-terminating program). The first of these facts is easy.

Exercise: 2 stars (WHILE_false_informal)

Write an informal proof of WHILE_false. (* FILL IN HERE *)
☐ To prove the second fact, we need an auxiliary lemma stating that while loops whose guards are equivalent to BTrue never terminate: Lemma: If b is equivalent to BTrue, then it cannot be the case that (WHILE b DO c END) / st ==> st'. Proof: Suppose that (WHILE b DO c END) / st ==> st'. We show, by induction on a derivation of (WHILE b DO c END) / st ==> st', that this assumption leads to a contradiction.

• Suppose (WHILE b DO c END) / st ==> st' is proved using rule E_WhileEnd. Then by assumption beval st b = false. But this contradicts the assumption that b is equivalent to BTrue.
• Suppose (WHILE b DO c END) / st ==> st' is proved using rule E_WhileLoop. Then we are given the induction hypothesis that (WHILE b DO c END) / st ==> st' is contradictory, which is exactly what we are trying to prove!
• Since these are the only rules that could have been used to prove (WHILE b DO c END) / st ==> st', the other cases of the induction are immediately contradictory. ☐

Exercise: 2 stars, optional (WHILE_true_nonterm_informal)

Explain what the lemma WHILE_true_nonterm means in English. (* FILL IN HERE *)
☐

Exercise: 2 stars

You'll want to use WHILE_true_nonterm here...

☐

Exercise: 2 stars, optional

Which of the following pairs of programs are equivalent? Write "yes" or "no" for each one. (a) and (* FILL IN HERE *)
(b) and (* FILL IN HERE *)
☐

Exercise: 2 stars

☐ Finally, let's look at simple equivalences involving assignments. This turns out to be a little tricky. To start with, we might expect to be able to show that certain kinds of "useless" assignments can be removed. Most trivially:

But here we're stuck. The goal looks reasonable, but in fact it is not provable! If we look back at the set of lemmas we proved about update in the last chapter, we can see that lemma update_same almost does the job, but not quite: it says that the original and updated states agree at all values, but this is not the same thing as saying that they are eq in Coq's sense!

What is going on here? Recall that our states are just functions from identifiers to values. For Coq, functions are only equal when their definitions are syntactically the same (after reduction). (Otherwise, attempts to apply the eq constructor will fail!) In practice, for functions built up out of update operations, this means that two functions are equal only if they were constructed using the same update operations, applied in the same order. In the theorem above, the sequence of updates on the first parameter cequiv is one longer than for the second parameter, so it is no wonder that the equality doesn't hold. But the problem is quite general. If we try to prove other "trivial" facts, such as or we'll get stuck in the same way: we'll have two functions that behave the same way on all inputs, but cannot be proven to be eq to each other. The principle we would like to use in these situations is called functional extensionality: Although this principle is not derivable in Coq, it turns out to be safe to add it as an (unproven) axiom.

It has been proven that adding this axiom doesn't introduce any inconsistencies into Coq. In this way, it is similar to adding one of the classical logic axioms, such as excluded_middle. With the benefit of this axiom we can prove our theorem:

Exercise: 2 stars

☐

A Digression on Equivalences.

Purists might object to using functional_extensionality. In general, it can be quite dangerous to add axioms, particularly several at once (as they may be mutually inconsistent). In fact, functional_extensionality and excluded_middle can both be assumed without any problems, but some Coq users prefer to avoid such "heavyweight" general techniques, and instead craft solutions for specific problems that stay within Coq's standard logic. For our particular problem here, rather than extending the definition of equality to do what we want on functions representing states, we could instead give an explicit notion of equivalence on states. For example:

It is easy to prove that stequiv is an equivalence (i.e., it is reflexive, symmetric, and transitive), so it partitions the set of all states into equivalence classes.

Exercise: 1 star

Exercise: 1 star

Exercise: 1 star

Another useful fact...

Exercise: 1 star

It is then straightforward to show that aeval and beval behave uniformly on all members of an equvalence class:

Exercise: 2 stars

Exercise: 2 stars

We can also characterize the behavior of ceval on equivalent states; this result is more complicated to state because ceval is a relation.

Now we need to redefine cequal to use ~ instead of =. Unfortunately, it is not so easy to do this in a way that keeps the definition simple and symmetric. But here is one approach (thanks to Andrew McCreight). We first define a looser variant of ==> that "folds in" the notion of equivalence.

Now the revised definition of cequiv' looks familiar:

A sanity check shows that the original notion of command equivalence is at least as strong as this new one. (The converse is not true, naturally.)

Exercise: 2 stars

Finally, here is our example once more... (You can complete the proof)

On the whole, this explicit equivalence approach is considerably harder to work with than relying on functional extensionality. (Coq does have an advanced mechanism called "setoids" that makes working with equivalences somewhat easier, by allowing them to be registered with the system so that standard rewriting tactics work for them almost as well as for equalities.) But it is worth knowing about, because it applies even in situations where the equivalence in question is *not* over functions. For example, if we chose to represent state mappings as binary search trees, we would need to use an explicit equivalence of this kind. End of digression.

Program Equivalence is an Equivalence

The equivalences on aexps, bexps, and coms are reflexive, symmetric, and transitive

Program Equivalence is a Congruence

Program equivalence is also a congruence. That is, the equivalence of two subprograms implies the equivalence of the whole programs in which they are embedded:

aequiv a1 a1'
cequiv (i ::= a1) (i ::= a1')

cequiv c1 c1'
cequiv c2 c2'
cequiv (c1;c2) (c1';c2')

And so on. Note that we are using the inference rule notation here not as part of a definition, but simply to write down some valid implications in a readable format. We prove these implications below. We will see why these congruence properties are important in the following section (in the proof of fold_constants_com_sound).

The congruence property for loops is a little more interesting, since it requires induction. Theorem: Equivalence is a congruence for WHILE -- that is, if b1 is equivalent to b1' and c1 is equivalent to c1', then WHILE b1 DO c1 END is equivalent to WHILE b1' DO c1' END. Proof: Suppose b1 is equivalent to b1' and c1 is equivalent to c1'. We must show, for every st and st', that WHILE b1 DO c1 END / st ==> st' iff WHILE b1' DO c1' END / st ==> st'. We consider each direction in turn.

• (---->) We show that WHILE b1 DO c1 END / st ==> st' implies WHILE b1' DO c1' END / st ==> st', by induction on a derivation of WHILE b1 DO c1 END / st ==> st'. The only nontrivial cases are when the final rule in the derivation is E_WhileEnd or E_WhileLoop.
  • E_WhileEnd: In this case, the form of the rule gives us beval st b1 = false and st = st'. But then, since b1 and b1' are equivalent, we have beval st b1' = false, and E-WhileEnd applies, giving us WHILE b1' DO c1' END / st ==> st', as required.
  • E_WhileLoop: The form of the rule now gives us beval st b1 = true, with c1 / st ==> st'0 and WHILE b1 DO c1 END / st'0 ==> st' for some state st'0, with the induction hypothesis WHILE b1' DO c1' END / st'0 ==> st'.
    Since c1 and c1' are equivalent, we know that c1' / st ==> st'0. And since b1 and b1' are equivalent, we have beval st b1' = true. Now E-WhileLoop applies, giving us WHILE b1' DO c1' END / st ==> st', as required.
• (<----) Similar. ☐

Exercise: 3 stars

☐

Exercise: 3 stars

☐

Case Study: Constant Folding

A program transformation is a function that takes a program as input and produces some variant of the program as its output. Compiler optimizations such as constant folding are a canonical example, but there are many others.

Soundness of Program Transformations

A program transformation is sound if it preserves the behavior of the original program. We can define a notion of soundness for translations of aexps, bexps, and coms.

The Constant-Folding Transformation

An expression is constant when it contains no variable references. Constant folding is an optimization that finds constant expressions and replaces them by their values.

Note that this version of constant folding doesn't eliminate trivial additions, etc. -- we are focusing attention on a single optimization for the sake of simplicity. It is not hard to incorporate other ways of simplifying expressions, but the definitions and proofs get longer.

Not only can we lift fold_constants_aexp to bexps (in the BEq and BLe cases), we can also find constant boolean expressions and reduce them in-place.

To fold constants in a command, we apply the appropriate folding functions on all embedded expressions.

Soundness of Constant Folding

Now we need to show that what we've done is correct.

Here's a shorter proof...

Exercise: 3 stars

Here is an informal proof of the BEq case of the soundness argument for boolean expression constant folding. Read it carefully and compare it to the formal proof that follows. Then fill in the BLe case of the formal proof (without looking at the BEq case, if possible). Theorem: The constant folding function for booleans, fold_constants_bexp, is sound. Proof: We must show that b is equivalent to fold_constants_bexp, for all boolean expressions b. Proceed by induction on b. We show just the case where b has the form BEq a1 a2. In this case, we must show There are two cases to consider:

• First, suppose fold_constants_aexp a1 = ANum n1 and fold_constants_aexp a2 = ANum n2 for some n1 and n2.
  In this case, we have
             fold_constants_bexp (BEq a1 a2)
           = if beq_nat n1 n2 then BTrue else BFalse
  and
             beval st (BEq a1 a2)
           = beq_nat (aeval st a1) (aeval st a2).
  By the soundness of constant folding for arithmetic expressions (Lemma fold_constants_aexp_sound), we know
             aeval st a1
           = aeval st (fold_constants_aexp a1)
           = aeval st (ANum n1)
           = n1
  and
             aeval st a2
           = aeval st (fold_constants_aexp a2)
           = aeval st (ANum n2)
           = n2,
  so
             beval st (BEq a1 a2)
           = beq_nat (aeval a1) (aeval a2)
           = beq_nat n1 n2.
  Also, it is easy to see (by considering the cases n1 = n2 and n1 <> n2 separately) that
             beval st (if beq_nat n1 n2 then BTrue else BFalse)
           = if beq_nat n1 n2 then beval st BTrue else beval st BFalse
           = if beq_nat n1 n2 then true else false
           = beq_nat n1 n2.
  So
             beval st (BEq a1 a2)
           = beq_nat n1 n2.
           = beval st (if beq_nat n1 n2 then BTrue else BFalse),
  as required.
• Otherwise, one of fold_constants_aexp a1 and fold_constants_aexp a2 is not a constant. In this case, we must show
             beval st (BEq a1 a2)
           = beval st (BEq (fold_constants_aexp a1)
                           (fold_constants_aexp a2)),
  which, by the definition of beval, is the same as showing
             beq_nat (aeval st a1) (aeval st a2)
           = beq_nat (aeval st (fold_constants_aexp a1))
                     (aeval st (fold_constants_aexp a2)).
  But the soundness of constant folding for arithmetic expressions (fold_constants_aexp_sound) gives us
           aeval st a1 = aeval st (fold_constants_aexp a1)
           aeval st a2 = aeval st (fold_constants_aexp a2),
  completing the case.

☐

Exercise: 3 stars

Complete the WHILE case of the following proof.

☐

Soundness of (0 + n) Elimination

Exercise: 4 stars (optimize_0plus)

Recall the definition optimize_0plus from Imp.v: Note that this function is defined over the old aexps, without states. Write a new version of this function, and analogous ones for bexps and commands: Prove that these three functions are sound, as we did for fold_constants_*. Make sure you use the congruence lemmas in the proof of optimize_0plus_com (otherwise it will be long!). Then define an optimizer on commands that first folds constants (using fold_constants_com) and then eliminates 0 + n terms (using optimize_0plus_com).

• Give a meaningful example of this optimizer's output.
• Prove that the optimizer is sound. (This part should be very easy.)

☐

Proving That Programs Are Not Equivalent

Suppose that c1 is a command of the form x ::= a1; y ::= a2 and c2 is the command x ::= a1; y ::= a2', where a2' is formed by substituting a1 for all occurrences of x in a2. For example, c1 and c2 might be: Clearly, this particular c1 and c2 are equivalent. But is this true in general? We will see that it is not, but it is worthwhile to pause, now, and see if you can find a counter-example on your own (or remember the one from the discussion from class). Here, formally, is the function that substitutes an arithmetic expression for each occurrence of a given location in another expression

And here is the property we are interested in, expressing the claim that commands c1 and c2 as described above are always equivalent.

Sadly, the property does not always hold. First, a helper lemma:

Now a proof by counter-example.

Exercise: 4 stars (better_subst_equiv)

The equivalence we had in mind above was not complete nonsense -- it was actually almost right. To make it correct, we just need to exclude the case where the variable x occurs in the right-hand-side of the first assignment statement.

☐

Exercise: 3 stars

☐

Reasoning about Imp programs

Recall the factorial program:

Here is an alternative "mathematical" definition of the factorial function:

We would like to show that they agree -- if we start fact_com in a state where variable X contains some number x, then it will terminate in a state where variable Y contains the factorial of x. To show this, we rely on the critical idea of a loop invariant.

Patching it all together...

One might wonder whether all this work with poking at states and unfolding definitions could be ameliorated with some more powerful lemmas and/or more uniform reasoning principles... Indeed, this is exactly the topic of next week's lectures!

Exercise: 3 stars (subtract_slowly_spec)

Prove a specification for subtract_slowly, using the above specification of fact_com and the invariant below as guides.

☐

Additional Exercises

Exercise: 3 stars, optional (update_eq_variant)

The way update_eq is stated (in the section on mappings in Imp.v) may have looked a bit surprising: wouldn't it be simpler just to say lookup k (update f k x) = Some x? Try changing the statement of the theorem to read like this; then work through some of this file and see how the proofs that use update_eq need to be changed to use the simplified version. ☐

Exercise: 4 stars, optional

This exercise extends an optional exercise from Imp.v, where you were asked to extend the language of commands with C-style for loops. Prove that the command: is equivalent to:

☐

Exercise: 3 stars