(** * Simple imperative programs
      Version of 2/24/2009 

   NOTE: This is a preliminary version of While.v.  Do not submit it.
   The material and exercises may change.  A full, revised version
   will be released on Wednesday.

   You'll need to compile the previous files in order to use this one.
*)

Require Export Logicsol.

(* ------------------------------------------------------- *)
(** * Informal proofs, again *)

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

   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 : 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 40).
Notation "a1 '---' a2" := (AMinus a1 a2) (at level 40).
Notation "a1 '***' a2" := (AMult a1 a2) (at level 50).

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

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

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

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

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

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

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


(* Exercise: 4 stars *)
(* 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]
*)

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

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.

(* Exercise: 3 stars (extend_eq_variant) *)
(* The way [extend_eq] is stated may be a bit surprising:
   wouldn't it be simpler just to say [lookup k (extend f k x) =
   Some x]?  Try changing the statement of the theorem to read
   like this; then work through some of the rest of the file and
   see how the proofs that use [extend_eq] need to be changed to
   use the simplified version.

   Briefly explain what changes are needed to use the variant and
   which version of the theorem you prefer.

   (This exercise is best done AFTER the rest of this week's
   homework.)

FILL IN HERE

*)

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

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

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

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

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


(* --------------------------------------------------- *)
(** ** WHILE program syntax *)

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

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