Require Export Logic.

(* Program analysis is often concerned with proving or disproving
   properties of programs.  To make sense of what this might mean, we
   have to study the *semantics* of programs, i.e., what programs
   *mean*. *)

(* There are several different kinds of semantics---in the first
   lecture, we mentioned

   Axiomatic semantics - the meaning of a program is what you can
   prove about it

   Denotational semantics - the meaning of a program is a mathematical
   object

   Operational semantics - the meaning of a program is the value you
   get when you execute the program

   Of these, operational semantics seems to be the most popular
   lately, because many of the proofs seem simpler.  So we'll be
   focusing on operational semantics. *)

(* To begin, we'll start simple:  We'll consider the meaning of
   arithmetic expressions.  Using standard notation, we'll define the
   *syntax* of  arithmetic expression as given by the following grammar:

   e ::= n | e + e | e - e | e * e

   where n is a nonterminal representing an arbitrary natural number
   and +, -, and * have the obvious meanings.

   Notice that e is essentially a recursive data type.  Thus, we can
   make an inductive definition for arithmetic expressions in Coq. *)

Module AExp_Simple.

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

(* 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).
Notation A6 := (ANum 6).
Notation A7 := (ANum 7).
Notation A8 := (ANum 8).
Notation A9 := (ANum 9).

Definition two_plus_two := A2 +++ A2.

(* For arithmetic expressions, we're going to define their meaning as
   the natural number they evaluate to.  One choice to do this would
   be with a recursive function. *)

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.

(* Having this definition in Coq already lets us do some neat stuff.
   For example, we could some simple testing. *)

(* CMSC 631 *)
Example test_aeval1:
  aeval two_plus_two = 4.
Proof.
  Admitted.

(* Or we can actually prove some theorems. *)

Theorem mult_plus_distrib : forall m n p : aexp ,
  aeval ((m +++ n) *** p) = aeval ((m *** p) +++ (n *** p)).
Proof.
  intros m n p.
  simpl.
  apply mult_plus_distr_r. (* Use theorem on nats *)
Qed.

(* Here's a more interesting example.  Let's write a program
   transformation that "optimizes" arithmetic expressions. *)

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.

(* Now we can prove that this transformation preserves the meaning of *)
(* an expression *)

Theorem optimize_0plus_sound: forall e,
  aeval (optimize_0plus e) = aeval e.
Proof.
  intros e. induction e; simpl.
  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.
*)

(* Consider the following definition of boolean expressions *)

Inductive bexp : Set := 
  | BTrue : bexp
  | BFalse : bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp
  | BOr : bexp -> bexp -> bexp.

(* CMSC 631 *)
(* Fill in the definition of beval below to correctly evaluate bexps
   and uncomment the Examples below to double-check your answer. *)
Fixpoint beval (e : bexp) {struct e} : bool :=
  true.

(*
Example test_beval0 : beval BTrue = true.
Proof. reflexivity. Qed.
Example test_beval1 : beval (BAnd BTrue BFalse) = false.
Proof. reflexivity.  Qed.
Example test_beval2 : beval (BOr (BNot BTrue) (BAnd BTrue BTrue)) = true.
Proof. reflexivity.  Qed.
*)

(* Here is a fancier optimization function *)
Fixpoint optimize_bexp (e:bexp) {struct e} : bexp :=
  match e with
  | BTrue => BTrue
  | BFalse => BFalse
  | BNot e =>
    let e' := optimize_bexp e in
      match e with
      | BTrue => BFalse
      | BFalse => BTrue
      | x => BNot x
      end
  | BAnd e1 e2 =>
    let e1' := optimize_bexp e1 in
    let e2' := optimize_bexp e2 in
      match e1', e2' with
      | BTrue, x => x
      | x, BTrue => x
      | x, y => BAnd x y
      end
  | BOr e1 e2 =>
    let e1' := optimize_bexp e1 in
    let e2' := optimize_bexp e2 in
      match e1', e2' with
      | BFalse, x => x
      | x, BFalse => x
      | x, y => BAnd x y
      end
  end.

(* CMSC 631 *)
(* Prove that optimize_bexp preserves the semantics of a boolean *)
(* expresion.  Or, if it does not, fix optimize_bexp so it does and *)
(* complete the proof.  Use the tacticals we discussed above to keep *)
(* your proof as short as possible. *)
(* WARNING:  The proof may be long and tedious, so you may
   want to use some tacticals. *)
Theorem optimize_bexp_sound : forall e:bexp ,
  beval (optimize_bexp e) = beval e.
Proof.
  Admitted.

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

(* What we've done above works fine for these examples, but it has
  some disadvantages in general.  The key issue is that if we define
  our semantics in terms of a Fixpoint, then the Fixpoint has to be a
  function we can evaluate.  But many times it's useful to have
  semantics that aren't so obvious---for example, it may be natural to
  specify a non-deterministic semantics for a language.  This is often
  done when reasoning about multi-threaded programs, since they may
  have many different behaviors depending on the scheduler. *)

(* So instead of definition evaluation with a (total) FUNCTION, let's
   define it as a RELATION. *)

(* Following standard notation, we will use *natural deduction* style
   rules to define a relation that says which expressions reduce to
   what values.  Natural deduction rules have the form

   H1 H2 ... Hn
  ----------------
   C1 ... Cm

   where the Hi are the *hypotheses* and the Cj are the
   *conclusions*.  The rule is read as, "if H1...Hn hold, then we can
   conclude that C1...Cm hold."  This style of rule was originally
   developed by Gentzen for reasoning about more traditional logic.
   For example, we can write *modus ponens* in this style as

   A   A->B
  -------------
   B

   i.e., if we know A and A implies B, then we can conclude B.

   Our operational semantic definitions will be similar.  This
   discussion will be in terms of our previous definition of
   expressions,

   e ::= n | e + e | e - e | e * e

   Here is the first rule:

   --------------
    n --> n

   It says that any number evaluates to itself.  Notice that even
   though we've written ``n'' on both sides of the arrow, in fact
   these are two different n's:  The one on the left is a *syntactic*
   natural number, and the one on the right is a *mathematical*
   number.  On paper, we'll usually know which is which by looking
   at the context.  In Coq, we'll actually be able to see the
   difference more precisely.

   The next rule tells us how to evaluate sums:

   e1 --> n1
   e2 --> n2
  ----------------------
   e1 +++ e2 --> n1+n2

   It says that if each ei evaluates to ni, then their sum evaluates
   to n1+n2.  Here we can more clearly see the difference between the
   left- and right-hand sides of the -->, since on the left we use the
   syntactic +++ and on the right we use the mathematical +.

   We can define rules for --- and *** similarly.  Put together,
   we're defined a *relation* that we write

   e --> n

   which is reading ``evaluating arithmetic expression e produces the
   value n.''
*)

 (* To formalize this semantics in Coq, we just need to look at what
    goes into each rule, and write down an inductive axiomatization
    of the whole logic.  In this case, the --> relates an arithmetic
    expression and a number.  Hence our inductive definition will
    accept an aexp (the left of the -->) and a nat (the right side). *)

Inductive aeval' : aexp -> nat -> Prop :=
  | AENum : forall n,
    aeval' (ANum n) n
  | AEPlus : forall a1 a2 n1 n2,
    aeval' a1 n1 ->
    aeval' a2 n2 ->
    aeval' (a1 +++ a2) (plus n1 n2)
  | AEMinus : forall a1 a2 n1 n2,
    aeval' a1 n1 ->
    aeval' a2 n2 ->
    aeval' (a1 --- a2) (minus n1 n2)
  | AEMult : forall a1 a2 n1 n2,
    aeval' a1 n1 ->
    aeval' a2 n2 ->
    aeval' (a1 *** a2) (mult n1 n2).

Definition foo := aeval' (A2 +++ (A5 --- A4)) 3.

Definition bar : aeval' (A5 --- A4) 1 :=
   AEMinus (ANum 5) (ANum 4) 5 4 (AENum 5) (AENum 4).

Definition qux : foo :=
   AEPlus (ANum 2) (A5 --- A4) 2 1 (AENum 2) bar.

Eval compute in qux.

Example quux : aeval' (A2 +++ (A5 --- A4)) 3.
Proof.
  assert (plus 2 1 = 3).
  reflexivity.
  rewrite <- H.
  apply AEPlus.
  apply AENum.
  assert (minus 5 4 = 1).
  reflexivity.
  rewrite <- H0.
  apply AEMinus.
  apply AENum.
  apply AENum.
Qed.

Print quux.

(* Stare at the definition above, and make sure you understand how
   it's related to the natural deduction style rules (which are far
   more common in the literature).

   Now if we want to work with the above definition, on paper we can
   put together the logical rules to form proof trees.  For example,
   [draw proof tree for (2+3)+4 --> 9].  These trees are completely
   equivalent to ``evidence'' in Coq that a relationship satisfies the
   aeval' definition above.  For example, *)

Definition Two_Plus_Three_Is_Five : aeval' (A2 +++ A3) 5 :=
  AEPlus A2 A3 2 3 (AENum 2) (AENum 3).

Definition Two_Plus_Three_Plus_Four_Is_Nine :
  aeval' ((A2 +++ A3) +++ A4) 9 :=
  AEPlus (A2 +++ A3) A4 5 4 Two_Plus_Three_Is_Five (AENum 4).

(* Be sure you understand how this definition relates to the picture
   we drew above. *)

(* Or, with tactics *)
Example Two_Plus_Three_Plus_Four_Is_Nine' :
  aeval' ((ANum 2 +++ ANum 3) +++ ANum 4) 9.
Proof.
  assert (plus 5 4 = 9).
  reflexivity.
  rewrite <- H.
  apply AEPlus.
  clear H.  (* New tactic:  forget a hypothesis *)
  assert (plus 2 3 = 5).
  reflexivity.
  rewrite <- H.
  apply AEPlus.
  clear H.
  apply AENum.
  apply AENum.
  apply AENum.
Qed.

Print Two_Plus_Three_Plus_Four_Is_Nine'.

(* CMSC 631 *)
(* Here's one for you to try.  Write a proof of the following
   directly as a term, rather than using tactics. *)
(*
Definition quuux : aeval' (A9 --- (A4 *** A2)) 1 := (* FILL IN *).
*)

(* Notice we did not get exactly the same term---when we're working
   ``on paper,'' we typically only explicitly use the logic of our
   system, and gloss over standard other things like equality.  In the
   Coq term, some of that other reasoning shows up. *)

(* Next, let's go further and prove that these two definitions of
   evaluation are equivalent. *)

(* CMSC 631 *)
(* Prove the following lemma. *)
Lemma aeval__aeval' : forall (a:aexp) (n:nat),
  aeval a = n -> aeval' a n.
Proof.
  Admitted.

(* CMSC 631 *)
(* Prove the following lemma. *)
Lemma aeval'__aeval : forall (a:aexp) (n:nat),
  aeval' a n -> aeval a = n.
Proof.
  Admitted.

(* CMSC 631 *)
Theorem aeval_aeval' : forall (a:aexp) (n:nat),
  aeval' a n <-> aeval a = n.
Proof.
  Admitted.

End AExp_Simple.

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

(*
Next, let's start adding features to our language of arithmetic
expressions, and explore their semantics.  The first thing we should
probably add is variables, since most programming languages have
those.
*)

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

Module AExp_Id.

(* The first step is to extend our source language to include
   identifiers.  On paper, we usually write "x" as a nonterminal ranging
   over variable names (similarly to using "n" as a nonterminal for
   natural numbers):

   e ::= n | x | e + e | e - e | e * e

   Now we can write expressions like "2+(3+x)".  If we want to use
   more than one variable, we can either subscript them or use other
   letters, e.g., "x_1+x_2" or "x*y".  The choice of which to use
   is mostly a matter of taste, though it's often a good idea to
   tell your readers if you're going to use more letters than just
   x to stand for variable names.

   In Coq, we could match this approach by using, say, strings or
   (as in a real compiler) some kind of fancier structure like
   symbols from a symbol table.  But to keep things simple, let's
   just use natural numbers as identifiers.  If this seems strange,
   just think of it as writing down a subscript on "x" to distinguish
   different variables.
*)

Definition id := nat.

(* Now we can extend expressions to include variables. *)

Inductive aexp : Set := 
  | ANum : nat -> aexp
  | AId : id -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

(* 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 shorthands for variables: *)
Definition VX : id := 0.
Definition VY : id := 1.
Definition VZ : id := 2.

(* Next, we want to define the semantics of this new kind of aexp.
   But since expressions now contain identifiers, we can only evaluate
   them if we know what the identifiers represent.  In other words,
   evaluation should now be parameterized by a [state] that
   associates a meaning, in this case a natural number, with each
   expression.  We're calling it a [state] because shortly
   we'll introduce an assignment operation that allows identifiers
   to change during evaluation.  For now, though, the state
   will be fixed during evaluation.  *)

Definition state := id -> nat.

(* Actually, the definition above is a bit odd.  In most programming
   languages, identifiers are ``scoped,'' which has two important
   consequences: First, identifiers can have different meanings in
   different contexts (e.g., x could be an ``int'' in one scope and a
   ``float'' in another); and second, identifiers might not be in
   scope, and so referring to them would be an error.

   Since [state] is a *total function*, we're not going to be able
   to distinguish between identifiers that are in and out of scope.
   So for now, all identifiers will always be in scope.
*)

(* Next, we'll define a couple of useful functions for building
   up [state]s.  These are going to seem a little excessive at first,
   but it will become clear later why we're designing [state]s in
   this way.

   We're going to give two ways of creating states:  We'll have
   an empty_state that just maps all identifiers to 0, and then
   we'll define a function [override] that ``adds'' (really,
   replaces) a mapping in a state.
*)

Definition empty_state := fun (k:nat) => 0.

Definition override (X : Set) (f : nat->X) (k:nat) (x:X) :=
  fun k' => if beq_nat k k' then x else f k'.

Implicit Arguments override [X].

(* For example, here is a state that maps X to 1 and Y to 2. *)

Definition G0 : state := override (override empty_state VX 1) VY 2.

(* Here are a couple of handy theorems about override *)

Theorem override_eq : forall (X:Set) x k (f : nat->X),
  (override f k x) k = x.
Proof.
  intros X x k f.
  unfold override.
  rewrite <- beq_nat_refl.
  reflexivity.
Qed.

(* Exercise: 2 stars *)
(* CMSC 631 *)
Theorem override_neq : forall (X:Set) x1 x2 k1 k2 (f : nat->X),
  f k1 = x1 ->
  beq_nat k2 k1 = false ->
  (override f k2 x2) k1 = x1.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Essentially what we've done is given another inductive definition
   of states.  On paper, letter s be a non-terminal ranging over
   states, we'd write them as

   s ::= 0 | x:n; s

   i.e., a state is either the empty state, which maps every
   identifier to 0 or it's a state ``x:n,s'' which is defined as a
   state that's just like s, except x maps to n.  (More traditionally,
   the state 0 would be a partial function with an empty domain,
   i.e., it maps no variables to anything.)
*)

(* Now, we can finally define evaluation.  Before, we defined a relation

   e --> n

   This time, we need to evaluate e given a particular state.  Thus,
   we should add s in to our relation:

   (s, e) --> n

   meaning, ``In state s, if we evaluate expression e, the result is
   the value n.''

   You can probably guess what the reduction rules will look like.
   The rule for natural numbers should ignore the state, since natural
   numbers are constant in any state:

   -------------
   (s, n) --> n

   You can read this as, ``In any state s, a natural number n evaluates
   to n.''  When evaluating a variable, we'll just apply the state
   mapping to the variable to get its value:

   ----------------
   (s, x) --> s(x)

   Finally, to evaluate a compound expression, we'll evaluate the
   pieces and put them together as usual:

   (s, e1) --> n1
   (s, e2) --> n2
  ----------------------
   (s, e1 +++ e2) --> n1+n2

   (And similarly for --- and ***.)

   Now let's write this down in Coq notation.
*)

Inductive aeval : state -> aexp -> nat -> Prop :=
  | AENum : forall st n,
    aeval st (ANum n) n
  | AEId : forall st x,
    aeval st (AId x) (st x)
  | AEPlus : forall st a1 a2 n1 n2,
    aeval st a1 n1 ->
    aeval st a2 n2 ->
    aeval st (a1 +++ a2) (plus n1 n2)
  | AEMinus : forall st a1 a2 n1 n2,
    aeval st a1 n1 ->
    aeval st a2 n2 ->
    aeval st (a1 --- a2) (minus n1 n2)
  | AEMult : forall st a1 a2 n1 n2,
    aeval st a1 n1 ->
    aeval st a2 n2 ->
    aeval st (a1 *** a2) (mult n1 n2).

(* CMSC 631 *)
(* Write a term that has the following type (without using
   tactics)
Definition two_plus_x_plus_y_is_6 :
  aeval G0 (AMult (APlus A2 (AId VX)) (AId VY)) 6 :=  (* FILL IN *)
*)

(* CMSC 631 *)
(* Translate the following informal reduction into an Example
   and prove it (either directly or using tactics).

   (x:2;y:3, x + y) --> 5

*)

(* CMSC 631 *)
Theorem eval_plus_var_comm : forall (st:state) (n m:nat),
  aeval st (APlus (AId VX) (ANum n)) m <->
  aeval st (APlus (ANum n) (AId VX)) m.
Proof.
  Admitted.

End AExp_Id. 

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

Module AExp_If_Let.

(* Next, we'll add two useful forms:  conditionals and scoping with
   ``let''.   Our new grammar will be:

   e ::= n | x | e + e | e - e | e * e
       | if0 e then e else e
       | let x = e in e

   This is a pure expression language, so the conditional if0 actually
   returns a result (similarly to the ``? :'' construct in C and Java).
   Given ``if0 e1 then e2 else e3,'' we'll return the value of e2 if
   e1 evaluates to 0, and e3 otherwise.

   Let binding introduces a new local scope.  ``let x = e1 in e2''
   evaluates e1, and then evaluates e2 with x bound to the value of e1.

   Here is the language definition.
*)

Definition id := nat.

Inductive aexp : Set := 
  | ANum : nat -> aexp
  | AId : id -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp
  | AIf0 : aexp -> aexp -> aexp -> aexp
  | ALet : id -> aexp -> aexp -> aexp.

Definition state := id -> nat.

Definition empty_state := fun (k:nat) => 0.

Definition override (X : Set) (f : nat->X) (k:nat) (x:X) :=
  fun k' => if beq_nat k k' then x else f k'.

Implicit Arguments override [X].

(* Now let's define the evalution rules.  This time, we'll go straight
   to the Coq definitions of the rules.  There are two interesting
   things to notice:  First, we separate out if0 into two separate
   cases, because there are two ways to show that if0 evaluates to
   something, depending on whether the guard evaluates to 0.  This
   is similar to the definition of [or] in Logic.v.  Second, in the
   case for let, x is bound to its new value only during the
   evaluation of e2. *)

Inductive aeval : state -> aexp -> nat -> Prop :=
  | AENum : forall st n,
    aeval st (ANum n) n
  | AEId : forall st x,
    aeval st (AId x) (st x)
  | AEPlus : forall st a1 a2 n1 n2,
    aeval st a1 n1 ->
    aeval st a2 n2 ->
    aeval st (APlus a1 a2) (plus n1 n2)
  | AEMinus : forall st a1 a2 n1 n2,
    aeval st a1 n1 ->
    aeval st a2 n2 ->
    aeval st (AMinus a1 a2) (minus n1 n2)
  | AEMult : forall st a1 a2 n1 n2,
    aeval st a1 n1 ->
    aeval st a2 n2 ->
    aeval st (AMult a1 a2) (mult n1 n2)
  | AEIf0_True : forall st a1 a2 a3 n2,
    aeval st a1 0 ->
    aeval st a2 n2 ->
    aeval st (AIf0 a1 a2 a3) n2
  | AEIf0_False : forall st a1 a2 a3 n1 n3,
    aeval st a1 n1 ->
    beq_nat n1 0 = false ->
    aeval st a3 n3 ->
    aeval st (AIf0 a1 a2 a3) n3
  | AELet : forall st x a1 a2 n1 n2,
    aeval st a1 n1 ->
    aeval (override st x n1) a2 n2 ->
    aeval st (ALet x a1 a2) n2.

(* Exercise:  Write out the evaluation rules for if0 and let
   in ``paper'' form.  You'll write down two separate rules
   for if0. *)

(* CMSC 631 *)
Example local_x : aeval empty_state (APlus (ALet 0 (ANum 3) (AId 0)) (AId 0)) 3.
Proof.
  Admitted.

(* CMSC 631 *)
Example if_example : aeval empty_state (AIf0 (APlus (ANum 3) (ANum 4)) (ANum 5) (ANum 6)) 6.
Proof.
  Admitted.

(* CMSC 631 *)
(* Translate the following informal reduction into an Example
   and prove it.

   (x:2, let y = 3 in x + y) --> 5
*)


(* Since our semantics is a relation rather than a function, we may be
   concerned about its properties.  For example, how do we know that
   aeval is deterministic?  Above, in the AExp_Simple module, we
   effectively proved this by showing the relation was equal to a
   function, but we haven't written down an evaluation function here.
   Instead, let's try to prove determinism directly.

   By now, you should really have a handle on proving this stuff
   by induction. *)
(* CMSC 631 *)
Theorem aeval_determinacy : forall st a n m,
  aeval st a n ->
  aeval st a m ->
  n = m.
Proof.
  Admitted.


(* Because our semantics treat all identifiers as being in scope at
   all times, we also can prove a slightly surprising property:
   That every term can be reduced to some value. *)
(* Optional *)
Theorem aeval_total : forall st a, exists n, aeval st a n.
Proof.
  Admitted.

End AExp_If_Let.

Module AExp_Big_Small.

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

(* The semantics we've constructed so far is a ``big-step'' semantics:
   One use of the relation

   (s, e) --> n

   tells us what (s,e) evaluates to.  Big-step semantics are quite
   natural, and (based on personal experience, though some would
   object) they're often easier to reason about.  However, they have
   one major drawback: They give no meaning to non-terminating
   computations.

   More concretely, suppose we added a ``while0 e1 e2'' form to the
   language.  (The exact semantics don't matter, but something like
   the following would work: ``while0 e1 e2'' evaluates e2 as long as
   e1 evaluates to 0.  The whole expression evaluates to the last
   thing e2 evaluated to or 0, if e1 was never 0.  This semantics is a
   bit silly because without side effects there's no point in
   reevaluating e2, but let's go with it.) Then there is no way to
   prove

   (s, while0 0 e) --> n

   for any s, e, and n:  Our inductive definition of --> gives a
   logic that lets us prove things with *finite* proof trees.  We
   would need to reason with *infinite* proof trees to show the
   above statement.  It turns out that's possible using a technique
   called coinduction, but that's a bit tricky, and is beyond the
   scope of this course.

*)

(* To address this issue, we can instead define a ``small-step'' semantics
   for our language.  Rather than evaluate a program all at once, in
   the small-step semantics it will take several steps to finally produce
   a value.  Non-terminating programs will have meaning, because we
   can just repeatedly apply the semantics to keep taking steps, forever.

   To keep things a bit simpler, we're going to get rid of ``let''
   from the language---we could certainly handle it in a small-step
   semantics, but it would require introducing a little extra
   machinery we'd like to avoid at the moment.  So without ``let,''
   the big-step semantics proves judgments of the form

   e --> n

   Small-step reduction rules will instead prove judgments of the form

   e --> e'

   In other words, evaluating e one step yields a new expression e'.
   An expression is ``fully evaluated'' or ``in normal form'' if
   it is just a natural number n.  To fully evaluate an expression,
   we just sequence multiple small-step rules together.  For example,
   here's one sequence of reductions that will hold in our semantics:

   (1 + 2) + 3 --> 3 + 3 --> 6

   We'll write -->* for the reflexive, transitive closure of -->, so

   (1 + 2) + 3 -->* 6
*)

(* Now let's reintroduce (yet again) the language syntax.  To keep
   our proofs a bit simpler, let's only include plus and if in
   the language. *)

Inductive aexp : Set := 
  | ANum : nat -> aexp
  | APlus : aexp -> aexp -> aexp
  | AIf0 : aexp -> aexp -> aexp -> aexp.

(* ...and give the small-step rules.  Here are the rules ``on paper.''
   First, several rules show how to apply + and if0 when their
   operands are fully reduced:

   --------------------
    n1 +++ n2 -> n1+n2

   We've used +++ on the left for syntactic plus, and + on the
   right for mathematical plus.  We have similar rules for if0:


   --------------------
    if0 0 e1 e2 -> e1


         n != 0
   --------------------
    if0 n e1 e2 -> e2

   Now we need ``congruence'' or ``context'' rules to tell us
   how to evaluate ``inside'' other expressions.

         e1 -> e1'
   -----------------------
   e1 +++ e2 -> e1' +++ e2

         e2 -> e2'
   -----------------------
   e1 +++ e2 -> e1 +++ e2'

              e1 -> e1'
   -------------------------------
    if0 e1 e2 e3 -> if0 e1' e2 e3

              e2 -> e2'
   -------------------------------
    if0 e1 e2 e3 -> if0 e1 e2' e3

              e3 -> e3'
   -------------------------------
    if0 e1 e2 e3 -> if0 e1 e2 e3'

   For those of you who know what call-by-value means (we'll define that
   later), you can see that this is not a call-by-value language,
   because you're allowed to evaluate the then and else branches of
   an if0 expression before the guard.  But for this language,
   order of evaluation is irrelevant, because there are no side
   effects.

   Here are the rules above, written out in Coq.
 *)

Inductive aeval_small : aexp -> aexp -> Prop :=
  | AEPlus : forall n1 n2,
    aeval_small (APlus (ANum n1) (ANum n2)) (ANum (plus n1 n2))
  | AEPlus_cong_left : forall a1 a1' a2,
    aeval_small a1 a1' -> aeval_small (APlus a1 a2) (APlus a1' a2)
  | AEPlus_cong_right : forall a1 a2 a2',
    aeval_small a2 a2' -> aeval_small (APlus a1 a2) (APlus a1 a2')
  | AEIF0_True : forall a2 a3,
    aeval_small (AIf0 (ANum 0) a2 a3) a2
  | AEIF0_False : forall a2 a3 n,
    beq_nat n 0 = false ->
    aeval_small (AIf0 (ANum n) a2 a3) a3
  | AEIf0_cong_left : forall a1 a1' a2 a3,
    aeval_small a1 a1' -> aeval_small (AIf0 a1 a2 a3) (AIf0 a1' a2 a3)
  | AEIf0_cong_mid : forall a1 a2 a2' a3,
    aeval_small a2 a2' -> aeval_small (AIf0 a1 a2 a3) (AIf0 a1 a2' a3)
  | AEIf0_cong_right : forall a1 a2 a3 a3',
    aeval_small a3 a3' -> aeval_small (AIf0 a1 a2 a3) (AIf0 a1 a2 a3').

(* Notice a few interesting things about the semantics:

   * The base rules AENum, AEPlus, AEIF0_True, and AEIF0_False
     are very clean---we'll let other rules take care of reducing
     complex expressions, and one expressions evaluate to
     numbers, then we apply these simple rules.

   * There's a pretty obvious pattern of what congruence rules look
     like, and there are actually some standard ways of writing all
     the congruence rules concisely, which we'll show a bit later.

   * The semantics are now *non-deterministic*.  For example,
     we can evaluate (1+2)+(3+4) in two different ways, either

     (1+2)+(3+4) --> 3+(3+4) --> 3+7 --> 10

     or

     (1+2)+(3+4) --> (1+2)+7 --> 3+7 --> 10

     However, notice that either way, we came to the same result.
     This property is called ``confluence,'' and we can actually
     prove it.
*)

(* We usually call a fully evaluated program a ``value.''  If
   we want to state some theorems about fully evaluated expressions,
   we need to define this precisely. *)
Inductive value : aexp -> Prop :=
  | VNum : forall n, value (ANum n).

(* In this particular semantics, if a program isn't fully evaluated
   we can always take a step.  For more complex languages, this
   will turn out to not always be true. *)
(* CMSC 631 *)
Theorem progress : forall a1,
  ~(value a1) -> (exists a2, aeval_small a1 a2).
Proof.
  Admitted.

(* We can also prove that no matter how you evaluate a program,
   you can always get to the same result.  The next theorem
   is sometimes called the ``diamond property.'' *)
(* Optional *)
Lemma confluence_small_one_step : forall a1 a2 a2',
  aeval_small a1 a2 -> aeval_small a1 a2' ->
  ((a2 = a2' /\ value a2) \/
   (exists a3, aeval_small a2 a3 /\ aeval_small a2' a3)).
Proof.
  Admitted.


(* Next, we'll define the reflexive, transitive closure of aeval_small *)
Inductive aeval_small_closed : aexp -> aexp -> Prop :=
  | AE_closed_step : forall a1 a2,
    aeval_small a1 a2 -> aeval_small_closed a1 a2
  | AE_closed_refl : forall a,
    aeval_small_closed a a
  | AE_closed_trans : forall a1 a2 a3,
    aeval_small_closed a1 a2 -> aeval_small_closed a2 a3 ->
      aeval_small_closed a1 a3.

(* We can use the above lemma to reason about multi-step
   computations. *)
(* Optional *)
Theorem confluence_small : forall a1 a2 a2',
  aeval_small_closed a1 a2 -> aeval_small_closed a1 a2' ->
  (exists a3, aeval_small_closed a2 a3 /\ aeval_small_closed a2' a3).
Proof.
  Admitted.

(* We can also prove that big-step and small-step semantics are
   equivalent *)
Inductive aeval_big : aexp -> nat -> Prop :=
  | AENum_big : forall n,
    aeval_big (ANum n) n
  | AEPlus_big : forall a1 a2 n1 n2,
    aeval_big a1 n1 ->
    aeval_big a2 n2 ->
    aeval_big (APlus a1 a2) (plus n1 n2)
  | AEIf0_True_big : forall a1 a2 a3 n2,
    aeval_big a1 0 ->
    aeval_big a2 n2 ->
    aeval_big (AIf0 a1 a2 a3) n2
  | AEIf0_False_big : forall a1 a2 a3 n1 n3,
    aeval_big a1 n1 ->
    beq_nat n1 0 = false ->
    aeval_big a3 n3 ->
    aeval_big (AIf0 a1 a2 a3) n3.

(* CMSC 631 *)
Lemma aeval_big_small : forall a n,
  aeval_big a n -> aeval_small_closed a (ANum n).
Proof.
  Admitted.

(* Notice that the following lemma says *if* a evaluates to a
   value, then it evaluates to the same value in the big-step
   semantics.  It doesn't say anything about the cases when
   the evaluation of a doesn't terminate. *)
(* Optional *)
Lemma aeval_small_big :  forall a n,
  aeval_small_closed a (ANum n) -> aeval_big a n.
Proof.
  Admitted.

End AExp_Big_Small.