(** * Imp: Simple imperative programs *)
(* Version of 11/3/2009 *)

(* Require Export Logic. *)

Require Export SfLib.

(* ####################################################### *)
(** * Templates for informal proofs by induction *)

(** In the real world of mathematical communication, written
    proofs range from extremely longwinded and pedantic to
    extremely brief and telegraphic.  The ideal is probably
    somewhere in between, but while you are getting used to the
    style it is better to start out at the pedantic end.  Also,
    during the learning phase, it is probably helpful to have a
    clear standard to compare against.  So...
 
    For the rest of the course, ALL your inductive proofs should
    match one of the two following templates.
 
    1) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN
    INDUCTIVELY DEFINED SET:
 
       THEOREM: <Universally quantified proposition of the form
       "For all [n:S], [P(n)]," where [S] is some inductively defined
       set.>
 
       PROOF: By induction on [n].
 
         <one case for each constructor [c] of [S]...>
         
         - Suppose [n = c a1 ... ak], where <...and here we state
           the IH for each of the [a]'s that has type [S], if any>.
           We must show <...and here we restate [P(c a1 ... ak)]>.
         
           <go on and prove [P(n)] to finish the case...>
         
         - <other cases similarly...>                        []
 
    EXAMPLE
 
      THEOREM: For all sets [X], lists [l : list X], and numbers
      [n], if [length l = n] then [index (S n) l = None].
 
      PROOF: By induction on [l].
 
      - Suppose [l = []].  We must show, for all numbers [n],
        that, if length [[] = n], then [index (S n) [] =
        None].
 
        This follows immediately from the definition of index.
 
      - Suppose [l = x :: l'] for some [x] and [l'], where
        [length l' = n'] implies [index (S n') l' = None], for
        any number [n'].  We must show, for all [n], that, if
        [length (x::l') = n] then [index (S n) (x::l') =
        None].
 
        Let [n] be a number with [length l = n].  Since
[[
          length l = length (x::l') = S (length l'),
]]
        it suffices to show that 
[[
          index (S (length l')) l' = None.
]]  
        But this follows directly from the induction hypothesis,
        picking [n'] to be length [l'].  []
 
 
    2) TEMPLATE FOR INFORMAL PROOFS BY INDUCTION OVER AN
    INDUCTIVELY DEFINED PROPOSITION (I.E., "INDUCTION ON
    DERIVATIONS"):
 
       THEOREM: <Proposition of the form "[Q -> P]," where [Q] is
       some inductively defined proposition.  (More generally,
       "For all [x] [y] [z], [Q x y z -> P x y z].">
 
       PROOF: By induction on a derivation of [Q].  <Or, more
       generally, "Suppose we are given [x], [y], and [z].  We
       show that [Q x y z] implies [P x y z], by induction on a
       derivation of [Q x y z]"...>
 
         <one case for each constructor [c] of [Q]...>
 
         - Suppose the final rule used to show [Q] is [c].  Then
           <...and here we state the types of all of the [a]'s
           together with any equalities that follow from the
           definition of the constructor and the IH for each of
           the [a]'s that has type [Q], if there are any>.  We must
           show <...and here we restate [P]>.
 
           <go on and prove [P] to finish the case...>
 
         - <other cases similarly...>                        []
 
    EXAMPLE
 
       THEOREM: The [<=] relation is transitive -- i.e., for all
       numbers [n], [m], and [o], if [n <= m] and [m <= o], then
       [n <= o].
 
       PROOF: By induction on a derivation of [m <= o].
 
         - Suppose the final rule used to show [m <= o] is
           [le_n].  Then [m = o] and the result is immediate.
 
         - Suppose the final rule used to show [m <= o] is
           [le_S].  Then [o = S o'] for some [o'] with [m <= o'].
           By induction hypothesis, [n <= o'].
 
           But then, by [le_S], [n <= o].  [] *)

(* ####################################################### *)
(** * Evaluating arithmetic expressions *)

Module AExp.

Inductive aexp : Type := 
  | ANum : nat -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

Definition two_plus_two := APlus (ANum 2) (ANum 2).

(** Since we're going to be writing a lot of these arithmetic
   expressions, let's introduce some concrete syntax that's nicer
   to look at. *)
Notation "a1 '+++' a2" := (APlus a1 a2) (at level 50).
Notation "a1 '---' a2" := (AMinus a1 a2) (at level 50).
Notation "a1 '***' a2" := (AMult a1 a2) (at level 40).

Notation A0 := (ANum 0).
Notation A1 := (ANum 1).
Notation A2 := (ANum 2).
Notation A3 := (ANum 3).
Notation A4 := (ANum 4).
Notation A5 := (ANum 5).

Definition two_plus_two' := A2 +++ A2.

Fixpoint aeval (e : aexp) {struct e} : nat :=
  match e with
  | ANum n => n
  | APlus a1 a2 => plus (aeval a1) (aeval a2)
  | AMinus a1 a2  => minus (aeval a1) (aeval a2)
  | AMult a1 a2 => mult (aeval a1) (aeval a2)
  end.

Example test_aeval1: 
  aeval two_plus_two = 4.
Proof. reflexivity. Qed.

Inductive bexp : Type := 
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLe : aexp -> aexp -> bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp
  | BOr : bexp -> bexp -> bexp.

Fixpoint beval (e : bexp) {struct e} : bool :=
  match e with 
  | BTrue       => true
  | BFalse      => false
  | BEq a1 a2   => beq_nat (aeval a1) (aeval a2)
  | BLe a1 a2   => ble_nat (aeval a1) (aeval a2)
  | BNot b1     => negb (beval b1)
  | BAnd b1 b2  => andb (beval b1) (beval b2)
  | BOr b1 b2   => orb (beval b1) (beval b2)
  end.

Notation "b1 '===' b2" := (BEq b1 b2) (at level 60).
Notation "b1 '<<=' b2" := (BLe b1 b2) (at level 60).

(* ####################################################### *)
(** * Correctness of a simple optimization *)

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.

Example test_optimize_0plus: 
  optimize_0plus (A2 +++ (A0 +++ (A0 +++ A1))) = A2 +++ A1.
Proof. reflexivity. Qed.

Theorem optimize_0plus_sound: forall e,
  aeval (optimize_0plus e) = aeval e.
Proof.
  intros e. induction e.
  Case "ANum". reflexivity.
  Case "APlus". destruct e1.
    SCase "e1 = ANum n". destruct n.
      SSCase "n = 0".  simpl. apply IHe2. 
      SSCase "n <> 0". simpl. rewrite IHe2. reflexivity.
    SCase "e1 = APlus e1_1 e1_2". 
      simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity.
    SCase "e1 = AMinus e1_1 e1_2". 
      simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity.
    SCase "e1 = AMult e1_1 e1_2". 
      simpl. simpl in IHe1. rewrite IHe1. rewrite IHe2. reflexivity.
  Case "AMinus".  
    simpl. rewrite IHe1. rewrite IHe2. reflexivity.
  Case "AMult".
    simpl. rewrite IHe1. rewrite IHe2. reflexivity.  Qed.


(* ####################################################### *)
(** * Tacticals *)

(** The repetition in this last proof is starting to be a little
    annoying.  It's still bearable here, but clearly, if either
    the language of arithmetic expressions or the optimization
    being proved sound were significantly more complex, it would
    start to be a real problem.
 
    So far, we've been doing all our proofs using just a small
    handful of Coq's tactics and completely ignoring its very
    powerful facilities for constructing proofs automatically.
    This section introduces some of these facilities, and we will
    see more over the next several chapters.  Getting used to
    them will take some energy -- Coq's automation is a power
    tool -- but it will allow us to scale up our efforts to more
    complex definitions and more interesting properties without
    becoming overwhelmed by boring, repetitive, or low-level
    details.
 
    "Tactical" is Coq's term for operations that manipulate
    tactics -- higher-order tactics, if you will.  *)

(* ####################################################### *)
(** ** The [try] tactical *)

(** One very simple tactical is [try]: If [T] is a tactic, then
    [try T] is a tactic that is just like [T] except that, if [T]
    fails, [try T] does nothing at all (instead of failing). *)

(* ####################################################### *)
(** ** The [;] tactical *)

(** Another very basic tactical is written [;].  If [T], [T1],
    ..., [Tn] are tactics, then
[[
      T; [T1 | T2 | ... | Tn] 
]]
   is a tactic that first performs [T] and then performs [T1] on
   the first subgoal generated by [T], performs [T2] on the
   second subgoal, etc.

   In the special case where all of the [Ti]s are the same tactic
   [T'], we can just write [T;T'] instead of:
[[
      T; [T' | T' | ... | T'] 
]]
   That is, if [T] and [T'] are tactics, then [T;T'] is a tactic
   that first performs [T] and then performs [T'] on EACH SUBGOAL
   generated by [T].  This is the form of [;] that is used most
   often in practice. *)

(** For example, consider the following trivial lemma *)
Lemma foo : forall n, ble_nat 0 n = true. 
Proof. 
  intros.
  destruct n. 
    (* Leaves two subgoals...  *) 
    Case "n=0". simpl. reflexivity.
    Case "n=Sn'". simpl. reflexivity.
    (* ... which are discharged similarly *)
Qed.

(** We can simplify the proof above using [;] *)
Lemma foo' : forall n, ble_nat 0 n = true.
Proof.
  intros. 
  (* Apply [destruct] to the current goal *)
  destruct n; 
  (* then apply [simpl] to each resulting subgoal *)
  simpl;
  (* then apply [reflexivity] to each resulting subgoal *)
  reflexivity.
Qed.
 
(** For a more interesting example of [;], consider the following
    proof... *)
Lemma foo'' : forall n, ble_nat 0 n = true.
Proof.
  intros.
  (* [destruct] the current goal ... *)
  destruct n; 
  (* [simpl] each resulting subgoal ... *)
  simpl.
  (* ... leaving _two_ trivial subgoals. *)
    reflexivity.
    reflexivity.
Qed.


(** Using [try] and [;] together, we can get rid of the repetition
    in the above proof. *)
Theorem optimize_0plus_sound': forall e,
  aeval (optimize_0plus e) = aeval e.
Proof.
  intros e.
  induction e; 
    (* Most cases follow directly by the IH *)
    try (simpl; rewrite IHe1; rewrite IHe2; reflexivity).
  Case "ANum". reflexivity.
  Case "APlus". 
    destruct e1; 
      (* Most cases follow directly by the IH *)
      try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity).
    (* The interesting case, on which the above fails, is when e1 = ANum n *)
    SCase "e1 = ANum n". destruct n.
      SSCase "n = 0". simpl. apply IHe2.
      SSCase "n <> 0". simpl. rewrite IHe2. reflexivity.  Qed.

(** In practice, Coq experts often use [try] with a tactic like
    [induction] to take care of many similar "straightforward"
    cases all at once.  Naturally, this practice has an analog in
    informal proofs.  Here is an informal proof of our example
    theorem that matches the structure of the formal one:
    
     Theorem: For all arithmetic expressions [e],
[[
       aeval (optimize_0plus e) = aeval e.
]]
     Proof: By induction on [e].  The [AMinus] and [AMult] cases
     follow directly from the IH.  The remaining cases are as follows: 
    
     - Suppose [e = ANum n] for some [n].  We must show 
[[
          aeval (optimize_0plus (ANum n)) = aeval (ANum n).
]]
       This is immediate from the definition of [optimize_0plus].
    
     - Suppose [e = APlus e1 e2] for some [e1] and [e2].  We
       must show
[[
          aeval (optimize_0plus (APlus e1 e2)) 
        = aeval (APlus e1 e2).
]]
       Consider the possible forms of [e1].  For most of them,
       [optimize_0plus] simply calls itself recursively for the
       subexpressions and rebuilds a new expression of the same
       form as [e1]; in these cases, the result follows directly
       from the IH.
    
       The interesting case is when [e1 = ANum n] for some [n].
       If [n = ANum 0], then
[[
          optimize_0plus (APlus e1 e2) = optimize_0plus e2
]]
       and the IH for [e2] is exactly what we need.  On the
       other hand, if [n = S n'] for some [n'], then again
       [optimize_0plus] simply calls itself recursively, and the
       result follows from the IH.  []
    
    This proof can still be improved: the first case (for [e =
    ANum n]) is very trivial -- even more trivial than the cases
    that we said simply followed from the IH -- yet we have chosen
    to write it out in full.  It would be better and clearer to
    drop it and just say, at the top, "Most cases are either
    immediate or direct from the IH.  The only interesting case is
    the one for [APlus]..."
    
    Of course, we'd like to do the same thing in our formal proof
    too!  Here's how this looks:
*)

Theorem optimize_0plus_sound'': forall e,
  aeval (optimize_0plus e) = aeval e.
Proof.
  intros e. 
  induction e; 
    (* Most cases follow directly by the IH *)
    try (simpl; rewrite IHe1; rewrite IHe2; reflexivity);
    (* ... or are immediate by definition *)
    try (reflexivity).
  (* The interesting case is when e = APlus e1 e2. *)
  Case "APlus". 
    destruct e1; 
      try (simpl; simpl in IHe1; rewrite IHe1; rewrite IHe2; reflexivity).
    SCase "e1 = ANum n". destruct n.
      SSCase "n = 0". apply IHe2.
      SSCase "n <> 0". simpl. rewrite IHe2. reflexivity.  Qed.


(* ####################################################### *)
(** * Defining new tactic notations *)

(** Coq also provides some handy ways to define "shorthand
    tactics" that, when invoked, apply several tactics at the
    same time. *)

Tactic Notation "simpl_and_try" tactic(c) :=
  simpl;
  try c.

(** Here's a more interesting use of this feature... *)

(* ####################################################### *)
(** ** Bulletproofing case analyses *)

(** Being able to deal with most of the cases of an [induction]
    or [destruct] all at the same time is very convenient, but it
    can also be a little confusing.  One problem that often comes
    up is that _maintaining_ proofs written in this style can be
    difficult.  For example, suppose that, later, we extended the
    definition of [aexp] with another constructor that also
    required a special argument.  The above proof might break
    because Coq generated the subgoals for this constructor
    before the one for [APlus], so that, at the point when we
    start working on the [APlus] case, Coq is actually expecting
    the argument for a completely different constructor.  What
    we'd like is to get a sensible error message saying "I was
    expecting the [AFoo] case at this point, but the proof script
    is talking about [APlus]."  Here's a nice little trick that
    smoothly achieves this. *)

Tactic Notation "aexp_cases" tactic(first) tactic(c) :=
  first;
  [ c "ANum" | c "APlus" | c "AMinus" | c "AMult" ].

(** If [e] is a variable of type [aexp], then doing
[[
      aexp_cases (induction e) (Case)
]]
    will perform an induction on [e] (the same as if we had just
    typed [induction e]) and _also_ add a [Case] tag to each
    subgoal labeling which constructor it comes from.  *)

(** **** Exercise: 3 stars (optimize_0plus_b) *)
(** Since the [optimize_0plus] tranformation doesn't change the
    value of [aexp]s, we should be able to apply it to all the
    [aexp]s that appear in a [bexp] without changing the [bexp]'s
    value.  Write a function which performs that transformation
    on [bexp]s, and prove it is sound.  Use the tacticals we've
    just seen to make the proof as elegant as possible. *)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 4 stars (optimizer) *)
(** DESIGN EXERCISE: The optimization implemented by our
   [optimize_0plus] function is only one of many imaginable
   optimizations on arithmetic and boolean expressions.  Write a
   more sophisticated optimizer and prove it correct.

(* FILL IN HERE *)
*)
(** [] *)

End AExp.

(* ####################################################### *)
(** ** A couple more handy tactics *)

(**
     - [clear H]

       remove hypothesis [H] from the context

     - [subst x]
     
       find an assumption [x = e] or [e = x] in the context,
       replace [x] with [e] throughout the context and current
       goal, and clear the assumption

     - [subst]

       substitute away _all_ assumptions of the form [x = e] or
       [e = x]

     - [assumption]
     
       tries to find a hypothesis [H] in the context that exactly
       matches the goal; if one is found, behaves just like
       [apply H] *)


(** We'll see many examples of these in the proofs below... *)

(* ####################################################### *)
(** * While programs *)

(* ##################################################### *)
(** ** Mappings *)

(** In the rest of the course, we'll often need to talk about
    "identifiers," such as program variables.  We could use
    strings for this, or (as in a real compiler) some kind of
    fancier structures like symbols from a symbol table.  For
    simplicity, though, let's just use natural numbers as
    identifiers.  We define a new inductive datatype so that we
    won't confuse identifiers and numbers. *)

Inductive id : Type := 
  Id : nat -> id.

Definition beq_id id1 id2 :=
  match (id1, id2) with
    (Id n1, Id n2) => beq_nat n1 n2
  end.

Theorem beq_id_refl : forall i,
  true = beq_id i i.
Proof.
  intros. destruct i.
  unfold beq_id. apply beq_nat_refl.  Qed.

(** **** Exercise: 1 star *)
Theorem beq_id_eq : forall i1 i2,
  true = beq_id i1 i2 -> i1 = i2.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 1 star *)
Theorem beq_id_false_not_eq : forall i1 i2,
  beq_id i1 i2 = false -> i1 <> i2.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 1 star *)
Theorem not_eq_beq_id_false : forall i1 i2,
  i1 <> i2 -> beq_id i1 i2 = false.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

Definition state := id -> nat.

Definition empty_state : state := fun _ => 0.
 
(* ####################################################### *) 
(** ** Operations on States *)

(** Next, we redefine basic operations on states to use the 
    new definition of [id]s *)

Definition override (st : state) (V:id) (n : nat) :=
  fun V' => if beq_id V V' then n else st V'.

Theorem override_eq : forall n V st,
  (override st V n) V = n.
Proof.
  intros n V st.
  unfold override.
  destruct V. unfold beq_id.
  rewrite <- beq_nat_refl.
  reflexivity.
Qed.

(** **** Exercise: 2 stars *)
Theorem override_neq : forall l2 l1 n2 st,
  beq_id l2 l1 = false ->
  (override st l2 n2) l1 = (st l1).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars, optional *)
(** Before starting to play with tactics, make sure you
    understand exactly what the theorem is saying! *)

Theorem override_example : forall (X:Type) (n:nat), 
  (override empty_state (Id 2) n) (Id 3) = 0.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars, optional *)
Theorem override_shadow : forall x1 x2 k1 k2 (f : state),
   (override  (override f k2 x1) k2 x2) k1 = (override f k2 x2) k1.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars, optional *)
Theorem override_same : forall x1 k1 k2 (f : state),
  f k1 = x1 ->
  (override f k1 x1) k2 = f k2.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars, optional *)
Theorem override_permute : forall x1 x2 k1 k2 k3 f,
  beq_id k2 k1 = false -> 
  (override (override f k2 x1) k1 x2) k3 = (override (override f k1 x2) k2 x1) k3.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ################################################### *)
(** ** Imp program syntax *)

(** We now define the Imp language, an imperative
    programming language with loops, conditionals, and
    arithmetic. *)

(** We add variables to the arithmetic expressions we had before: *)
Inductive aexp : Type := 
  | ANum : nat -> aexp
  | AId : id -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

Tactic Notation "aexp_cases" tactic(first) tactic(c) :=
  first;
  [ c "ANum" | c "AId" | c "APlus" | c "AMinus" | c "AMult" ].

(** Same notations as before... *)
Notation A0 := (ANum 0).
Notation A1 := (ANum 1).
Notation A2 := (ANum 2).
Notation A3 := (ANum 3).
Notation A4 := (ANum 4).
Notation A5 := (ANum 5).
Notation A6 := (ANum 6).

Notation "a1 '***' a2" := (AMult a1 a2)
  (at level 50).

Notation "a1 '---' a2" := (AMinus a1 a2)
  (at level 40).

Notation "a1 '+++' a2" := (APlus a1 a2)
  (at level 40).

(** ...plus one more: *)
Notation "'!' X" := (AId X)
  (at level 30).

(** Shorthands for variables: *)
Definition X : id := Id 0.
Definition Y : id := Id 1.
Definition Z : id := Id 2.


(** Note that the choice of variable names ([X], [Y], [Z])
    clashes a bit with our earlier use of uppercase letters for
    [Types].  Since we're not using polymorphism heavily in this
    section, this overloading will hopefully not cause
    confusion. *)

(** Same [bexp]s as before (using the new [aexp]s) *)
Inductive bexp : Type := 
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLe : aexp -> aexp -> bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp
  | BOr : bexp -> bexp -> bexp.

Notation "b1 '===' b2" := (BEq b1 b2)
  (at level 60).

Notation "b1 '<<=' b2" := (BLe b1 b2)
  (at level 60).

Tactic Notation "bexp_cases" tactic(first) tactic(c) :=
  first;
  [ c "BTrue" | c "BFalse" | 
    c "BEq" | c "BLe" | 
    c "BNot" | c "BAnd" | c "BOr" ].

(** Finally, we can define the set of commands *)
Inductive com : Type :=
  | CSkip : com
  | CAss : id -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com.

Tactic Notation "com_cases" tactic(first) tactic(c) :=
  first;
  [ c "CSkip" | c "CAss" | c "CSeq" | c "CIf" | c "CWhile" ].

Notation "'SKIP'" := 
  CSkip.
Notation "c1 ; c2" := 
  (CSeq c1 c2) (at level 80, right associativity).
Notation "l '::=' a" := 
  (CAss l a) (at level 60).
Notation "'WHILE' b 'DO' c 'LOOP'" := 
  (CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3" := 
  (CIf e1 e2 e3) (at level 80, right associativity).

(* ####################################################### *)
(** ** Some programs... *)

Definition plus2 : com :=
  X ::= !X +++ A2.

(** Note that the notations we introduced make it easy to write
   down commands that look close to how they would in a real
   imperative programming language; for example, here's what
   [plus2] looks like fully expanded: *)
Example plus2_notation :
  plus2 = 
  CAss (Id 0) (APlus (AId (Id 0)) (ANum 2)).
Proof. reflexivity. Qed.

Definition XtimesYinZ : com :=
  Z ::= !X *** !Y.

(** loops *)
Definition subtract_slowly_body : com :=
  Z ::= !Z --- A1;
  X ::= !X --- A1.

Definition subtract_slowly : com :=
  WHILE BNot (!X === A0) DO
    subtract_slowly_body
  LOOP.

Definition subtract_3_from_5_slowly : com :=
  X ::= A3;
  Z ::= A5;
  WHILE BNot (!X === A0) DO
    subtract_slowly_body
  LOOP.

(** an infinite loop *)
Definition loop : com :=
  WHILE BTrue DO
    SKIP
  LOOP.

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

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

Definition fact_loop : com :=
  WHILE BNot (!Z === A0) DO
    fact_body
  LOOP.

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

(** exponentiation *)
Definition exp_body : com :=
    Z ::= !Z *** !X;
    Y ::= !Y --- A1.
    
Definition pexp : com :=
  WHILE BNot (!Y === (ANum 0)) DO
    exp_body
  LOOP.

(** Note that [pexp] should be run in a state where [Z] is
    [1]. *)

(** **** Exercise: 2 stars *)
(** Write a [While] program that sums the numbers from [1] to [X]
   (inclusive: [1 + 2 + ... + X]) in the variable [Y].  *)

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 2 stars *)
(** Write a [While] program that sets [Z] to [0] if [X] is even
    and sets [Z] to [1] otherwise. *)

(* FILL IN HERE *)
(** [] *)

(* ################################################################ *)
(** * Evaluation *)

(** Now we will define what it means to evaluate an Imp program *)

(** We extend the arith evaluator to handle variables. *)
Fixpoint aeval (st : state) (e : aexp) {struct e} : nat :=
  match e with
  | ANum n => n
  | AId i => st i
  | APlus a1 a2 => plus (aeval st a1) (aeval st a2)
  | AMinus a1 a2  => minus (aeval st a1) (aeval st a2)
  | AMult a1 a2 => mult (aeval st a1) (aeval st a2)
  end.

(** We update the boolean evaluator with the new [aeval]. *)
Fixpoint beval (st : state) (e : bexp) {struct e} : bool :=
  match e with 
  | BTrue       => true
  | BFalse      => false
  | BEq a1 a2   => beq_nat (aeval st a1) (aeval st a2)
  | BLe a1 a2 => ble_nat (aeval st a1) (aeval st a2)
  | BNot b1     => negb (beval st b1)
  | BAnd b1 b2  => andb (beval st b1) (beval st b2)
  | BOr b1 b2   => orb (beval st b1) (beval st b2)
  end.

(** First try at an evaluator for commands, omitting [CWhile]. *)
Fixpoint ceval_step1 (st : state) (c : com) {struct c} : state :=
  match c with 
    | CSkip => 
        st
    | CAss l a1 => 
        override st l (aeval st a1)
    | CSeq c1 c2 => 
        let st' := ceval_step1 st c1 in
        ceval_step1 st' c2
    | CIf b c1 c2 => 
        if (beval st b) then ceval_step1 st c1 else ceval_step1 st c2
    | CWhile b1 c1 => 
        st  (* bogus *)
  end.

(** Second try, using an extra "step index" to ensure that
    evaluation always terminates *)
Fixpoint ceval_step2 (st : state) (c : com) (i : nat) {struct i} : state :=
  match i with 
  | O => empty_state
  | S i' =>
    match c with 
      | CSkip => 
          st
      | CAss l a1 => 
          override st l (aeval st a1)
      | CSeq c1 c2 => 
          let st' := ceval_step2 st c1 i' in
          ceval_step2 st' c2 i' 
      | CIf b c1 c2 => 
          if (beval st b) then ceval_step2 st c1 i' else ceval_step2 st c2 i'
      | CWhile b1 c1 => 
          if (beval st b1) 
          then let st' := ceval_step2 st c1 i' in
               ceval_step2 st' (CWhile b1 c1) i'
          else st
    end
  end.

(** NOTE: It is tempting to think that the index [i] here is
   counting the "number of steps of evaluation."  But if you look
   closely you'll see that this is not the case: for example, in
   the [CSeq] rule, the same [i] is passed to both recursive
   calls.  Understanding the exact way that [i] is treated will
   be important in the proof of [ceval__ceval_step], which is
   given as an exercise below. *)

Definition bind_option (X Y : Type) (xo : option X) (f : X -> option Y) 
                      : option Y :=
  match xo with
    | None => None
    | Some x => f x
  end.
Implicit Arguments bind_option [X Y].

(** Third try, returning an [option state] instead of just a
    [state] so that we can distinguish between normal and abnormal
    termination. *)
Fixpoint ceval_step (st : state) (c : com) (i : nat) 
                    {struct i} : option state :=
  match i with 
  | O => None
  | S i' =>
    match c with 
      | CSkip => 
          Some st
      | CAss l a1 => 
          Some (override st l (aeval st a1))
      | CSeq c1 c2 => 
          bind_option 
            (ceval_step st c1 i')
            (fun st' => ceval_step st' c2 i')
      | CIf b c1 c2 => 
          if (beval st b) then ceval_step st c1 i' else ceval_step st c2 i'
      | CWhile b1 c1 => 
          if (beval st b1)           
          then bind_option 
                 (ceval_step st c1 i')
                 (fun st' => ceval_step st' (CWhile b1 c1) i')
          else Some st
    end
  end.

Reserved Notation "c1 '/' st '~~>' st'" (at level 40).

(** A better way: define [ceval] as a _relation_, rather than a
    (total) _function_. *)
Inductive ceval : state -> com -> state -> Prop :=
  | CESkip : forall st,
      ceval st CSkip st
  | CEAss  : forall st a1 n l,
      aeval st a1 = n ->
      (CAss l a1) / st ~~> (override st l n)
  | CESeq : forall c1 c2 st st' st'',
      c1 / st  ~~> st' ->
      c2 / st' ~~> st'' ->
      (CSeq c1 c2) / st ~~> st''
  | CEIfTrue : forall st st' b1 c1 c2,
      beval st b1 = true ->
      c1 / st ~~> st' ->
      (CIf b1 c1 c2) / st ~~> st'
  | CEIfFalse : forall st st' b1 c1 c2,
      beval st b1 = false ->
      c2 / st ~~> st' ->
      (CIf b1 c1 c2) / st ~~> st'
  | CEWhileEnd : forall b1 st c1,
      beval st b1 = false ->
      (CWhile b1 c1) / st ~~> st
  | CEWhileLoop : forall st st' st'' b1 c1,
      beval st b1 = true ->
      c1 / st ~~> st' ->
      (CWhile b1 c1) / st' ~~> st'' ->
      (CWhile b1 c1) / st ~~> st''

  where "c1 '/' st '~~>' st'" := (ceval st c1 st').


(** **** Exercise: 3 stars (aeval_beval_rel) *)
(** Write relations [aeval_rel] and [beval_rel] in the same style
    as [ceval], and prove that they are equivalent to [aeval] and
    [beval]. *)

(* FILL IN HERE *)
(** [] *)

Tactic Notation "ceval_cases" tactic(first) tactic(c) := first; [
    c "CESkip" | c "CEAss" | c "CESeq" | c "CEIfTrue" | c "CEIfFalse" 
  | c "CEWhileEnd" | c "CEWhileLoop" ].

Example ceval_example1:
    (X ::= A2; IFB !X <<= A1 THEN Y ::= A3 ELSE Z ::= A4) / empty_state ~~>
    (override (override empty_state X 2) Z 4).
Proof.
  (* We need to supply the intermediate state *)
  apply CESeq with (override empty_state X 2). 
    Case "assignment command".
    apply CEAss. reflexivity.
  Case "if command".
    apply CEIfFalse.
      reflexivity.
      apply CEAss. reflexivity.  Qed.

(** And here's the similar output of ceval_step *)
(*
Eval compute in  
  (ceval_step empty_state 
              (X ::= A2; 
               IFB !X <<= A1 THEN Y ::= A3 ELSE Z ::= A4)
              500). 

Eval compute in 
  (match ceval_step empty_state 
              (X ::= A2; 
               IFB !X <<= A1 THEN Y ::= A3 ELSE Z ::= A4)
              500
   with
   | None    => (None,None) (* shouldn't happen, if 500 is big enough *)
   | Some st => (st X, st Z)
   end).  
*)

(** **** Exercise: 2 stars *)
Example ceval_example2:
    (X ::= A0; Y ::= A1; Z ::= A2) / empty_state ~~>
    (override (override (override empty_state X 0) Y 1) Z 2).
Proof. 
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ####################################################### *)
(** * Equivalence of step-indexed and relational evaluation *)

Theorem ceval_step__ceval: forall c st st',
      (exists i, ceval_step st c i = Some st')
   -> c / st ~~> st'.
Proof. 
  intros c st st' H.
  inversion H as [i E].
  clear H.
  generalize dependent st'.
  generalize dependent st.
  generalize dependent c.
  induction i as [| i' ].
  Case "i = 0 -- contradictory".
    intros c st st' H. inversion H.
  Case "i = S i'".
    intros c st st' H.
    (com_cases (destruct c) SCase); simpl in H; inversion H; subst; clear H. 
      SCase "CSkip". apply CESkip.
      SCase "CAss". apply CEAss. reflexivity.

      SCase "CSeq".
        remember (ceval_step st c1 i') as r1. destruct r1.
        SSCase "Evaluation of r1 terminates normally".
          apply CESeq with s. 
            apply IHi'. rewrite Heqr1. reflexivity.
            apply IHi'. simpl in H1. apply H1.
        SSCase "Evaluation of r1 terminates abnormally -- contradiction".
          inversion H1.

      SCase "CIf". 
        remember (beval st b) as r. destruct r.
        SSCase "r = true".
          apply CEIfTrue. rewrite Heqr. reflexivity.
          apply IHi'. apply H1.
        SSCase "r = false".
          apply CEIfFalse. rewrite Heqr. reflexivity.
          apply IHi'. apply H1.

      SCase "CWhile". remember (beval st b) as r. destruct r.
        SSCase "r = true". 
          remember (ceval_step st c i') as r1. destruct r1. 
          SSSCase "r1 = Some s".
            apply CEWhileLoop with s. rewrite Heqr. reflexivity.
            apply IHi'. rewrite Heqr1. reflexivity. 
            apply IHi'. simpl in H1. apply H1.
          SSSCase "r1 = None".
            inversion H1.
        SSCase "r = false".
          inversion H1. 
          apply CEWhileEnd. 
          rewrite Heqr. subst. reflexivity.  Qed.

(** **** Exercise: 4 stars (ceval_step__ceval_inf) *)
(** Write an informal proof of [ceval_step__ceval], following the
    template at the top of the file.  (The template for case
    analysis on an inductively defined value should look the same
    as for induction, except that there are no induction
    hypothesis.)  Make your proof communicate the main ideas to a
    human reader; do *not* simply transcribe the steps of the
    formal proof.

(* FILL IN HERE *)
[]
*)

Theorem ceval_step_more: forall i1 i2 st st' c,
  i1 <= i2 -> ceval_step st c i1 = Some st' -> 
  ceval_step st c i2 = Some st'.
Proof. 
induction i1 as [|i1']; intros i2 st st' c Hle Hceval.
  Case "i1 = 0".
    inversion Hceval.
  Case "i1 = S i1'".
    destruct i2 as [|i2']. inversion Hle. 
    assert (Hle': i1' <= i2') by omega.
    com_cases (destruct c) SCase.
    SCase "CSkip".
      simpl in Hceval. inversion Hceval. 
      reflexivity.
    SCase "CAss".
      simpl in Hceval. inversion Hceval.
      reflexivity.
    SCase "CSeq".
      simpl in Hceval. simpl. 
      remember (ceval_step st c1 i1') as st1'o.
      destruct st1'o.
      SSCase "st1'o = Some".
        apply sym_eq in Heqst1'o.
        apply (IHi1' i2') in Heqst1'o; try assumption.
        rewrite Heqst1'o. simpl. simpl in Hceval.
        apply (IHi1' i2') in Hceval; try assumption.
      SSCase "st1'o = None".
        inversion Hceval.

    SCase "CIf".
      simpl in Hceval. simpl.
      remember (beval st b) as bval.
      destruct bval; apply (IHi1' i2') in Hceval; assumption.
    
    SCase "CWhile".
    simpl in Hceval. simpl.
      destruct (beval st b); try assumption. 
      remember (ceval_step st c i1') as st1'o.
      destruct st1'o.
      SSCase "st1'o = Some".
        apply sym_eq in Heqst1'o.
        apply (IHi1' i2') in Heqst1'o; try assumption. 
        rewrite -> Heqst1'o. simpl. simpl in Hceval. 
        apply (IHi1' i2') in Hceval; try assumption.
      SSCase "i1'o = None".
        simpl in Hceval. inversion Hceval.  Qed.

(** **** Exercise: 4 stars *)
(** Finish the following proof.  You'll need [ceval_step_more] in
    a few places, as well as some basic facts about [<=] and
    [plus]. *)

Theorem ceval__ceval_step: forall c st st',
      c / st ~~> st'
   -> exists i, ceval_step st c i = Some st'.
Proof. 
  intros c st st' Hce.
  ceval_cases (induction Hce) Case.
  (* FILL IN HERE *) Admitted.
(** [] *)

Theorem ceval_and_ceval_step_coincide: forall c st st',
      c / st ~~> st'
  <-> exists i, ceval_step st c i = Some st'.
Proof.
  intros c st st'.
  split. apply ceval__ceval_step. apply ceval_step__ceval.
Qed.

(* ####################################################### *)
(** * Reasoning about programs *)

Theorem plus2_spec : forall st n st',
  st X = n ->
  plus2 / st ~~> st' ->
  st' X = plus n 2.
Proof.
  intros st n st' HX Heval.
  (* inverting Heval essentially forces coq to expand one step of the ceval
     computation - in this case revealing that st' must be st extended with
     the new value of X, since plus2 is an assignment *) 
  inversion Heval. subst.
  apply override_eq.  Qed.

(** **** Exercise: 3 stars (XtimesYinZ_spec) *)
(** State and prove a specification of the XtimesYinZ Imp program *)
(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 3 stars *)
Theorem loop_never_stops : forall st st',
  ~(loop / st ~~> st').
Proof.
  intros st st' contra. unfold loop in contra.
  remember (WHILE BTrue DO SKIP LOOP) as loopdef.
  (* Proceed by induction on the assumed derivation showing that
     loopdef terminates.  Most of the cases are immediately
     contradictory (and so can be solved in one step with
     [inversion]). *)
  (* FILL IN HERE *) Admitted.
(** [] *)

Fixpoint no_whiles (c : com) {struct c} : bool :=
  match c with
  | CSkip       => true
  | CAss _ _    => true
  | CSeq c1 c2  => andb (no_whiles c1) (no_whiles c2)
  | CIf _ ct cf => andb (no_whiles ct) (no_whiles cf)
  | CWhile _ _  => false
  end.

(** **** Exercise: 2 stars *)
(** The [no_whiles] predicate yields [true] on just those
  programs that have no while loops.  Using [Inductive], 
  write a predicate [no_Whiles] that returns [True] instead
  of [true]. Then prove its equivalence with 
  [no_whiles].  Hint: If some case of an inductive definitions is always
  False, you can simply leave it out.  *)

Inductive no_Whiles: com -> Prop := 
 (* FILL IN HERE *) 
  .

Theorem no_whiles_eqv:
   forall c, no_whiles c = true <-> no_Whiles c.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)


(** **** Exercise: 4 stars *)
(** On the other hand, Imp programs that don't involve while
    loops always terminate.  State and prove a theorem that says
    this.  Use either [no_whiles] or [no_Whiles], as you prefer. *)
(* FILL IN HERE *)
(** [] *)