Require Export While.

(* ------------------------------------------------------- *)

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

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

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

(* ------------------------------------------------------- *)

(* We'll use this lemma in a few places where we'd like you to
   finish just one case in the middle of a proof.  Don't use it
   yourself (in anything you turn in)... it's cheating! *)
Lemma cheating : forall P, P.
Proof. Admitted.

(* ------------------------------------------------------- *)

(* 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 ->.
*)
Notation "c1 '/' st '-->' st'" := (ceval st c1 st') (at level 40).

(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)

(* 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.
  assert (i2 <= i1 + i2) as Hle2 by (rewrite plus_comm; apply le_plus).
  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.

(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)

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

(* ------------------------------------------------------- *)

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

(* ------------------------------------------------------- *)

Theorem aequiv_example:
  aequiv (!X --- !X) A0.
Proof.
  unfold aequiv. intros st. unfold aeval.
  destruct (lookup X st). apply minus_n_n. reflexivity. Qed.

Theorem bequiv_example:
  bequiv (!X --- !X === A0) BTrue.
Proof.
  unfold bequiv. intros st. unfold beval.
  rewrite aequiv_example. rewrite beq_nat_refl with (aeval st A0).
  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.

Theorem skip_right: forall c,
  cequiv
    (c; skip)
    c.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem CIf_true_simple: forall c1 c2,
  cequiv
    (testif BTrue then c1 else 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
       (testif b then c1 else 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)".
      unfold bequiv in Hb.
      rewrite -> Hb in H5.
      inversion H5.
  Case "<-".
    apply CEIfTrue; try assumption.
    unfold bequiv in Hb.
    rewrite -> Hb. reflexivity. Qed.

(* An informal proof of CIf_true:

   THEOREM: forall b c1 c2, if b is equivalent to BTrue,
   then (testif 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 (testif b then c1 else c2) /
   st --> st' then c1 / st --> st'.

   There are only two ways we can have (testif b then c1 else
   c2) / st --> st': using CEIfTrue and CEIfFalse.

     - Suppose the final rule used to show (testif 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 (testif 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 (testif 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 (testif b then c1 else c2) / st --> st'.                                      
*)

Theorem CIf_false: forall b c1 c2,
     bequiv b BFalse
  -> cequiv
       (testif b then c1 else c2)
       c2.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

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

(* Explain what the lemma CWhile_true_nonterm means in English.

(* FILL IN HERE *)
*)

Theorem CWhile_true: forall b c,
     bequiv b BTrue
  -> cequiv
       (while b do c)
       (while BTrue do skip).
Proof.
  (* You'll want to use CWhile_true_nonterm here... *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

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

(*
   Write an informal proof of CWhile_false.

(* FILL IN HERE *)
*)

Theorem loop_unrolling: forall b c,
  cequiv
    (while b do c)
    (testif b then (c; while b do c) else 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 "look doesn't run".
      inversion H5; subst. apply CEWhileEnd. assumption. Qed.

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

Theorem swap_if_branches: forall b e1 e2,
  cequiv
    (testif b then e1 else e2)
    (testif (BNot b) then e2 else e1).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------- *)

(* The equivalences on aexps, bexps, and commands 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.
  unfold aequiv. 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.
  inversion H'.
  split; intros H2.
  Case "->".
    apply H1. assumption.
  Case "->".
    apply H0. assumption. Qed.

Lemma trans_iff : 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 trans_iff with (c2 / st --> st'). apply H12. apply H23. Qed.

(* ------------------------------------------------------- *)

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

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.
  (* Both directions of the proof are a little tricky - we need
     to go by induction... *)
  Case "->".
    remember (while b1 do c1) 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') 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.

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

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 (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------- *)

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

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
   BEq and BLtEq 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
  | BLtEq 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') => BLtEq 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;
                      (testif (!X --- !Y === A2 +++ A4)
                       then skip
                       else Y ::= A0);
                      (testif (A0 <<= A4 --- (A2 +++ A1))
                       then Y ::= A0
                       else skip);
                      while (!Y === A0) do X ::= !X +++ A1) =
  (X ::= ANum 9;
   Y ::= !X --- A3;
   (testif (!X --- !Y === A6)
    then skip
    else Y ::= A0);
   Y ::= A0;
   while (!Y === A0) do X ::= !X +++ A1).
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.

(* 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 (remember (fold_constants_aexp a1) as a1';
         remember (fold_constants_aexp a2) as a2';
         rewrite IHa1; rewrite IHa2;
         destruct a1'; destruct a2'; reflexivity). Qed.

(* Complete the BLtEq 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 "BLtEq".
    (* Delete this application and complete the proof *) apply cheating.
  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.

(* 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 testif, 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 (and delete "Admitted") *) Admitted.

(* ------------------------------ *)
(* Soundness of (0 + n) elimination *)

(* Recall the definition optimize_0plus from While.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 versions:

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

(* ------------------------------------------------------- *)

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

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 (extend (extend empty_state X 1) Y 1) as st'.
  remember (extend (extend 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 (extend 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 (extend 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!    
     *)

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

Theorem inequiv_exercise:
  ~ cequiv (while BTrue do skip) skip.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)
(* ------------------------------------------------------- *)

(* A slightly different version of the factorial program *)

Definition fact_body : com :=
  Y ::= !Y *** !Z;
  Z ::= !Z --- A1.

Definition fact_loop : com :=
  while BNot (!Z === A0) do
    fact_body.

Definition fact_com : com :=
  Z ::= !X;
  Y ::= ANum 1;
  fact_loop.

Definition fact_invariant (x:nat) (st:state) :=
  exists y, exists z,
     lookup Y st = Some y
  /\ lookup Z st = Some z
  /\ mult y (factorial z) = factorial x.

Theorem fact_body_preserves_invariant: forall st st' x,
     fact_invariant x st
  -> lookup Z st <> Some 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]. subst z.
  (* 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 HY. rewrite HZ.
  assert (lookup Z (extend st Y (mult y (S z'))) = Some (S z')) as HZ'.
    apply extend_neq. assumption.
    reflexivity.
  rewrite HZ'.
  split. Case "Y correct".
    reflexivity.
  split. Case "Z correct".
    reflexivity.
  Case "mult invariant preserved".
  rewrite <- Hm.
  simpl. rewrite <- mult_assoc.
  assert (mult (S z') (factorial z') = plus (factorial z') (mult z' (factorial z'))).
    simpl. reflexivity.
  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 (lookup Z st <> Some 0) as HZnz.
      intros Contra.
      inversion H0; subst. apply negb_flip 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) / st --> st'
  -> beval st' b = false.
Proof.
  intros b c st st' Hce.
  remember (while b do c) 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,
     lookup X st = Some x
  -> fact_com / st --> st'
  -> lookup Y st' = Some (factorial 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 (extend (extend st Z (aeval st (!X))) Y
            (aeval (extend st Z (aeval st (!X))) A1)) as st'.
  assert (fact_invariant x st').
    unfold fact_invariant.
    exists 1. exists x.
    split.
      subst st'. reflexivity.
    split.
      subst st'. simpl. rewrite HX. reflexivity.
      apply mult_1_l.
  (* and that when the loop is done running, the invariant is maintained *)
  assert (fact_invariant 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. apply negb_flip in H0.
  rewrite HZ in H0. symmetry in H0.
  apply beq_nat_eq in H0. subst z.
  simpl 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! *)

(* 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',
     lookup X st = Some x'
  /\ lookup Z st = Some z'
  /\ minus z' x' = minus z x.

(* FILL IN HERE *)

(* ------------------------------------------------------- *)

(* The way extend_eq is stated (in the section on mappings in
   While.v) may have looked a bit surprising: wouldn't it be
   simpler just to say lookup k (extend 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
   extend_eq need to be changed to use the simplified
   version. *)

(* Add C-style for loops to the language of commands in
   While.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 While.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
       } 
*)
(* FILL IN HERE *)

(* mode: outline-minor *)
(* outline-heading-end-regexp: "\n" *)