Before You Get Started:

• Create a fresh directory for this volume. (Do not try to mix the files from this volume with files from Logical Foundations in the same directory: the result will not make you happy.) You can either start with an empty directory and populate it with the files listed below, or else download the whole PLF zip file and unzip it.
• The new directory should contain at least the following files:
  • Imp.v (make sure it is the one from the PLF distribution, not the one from LF: they are slightly different);
  • Maps.v (ditto)
  • Equiv.v (this file)
  • _CoqProject, containing the following line:
               -Q . PLF
• If you see errors like this...
               Compiled library PLF.Maps (in file
               /Users/.../plf/Maps.vo) makes inconsistent assumptions
               over library Coq.Init.Logic ... it may mean something went wrong with the above steps. Doing "make clean" (or manually removing everything except .v and _CoqProject files) may help.
• If you are using VSCode with the VSCoq extension, you'll then want to open a new window in VSCode, click Open Folder > plf, and run make. If you get an error like "Cannot find a physical path..." error, it may be because you didn't open plf directly (you instead opened a folder containing both lf and plf, for example).

Advice for Working on Exercises:

• Most of the Coq proofs we ask you to do in this chapter are similar to proofs that we've provided. Before starting to work on exercises, take the time to work through our proofs (both informally and in Coq) and make sure you understand them in detail. This will save you a lot of time.
• The Coq proofs we're doing now are sufficiently complicated that it is more or less impossible to complete them by random experimentation or following your nose. 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. Alternately, grab a friend and try to convince them that the theorem is true; then try to formalize your explanation.
• Use automation to save work! The proofs in this chapter can get pretty long if you try to write out all the cases explicitly.

Behavioral Equivalence

In an earlier 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 in that setting 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 for the full Imp language -- in particular, assignment -- we need to consider the role of mutable state and develop a more sophisticated notion of correctness, which we'll call behavioral equivalence..

Definitions

For aexps and bexps with variables, the definition we want is clear: Two aexps or bexps are "behaviorally equivalent" if they evaluate to the same result in every state.

Here are some simple examples of equivalences of arithmetic and boolean expressions.

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 started in the same initial state," because some commands, when run 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 (1) both diverge or (2) both terminate in the same final state. A compact way to express this is "if the first one terminates in a particular state then so does the second, and vice versa."

Simple Examples

For examples of command equivalence, let's start by looking at some trivial program equivalences involving skip:

Exercise: 2 stars, standard (skip_right)

Prove that adding a skip after a command results in an equivalent program

Similarly, here is a simple equivalence that optimizes if commands:

Of course, no (human) programmer would write a conditional whose condition is literally true. But they might write one whose condition is equivalent to true: Theorem: If b is equivalent to true, then if b then c₁ else c₂ end is equivalent to c₁. Proof:

• (→) We must show, for all st and st', that if st =[ if b then c₁ else c₂ end ]=> st' then st =[ c₁ ]=> st'.
  Proceed by cases on the rules that could possibly have been used to show st =[ if b then c₁ else c₂ end ]=> st', namely E_IfTrue and E_IfFalse.
  • Suppose the final rule in the derivation of st =[ if b then c₁ else c₂ end ]=> st' was E_IfTrue. We then have, by the premises of E_IfTrue, that st =[ c₁ ]=> st'. This is exactly what we set out to prove.
  • On the other hand, suppose the final rule in the derivation of st =[ if b then c₁ else c₂ end ]=> st' was E_IfFalse. We then know that beval st b = false and st =[ c₂ ]=> st'.
    Recall that b is equivalent to true, i.e., forall st, beval st b = beval st <{true}> . In particular, this means that beval st b = true, since beval st <{true}> = true. But this is a contradiction, since E_IfFalse requires that beval st b = false. Thus, the final rule could not have been E_IfFalse.
• (<-) We must show, for all st and st', that if st =[ c₁ ]=> st' then st =[ if b then c₁ else c₂ end ]=> st'.
  Since b is equivalent to true, we know that beval st b = beval st <{true}> = true. Together with the assumption that st =[ c₁ ]=> st', we can apply E_IfTrue to derive st =[ if b then c₁ else c₂ end ]=> st'. ☐

Here is the formal version of this proof:

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

Exercise: 3 stars, standard (swap_if_branches)

Show that we can swap the branches of an if if we also negate its condition.

For while loops, we can give a similar pair of theorems. A loop whose guard is equivalent to false is equivalent to skip, while a loop whose guard is equivalent to true is equivalent to while true do skip end (or any other non-terminating program). The first of these facts is easy.

Exercise: 2 stars, advanced, optional (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 true never terminate. Lemma: If b is equivalent to true, then it cannot be the case that st =[ while b do c end ]=> st'. Proof: Suppose that st =[ while b do c end ]=> st'. We show, by induction on a derivation of st =[ while b do c end ]=> st', that this assumption leads to a contradiction. The only two cases to consider are E_WhileFalse and E_WhileTrue, the others are contradictory.

• Suppose st =[ while b do c end ]=> st' is proved using rule E_WhileFalse. Then by assumption beval st b = false. But this contradicts the assumption that b is equivalent to true.
• Suppose st =[ while b do c end ]=> st' is proved using rule E_WhileTrue. We must have that:
  1. beval st b = true, 2. there is some st₀ such that st =[ c ]=> st₀ and st₀ =[ while b do c end ]=> st', 3. and we are given the induction hypothesis that st₀ =[ while b do c end ]=> st' leads to a contradiction,
  We obtain a contradiction by 2 and 3. ☐

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

Prove the following theorem. Hint: You'll want to use while_true_nonterm here.

A more interesting fact about while commands is that any number of copies of the body can be "unrolled" without changing meaning. Loop unrolling is an important transformation in any real compiler, so its correctness is of more than academic interest!

Proving program properties involving assignments is one place where the fact that program states are treated extensionally (e.g., x !-> m x ; m and m are equal maps) comes in handy.

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

Properties of Behavioral Equivalence

We next consider some fundamental properties of program equivalence.

Behavioral Equivalence Is an Equivalence

First, let's verify that the equivalences on aexps, bexps, and coms really are equivalences -- i.e., that they are reflexive, symmetric, and transitive. The proofs are all easy.

Behavioral Equivalence Is a Congruence

Less obviously, behavioral equivalence is also a congruence. That is, the equivalence of two subprograms implies the equivalence of the larger programs in which they are embedded:

aequiv a a'
cequiv (x := a) (x := a')

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

... and so on for the other forms of commands. (Note that we are using the inference rule notation here not as part of an inductive definition, but simply to write down some valid implications in a readable format. We prove these implications below.) We will see a concrete example of why these congruence properties are important in the following section (in the proof of fold_constants_com_sound), but the main idea is that they allow us to replace a small part of a large program with an equivalent small part and know that the whole large programs are equivalent without doing an explicit proof about the parts that didn't change -- i.e., the "proof burden" of a small change to a large program is proportional to the size of the change, not the program!

The congruence property for loops is a little more interesting, since it requires induction. Theorem: Equivalence is a congruence for while -- that is, if b is equivalent to b' and c is equivalent to c', then while b do c end is equivalent to while b' do c' end. Proof: Suppose b is equivalent to b' and c is equivalent to c'. We must show, for every st and st', that st =[ while b do c end ]=> st' iff st =[ while b' do c' end ]=> st'. We consider the two directions separately.

• (→) We show that st =[ while b do c end ]=> st' implies st =[ while b' do c' end ]=> st', by induction on a derivation of st =[ while b do c end ]=> st'. The only nontrivial cases are when the final rule in the derivation is E_WhileFalse or E_WhileTrue.
  • E_WhileFalse: In this case, the form of the rule gives us beval st b = false and st = st'. But then, since b and b' are equivalent, we have beval st b' = false, and E_WhileFalse applies, giving us st =[ while b' do c' end ]=> st', as required.
  • E_WhileTrue: The form of the rule now gives us beval st b = true, with st =[ c ]=> st'0 and st'0 =[ while b do c end ]=> st' for some state st'0, with the induction hypothesis st'0 =[ while b' do c' end ]=> st'.
    Since c and c' are equivalent, we know that st =[ c' ]=> st'0. And since b and b' are equivalent, we have beval st b' = true. Now E_WhileTrue applies, giving us st =[ while b' do c' end ]=> st', as required.
• (<-) Similar. ☐

Exercise: 3 stars, standard (CSeq_congruence)

Exercise: 3 stars, standard (CIf_congruence)

For example, here are two equivalent programs and a proof of their equivalence...

Program Transformations

A program transformation is a function that takes a program as input and produces a modified program as output. Compiler optimizations such as constant folding are a canonical example, but there are many others. A program transformation is said to be sound if it preserves the behavior of the original program.

The Constant-Folding Transformation

An expression is constant if 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 do other "obvious" things like eliminating trivial additions (e.g., rewriting 0 + X to just X).: we are focusing attention on a single optimization for the sake of simplicity. It is not hard to incorporate other ways of simplifying expressions -- the definitions and proofs just get longer. We'll consider optimizations in the exercises.

Not only can we lift fold_constants_aexp to bexps (in the BEq, BNeq, and BLe cases); we can also look for constant boolean expressions and evaluate them in-place as well.

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

Proving Inequivalence

Next, let's look at some programs that are not equivalent. Suppose that c₁ is a command of the form
       X := a₁; Y := a₂ and c₂ is the command
       X := a₁; Y := a₂' where a₂' is formed by substituting a₁ for all occurrences of X in a₂. For example, c₁ and c₂ might be:
       c₁ = (X := 42 + 53;
               Y := Y + X)
       c₂ = (X := 42 + 53;
               Y := Y + (42 + 53)) Clearly, this particular c₁ and c₂ are equivalent. Is this true in general? We will see in a moment that it is not, but it is worthwhile to pause, now, and see if you can find a counter-example on your own. More formally, here is the function that substitutes an arithmetic expression u for each occurrence of a given variable x in another expression a:

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

Sadly, the property does not always hold. Here is a counterexample:
       X := X + 1; Y := X If we perform the substitution, we get
       X := X + 1; Y := X + 1 which clearly isn't equivalent.

Exercise: 3 stars, standard (inequiv_exercise)

Prove that an infinite loop is not equivalent to skip