(*

   Project 4.

   Due 11/9/2011

   Upload this file to the submit server with your answers filled in.

   These exercises were taken from Rel.v, Imp.v, and Smallstep.v.

*)

Require Export SfLib.

Definition admit {T: Type} : T.  Admitted.

(***********************************************************************)

(* Be sure you refer to Rel.v and contemplate using some of the properites
   proved there in your proofs (which may be already part of the Coq
   preloaded environment, or in SfLib.v; if not, copy over freely). *)

Print le.  (* This is Coq's built-in <= relation *)

(* 1 point *)
Theorem le_S_n : forall n m,
  (S n <= S m) -> (n <= m).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** 1 point *)
Theorem le_Sn_n : forall n,
  ~ (S n <= n).
Proof.
  (* FILL IN HERE *) Admitted.

Definition symmetric {X: Type} (R: relation X) :=
  forall a b : X, (R a b) -> (R b a).

(* 2 points *)
Theorem le_not_symmetric :
  ~ (symmetric le).
Proof.
  (* FILL IN HERE *) Admitted.

(* 2 points *)
Theorem rsc_trans :
  forall (X:Type) (R: relation X) (x y z : X),
      refl_step_closure R x y  ->
      refl_step_closure R y z ->
      refl_step_closure R x z.
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(* The following definitions are taken from Imp.v.  Feel free to copy over
   any other definitions/lemmas/etc. that you need. *)

Module NoVars.

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

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

Fixpoint aeval (e : aexp) : nat :=
  match e with
  | ANum n => n
  | APlus a1 a2 => (aeval a1) + (aeval a2)
  | AMinus a1 a2  => (aeval a1) - (aeval a2)
  | AMult a1 a2 => (aeval a1) * (aeval a2)
  end.

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

Fixpoint optimize_0plus (e:aexp) : 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.

(** 3 points *)
(** Since the [optimize_0plus] tranformation doesn't change the value
    of [aexp]s, we should be able to apply it to all the [aexp]s that
    appear in a [bexp] without changing the [bexp]'s value.  Write a
    function which performs that transformation on [bexp]s, and prove
    it is sound.  Use tacticals to make the proof  as elegant as possible. *)
Fixpoint optimize_0plusb (e:bexp) : bexp := e.  (* bogus; FILL IN HERE *)

Theorem optimize_0plusb_sound: forall e,
  beval (optimize_0plusb e) = beval e.
Proof.
  Admitted. (* FILL IN HERE *)

(** 1 point *)
(** Write a relation [bevalR] in the same style as [aevalR]. *)

Inductive bevalR: bexp -> bool -> Prop := .
(* FILL IN HERE *)

(** 2 points *)
(* Prove the above relation is equivalent to [beval] *)

Theorem beval_iff_bevalR : forall e b,
  (bevalR e b) <-> beval e = b.
Proof.
  Admitted.  (* FILL IN HERE *)

End NoVars.

(***********************************************************************)

(* More definitions from Imp; here we extend expressions to include
   variables. *)

Definition X : id := Id 0.
Definition Y : id := Id 1.
Definition Z : id := Id 2.

Definition state := id -> nat.

Definition empty_state : state := 
  fun _ => 0.
 
Definition update (st : state) (X:id) (n : nat) : state :=
  fun X' => if beq_id X X' then n else st X'.

(***********************************************************************)

(** 2 points *)
Theorem update_shadow : forall x1 x2 k1 k2 (f : state),
   (update  (update f k2 x1) k2 x2) k1 = (update f k2 x2) k1.
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(* More Imp definitions ... *)

Inductive aexp : Type := 
  | ANum : nat -> aexp
  | AId : id -> aexp                                     (* <----- NEW *)
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

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

Fixpoint aeval (st : state) (e : aexp) : nat :=
  match e with
  | ANum n => n
  | AId X => st X                                        (* <----- NEW *)
  | APlus a1 a2 => (aeval st a1) + (aeval st a2)
  | AMinus a1 a2  => (aeval st a1) - (aeval st a2)
  | AMult a1 a2 => (aeval st a1) * (aeval st a2)
  end.

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

Inductive com : Type :=
  | CSkip : com
  | CAss : id -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com.

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

Notation "'LETOPT' x <== e1 'IN' e2" 
   := (match e1 with
         | Some x => e2
         | None => None
       end)
   (right associativity, at level 60).

Fixpoint ceval_step (st : state) (c : com) (i : nat) 
                    : option state :=
  match i with 
  | O => None
  | S i' =>
    match c with 
      | SKIP => 
          Some st
      | l ::= a1 => 
          Some (update st l (aeval st a1))
      | c1 ; c2 => 
          LETOPT st' <== ceval_step st c1 i' IN
          ceval_step st' c2 i'
      | IFB b THEN c1 ELSE c2 FI => 
          if (beval st b) 
            then ceval_step st c1 i' 
            else ceval_step st c2 i'
      | WHILE b1 DO c1 END => 
          if (beval st b1)           
          then LETOPT st' <== ceval_step st c1 i' IN
               ceval_step st' c i'
          else Some st
    end
  end.

Definition test_ceval (st:state) (c:com) := 
  match ceval_step st c 500 with
  | None    => None
  | Some st => Some (st X, st Y, st Z)
  end.  

Reserved Notation "c1 '/' st '||' st'" (at level 40, st at level 39).

Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st,
      SKIP / st || st
  | E_Ass  : forall st a1 n l,
      aeval st a1 = n ->
      (l ::= a1) / st || (update st l n)
  | E_Seq : forall c1 c2 st st' st'',
      c1 / st  || st' ->
      c2 / st' || st'' ->
      (c1 ; c2) / st || st''
  | E_IfTrue : forall st st' b1 c1 c2,
      beval st b1 = true ->
      c1 / st || st' ->
      (IFB b1 THEN c1 ELSE c2 FI) / st || st'
  | E_IfFalse : forall st st' b1 c1 c2,
      beval st b1 = false ->
      c2 / st || st' ->
      (IFB b1 THEN c1 ELSE c2 FI) / st || st'
  | E_WhileEnd : forall b1 st c1,
      beval st b1 = false ->
      (WHILE b1 DO c1 END) / st || st
  | E_WhileLoop : forall st st' st'' b1 c1,
      beval st b1 = true ->
      c1 / st || st' ->
      (WHILE b1 DO c1 END) / st' || st'' ->
      (WHILE b1 DO c1 END) / st || st''

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


(***********************************************************************)

(** 2 points *)
(** Write an Imp program that sums the numbers from [1] to
   [X] (inclusive: [1 + 2 + ... + X]) in the variable [Y].  Make sure
   your solution satisfies the test that follows. *)

Definition pup_to_n : com := 
  (* FILL IN HERE *) admit.

Example pup_to_n_1 : 
  test_ceval (update empty_state X 5) pup_to_n
  = Some (0, 15, 0).
Proof. 
  Admitted. (* Change to the following and it should work if pup_to_n is correct
  reflexivity. Qed. 
*)

(***********************************************************************)

Definition loop : com :=
  WHILE BTrue DO
    SKIP
  END.

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

(***********************************************************************)

(* The following definitions are from Smallstep.v.  Feel free to include
   others you might need. *)

Inductive tm : Type :=
  | tm_const : nat -> tm
  | tm_plus : tm -> tm -> tm.

Reserved Notation " t '||' t' " (at level 50, left associativity).

Inductive eval : tm -> tm -> Prop :=
  | E_Const : forall n1,
        tm_const n1 || tm_const n1
  | E_Plus : forall t1 n1 t2 n2,
        t1 || tm_const n1 ->
        t2 || tm_const n2 ->
        tm_plus t1 t2 || tm_const (plus n1 n2)

  where " t '||' t' " := (eval t t').

Inductive value : tm -> Prop :=
  v_const : forall n, value (tm_const n).

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
          tm_plus (tm_const n1) (tm_const n2)
      ==> tm_const (plus n1 n2)
  | ST_Plus1 : forall t1 t1' t2,
        t1 ==> t1' ->
        tm_plus t1 t2 ==> tm_plus t1' t2
  | ST_Plus2 : forall v1 t2 t2',
        value v1 ->                     (* <----- n.b. *) 
        t2 ==> t2' ->
        tm_plus v1 t2 ==> tm_plus v1 t2'

  where " t '==>' t' " := (step t t').

(***********************************************************************)

(** 2 points *)

Example test_step_2 : 
      tm_plus 
        (tm_const 0)
        (tm_plus 
          (tm_const 2) 
          (tm_plus (tm_const 0) (tm_const 3)))
      ==>
      tm_plus 
        (tm_const 0)
        (tm_plus 
          (tm_const 2) 
          (tm_const (plus 0 3))).
Proof. 
  (* FILL IN HERE *) Admitted.
(** [] *)

(***********************************************************************)
(** 3 points *)

Theorem step_deterministic:
  partial_function step.
Proof.
  Admitted.

(***********************************************************************)
(** 3 points *)
Theorem step__eval : forall t t' v,
     t ==> t' ->
     t' || v ->
     t || v.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(***********************************************************************)

Module NonDet.

(* Consider the following small-step evaluation relationship, which is
   non-deterministic *)

Reserved Notation " t '-->' t' " (at level 40).

Inductive step_nd : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
          tm_plus (tm_const n1) (tm_const n2)
      --> tm_const (plus n1 n2)
  | ST_Plus1 : forall t1 t1' t2,
        t1 --> t1' ->
        tm_plus t1 t2 --> tm_plus t1' t2
  | ST_Plus2 : forall t1 t2 t2',
        t2 --> t2' ->
        tm_plus t1 t2 --> tm_plus t1 t2'

  where " t '-->' t' " := (step_nd t t').

Tactic Notation "step_cases" tactic(first) tactic(c) :=
  first;
  [ c "ST_PlusConstConst" | c "ST_Plus1" | c "ST_Plus2" ].

Definition stepmany := refl_step_closure step_nd.

Notation " t '-->*' t' " := (stepmany t t') (at level 40).

(* 3 points *)
(* Prove confluence, a.k.a. the dianond property *)
Theorem diamond_property : forall t t1 t2,
   t --> t1 -> t --> t2 -> exists t', t1 -->* t' /\ t2 -->* t'.
Proof.
  Admitted.

End NonDet.