Equiv: Program Equivalence

(* Version of 4/21/2010 *)

Require Export Imp.

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.

Definition aequiv (a1 a2 : aexp) : Prop :=
  forall (st:state),
    aeval st a1 = aeval st a2.

Definition bequiv (b1 b2 : bexp) : Prop :=
  forall (st:state),
    beval st b1 = beval st b2.

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.

Definition cequiv (c1 c2 : com) : Prop :=
forall (st st':state),
(c1 / st ==> st') <-> (c2 / st ==> st').

Examples

Theorem aequiv_example:
  aequiv (AMinus (AId X) (AId X)) (ANum 0).
Proof.
  unfold aequiv. intros st. simpl.
  apply minus_diag.
Qed.

Theorem bequiv_example:
  bequiv (BEq (AMinus (AId X) (AId X)) (ANum 0)) BTrue.
Proof.
  unfold bequiv. intros. unfold beval.
  rewrite aequiv_example. reflexivity.
Qed.

Theorem skip_left: forall c,
  cequiv
     (SKIP; c)
     c.
Proof.
  unfold cequiv. intros c st st'.
  split; intros H.
  Case "->".
    inversion H. subst.
    inversion H3. subst.
    assumption.
  Case "<-".
    apply E_Seq with st.
    apply E_Skip.
    assumption.
Qed.

Exercise: 2 stars

Theorem skip_right: forall c,
  cequiv
    (c; SKIP)
    c.
Proof.
  (* FILL IN HERE *) Admitted.

☐

Theorem IFB_true_simple: forall c1 c2,
  cequiv
    (IFB BTrue THEN c1 ELSE c2 FI)
    c1.
Proof.
  intros c1 c2.
  split; intros H.
  Case "->".
    inversion H; subst. assumption. inversion H5.
  Case "<-".
    apply E_IfTrue. reflexivity. assumption. Qed.

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:

Theorem IFB_true: forall b c1 c2,
     bequiv b BTrue ->
     cequiv
       (IFB b THEN c1 ELSE c2 FI)
       c1.
Proof.
  intros b c1 c2 Hb.
  split; intros H.
  Case "->".
    inversion H; subst.
    SCase "b evaluates to true".
      assumption.
    SCase "b evaluates to false (contradiction)".
      rewrite Hb in H5.
      inversion H5.
  Case "<-".
    apply E_IfTrue; try assumption.
    rewrite Hb. reflexivity. Qed.

(* Similarly: *)

Exercise: 2 stars

Theorem IFB_false: forall b c1 c2,
  bequiv b BFalse ->
  cequiv
    (IFB b THEN c1 ELSE c2 FI)
    c2.
Proof.
  (* FILL IN HERE *) Admitted.

☐

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.

Theorem WHILE_false : forall b c,
     bequiv b BFalse ->
     cequiv
       (WHILE b DO c END)
       SKIP.
Proof.
  intros b c Hb.
  unfold cequiv. split; intros.
  Case "->".
    inversion H; subst.
    SCase "E_WhileEnd".
      apply E_Skip.
    SCase "E_WhileLoop".
      rewrite Hb in H2. inversion H2.
  Case "<-".
    inversion H; subst.
    apply E_WhileEnd.
    rewrite Hb.
    reflexivity. Qed.

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. ☐

Lemma WHILE_true_nonterm : forall b c st st',
     bequiv b BTrue ->
     ~( (WHILE b DO c END) / st ==> st' ).
Proof.
  intros b c st st' Hb.
  intros H.
  remember (WHILE b DO c END) as cw.
  (ceval_cases (induction H) Case);
    (* most rules don't apply, and we can rule them out by inversion *)
    inversion Heqcw; subst; clear Heqcw.

  Case "E_WhileEnd". (* contradictory -- b is always true! *)
    rewrite Hb in H. inversion H.
  Case "E_WhileLoop". (* immediate from the IH *)
    apply IHceval2. reflexivity. Qed.

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...

Theorem WHILE_true: forall b c,
     bequiv b BTrue ->
     cequiv
       (WHILE b DO c END)
       (WHILE BTrue DO SKIP END).
Proof.
  (* FILL IN HERE *) Admitted.

☐

Exercise: 2 stars (WHILE_false_inf)

Write an informal proof of WHILE_false.

(* FILL IN HERE *)
☐

Theorem loop_unrolling: forall b c,
  cequiv
    (WHILE b DO c END)
    (IFB b THEN (c; WHILE b DO c END) ELSE SKIP FI).
Proof.
  (* WORKED IN CLASS *)
  unfold cequiv. intros b c st st'.
  split; intros Hce.
  Case "->".
    inversion Hce; subst.
    SCase "loop doesn't run".
      apply E_IfFalse. assumption. apply E_Skip.
    SCase "loop runs".
      apply E_IfTrue. assumption.
      apply E_Seq with (st' := st'0). assumption. assumption.
  Case "<-".
    inversion Hce; subst.
    SCase "loop runs".
      inversion H5; subst.
      apply E_WhileLoop with (st' := st'0).
      assumption. assumption. assumption.
    SCase "loop doesn't run".
      inversion H5; subst. apply E_WhileEnd. assumption. Qed.

Exercise: 2 stars

Theorem seq_assoc : forall c1 c2 c3,
cequiv ((c1;c2);c3) (c1;(c2;c3)).
Proof.
(* FILL IN HERE *) Admitted.

☐

Exercise: 3 stars

Theorem swap_if_branches: forall b e1 e2,
  cequiv
    (IFB b THEN e1 ELSE e2 FI)
    (IFB BNot b THEN e2 ELSE e1 FI).
Proof.
  (* FILL IN HERE *) Admitted.

☐

Exercise: 2 stars, optional

Which of the following pairs of programs are equivalent? Write "yes" or "no" for each one.

(a)

    WHILE (BLe (ANum 1) (AId X)) DO
      X ::= APlus (AId X) (ANum 1)
    END

and

    WHILE (BLe (ANum 2) (AId X)) DO
      X ::= APlus (AId X) (ANum 1)
    END

(* FILL IN HERE *)

(b)

    WHILE BTrue DO
      WHILE BFalse DO X ::= APlus (AId X) (ANum 1) END
    END

and

    WHILE BFalse DO
      WHILE BTrue DO X ::= APlus (AId X) (ANum 1) END
    END

(* FILL IN HERE *)

☐

Program Equivalence is an Equivalence

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

Lemma refl_aequiv : forall (a : aexp), aequiv a a.
Proof.
  unfold aequiv. intros a st. reflexivity. Qed.

Lemma sym_aequiv : forall (a1 a2 : aexp),
  aequiv a1 a2 -> aequiv a2 a1.
Proof.
  intros a1 a2 H. intros st. symmetry. apply H. Qed.

Lemma trans_aequiv : forall (a1 a2 a3 : aexp),
  aequiv a1 a2 -> aequiv a2 a3 -> aequiv a1 a3.
Proof.
  unfold aequiv. intros a1 a2 a3 H12 H23 st.
  rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.

Lemma refl_bequiv : forall (b : bexp), bequiv b b.
Proof.
  unfold bequiv. intros b st. reflexivity. Qed.

Lemma sym_bequiv : forall (b1 b2 : bexp),
  bequiv b1 b2 -> bequiv b2 b1.
Proof.
  unfold bequiv. intros b1 b2 H. intros st. symmetry. apply H. Qed.

Lemma trans_bequiv : forall (b1 b2 b3 : bexp),
  bequiv b1 b2 -> bequiv b2 b3 -> bequiv b1 b3.
Proof.
  unfold bequiv. intros b1 b2 b3 H12 H23 st.
  rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.

Lemma refl_cequiv : forall (c : com), cequiv c c.
Proof.
  unfold cequiv. intros c st st'. apply iff_refl. Qed.

Lemma sym_cequiv : forall (c1 c2 : com),
  cequiv c1 c2 -> cequiv c2 c1.
Proof.
  unfold cequiv. intros c1 c2 H st st'.
  assert (c1 / st ==> st' <-> c2 / st ==> st') as H'.
    SCase "Proof of assertion". apply H.
  apply iff_sym. assumption.
Qed.

Lemma iff_trans : forall (P1 P2 P3 : Prop),
  (P1 <-> P2) -> (P2 <-> P3) -> (P1 <-> P3).
Proof.
  intros P1 P2 P3 H12 H23.
  inversion H12. inversion H23.
  split; intros A.
    apply H1. apply H. apply A.
    apply H0. apply H2. apply A. Qed.

Lemma trans_cequiv : forall (c1 c2 c3 : com),
  cequiv c1 c2 -> cequiv c2 c3 -> cequiv c1 c3.
Proof.
  unfold cequiv. intros c1 c2 c3 H12 H23 st st'.
  apply iff_trans with (c2 / st ==> st'). apply H12. apply H23. Qed.

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).

Theorem CAss_congruence : forall i a1 a1',
  aequiv a1 a1' ->
  cequiv (CAss i a1) (CAss i a1').
Proof.
  unfold aequiv,cequiv. intros i a1 a2 Heqv st st'.
  split; intros Hceval.
  Case "->".
    inversion Hceval. subst. apply E_Ass.
    rewrite Heqv. reflexivity.
  Case "<-".
    inversion Hceval. subst. apply E_Ass.
    rewrite Heqv. reflexivity. Qed.

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. ☐

Theorem WHILE_congruence : forall b1 b1' c1 c1',
  bequiv b1 b1' -> cequiv c1 c1' ->
  cequiv (WHILE b1 DO c1 END) (WHILE b1' DO c1' END).
Proof.
  unfold bequiv,cequiv.
  intros b1 b1' c1 c1' Hb1e Hc1e st st'.
  split; intros Hce.
  Case "->".
    remember (WHILE b1 DO c1 END) as cwhile.
    induction Hce; try (inversion Heqcwhile); subst.
    SCase "E_WhileEnd".
      apply E_WhileEnd. rewrite <- Hb1e. apply H.
    SCase "E_WhileLoop".
      apply E_WhileLoop with (st' := st').
      SSCase "show loop runs". rewrite <- Hb1e. apply H.
      SSCase "body execution".
        destruct (Hc1e st st') as [Hc1c1' _].
        apply Hc1c1'. apply Hce1.
      SSCase "subsequent loop execution".
        apply IHHce2. reflexivity.
  Case "<-".
    remember (WHILE b1' DO c1' END) as c'while.
    induction Hce; try (inversion Heqc'while); subst.
    SCase "E_WhileEnd".
      apply E_WhileEnd. rewrite -> Hb1e. apply H.
    SCase "E_WhileLoop".
      apply E_WhileLoop with (st' := st').
      SSCase "show loop runs". rewrite -> Hb1e. apply H.
      SSCase "body execution".
        destruct (Hc1e st st') as [_ Hc1'c1].
        apply Hc1'c1. apply Hce1.
      SSCase "subsequent loop execution".
        apply IHHce2. reflexivity. Qed.

Exercise: 3 stars

Theorem CSeq_congruence : forall c1 c1' c2 c2',
  cequiv c1 c1' -> cequiv c2 c2' ->
  cequiv (c1;c2) (c1';c2').
Proof.
  (* FILL IN HERE *) Admitted.

☐

Exercise: 3 stars

Theorem IFB_congruence : forall b b' c1 c1' c2 c2',
  bequiv b b' -> cequiv c1 c1' -> cequiv c2 c2' ->
  cequiv (IFB b THEN c1 ELSE c2 FI) (IFB b' THEN c1' ELSE c2' FI).
Proof.
  (* FILL IN HERE *) Admitted.

☐

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.

Definition atrans_sound (atrans : aexp -> aexp) : Prop :=
  forall (a : aexp),
    aequiv a (atrans a).

Definition btrans_sound (btrans : bexp -> bexp) : Prop :=
  forall (b : bexp),
    bequiv b (btrans b).

Definition ctrans_sound (ctrans : com -> com) : Prop :=
  forall (c : com),
    cequiv c (ctrans c).

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.

Fixpoint fold_constants_aexp (a : aexp) : aexp :=
  match a with
  | ANum n => ANum n
  | AId i => AId i
  | APlus a1 a2 =>
      match (fold_constants_aexp a1, fold_constants_aexp a2) with
      | (ANum n1, ANum n2) => ANum (plus n1 n2)
      | (a1', a2') => APlus a1' a2'
      end
  | AMinus a1 a2 =>
      match (fold_constants_aexp a1, fold_constants_aexp a2) with
      | (ANum n1, ANum n2) => ANum (minus n1 n2)
      | (a1', a2') => AMinus a1' a2'
      end
  | AMult a1 a2 =>
      match (fold_constants_aexp a1, fold_constants_aexp a2) with
      | (ANum n1, ANum n2) => ANum (mult n1 n2)
      | (a1', a2') => AMult a1' a2'
      end
  end.

Example fold_aexp_ex1 :
    fold_constants_aexp
      (AMult (APlus (ANum 1) (ANum 2)) (AId X))
  = AMult (ANum 3) (AId X).
Proof. reflexivity. Qed.

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.

Example fold_aexp_ex2 :
    fold_constants_aexp
      (AMinus (AId X) (APlus (AMult (ANum 0) (ANum 6)) (AId Y)))
  = AMinus (AId X) (APlus (ANum 0) (AId Y)).
Proof. reflexivity. Qed.

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.

Fixpoint fold_constants_bexp (b : bexp) : bexp :=
  match b with
  | BTrue => BTrue
  | BFalse => BFalse
  | BEq a1 a2 =>
      match (fold_constants_aexp a1, fold_constants_aexp a2) with
      | (ANum n1, ANum n2) => if beq_nat n1 n2 then BTrue else BFalse
      | (a1', a2') => BEq a1' a2'
      end
  | BLe a1 a2 =>
      match (fold_constants_aexp a1, fold_constants_aexp a2) with
      | (ANum n1, ANum n2) => if ble_nat n1 n2 then BTrue else BFalse
      | (a1', a2') => BLe a1' a2'
      end
  | BNot b1 =>
      match (fold_constants_bexp b1) with
      | BTrue => BFalse
      | BFalse => BTrue
      | b1' => BNot b1'
      end
  | BAnd b1 b2 =>
      match (fold_constants_bexp b1, fold_constants_bexp b2) with
      | (BTrue, BTrue) => BTrue
      | (BTrue, BFalse) => BFalse
      | (BFalse, BTrue) => BFalse
      | (BFalse, BFalse) => BFalse
      | (b1', b2') => BAnd b1' b2'
      end
  end.

Example fold_bexp_ex1 :
    fold_constants_bexp (BAnd BTrue (BNot (BAnd BFalse BTrue)))
  = BTrue.
Proof. reflexivity. Qed.

Example fold_bexp_ex2 :
    fold_constants_bexp
      (BAnd (BEq (AId X) (AId Y))
            (BEq (ANum 0)
                 (AMinus (ANum 2) (APlus (ANum 1) (ANum 1)))))
  = BAnd (BEq (AId X) (AId Y)) BTrue.
Proof. reflexivity. Qed.

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

Fixpoint fold_constants_com (c : com) : com :=
  match c with
  | SKIP =>
      SKIP
  | i ::= a =>
      CAss i (fold_constants_aexp a)
  | c1 ; c2 =>
      (fold_constants_com c1) ; (fold_constants_com c2)
  | IFB b THEN c1 ELSE c2 FI =>
      match fold_constants_bexp b with
      | BTrue => fold_constants_com c1
      | BFalse => fold_constants_com c2
      | b' => IFB b' THEN fold_constants_com c1 ELSE fold_constants_com c2 FI
      end
  | WHILE b DO c END =>
      match fold_constants_bexp b with
      | BTrue => WHILE BTrue DO SKIP END
      | BFalse => SKIP
      | b' => WHILE b' DO (fold_constants_com c) END
      end
  end.

Example fold_com_ex1 :
  fold_constants_com
    (X ::= APlus (ANum 4) (ANum 5);
     Y ::= AMinus (AId X) (ANum 3);
     IFB BEq (AMinus (AId X) (AId Y)) (APlus (ANum 2) (ANum 4)) THEN
       SKIP
     ELSE
       Y ::= ANum 0
     FI;
     IFB BLe (ANum 0) (AMinus (ANum 4) (APlus (ANum 2) (ANum 1))) THEN
       Y ::= ANum 0
     ELSE
       SKIP
     FI;
     WHILE BEq (AId Y) (ANum 0) DO
       X ::= APlus (AId X) (ANum 1)
     END) =
  (X ::= ANum 9;
   Y ::= AMinus (AId X) (ANum 3);
   IFB BEq (AMinus (AId X) (AId Y)) (ANum 6) THEN
     SKIP
   ELSE
     (Y ::= ANum 0)
   FI;
   Y ::= ANum 0;
   WHILE BEq (AId Y) (ANum 0) DO
     X ::= APlus (AId X) (ANum 1)
   END).
Proof. reflexivity. Qed.

Soundness of Constant Folding

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

Theorem fold_constants_aexp_sound:
  atrans_sound fold_constants_aexp.
Proof.
  unfold atrans_sound. intros a. unfold aequiv. intros st.
  aexp_cases (induction a) Case.
  Case "ANum". reflexivity.
  Case "AId". reflexivity.
  Case "APlus". simpl.
    remember (fold_constants_aexp a1) as a1'.
    remember (fold_constants_aexp a2) as a2'.
    rewrite IHa1. rewrite IHa2.
    destruct a1'; destruct a2'; reflexivity.
  Case "AMinus". simpl.
    remember (fold_constants_aexp a1) as a1'.
    remember (fold_constants_aexp a2) as a2'.
    rewrite IHa1. rewrite IHa2.
    destruct a1'; destruct a2'; reflexivity.
  Case "AMult". simpl.
    remember (fold_constants_aexp a1) as a1'.
    remember (fold_constants_aexp a2) as a2'.
    rewrite IHa1. rewrite IHa2.
    destruct a1'; destruct a2'; reflexivity. Qed.

Here's a shorter proof...

Theorem fold_constants_aexp_sound' :
  atrans_sound fold_constants_aexp.
Proof.
  unfold atrans_sound. intros a. unfold aequiv. intros st.
  (aexp_cases (induction a) Case); simpl;
    (* ANum and AId follow immediately *)
    try reflexivity;
    (* APlus, AMinus, and AMult follow from the IH
       and the observation that
              aeval st (APlus a1 a2)
            = ANum (plus (aeval st a1) (aeval st a2))
            = aeval st (ANum (plus (aeval st a1) (aeval st a2)))
       (and similarly for AMinus/minus and AMult/mult) *)
    try (destruct (fold_constants_aexp a1);
         destruct (fold_constants_aexp a2);
         rewrite IHa1; rewrite IHa2; reflexivity). Qed.

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

beval st (BEq a1 a2)
= beval st (fold_constants_bexp (BEq a1 a2)).

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.

Theorem fold_constants_bexp_sound:
  btrans_sound fold_constants_bexp.
Proof.
  unfold btrans_sound. intros b. unfold bequiv. intros st.
  (bexp_cases (induction b) Case);
    (* BTrue and BFalse are immediate *)
    try reflexivity.
  Case "BEq".
    (* Doing induction when there are a lot of constructors makes
       specifying variable names a chore, but Coq doesn't always
       choose nice variable names.  You can rename entries in the
       context with the rename tactic: rename a into a1 will
       change a to a1 in the current goal and context. *)
    rename a into a1. rename a0 into a2. simpl.
    remember (fold_constants_aexp a1) as a1'.
    remember (fold_constants_aexp a2) as a2'.
    assert (aeval st a1 = aeval st a1') as H1.
      SCase "Proof of assertion". subst a1'. apply fold_constants_aexp_sound.
    assert (aeval st a2 = aeval st a2') as H2.
      SCase "Proof of assertion". subst a2'. apply fold_constants_aexp_sound.
    rewrite H1. rewrite H2.
    destruct a1'; destruct a2'; try reflexivity.
      (* The only interesting case is when both a1 and a2
         become constants after folding *)
      simpl. destruct (beq_nat n n0); reflexivity.
  Case "BLe".
    (* FILL IN HERE *) admit.
  Case "BNot".
    simpl. remember (fold_constants_bexp b) as b'.
    rewrite IHb.
    destruct b'; reflexivity.
  Case "BAnd".
    simpl.
    remember (fold_constants_bexp b1) as b1'.
    remember (fold_constants_bexp b2) as b2'.
    rewrite IHb1. rewrite IHb2.
    destruct b1'; destruct b2'; reflexivity. Qed.

☐

Exercise: 3 stars

Complete the WHILE case of the following proof.

Theorem fold_constants_com_sound :
  ctrans_sound fold_constants_com.
Proof.
  unfold ctrans_sound. intros c.
  (com_cases (induction c) Case); simpl.
  Case "SKIP". apply refl_cequiv.
  Case "::=". apply CAss_congruence. apply fold_constants_aexp_sound.
  Case ";". apply CSeq_congruence; assumption.
  Case "IFB".
    assert (bequiv b (fold_constants_bexp b)).
      SCase "Pf of assertion". apply fold_constants_bexp_sound.
    remember (fold_constants_bexp b) as b'.
    destruct b';
      (* If the optimization doesn't eliminate the if, then the result
         is easy to prove from the IH and fold_constants_bexp_sound *)
      try (apply IFB_congruence; assumption).
    SCase "b always true".
      apply trans_cequiv with c1; try assumption.
      apply IFB_true; assumption.
    SCase "b always false".
      apply trans_cequiv with c2; try assumption.
      apply IFB_false; assumption.
  Case "WHILE".
    (* FILL IN HERE *) Admitted.

☐

Soundness of (0 + n) elimination

Exercise: 4 stars (optimize_0plus)

Recall the definition optimize_0plus from Imp.v:

    Fixpoint optimize_0plus (e:aexp) : aexp :=
      match e with
      | ANum n => ANum n
      | APlus (ANum 0) e2 => optimize_0plus e2
      | APlus e1 e2 => APlus (optimize_0plus e1) (optimize_0plus e2)
      | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2)
      | AMult e1 e2 => AMult (optimize_0plus e1) (optimize_0plus e2)
      end.

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:

     optimize_0plus_aexp
     optimize_0plus_bexp
     optimize_0plus_com

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.)

(* FILL IN HERE *)

☐

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:

       c1 = (x ::= 42 + 53;
               y ::= y + x)
       c2 = (x ::= 42 + 53;
               y ::= y + (42 + 53))

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

Fixpoint subst_aexp (i : id) (u : aexp) (a : aexp) : aexp :=
  match a with
  | ANum n => ANum n
  | AId i' => if beq_id i i' then u else AId i'
  | APlus a1 a2 => APlus (subst_aexp i u a1) (subst_aexp i u a2)
  | AMinus a1 a2 => AMinus (subst_aexp i u a1) (subst_aexp i u a2)
  | AMult a1 a2 => AMult (subst_aexp i u a1) (subst_aexp i u a2)
  end.

Example subst_aexp_ex :
  subst_aexp X (APlus (ANum 42) (ANum 53)) (APlus (AId Y) (AId X)) =
  (APlus (AId Y) (APlus (ANum 42) (ANum 53))).
Proof. reflexivity. Qed.

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

Definition subst_equiv_property := forall i1 i2 a1 a2,
cequiv (i1 ::= a1; i2 ::= a2)
(i1 ::= a1; i2 ::= subst_aexp i1 a1 a2).

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

Lemma cequiv_state: forall c1 c2 st st' st'',
  cequiv c1 c2 ->
  c1 / st ==> st' ->
  c2 / st ==> st'' ->
  st' = st''.
Proof.
  intros c1 c2 st st' st'' Hcequiv Hc1 Hc2.
  unfold cequiv in Hcequiv. destruct (Hcequiv st st') as [Hc12 _].
   (* By equivalence c2 / st ==> st' *)
   apply Hc12 in Hc1.
   (* By determinacy, st' = st'' *)
   apply (ceval_deterministic c2 st); assumption. Qed.

Now a proof by counter-example.

Theorem subst_inequiv :
  ~ subst_equiv_property.
Proof.
  unfold subst_equiv_property.
  intros Contra.

  (* Here is the counterexample: assuming that subst_equiv_property
     holds allows us to prove that these two programs are
     equivalent... *)
  remember (X ::= APlus (AId X) (ANum 1);
            Y ::= AId X)
      as c1.
  remember (X ::= APlus (AId X) (ANum 1);
            Y ::= APlus (AId X) (ANum 1))
      as c2.
  assert (cequiv c1 c2) by (subst; apply Contra).

  (* This allows us to show that the command
        X ::= APlus (AId X) (ANum 1); Y ::= AId X
     can terminate in two different final states:
        st'  = {X |-> 1, Y |-> 1}
        st'' = {X |-> 1, Y |-> 2}. *)
  remember (update (update empty_state X 1) Y 1) as st'.
  remember (update (update empty_state X 1) Y 2) as st''.
  assert (st' = st'') as Hcontra.
  Case "Pf of Hcontra".
  (* This can be shown by using cequiv_state,
     with appropriate "final" states for c1 and c2 *)
    assert (c1 / empty_state ==> st') as H1;
    assert (c2 / empty_state ==> st'') as H2;
    try (subst;
         apply E_Seq with (st' := (update empty_state X 1));
         apply E_Ass; reflexivity).
    apply (cequiv_state c1 c2 empty_state st' st''); try assumption.

  (* Finally, we use the "equality" of the different states
     to obtain a contradiction. *)
  assert (st' Y = st'' Y) as Hcontra'
    by (rewrite Hcontra; reflexivity).
  subst; inversion Hcontra'. Qed.

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.

Formalize this claim and prove it correct.

(* FILL IN HERE *)

☐

Exercise: 3 stars

Theorem inequiv_exercise:
~ cequiv (WHILE BTrue DO SKIP END) SKIP.
Proof.
(* FILL IN HERE *) Admitted.

☐

Reasoning about Imp programs

Recall the factorial program:

(* Print fact_body. Print fact_loop. Print fact_com. *)

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

Fixpoint real_fact (n:nat) : nat :=
  match n with
  | O => 1
  | S n' => mult n (real_fact n')
  end.

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.

Definition fact_invariant (x:nat) (st:state) :=
  mult (st Y) (real_fact (st Z)) = real_fact x.

Theorem fact_body_preserves_invariant: forall st st' x,
     fact_invariant x st ->
     st Z <> 0 ->
     fact_body / st ==> st' ->
     fact_invariant x st'.
Proof.
  intros st st' x Hm HZnz He.
  unfold fact_invariant in Hm.
  (* first, note that (st Z) = S z' for some z' *)
  remember (st Z) as z.
  assert (exists z', z = S z').
    destruct z as [| z'].
    Case "z = 0 (contra)".
      apply ex_falso_quodlibet.
      apply HZnz. reflexivity.
    Case "z = S z'".
      exists z'. reflexivity.
  destruct H as [z' Heqz']. rewrite Heqz' in Heqz.
  (* next, we see what reduction of fact_body does...*)
  unfold fact_body in He.
  unfold fact_invariant.
  inversion He; subst.
  inversion H2; subst.
  inversion H4; subst.
  simpl. rewrite <- Heqz.
  rewrite (update_neq Z Y); try reflexivity.
  rewrite (update_neq Y Z); try reflexivity.
  rewrite update_eq. rewrite update_eq.
    (* Here's one of those pesky arithmetic proofs that often come
       up.  We want to solve the goal st Z - 1 = z', which is
       obviously true given the hypothesis Heqz: S z' = st Z.  It is
       beneath the dignity of us humans to search around for the right
       lemma to do this.  Fortunately, omega does the job. *)
  assert (st Z - 1 = z') as Heqz_minus_1.
    omega.
  rewrite Heqz_minus_1. rewrite <- Hm.
  simpl.
  rewrite <- mult_assoc.
  assert ( mult (S z') (real_fact z')
          = plus (real_fact z') (mult z' (real_fact z'))).
    simpl. omega.
  rewrite H. reflexivity. Qed.

Theorem fact_loop_preserves_invariant : forall st st' x,
     fact_invariant x st ->
     fact_loop / st ==> st' ->
     fact_invariant x st'.
Proof.
  intros st st' x H Hce.
  remember fact_loop as c.
  (ceval_cases (induction Hce) Case); inversion Heqc; subst; clear Heqc.
  Case "E_WhileEnd".
    (* trivial when the loop doesn't run... *)
    assumption.
  Case "E_WhileLoop".
    (* if the loop does run, we know that fact_body preserves
       fact_invariant -- we just need to assemble the pieces *)
    assert (st Z <> 0) as HZnz.
      intros Contra.
      inversion H0; subst. symmetry in H2; apply negb_sym in H2.
      rewrite Contra in H2. inversion H2.
    assert (fact_invariant x st').
      apply fact_body_preserves_invariant with st; assumption.
    apply IHHce2. assumption. reflexivity. Qed.

Theorem guard_false_after_loop: forall b c st st',
     (WHILE b DO c END) / st ==> st' ->
     beval st' b = false.
Proof.
  intros b c st st' Hce.
  remember (WHILE b DO c END) as cloop.
  (ceval_cases (induction Hce) Case); try (inversion Heqcloop; subst).
  Case "E_WhileEnd".
    assumption.
  Case "E_WhileLoop".
    apply IHHce2. reflexivity. Qed.

Patching it all together...

Theorem fact_com_correct : forall st st' x,
     st X = x ->
     fact_com / st ==> st' ->
     st' Y = real_fact x.
Proof.
  intros st st' x HX Hce.
  inversion Hce; subst.
  inversion H2; subst.
  inversion H4; subst.
  inversion H3; subst.
  rename st' into st''.
  (* we notice that the invariant is set up before the loop runs... *)
  remember (update (update st Z (aeval st (AId X))) Y
            (aeval (update st Z (aeval st (AId X))) (ANum 1))) as st'.
  assert (fact_invariant (st X) st').
    unfold fact_invariant. subst st'.
    simpl.
    rewrite update_neq; try reflexivity.
    rewrite update_eq.
    omega.
  (* ...and that when the loop is done running, the invariant
     is maintained *)
  assert (fact_invariant (st X) st'').
    apply fact_loop_preserves_invariant with st'; assumption.
  unfold fact_invariant in H0.
  (* Finally, if the loop terminated, then z is 0; so y must be
     factorial of x *)
  assert (beval st'' (BNot (BEq (AId Z) (ANum 0))) = false).
    apply guard_false_after_loop with (st := st') (c := fact_body).
    apply H6.
  simpl in H1. symmetry in H1; apply negb_sym in H1; symmetry in H1. simpl in H1.
  apply beq_nat_eq in H1.
  rewrite H1 in H0. simpl in H0. rewrite mult_1_r in H0.
  rewrite H0. reflexivity.
Qed.

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.

Definition ss_invariant (x:nat) (z:nat) (st:state) :=
minus (st Z) (st X) = minus z x.

(* FILL IN HERE *)

☐

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:

      for (c1 ; b ; c2) {
          c3
      }

is equivalent to:

       c1 ;
       WHILE b DO
         c3 ;
         c2
       END

(* FILL IN HERE *)

☐