Require Export Logic.

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

(* Q: What is the relation between a formal proof of a
      proposition P and an informal proof of the same proposition P?

   A: The latter should *teach* the reader how to produce the
      former.

   Q: How much detail is needed?

   A: There is no single right answer; rather, there is a range
      of choices.  

      At one end of the spectrum, we can essentially give the
      reader the whole formal proof (i.e., the informal proof
      amounts to just transcribing the formal one into words).
      This gives the reader the *ability* to reproduce the formal
      one for themselves, but it doesn't *teach* them anything.

      At the other end of the spectrum, we can say "The theorem
      is true and you can figure out why for yourself if you
      think about it hard enough."  This is also not a good
      teaching strategy, because usually writing the proof
      requires some deep insights into the thing we're proving,
      and most readers will give up before they rediscover all
      the same insights as we did.

      In the middle is the golden mean -- a proof that includes
      all of the essential insights (saving the reader the hard
      part of work that we went through to find the proof in the
      first place) and clear high-level suggestions for the more
      routine parts to save the reader from spending too much
      time reconstructing these parts (e.g., what the IH says and
      what must be shown in each case of an inductive proof), but
      not so much detail that the main ideas are obscured.

                           -----------------

   Another key point: if we're talking about a formal proof of a
   proposition P and an informal proof of P, the proposition P
   doesn't change.  That is, formal and informal proofs are
   TALKING ABOUT THE SAME WORLD and they must PLAY BY THE SAME
   RULES.

   In particular, whether we are talking about formal or informal
   proofs, propositions and booleans are different things!

      * Booleans are VALUES in the COMPUTATIONAL world.  Every
        expression of type bool (with no free variables) can be
        simplified to either true or false.

      * Propositions are TYPES in the LOGICAL world.  They are
        either PROVABLE (i.e., there is some expression that has
        this type) or not (there is no such expression).  It
        doesn't make sense to say that a proposition is
        "equivalent to true," and it is not necessarily the
        case that, if a proposition P is not provable, then
        ~P is provable.

        We do sometimes use the words "true" and "false" when
        referring to propositions.  Strictly speaking, we should
        not: a proposition is either provable or it is not.
*)

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

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

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

Module AExp.

Inductive aexp : Set :=
  | 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 : Set :=
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLtEq : 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)
  | BLtEq 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" := (BLtEq b1 b2) (at level 60).

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

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.

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

(* 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 as data -- higher-order tactics, if you will. *)

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

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

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

(* 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 is when e1 = ANum n *)
    SCase "e1 = ANum n". destruct n.
      SSCase "n = 0". 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 (ANum 0) 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.

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

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

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

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

(* Since the optimize_0plus tranformation doesn't change the
   value of aexps, we should be able to apply it to all the aexps
   that appear in a bexp without changing the bexp's value.
   Write a function which performs that transformation on bexps,
   and prove it is sound.  Use the tacticals we've just seen to
   make the proof as elegant as possible. *)
(* FILL IN HERE *)

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

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

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

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

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

(* 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. *)
Definition id := nat.

(* Now, a mapping is a partial function from identifiers to
   members of some other type, X.  We use an option in the
   result type to represent partiality: A result of None means
   that the mapping is not defined for the given id. *)
Definition mapping (X : Set) := id -> option X.

Definition lookup (X : Set) (k : id) (f : mapping X)
                  : option X :=
  f k.

Implicit Arguments lookup [X].

Definition empty_mapping (X:Set) : (mapping X) := constfun None.

(* Extend takes a function (from ids to option nats) and
   builds a function that behaves exactly the same as the one it
   was given except on the particular input k, for which it
   returns Some x. *)
Definition extend (X : Set) (f : mapping X) (k:id) (x:X) :=
  override f k (Some x).

Implicit Arguments extend [X].

Definition remove (X : Set) (f : mapping X) (k:id) :=
  override f k None.

Implicit Arguments remove [X].

(* Since the critical functions on mappings, extend and
   remove, are implemented in terms of the override operator
   that we studied before, their properties can also be derived
   from those of override. *)

Theorem extend_eq : forall X x x' k (f : mapping X),
  x = x' ->
  lookup k (extend f k x) = Some x'.
Proof.
  intros X x x' k f Heq. rewrite Heq.
  unfold lookup, extend.
  apply override_eq. Qed.

Theorem extend_neq : forall X o1 x2 k1 k2 (f : mapping X),
  lookup k1 f = o1 ->
  beq_nat k2 k1 = false ->
  lookup k1 (extend f k2 x2) = o1.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem extend_example : forall (X:Set) (b:bool),
  lookup 3 (extend (empty_mapping _) 2 b) = None.
Proof.
  (* Before starting to play with tactics, make sure you 
     understand exactly what the theorem is saying! *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem extend_shadow : forall X x1 x2 k1 k2 (f : mapping X),
  lookup k1 (extend (extend f k2 x1) k2 x2) = lookup k1 (extend f k2 x2).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem extend_same : forall X x1 k1 k2 (f : mapping X),
  lookup k1 f = Some x1 ->
  lookup k2 (extend f k1 x1) = lookup k2 f.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem extend_permute : forall X x1 x2 k1 k2 k3 (f : mapping X),
     false = beq_nat k2 k1
  -> lookup k3 (extend (extend f k2 x1) k1 x2)
     = lookup k3 (extend (extend f k1 x2) k2 x1).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

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

Definition state := (mapping nat).

Definition empty_state := empty_mapping nat.

(* Adding variables to what we had before *)
Inductive aexp : Set :=
  | 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 := 0.
Definition Y : id := 1.
Definition Z : id := 2.

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

(* Same bexps as before (using the new aexps) *)
Inductive bexp : Set :=
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLtEq : 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" := (BLtEq b1 b2)
  (at level 60).

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

Inductive com : Set :=
  | 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" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'testif' e1 'then' e2 'else' e3" :=
  (CIf e1 e2 e3) (at level 80, right associativity).

(* Note that CIf is written testif...then...else... to avoid
   confusion with Coq's existing if...then...else... syntactic
   sugar. *)

(* ------------------------------------------------------- *)
(* 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 0 (APlus (AId 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_X_slowly : com :=
  while BNot (!X === A0) do
    subtract_slowly_body.

Definition subtract_3_from_5_slowly : com :=
  X ::= A3;
  Z ::= A5;
  while BNot (!X === A0) do
    subtract_slowly_body.

(* an infinite loop *)
Definition loop : com :=
  while BTrue do
    skip.

(* factorial *)
Definition fact_body : com :=
  Z ::= !Z *** !X;
  X ::= !X --- A1.

Definition pfactorial : com :=
  while BLtEq A1 (!X) do
    fact_body.
(* Note that pfactorial should be run in a state where Z is 1 

   We could enforce this with the following program:
*)
Definition pfactorial' : com :=
  Z ::= ANum 1;
  pfactorial.

(* exponentiation *)
Definition exp_body : com :=
    Z ::= !Z *** !X;
    Y ::= !Y --- A1.

Definition pexp : com :=
  while BNot (!Y === (ANum 0)) do
    exp_body.
(* Note that pexp should be run in a state where Z is 1 *)

(* Write a While program that sums the numbers from 1 to X
   (inclusive: 1 + 2 + ... + X) in the variable Y.  *)
(* FILL IN HERE *)

(* Write a While program that sets Z to 0 if X is even and sets Z
   to 1 otherwise. *)
(* FILL IN HERE *)

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

Fixpoint aeval (st : state) (e : aexp) {struct e} : nat :=
  match e with
  | ANum n => n
  | AId l => match lookup l st with
               | Some n => n
               | None => O
             end
  | 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.

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)
  | BLtEq 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 =>
        extend 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 =>
          extend 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 : Set) (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 (extend 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.

(* 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 ->
      ceval st (CAss l a1) (extend st l n)
  | CESeq : forall c1 c2 st st' st'',
      ceval st c1 st' ->
      ceval st' c2 st'' ->
      ceval st (CSeq c1 c2) st''
  | CEIfTrue : forall st st' b1 c1 c2,
      beval st b1 = true ->
      ceval st c1 st' ->
      ceval st (CIf b1 c1 c2) st'
  | CEIfFalse : forall st st' b1 c1 c2,
      beval st b1 = false ->
      ceval st c2 st' ->
      ceval st (CIf b1 c1 c2) st'
  | CEWhileEnd : forall b1 st c1,
      beval st b1 = false ->
      ceval st (CWhile b1 c1) st
  | CEWhileLoop : forall st st' st'' b1 c1,
      beval st b1 = true ->
      ceval st c1 st' ->
      ceval st' (CWhile b1 c1) st'' ->
      ceval st (CWhile b1 c1) st''.

(* 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:
  ceval
    empty_state
    (X ::= A2; testif !X <<= A1 then Y ::= A3 else Z ::= A4)
    (extend (extend empty_state X 2) Z 4).
Proof.
  apply CESeq with (extend 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; 
               testif !X <<= A1 then Y ::= A3 else Z ::= A4)
              500). *)
(* Eval compute in 
  (match ceval_step empty_state 
              (X ::= A2; 
               testif !X <<= A1 then Y ::= A3 else Z ::= A4)
              500
   with
   | None    => (None,None) (* shouldn't happen, if 500 is big enough *)
   | Some st => (lookup X st, lookup Z st)
   end). *)

Example ceval_example2:
  ceval
    empty_state
    (X ::= A0; Y ::= A1; Z ::= A2)
    (extend (extend (extend empty_state X 0) Y 1) Z 2).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

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

Theorem ceval_step__ceval: forall c st st',
      (exists i, ceval_step st c i = Some st')
   -> ceval st c 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.

(* 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.
    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. apply le_S_n in Hle.
      remember (ceval_step st c1 i1') as i1'o.
      destruct i1'o.
      SSCase "i1'o = Some".
        apply sym_eq in Heqi1'o.
        apply (IHi1' i2') in Heqi1'o; try assumption.
        rewrite Heqi1'o. simpl. simpl in Hceval.
        apply (IHi1' i2') in Hceval; try assumption.
      SSCase "i1'o = None".
        inversion Hceval.

    SCase "CIf".
      simpl in Hceval. simpl. apply le_S_n in Hle.
      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.
      apply le_S_n in Hle.
      remember (ceval_step st c i1') as i1'o.
      destruct i1'o.
      SSCase "i1'o = Some".
        apply sym_eq in Heqi1'o.
        apply (IHi1' i2') in Heqi1'o; try assumption.
        rewrite -> Heqi1'o. simpl. simpl in Hceval.
        apply (IHi1' i2') in Hceval; try assumption.
      SSCase "i1'o = None".
        simpl in Hceval. inversion Hceval. Qed.

(* 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',
      ceval st c st'
   -> exists i, ceval_step st c i = Some st'.
Proof.
  intros c st st' Hce.
  ceval_cases (induction Hce) Case.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem ceval_and_ceval_step_coincide: forall c st st',
      ceval st c 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.

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

Theorem plus2_spec : forall st n st',
  lookup X st = Some n ->
  ceval st plus2 st' ->
  lookup X st' = Some (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 extend_eq. simpl. rewrite -> HX.
  reflexivity. Qed.

(* State and prove a specification of the XtimesYinZ while
   program *)
(* FILL IN HERE *)

Theorem loop_never_stops : forall st st',
  ~(ceval st loop st').
Proof.
  intros st st' contra. unfold loop in contra.
  remember (while BTrue do skip) 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 (and delete "Admitted") *) 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.

(* On the other hand, programs that don't involve while loops
   always terminate.  State and prove a theorem that says this. *)
(* FILL IN HERE *)