Equiv: Program equivalence

(* Version of 11/3/2009 *)

Require Export Imp.

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 in your mind about why the property is true and how the proof is going to go. The best way to do this is actually to write out an informal proof on paper -- one that convinces you of the truth of the theorem -- before starting to work on the formal one.

  • Use automation to save work! Some of these proofs are extremely long and tedious if you try to write out all the cases explicitly.

One more tactic


The tactic admit automatically solves the current subgoal in any proof. This can be useful for skipping to the interesting parts of proofs, and we'll use it in exercises where we'd like you to finish just one case. Don't use it in anything you turn in, though - it's cheating.

Notation for evaluation


Last week, we defined a proposition ceval, indexed by two states and a command. Formally, this definition is no different from other indexed propositions we've defined, like ev or le. When discussing ceval, though, it's convenient (and standard) to use some special notations.

First, from now on, we'll write the Coq proposition ceval st c st' as c / st ~~> st', which can be read as "c takes state st to st'".

Second, we will sometimes (especially in informal discussions) write the rules for ceval in a more "graphical" form called inference rules, where the premises above the line allow you to derive the conclusion below the line. For example, the constructor CESeq would be written like this as an inference rule:
        c1 / st ~~> st'    c2 / st' ~~> st''
        ------------------------------------ CESeq
                c1;c2 / st ~~> st''
Such rules can read either from the bottom up...
  • "To show that c1;c2 takes st to st'', then by rule CESeq it suffices to show that c1 takes st to st' and c2 takes st' to st''."
...or from the top down:
  • "If c1 takes st to st' and c2 takes st' to st'', then c1;c2 takes st to st'' by rule CESeq."
Formally, there is nothing deep or complex about such rules: they are just implications. You can read the rule name on the right as the name of the constructor and read both the spaces between premises above the line and the line itself as ->.

Determinacy of evaluation


Changing from a computational to a relational definition of evaluation is a good move because it allows us to escape from the artificial requirement (imposed by Coq's restrictions on Fixpoint definitions) that evaluation should be a total function. But it also raises a question: Is the second definition of evaluation even a partial function? That is, is it possible that, beginning from the same state st, we could evaluate some command c in different ways to reach two different output states st' and st''?

In fact, this is not possible: the evaluation relation ceval is a partial function. Here's the proof:

Theorem ceval_deterministic: forall c st st1 st2,
     c / st ~~> st1
  -> c / st ~~> st2
  -> st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2.
  (ceval_cases (induction E1) Case); intros st2 E2; inversion E2; subst.
  Case "CESkip". reflexivity.
  Case "CEAss". reflexivity.
  Case "CESeq".
    assert (st' = st'0) as EQ1.
      SCase "Proof of assertion". apply IHE1_1; assumption.
    subst st'0.
    apply IHE1_2. assumption.
  Case "CEIfTrue".
    SCase "b1 evaluates to true".
      apply IHE1. assumption.
    SCase "b1 evaluates to false (contradiction)".
      rewrite H in H5. inversion H5.
  Case "CEIfFalse".
    SCase "b1 evaluates to true (contradiction)".
      rewrite H in H5. inversion H5.
    SCase "b1 evaluates to false".
      apply IHE1. assumption.
  Case "CEWhileEnd".
    SCase "b1 evaluates to true".
      reflexivity.
    SCase "b1 evaluates to false (contradiction)".
      rewrite H in H2. inversion H2.
  Case "CEWhileLoop".
    SCase "b1 evaluates to true (contradiction)".
      rewrite H in H4. inversion H4.
    SCase "b1 evaluates to false".
      assert (st' = st'0) as EQ1.
        SSCase "Proof of assertion". apply IHE1_1; assumption.
      subst st'0.
      apply IHE1_2. assumption. Qed.

A slicker proof, using the step-indexed definition of evaluation

Theorem ceval_deterministic' : forall c st st1 st2,
     c / st ~~> st1
  -> c / st ~~> st2
  -> st1 = st2.
Proof.
  intros c st st1 st2 He1 He2.
  apply ceval__ceval_step in He1.
  apply ceval__ceval_step in He2.
  destruct He1 as [i1 He1].
  destruct He2 as [i2 He2].

  assert (i1 <= i1 + i2) as Hle1 by apply le_plus_l.
  assert (i2 <= i1 + i2) as Hle2 by (rewrite plus_comm; apply le_plus_l).
  assert (ceval_step st c (i1 + i2) = Some st1).
    apply ceval_step_more with i1; assumption.
  assert (ceval_step st c (i1 + i2) = Some st2).
    apply ceval_step_more with i2; assumption.
  rewrite -> H in H0. inversion H0. reflexivity. Qed.

Behavioral equivalence


In the last lecture, we investigated the correctness of some very simple program transformations. There, 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 the state.

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

Definitions


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.

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

Examples of program equivalence


Theorem aequiv_example:
  aequiv (!X --- !X) A0.
Proof.
  unfold aequiv. intros st. simpl.
  apply minus_diag. Qed.

Theorem bequiv_example:
  bequiv (!X --- !X === A0) 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 CESeq with st.
    apply CESkip.
    assumption. Qed.

Exercise: 2 stars (skip_right)

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

Theorem CIf_true_simple: forall c1 c2,
  cequiv
    (CIf BTrue c1 c2)
    c1.
Proof.
  intros c1 c2.
  split; intros H.
  Case "->".
    inversion H; subst. assumption. inversion H5.
  Case "<-".
    apply CEIfTrue. reflexivity. assumption. Qed.

Theorem CIf_true: forall b c1 c2,
     bequiv b BTrue
  -> cequiv
       (CIf b c1 c2)
       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 CEIfTrue; try assumption.
    rewrite Hb. reflexivity. Qed.

An informal proof of CIf_true:

Theorem: forall b c1 c2, if b is equivalent to BTrue, then IFB b THEN c1 ELSE c2 is equivalent to c1.

Proof:
  • (->) We are given that b is equivalent to BTrue. We must show, for all st and st', that if (IFB b THEN c1 ELSE c2) / st ~~> st' then c1 / st ~~> st'.

    There are only two ways we can have IFB b THEN c1 ELSE c2) / st ~~> st', using CEIfTrue or CEIfFalse.

    • Suppose the final rule used to show (IFB b THEN c1 ELSE c2) / st ~~> st' was CEIfTrue. We then have, by the premises of CEIfTrue, that c1 / st ~~> st'. This is exactly what we set out to prove.

    • Suppose the final rule used to show (IFB b THEN c1 ELSE c2) / st ~~> st' was CEIfFalse. 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 CEIfFalse requires that beval st b = false. We therefore conclude that the final rule could not have been CEIfFalse.

  • (<-) Again, we are given that b is equivalent to BTrue. We must show, for all st and st', that if c1 / st ~~> st' then (IFB b THEN c1 ELSE c2) / 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 CEIfTrue to derive (IFB b THEN c1 ELSE c2) / st ~~> st'.

Exercise: 2 stars (CIf_false)

Theorem CIf_false: forall b c1 c2,
     bequiv b BFalse
  -> cequiv
       (CIf b c1 c2)
       c2.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem CWhile_true_nonterm : forall b c st st',
     bequiv b BTrue
  -> ~( (WHILE b DO c LOOP) / st ~~> st' ).
Proof.
  intros b c st st' Hb.
  intros H.
  remember (WHILE b DO c LOOP) 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 "CEWhileEnd". (* contradictory -- b is always true! *)
    rewrite Hb in H. inversion H.
  Case "CEWhileLoop". (* immediate from the IH *)
    apply IHceval2. reflexivity. Qed.

Exercise: 3 stars (CWhile_nonterm_understanding)

Explain what the lemma CWhile_true_nonterm means in English.

(* FILL IN HERE *)

Exercise: 2 stars (CWhile_true)

You'll want to use CWhile_true_nonterm here...

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

Theorem CWhile_false : forall b c,
     bequiv b BFalse
  -> cequiv
       (WHILE b DO c LOOP)
       SKIP.
Proof.
  intros b c Hb.
  unfold cequiv. split; intros.
  Case "->".
    inversion H; subst.
    SCase "CEWhileEnd".
      apply CESkip.
    SCase "CEWhileLoop".
      rewrite Hb in H2. inversion H2.
  Case "<-".
    inversion H; subst.
    apply CEWhileEnd.
    rewrite Hb.
    reflexivity. Qed.

Exercise: 2 stars (CWhile_false_inf)

Write an informal proof of CWhile_false.

(* FILL IN HERE *)

Theorem loop_unrolling: forall b c,
  cequiv
    (WHILE b DO c LOOP)
    (CIf b (c; WHILE b DO c LOOP) SKIP).
Proof.
  unfold cequiv. intros b c st st'.
  split; intros Hce.
  Case "->".
    inversion Hce; subst.
    SCase "loop doesn't run".
      apply CEIfFalse. assumption. apply CESkip.
    SCase "loop runs".
      apply CEIfTrue. assumption.
      apply CESeq with (st' := st'0). assumption. assumption.
  Case "<-".
    inversion Hce; subst.
    SCase "loop runs".
      inversion H5; subst.
      apply CEWhileLoop with (st' := st'0).
      assumption. assumption. assumption.
    SCase "loop doesn't run".
      inversion H5; subst. apply CEWhileEnd. assumption. Qed.

Exercise: 2 stars (seq_assoc)

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

Exercise: 3 stars (swap_if_branches)

Theorem swap_if_branches: forall b e1 e2,
  cequiv
    (CIf b e1 e2)
    (CIf (BNot b) e2 e1).
Proof.
  (* FILL IN HERE *) Admitted.

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. apply sym_eq. 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. apply sym_eq. 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. We prove these lemmas below.

Motivating example (see below): 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 CEAss.
    rewrite Heqv. reflexivity.
  Case "<-".
    inversion Hceval. subst. apply CEAss.
    rewrite Heqv. reflexivity. Qed.

Both directions of this next proof are a little tricky - we need to go by induction...

Theorem CWhile_congruence : forall b1 b1' c1 c1',
  bequiv b1 b1' -> cequiv c1 c1' ->
  cequiv (CWhile b1 c1) (CWhile b1' c1').
Proof.
  unfold bequiv,cequiv.
  intros b1 b1' c1 c1' Hb1e Hc1e st st'.
  split; intros Hce.
  Case "->".
    remember (WHILE b1 DO c1 LOOP) as cwhile.
    induction Hce; try (inversion Heqcwhile); subst.
    SCase "CEWhileEnd".
      apply CEWhileEnd. rewrite <- Hb1e. apply H.
    SCase "CEWhileLoop".
      apply CEWhileLoop 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' LOOP) as c'while.
    induction Hce; try (inversion Heqc'while); subst.
    SCase "CEWhileEnd".
      apply CEWhileEnd. rewrite -> Hb1e. apply H.
    SCase "CEWhileLoop".
      apply CEWhileLoop 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 (CSeq_congruence)

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 (CIf_congruence)

Theorem CIf_congruence : forall b b' c1 c1' c2 c2',
  bequiv b b' -> cequiv c1 c1' -> cequiv c2 c2' ->
  cequiv (CIf b c1 c2) (CIf b' c1' c2').
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 reduces them.

Fixpoint fold_constants_aexp (a : aexp) {struct a} : 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 ((A1 +++ A2) *** !X) = A3 *** !X.
Proof. reflexivity. Qed.

Note that this version of constant folding doesn't eliminate trivial additions, etc.

Example fold_aexp_ex2 :
  fold_constants_aexp (!X --- ((A0 *** A6) +++ !Y))
  = !X --- (A0 +++ !Y).
Proof. reflexivity. Qed.

Not only can we "lift" fold_constants_aexp to bexps (in the BfEq and BLe cases), we can find constant boolean expressions and "fold" them, too.

Fixpoint fold_constants_bexp (b : bexp) {struct b} : 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
  | BOr b1 b2 =>
      match (fold_constants_bexp b1, fold_constants_bexp b2) with
      | (BTrue, BTrue) => BTrue
      | (BTrue, BFalse) => BTrue
      | (BFalse, BTrue) => BTrue
      | (BFalse, BFalse) => BFalse
      | (b1', b2') => BOr b1' b2'
      end
  end.

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

Example fold_bexp_ex2 :
    fold_constants_bexp
       (BAnd (!X === !Y) (A0 === (A2 --- (A1 +++ A1))))
  = BAnd (!X === !Y) BTrue.
Proof. reflexivity. Qed.

Fixpoint fold_constants_com (c : com) {struct c} : com :=
  match c with
  | CSkip =>
      CSkip
  | CAss i a =>
      CAss i (fold_constants_aexp a)
  | CSeq c1 c2 =>
      CSeq (fold_constants_com c1) (fold_constants_com c2)
  | CIf b c1 c2 =>
      match fold_constants_bexp b with
      | BTrue => fold_constants_com c1
      | BFalse => fold_constants_com c2
      | b' => CIf b' (fold_constants_com c1) (fold_constants_com c2)
      end
  | CWhile b c =>
      match fold_constants_bexp b with
      | BTrue => CWhile BTrue CSkip
      | BFalse => CSkip
      | b' => CWhile b' (fold_constants_com c)
      end
  end.

Example fold_com_ex1 :
  fold_constants_com (X ::= A4 +++ A5;
                      Y ::= !X --- A3;
                      (CIf (!X --- !Y === A2 +++ A4)
                       SKIP
                       (Y ::= A0));
                      (CIf (A0 <<= A4 --- (A2 +++ A1))
                       (Y ::= A0)
                       SKIP);
                      WHILE (!Y === A0) DO X ::= !X +++ A1 LOOP) =
  (X ::= ANum 9;
   Y ::= !X --- A3;
   (CIf (!X --- !Y === A6)
    SKIP
    (Y ::= A0));
   Y ::= A0;
   WHILE (!Y === A0) DO X ::= !X +++ A1 LOOP).
Proof. reflexivity. Qed.

Soundness of constant folding


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.

Or, 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 (fold_constants_bexp_sound_BNot_case)

Complete the BLe case of the following proof

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".
  (* Informal proof of this case:

     TO SHOW: beval st (a1 === a2) = beval st (fold_constants_bexp (a1 === a2))

     PROOF: We consider two cases:

     - 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 (a1 === a2) = if beq_nat n1 n2 then BTrue else BFalse

     and

       beval st (a1 === a2) = beq_nat (aeval st a1) (aeval st a2)

     By the lemma fold_constants_aexp_sound, we know that 

       aeval st a1 = aeval st (fold_constants_aexp a1) = aeval st (ANum n1) = n1
       aeval st a2 = aeval st (fold_constants_aexp a2) = aeval st (ANum n2) = n2

     So we show:

       beq_nat n1 n2 = beval st (fold_constants_bexp (a1 === a2))
                     = beval st (if beq_nat n1 n2 then BTrue else BFalse)
                     = if beq_nat n1 n2 then true else false
                     = beq_nat n1 n2

     This completes this case.

     - One of fold_constants_aexp a1 and fold_constants_aexp a2 is not equal to ANum n for any n.  In this case, we
     must show:

       beval st (a1 === a2) = beval st (fold_constants_bexp (a1 === a2))
                            = beval st ((fold_constants_aexp a1) ===
                                        (fold_constants_aexp a2))

     which, by the definition of beval, is the same as:

       beq_nat (aeval st a1) (aeval st a2) = 
       beq_nat (aeval st (fold_constants_aexp a1))
               (aeval st (fold_constants_aexp a2))
                                           
     But the lemma fold_constants_aexp_sound shows that

       aeval st a1 = aeval st (fold_constants_aexp a1)
       aeval st a2 = aeval st (fold_constants_aexp a2)

     And we can see that the equation above holds.                 
     *)

    (* 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
       rename a into 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.
  Case "BOr".
    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 (fold_constants_com_sound_CWhile_case)

Complete the CWhile case of the following proof. Most cases are easy, following from the congruence lemmas and the soundness theorems above.

Theorem fold_constants_com_sound :
  ctrans_sound fold_constants_com.
Proof.
  unfold ctrans_sound. intros c.
  (com_cases (induction c) Case); simpl.
  Case "CSkip". apply refl_cequiv.
  Case "CAss". apply CAss_congruence. apply fold_constants_aexp_sound.
  Case "CSeq". apply CSeq_congruence; assumption.
  Case "CIf".
    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 CIf_congruence; assumption).
    SCase "b always true".
      apply trans_cequiv with c1; try assumption.
      apply CIf_true; assumption.
    SCase "b always false".
      apply trans_cequiv with c2; try assumption.
      apply CIf_false; assumption.
  Case "CWhile".
    (* 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) {struct e} : 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, lifting it all the way up to commands. You should have three functions:

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

Then go on to 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. (Note: this part should be very easy!)

(* FILL IN HERE *)

Case study: 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)

and

       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 subst that substitutes an arithmetic expression for each occurrence of a given location in another expression

Fixpoint subst_aexp (i : id) (u : aexp) (a : aexp) {struct a} : 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 ((ANum 42) +++ (ANum 53)) (!Y +++ !X) =
  (!Y +++ ((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).

Here is the proof that the property does not 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.

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 ::= !X +++ A1; Y ::= !X) as c1.
  remember (X ::= !X +++ A1; Y ::= !X +++ A1) as c2.
  assert (cequiv c1 c2) by (subst; apply Contra).

  (* This allows us to show that the command 
     X ::= !X +++ A1; Y ::= !X 
     can terminate in two different final states:
        st'  = {X |-> 1, Y |-> 1} 
        st'' = {X |-> 1, Y |-> 2}. *)

  remember (override (override empty_state X 1) Y 1) as st'.
  remember (override (override 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 CESeq with (st' := (override empty_state X 1));
         apply CEAss; 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.

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

  assert (cequiv (X ::= !X +++ A1; Y ::= !X)
                 (X ::= !X +++ A1; Y ::= (subst_aexp X (!X +++ A1) (!X)))) as BAD by apply Contra.
  simpl in BAD. unfold cequiv in BAD. clear Contra.
  (* This, in turn, allows us to show that the command 
     X ::= !X +++ A1; Y ::= !X can terminate in two different
     final states:
        st'  = {X |-> 1, Y |-> 1} 
        st'' = {X |-> 1, Y |-> 2}. *)

  remember (override (override empty_state X 1) Y 1) as st'.
  remember (override (override empty_state X 1) Y 2) as st''.
  (* Show termination in st'' (directly) *)
  assert ((X ::= !X +++ A1; Y ::= !X) / empty_state ~~> st') as H.
    Case "Pf of assertion".
      apply CESeq with (override empty_state X 1).
      apply CEAss. reflexivity.
      subst st'. apply CEAss. reflexivity.
  (* Show termination in st' (using BAD equivalence) *)
  assert ((X ::= !X +++ A1; Y ::= !X) / empty_state ~~> st'') as H'.
    Case "Pf of assertion".
      assert ((X ::= !X +++ A1; Y ::= !X) / empty_state ~~> st'' <->
              (X ::= !X +++ A1; Y ::= !X +++ A1) / empty_state ~~> st'') as Hequiv.
        SCase "Proof of sub-assertion". apply BAD.
      inversion Hequiv as [Hequiv1 Hequiv2]. clear Hequiv Hequiv1. apply Hequiv2.
      apply CESeq with (override empty_state X 1).
      apply CEAss. reflexivity.
      subst st''. apply CEAss. reflexivity.
  (* But this contradicts the determinacy of evaluation *)
  assert (st' = st'') as WORSE.
    Case "Pf of assertion".
      apply ceval_deterministic
        with (c := (X ::= !X +++ A1; Y ::= !X))
             (st := empty_state); assumption.
  assert (st' Y = st'' Y) as REALLYBAD.
    Case "Pf of assertion". rewrite WORSE. reflexivity.
  subst. inversion REALLYBAD. Qed.

An informal proof of subst_inequiv

Theorem: It is not the case that, for all i1, i2, a1, and a2,

      cequiv (i1 ::= a1; i2 ::= a2)
             (i1 ::= a1; i2 ::= subst_aexp i1 a1 a2)

Proof: Suppose, for a contradiction, that for all i1, i2, a1, and a2, we have

      cequiv (i1 ::= a1; i2 ::= a2)
             (i1 ::= a1; i2 ::= subst_aexp i1 a1 a2)

Consider the following program:

      X ::= !X +++ A1; Y ::= !X

And note that

      (X ::= !X +++ A1; Y ::= !X) / empty_state ~~> st'

where st' = { X |-> 1, Y |-> 1 }.

By our assumption, we know that

      cequiv (X ::= !X +++ A1; Y ::= !X)
             (X ::= !X +++ A1; Y ::= !X +++ A1)

so, by the definition of cequiv, we have

      (X ::= !X +++ A1; Y ::= !X +++ A1) / empty_state ~~> st'

But we can also derive

      (X ::= !X +++ A1; Y ::= !X +++ A1) / empty_state ~~> st''

where st'' = { X |-> 1, Y |-> 2 }. Note that st' <> st''; this is a contradiction, since ceval is deterministic!

Exercise: 4 stars, optional (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 that it is correct.

(* FILL IN HERE *)

Exercise: 3 stars

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

Reasoning about Imp programs


(* Recall the factorial program: *)
(* Print fact_body. Print fact_loop. Print fact_com. *)

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

Definition fact_invariant (x:nat) (st:state) :=
  exists y, exists z,
     st Y = y
  /\ st Z = z
  /\ mult y (real_fact 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 H HZnz He.
  unfold fact_invariant in H.
  destruct H as [y [z [HY [HZ Hm]]]].
  (* first, note that z = S z' for some z' *)
  assert (exists z', z = S z').
    destruct z as [| z'].
    Case "z = 0 (contra)".
      apply ex_falso_quodlibet.
      apply HZnz. apply HZ.
    Case "z = S z'".
      exists z'. reflexivity.
  destruct H as [z' Heqz]. rewrite Heqz in HZ.
  (* next, we see what reduction of fact_body does...*)
  unfold fact_body in He.
  unfold fact_invariant.
  exists (mult y (S z')).
  exists z'.
  inversion He; subst.
  inversion H2; subst.
  inversion H4; subst.
  simpl. rewrite HZ.
  rewrite (override_neq Z Y); auto.
  rewrite (override_neq Y Z); auto.
  repeat rewrite override_eq in *.
  split. Case "Y correct".
    reflexivity.
  split. Case "Z correct".
(* 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 HZ: st Z = S z'.
  It is beneath the dignity of us humans to search
  around for the right lemma to do this.  Fortunately, there's
  a powerful tactic for solving linear arithmetic inequalities (and
  equalities).  It's called omega, and it's based on the Omega
  algorithm invented in 1992 by William Pugh.  *)

  omega.
(* omega isn't magic.  For example, it can't handle nonlinear
   equations such as x*x*y.  But it often helps.  *)

  Case "mult invariant preserved".
  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 "CEWhileEnd".
    (* trivial when the loop doesn't run... *)
    assumption.
  Case "CEWhileLoop".
    (* 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 LOOP) / st ~~> st'
  -> beval st' b = false.
Proof.
  intros b c st st' Hce.
  remember (WHILE b DO c LOOP) as cloop.
  (ceval_cases (induction Hce) Case); try (inversion Heqcloop; subst).
  Case "CEWhileEnd".
    assumption.
  Case "CEWhileLoop".
    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 (override (override st Z (aeval st (!X))) Y
            (aeval (override st Z (aeval st (!X))) A1)) as st'.
  assert (fact_invariant (st X) st').
    unfold fact_invariant.
    exists 1. exists (st X).
    split.
      subst st'. reflexivity.
    split.
      subst st'. simpl. reflexivity.
      apply mult_1_l.
  (* 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.
  destruct H0 as [y [z [HY [HZ Hf]]]].

  (* finally, if the loop terminated, then z is 0, so y must be
     factorial x *)

  assert (beval st'' (BNot (!Z === A0)) = false).
    apply guard_false_after_loop with (st := st') (c := fact_body).
    apply H6.
  simpl in H0. symmetry in H0; apply negb_sym in H0.
  rewrite HZ in H0. symmetry in H0.
  apply beq_nat_eq in H0. subst z.
  simpl in Hf. rewrite H0 in Hf. rewrite mult_1_r in Hf. subst y.
  assumption. 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) :=
  exists x', exists z',
     st X = x'
  /\ st Z = z'
  /\ minus z' x' = minus z x.

(* FILL IN HERE *)

Additional exercises


Exercise: 3 stars, optional (override_eq_variant)

The way override_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 (override 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 override_eq need to be changed to use the simplified version.

Exercise: 4 stars, optional (add_for_loop)

Add C-style for loops to the language of commands in Imp.v, update the cevals definition to define the semantics of for loops, and add cases for for loops as needed so that all the proofs in Imp.v and this file are accepted by Coq.

A for loop should be parameterized by (a) a statement executed initially, (b) a test that is run on each iteration of the loop to determine whether the loop should continue, (c) a statement executed at the end of each loop iteration, and (d) a statement that makes up the body of the loop. (You don't need to worry about making up a concrete Notation for for loops, but feel free to play with this too if you like.)

Next, prove that the command:

      for (c1 ; b ; c2) {
          c3
      }

is equivalent to:

       c1 ;
       WHILE b DO
         c3 ;
         c2
       LOOP

(* FILL IN HERE *)