(** * 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 [aexp]s and [bexp]s, the definition we want is clear.  We
    say that two [aexp]s or [bexp]s 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 [com]s 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
    [aexp]s, [bexp]s, and [com]s. *)

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 [bexp]s (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 [aexp]s,
   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 *)
(** [] *)