(** * Simple imperative programs, part 2
      Version of 3/2/2009 *)

Require Export Whilesol.

(* ------------------------------------------------------- *)
(** * Advice for the homework *)

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

(* ------------------------------------------------------- *)
(** * A useful little hack *)

(* 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... it's cheating! *)
Lemma cheating : forall P, P.  
Proof. Admitted.

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

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

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

(* ------------------------------------------------------- *)
(** ** 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. 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. 
  (* Make sure you understand why this [assert] is here -- i.e.,
     why would things go wrong if we tried to get away without
     it. *)
  assert ((aeval st (!X --- !X)) = (aeval st A0)) as H. 
  apply aequiv_example. rewrite H. apply sym_eq. apply beq_nat_refl.  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 (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'].                                      []
*)

(* Exercise: 2 stars *)
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.

(* Exercise: 3 stars (CWhile_nonterm_understanding) *)
(* Explain what the lemma CWhile_true_nonterm means in English.

(* FILL IN HERE *)

*)

(* Exercise: 2 stars (CWhile_true) *)
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.

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

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

(* Exercise: 3 stars (swap_if_branches) *)
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.

(* ------------------------------------------------------- *)
(** ** Program equivalence is an equivalence *)

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

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.

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