Imp.v

(** * Imp: Simple Imperative Programs *)

Set Warnings "-notation-overridden,-notation-incompatible-prefix".
From Stdlib Require Import Bool.
From Stdlib Require Import Init.Nat.
From Stdlib Require Import Arith.
From Stdlib Require Import EqNat. Import Nat.
From Stdlib Require Import Lia.
From Stdlib Require Import List. Import ListNotations.
From Stdlib Require Import Strings.String.
From LF Require Import Maps.
Set Default Goal Selector "!".

Module AExp.

Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Inductive bexp : Type :=
  | BTrue 
  | BFalse 
  | BEq (a1 a2 : aexp) 
  | BNeq (a1 a2 : aexp)
  | BLe (a1 a2  : aexp)
  | BGt (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Fixpoint aeval (a : aexp) : nat :=
  match a 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.

Example test_aeval1 : 
  aeval (APlus (ANum 2) (ANum 2)) = 4.
Proof. reflexivity. Qed.

Fixpoint beval (b : bexp) : bool :=
  match b with 
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => (aeval a1) =? (aeval a2)
  | BNeq a1 a2 => negb ((aeval a1) =? (aeval a2))
  | BLe a1 a2 => (aeval a1) <=? (aeval a2)
  | BGt a1 a2 => negb ((aeval a1) <=? (aeval a2))
  | BNot b1 => negb (beval b1)
  | BAnd b1 b2 => andb (beval b1)(beval b2)
  end.

Fixpoint optimize_0plus (a : aexp) : aexp :=
  match a 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 (APlus (ANum 2)
                        (APlus (ANum 0)
                        (APlus (ANum 0)(ANum 1))))
  = APlus (ANum 2) (ANum 1).
Proof. reflexivity. Qed.

Theorem optimize_0plus_sound : forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros. induction a.
  - reflexivity.
  - destruct a1 eqn:Ea1.
    + destruct n eqn:En.
      * simpl. apply IHa2.
      * simpl. rewrite IHa2. reflexivity.
    + simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
    + simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
    + simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
  - simpl. rewrite IHa1. rewrite IHa2. reflexivity.
  - simpl. rewrite IHa1. rewrite IHa2. reflexivity.
Qed.

(* ROCQ AUTOMATION *)

Theorem silly1 :forall (P : Prop), P -> P.
Proof.
  intros P HP.
  try reflexivity.
  apply HP.
Qed.

Theorem silly2 : forall ae, aeval ae = aeval ae.
Proof.
  try reflexivity.
Qed.

Lemma foo : forall n, 0 <=? n = true.
Proof.
  intros.
  destruct n.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

Lemma foo' : forall n, 0 <=? n = true.
Proof.
  intros.
  destruct n; 
  simpl; 
  reflexivity.
Qed.

Theorem optimize_0plus_sound' : forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  induction a; 
    try (simpl; rewrite IHa1; rewrite IHa2; reflexivity).
  - reflexivity.
  - destruct a1 eqn:Ea1;
      try (simpl; simpl in IHa1; rewrite IHa1; rewrite IHa2; reflexivity).
    + destruct n eqn:En; simpl; rewrite IHa2; reflexivity. 
Qed.

Theorem optimize_0plus_sound'': forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  induction a;
    (* Most cases follow directly by the IH *)
    try (simpl; rewrite IHa1; rewrite IHa2; reflexivity);
    (* ... or are immediate by definition *)
    try reflexivity.
  (* The interesting case is when a = APlus a1 a2. *)
  - (* APlus *)
    destruct a1; try (simpl; simpl in IHa1; rewrite IHa1;
                      rewrite IHa2; reflexivity).
    + (* a1 = ANum n *) destruct n;
      simpl; rewrite IHa2; reflexivity.
Qed.


Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; reflexivity); right).
Qed.

Theorem In10' : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat simpl.
  repeat (left; reflexivity).
  repeat (right; try (left; reflexivity)).
Qed.

(** The tactic [repeat T] does not have any upper bound on the
    number of times it applies [T].  If [T] is a tactic that _always_
    succeeds (and makes progress), then repeat [T] will loop
    forever. *)

Theorem repeat_loop : forall (m n : nat),
  m + n = n + m.
Proof.
  intros m n.
  (* Uncomment the next line to see the infinite loop occur.  You will
     then need to interrupt Coq to make it listen to you again.  (In
     Proof General, [C-c C-c] does this.) *)
  (* repeat rewrite Nat.add_comm. *)
Admitted.

Fixpoint optimize_0plus_b (b : bexp) : bexp :=
  match b with 
  | BTrue      => BTrue
  | BFalse     => BFalse
  | BEq a1 a2  => BEq(optimize_0plus a1)(optimize_0plus a2)
  | BNeq a1 a2 => BNeq (optimize_0plus a1)(optimize_0plus a2)
  | BLe a1 a2  => BLe (optimize_0plus a1)(optimize_0plus a2)
  | BGt a1 a2  => BGt (optimize_0plus a1)(optimize_0plus a2)
  | BNot b     => BNot (optimize_0plus_b b)
  | BAnd b1 b2 =>  BAnd (optimize_0plus_b b1) (optimize_0plus_b b2)
  end.

Example optimize_0plus_b_test1:
  optimize_0plus_b (BNot (BGt (APlus (ANum 0) (ANum 4)) (ANum 8))) =
                   (BNot (BGt (ANum 4) (ANum 8))).
Proof. reflexivity. Qed.

Example optimize_0plus_b_test2:
  optimize_0plus_b (BAnd (BLe (APlus (ANum 0) (ANum 4)) (ANum 5)) BTrue) =
                   (BAnd (BLe (ANum 4) (ANum 5)) BTrue).
Proof. reflexivity. Qed.

Theorem optimize_0plus_b_sound : forall b,
  beval (optimize_0plus_b b) = beval b.
Proof.
  intros.
  induction b;
  try ( simpl; repeat (rewrite optimize_0plus_sound); reflexivity).
  - simpl. rewrite IHb. reflexivity.
  - simpl. rewrite IHb1. rewrite IHb2. reflexivity.
Qed.
(** [] *)

(* (** **** Exercise: 4 stars, standard, optional (optimize) *)  *)

Fixpoint optimize ( a : aexp) : aexp :=
  match a with 
  | ANum n => ANum n 
  | APlus e1 e2 =>
      match optimize e1 with 
      | ANum 0 => optimize e2
      | e1 =>
        match optimize e2 with 
        | ANum 0 => e1 
        | e2 => APlus e1 e2
        end
      end 
  | AMinus e1 e2 => 
      match optimize e1 with 
      | ANum 0 => ANum 0
      | e1 =>
        match optimize e2 with 
        | ANum 0 => e1
        | e2 => AMinus e1 e2 
        end 
    end 
  | AMult e1 e2 => 
      match optimize e1 with 
      | ANum 0 => ANum 0 
      | ANum 1 => optimize e2 
      | e1 => 
        match optimize e2 with 
        | ANum 0 => ANum 0
        | ANum 1 => e1 
        | e2 => AMult e1 e2 
        end 
      end 
  end.

Theorem optimize_sound : forall a,
  aeval (optimize a) = aeval a.
Proof.
  intros a.
  induction a.
  - reflexivity.
  - simpl. rewrite <- IHa1. rewrite <- IHa2. destruct (optimize a1);
    try (destruct (optimize a2); [destruct n; [rewrite add_0_r; reflexivity | reflexivity] | reflexivity | reflexivity | reflexivity]).
    + destruct n.
      * reflexivity.
      * destruct (optimize a2).
        ** destruct n0.
           *** rewrite add_0_r. reflexivity.
           *** reflexivity.
        ** reflexivity.
        ** reflexivity.
        ** reflexivity.
  - simpl. rewrite <- IHa1. rewrite <- IHa2. destruct (optimize a1);
    try (destruct (optimize a2); [destruct n; [rewrite sub_0_r; reflexivity | reflexivity] | reflexivity | reflexivity | reflexivity]).
    + destruct n.
      * reflexivity.
      * destruct (optimize a2).
        ** destruct n0.
           *** reflexivity.
           *** reflexivity.
        ** reflexivity.
        ** reflexivity.
        ** reflexivity.
  - simpl. rewrite <- IHa1. rewrite <- IHa2. destruct (optimize a1);
    try (destruct (optimize a2); [destruct n; [rewrite mul_0_r; reflexivity | destruct n; [rewrite mul_1_r; reflexivity | reflexivity]] | reflexivity | reflexivity | reflexivity]).
    + destruct n.
      * reflexivity.
      * destruct n.
        ** simpl. rewrite add_0_r. reflexivity.
        ** destruct (optimize a2).
          *** destruct n0.
              **** rewrite mul_0_r. reflexivity.
              **** destruct n0.
                   ***** rewrite mul_1_r. reflexivity.
                   ***** reflexivity.
          *** reflexivity.
          *** reflexivity.
          *** reflexivity.
Qed.

Ltac invert H :=
  inversion H; subst; clear H.

Lemma invert_example1: forall {a b c: nat}, [a ;b] = [a;c] -> b = c.
  intros.
  invert H.
  reflexivity.
Qed.

Example silly_presburger_example : forall m n o p,
  m + n <= n + o /\ o + 3 = p + 3 ->
  m <= p.
Proof.
  intros. lia.
Qed.

Example add_comm__lia : forall m n,
    m + n = n + m.
Proof.
  intros. lia.
Qed.

Example add_assoc__lia : forall m n p,
    m + (n + p) = m + n + p.
Proof.
  intros. lia.
Qed.

Module aevalR_first_try.

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n : nat) : 
      aevalR (ANum n) n
  | E_APlus (e1 e2 : aexp) (n1 n2 : nat ) : 
      aevalR e1 n1 -> 
      aevalR e2 n2 -> 
      aevalR (AMinus e1 e2) (n1 + n2)
 | E_AMinus (e1 e2 : aexp) (n1 n2 : nat ) : 
      aevalR e1 n1 -> 
      aevalR e2 n2 -> 
      aevalR (AMinus e1 e2) (n1 - n2) 
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat ) : 
      aevalR e1 n1 -> 
      aevalR e2 n2 -> 
      aevalR (AMinus e1 e2) (n1 * n2).

Module HypothesisNames.

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n : nat) :
      aevalR (ANum n) n
  | E_APlus (e1 e2 : aexp) (n1 n2 : nat)
      (H1 : aevalR e1 n1)
      (H2 : aevalR e2 n2) :
      aevalR (APlus e1 e2) (n1 + n2)
  | E_AMinus (e1 e2 : aexp) (n1 n2 : nat)
      (H1 : aevalR e1 n1)
      (H2 : aevalR e2 n2) :
      aevalR (AMinus e1 e2) (n1 - n2)
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat)
      (H1 : aevalR e1 n1)
      (H2 : aevalR e2 n2) :
      aevalR (AMult e1 e2) (n1 * n2).

End HypothesisNames.

Notation "e '==>' n"
         := (aevalR e n)
            (at level 90, left associativity)
         : type_scope.

End aevalR_first_try.

Reserved Notation "e '==>' n" (at level 90, left associativity).

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n :nat) :
      (ANum n) ==> n 
  | E_APlus (e1 e2 : aexp) (n1 n2 :nat ) :
      (e1 ==> n1) ->
      (e2 ==> n2) ->
      (APlus e1 e2) ==> (n1+n2)
  | E_AMinus (e1 e2 : aexp) (n1 n2 : nat) :
      (e1 ==> n1) -> 
      (e2 ==> n2) -> 
      (AMinus e1 e2) ==> (n1 - n2)
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat) : 
      (e1 ==> n1) ->
      (e2 ==> n2) -> 
      (AMult e1 e2) ==> (n1*n2)
  where "e '==>' n" := (aevalR e n) : type_scope.

Theorem aevalR_iff_aeval : forall a n,
  (a ==> n) <-> aeval a = n.
Proof.
  split.
  - (* -> *)
    intros H.
    induction H; simpl.
    + (* E_ANum *)
      reflexivity.
    + (* E_APlus *)
      rewrite IHaevalR1.  rewrite IHaevalR2.  reflexivity.
    + (* E_AMinus *)
      rewrite IHaevalR1.  rewrite IHaevalR2.  reflexivity.
    + (* E_AMult *)
      rewrite IHaevalR1.  rewrite IHaevalR2.  reflexivity.
  - (* <- *)
    generalize dependent n.
    induction a;
       simpl; intros; subst.
    + (* ANum *)
      apply E_ANum.
    + (* APlus *)
      apply E_APlus.
      * apply IHa1. reflexivity.
      * apply IHa2. reflexivity.
    + (* AMinus *)
      apply E_AMinus.
      * apply IHa1. reflexivity.
      * apply IHa2. reflexivity.
    + (* AMult *)
      apply E_AMult.
      * apply IHa1. reflexivity.
      * apply IHa2. reflexivity.
Qed.

(** Again, we can make the proof quite a bit shorter using some
    tacticals. *)

Theorem aevalR_iff_aeval' : forall a n,
  (a ==> n) <-> aeval a = n.
Proof.
  (* WORKED IN CLASS *)
  split.
  - (* -> *)
    intros H; induction H; subst; reflexivity.
  - (* <- *)
    generalize dependent n.
    induction a; simpl; intros; subst; constructor;
       try apply IHa1; try apply IHa2; reflexivity.
Qed.

(** **** Exercise: 3 stars, standard (bevalR)

    Write a relation [bevalR] in the same style as
    [aevalR], and prove that it is equivalent to [beval]. *)

Reserved Notation "e '==>b' b" (at level 90, left associativity).
Inductive bevalR: bexp -> bool -> Prop :=
  | E_BTrue : BTrue ==>b true 
  | E_BFalse : BFalse ==>b false 
  | E_BEq (e1 e2 : aexp) (n1 n2 : nat) (H1 : aevalR e1 n1) (H2 : aevalR e2 n2) : BEq e1 e2 ==>b n1 =? n2 
  | E_BNeq (e1 e2 : aexp)(n1 n2 : nat)(H1: aevalR e1 n1) (H2 : aevalR e2 n2) :   BNeq e1 e2 ==>b negb(n1 =? n2) 
  | E_BLe (e1 e2 : aexp) (n1 n2 : nat) (H1 : aevalR e1 n1) (H2 : aevalR e2 n2) : BLe e1 e2 ==>b n1 <=? n2
  | E_BGt (e1 e2 : aexp) (n1 n2 : nat) (H1 : aevalR e1 n1) (H2 : aevalR e2 n2) : BGt e1 e2 ==>b negb (n1 <=? n2)
  | E_BNot (e : bexp) (b : bool) (H : bevalR e b) : BNot e ==>b negb b
  | E_BAnd (e1 e2 : bexp) (b1 b2 : bool) (H1 : bevalR e1 b1) (H2 : bevalR e2 b2) : BAnd e1 e2 ==>b andb b1 b2
where "e '==>b' b" := (bevalR e b) : type_scope
.

Lemma bevalR_iff_beval : forall b bv,
  b ==>b bv <-> beval b = bv.
Proof.
  split.
  - intros. induction H; simpl; 
    try (apply aevalR_iff_aeval in H1; apply aevalR_iff_aeval in H2); subst; reflexivity.
  - intros. 
    destruct b;
      subst; constructor;
      try (apply aevalR_iff_aeval; reflexivity);
      [ | rename b1 into b | rename b2 into b ];
      induction b;
      constructor;
      try (apply aevalR_iff_aeval; reflexivity);
      try (apply IHb);
      try (apply IHb1);
      try (apply IHb2).
Qed.

End AExp.

Module aevalR_division.

Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp)
  | ADiv (a1 a2 : aexp).         (* <--- NEW *)

Reserved Notation "e '==>' n"
                  (at level 90, left associativity).

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n : nat) :
      (ANum n) ==> n
  | E_APlus (a1 a2 : aexp) (n1 n2 : nat) :
      (a1 ==> n1) -> (a2 ==> n2) -> (APlus a1 a2) ==> (n1 + n2)
  | E_AMinus (a1 a2 : aexp) (n1 n2 : nat) :
      (a1 ==> n1) -> (a2 ==> n2) -> (AMinus a1 a2) ==> (n1 - n2)
  | E_AMult (a1 a2 : aexp) (n1 n2 : nat) :
      (a1 ==> n1) -> (a2 ==> n2) -> (AMult a1 a2) ==> (n1 * n2)
  | E_ADiv (a1 a2 : aexp) (n1 n2 n3 : nat) :          (* <----- NEW *)
      (a1 ==> n1) -> (a2 ==> n2) -> (n2 > 0) ->
      (mult n2 n3 = n1) -> (ADiv a1 a2) ==> n3
where "a '==>' n" := (aevalR a n) : type_scope.

End aevalR_division.

Module aevalR_extended.

Reserved Notation "e '==>' n" (at level 90, left associativity).

Inductive aexp : Type :=
  | AAny                           (* <--- NEW *)
  | ANum (n : nat)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Inductive aevalR : aexp -> nat -> Prop :=
  | E_Any (n : nat) :
      AAny ==> n                        (* <--- NEW *)
  | E_ANum (n : nat) :
      (ANum n) ==> n
  | E_APlus (a1 a2 : aexp) (n1 n2 : nat) :
      (a1 ==> n1) -> (a2 ==> n2) -> (APlus a1 a2) ==> (n1 + n2)
  | E_AMinus (a1 a2 : aexp) (n1 n2 : nat) :
      (a1 ==> n1) -> (a2 ==> n2) -> (AMinus a1 a2) ==> (n1 - n2)
  | E_AMult (a1 a2 : aexp) (n1 n2 : nat) :
      (a1 ==> n1) -> (a2 ==> n2) -> (AMult a1 a2) ==> (n1 * n2)

where "a '==>' n" := (aevalR a n) : type_scope.

End aevalR_extended.

Definition state := total_map nat.

Inductive aexp : Type :=
  | ANum (n : nat)
  | AId (x : string)              (* <--- NEW *)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Definition W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BNeq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BGt (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.

Declare Custom Entry com.
Declare Scope com_scope.
Declare Custom Entry com_aux.

Notation "<{ e }>" := e
  (e custom com, format "'[hv' <{ '/ ' '[v' e ']' '/' }> ']'") : com_scope.
Notation "( x )" := x (in custom com, x at level 99).
Notation "x" := x (in custom com at level 0, x constr at level 0).
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 1,
                      y constr at level 1).
Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity).
Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity).
Notation "'true'" := true (at level 1).
Notation "'true'" := BTrue (in custom com at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := BFalse (in custom com at level 0).
Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity).
Notation "x > y" := (BGt x y) (in custom com at level 70, no associativity).
Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity).
Notation "x <> y" := (BNeq x y) (in custom com at level 70, no associativity).
Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity).
Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity).
Open Scope com_scope.

Definition example_aexp : aexp := <{ 3 + (X+2)}>.
Definition example_bexp : bexp := <{ true && ~(X <= 4)}>.

Fixpoint aeval (st : state) 
               (a : aexp) : nat :=
  match a with 
  | ANum n => n 
  | AId x => st x 
  | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
  | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
  | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
  end.

Fixpoint beval (st : state) 
               (b : bexp) : bool :=
  match b with 
  | <{true}> => true
  | <{false}> => false
  | <{a1 = a2}> => (aeval st a1) =? (aeval st a2)
  | <{a1 <> a2}> => negb ((aeval st a1) =? (aeval st a2))
  | <{a1 <= a2}> => (aeval st a1) <=? (aeval st a2)
  | <{a1 > a2}> => negb ((aeval st a1) <=? (aeval st a2))
  | <{~b1}> => negb (beval st b1) 
  | <{b1 && b2}> => andb (beval st b1)(beval st b2)
  end.

Definition empty_st := (_ !-> 0).

Notation "x '!->' v" := (x !-> v ; empty_st)(at level 100, right associativity).

Example aexp1 : 
  aeval (X !-> 5) <{ 3 + (X*2)}> = 13.
Proof. reflexivity. Qed.

Example aexp2 :
  aeval (X !-> 5 ; Y !-> 4) <{ Z + (X * Y) }>
= 20.
Proof. reflexivity. Qed.

Example bexp1 : 
  beval (X !-> 5) <{ true && ~(X <= 4)}> = true.
Proof. reflexivity. Qed.

Inductive com : Type :=
  | CSkip 
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp)(c1 c2 : com)
  | CWhile (b:bexp)(c:com).

Notation "'skip'" := CSkip
  (in custom com at level 0) : com_scope.
Notation "x := y" := (CAsgn x y)
  (in custom com at level 0, x constr at level 0, y at level 85, no associativity,
    format "x := y") : com_scope.
Notation "x ; y" := (CSeq x y)
  (in custom com at level 90,
    right associativity,
    format "'[v' x ; '/' y ']'") : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" := (CIf x y z)
  (in custom com at level 89, x at level 99, y at level 99, z at level 99,
    format "'[v' 'if' x 'then' '/ ' y '/' 'else' '/ ' z '/' 'end' ']'") : com_scope.
Notation "'while' x 'do' y 'end'" := (CWhile x y)
  (in custom com at level 89, x at level 99, y at level 99,
    format "'[v' 'while' x 'do' '/ ' y '/' 'end' ']'") : com_scope.

Definition fact_in_coq : com :=
  <{  Z := X;
      Y := 1;
      while Z <> 0 do
        Y := Y*Z;
        Z := Z -1
      end }>.
Print fact_in_coq.

Unset Printing Notations.
Print fact_in_coq.

Set Printing Notations.

Print example_bexp.
(* ===> example_bexp = <{(true && ~ (X <= 4))}> *)

Set Printing Coercions.
Print example_bexp.
(* ===> example_bexp = <{(true && ~ (AId X <= ANum 4))}> *)

Print fact_in_coq.

Unset Printing Coercions.


Locate aexp.

Locate "&&".

Locate ";".

Locate "while".


(* ================================================================= *)
(** ** More Examples *)

(* ----------------------------------------------------------------- *)
(** *** Assignment: *)

Definition plus2 : com :=
  <{ X := X + 2 }>.

Definition XtimesYinZ : com :=
  <{ Z := X * Y }>.

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

Definition subtract_slowly_body : com :=
  <{ Z := Z - 1 ;
     X := X - 1 }>.

Definition subtract_slowly : com :=
  <{ while X <> 0 do
       subtract_slowly_body
     end }>.

Definition subtract_3_from_5_slowly : com :=
  <{ X := 3 ;
     Z := 5 ;
     subtract_slowly }>.

(* ----------------------------------------------------------------- *)
(** *** An infinite loop: *)

Definition loop : com :=
  <{ while true do
       skip
     end }>.

(* ################################################################# *)
(** * Evaluating Commands *)

(** Next we need to define what it means to evaluate an Imp command.
    The fact that [while] loops don't necessarily terminate makes
    defining an evaluation function tricky... *)

(* ================================================================= *)
(** ** Evaluation as a Function (Failed Attempt) *)

(** Here's an attempt at defining an evaluation function for commands
    (with a bogus [while] case). *)

Fixpoint ceval_fun_no_while (st : state) (c : com) : state :=
  match c with 
  | <{ skip }> => st 
  | <{ x := a}> => (x !-> aeval st a ; st)
  | <{ c1 ; c2}> => 
      let st' := ceval_fun_no_while st c1 in 
      ceval_fun_no_while st' c2
  | <{ if b then c1 else c2 end}> => 
      if (beval st b)
          then ceval_fun_no_while st c1
          else ceval_fun_no_while st c2
  | <{ while b do c end }> =>
      st 
  end.

Reserved Notation
         "st '=[' c ']=>' st'"
         (at level 40, c custom com at level 99,
          st constr, st' constr at next level).

Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st,
      st =[ skip ]=> st
  | E_Asgn  : forall st a n x,
      aeval st a = n ->
      st =[ x := a ]=> (x !-> n ; st)
  | E_Seq : forall c1 c2 st st' st'',
      st  =[ c1 ]=> st'  ->
      st' =[ c2 ]=> st'' ->
      st  =[ c1 ; c2 ]=> st''
  | E_IfTrue : forall st st' b c1 c2,
      beval st b = true ->
      st =[ c1 ]=> st' ->
      st =[ if b then c1 else c2 end]=> st'
  | E_IfFalse : forall st st' b c1 c2,
      beval st b = false ->
      st =[ c2 ]=> st' ->
      st =[ if b then c1 else c2 end]=> st'
  | E_WhileFalse : forall b st c,
      beval st b = false ->
      st =[ while b do c end ]=> st
  | E_WhileTrue : forall st st' st'' b c,
      beval st b = true ->
      st  =[ c ]=> st' ->
      st' =[ while b do c end ]=> st'' ->
      st  =[ while b do c end ]=> st''

  where "st =[ c ]=> st'" := (ceval c st st').

Example ceval_example1:
  empty_st =[
     X := 2;
     if (X <= 1)
       then Y := 3
       else Z := 4
     end
  ]=> (Z !-> 4 ; X !-> 2).
Proof.
  (* We must supply the intermediate state *)
  apply E_Seq with (X !-> 2).
  - (* assignment command *)
    apply E_Asgn. reflexivity.
  - (* if command *)
    apply E_IfFalse.
    + reflexivity.
    + apply E_Asgn. reflexivity.
Qed.

(** **** Exercise: 2 stars, standard (ceval_example2) *)
Example ceval_example2:
  empty_st =[
    X := 0;
    Y := 1;
    Z := 2
  ]=> (Z !-> 2 ; Y !-> 1 ; X !-> 0).
Proof.
  apply E_Seq with (X !-> 0).
  - apply E_Asgn. reflexivity.
  - apply E_Seq with ( Y !-> 1 ; X !-> 0).
    + apply E_Asgn. reflexivity.
    + apply E_Asgn. reflexivity.
Qed.


Set Printing Implicit.
Check @ceval_example2.

Definition pup_to_n : com :=
  <{ Y := 0;
     while X > 0 do 
      Y := Y + X;
      X := X -1
      end }>.


Theorem pup_to_2_ceval :
  (X !-> 2) =[
    pup_to_n
  ]=> (X !-> 0 ; Y !-> 3 ; X !-> 1 ; Y !-> 2 ; Y !-> 0 ; X !-> 2).
Proof.
  apply E_Seq with ( Y !-> 0 ; X !-> 2).
  - apply E_Asgn. reflexivity.
  - apply E_WhileTrue with (X !-> 1; Y !-> 2 ; Y !-> 0 ; X !-> 2).
    + reflexivity.
    + apply E_Seq with (Y !-> 2 ; Y !-> 0 ; X !-> 2).
      * apply E_Asgn. reflexivity.
      * apply E_Asgn. reflexivity.
    + apply E_WhileTrue with (X !-> 0 ; Y !-> 3 ; X !-> 1 ; Y !-> 2 ; Y !-> 0 ; X !-> 2).
      * reflexivity.
      * apply E_Seq with (Y !-> 3 ; X !-> 1 ; Y !-> 2 ; Y !-> 0 ; X !-> 2).
        ** apply E_Asgn. reflexivity.
        ** apply E_Asgn. reflexivity.
      * apply E_WhileFalse. reflexivity.
Qed.


Theorem ceval_deterministic: forall c st st1 st2,
     st =[ c ]=> st1  ->
     st =[ c ]=> st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2.
  induction E1; intros st2 E2; inversion E2; subst.
  - (* E_Skip *) reflexivity.
  - (* E_Asgn *) reflexivity.
  - (* E_Seq *)
    rewrite (IHE1_1 st'0 H1) in *.
    apply IHE1_2. assumption.
  - (* E_IfTrue, b evaluates to true *)
      apply IHE1. assumption.
  - (* E_IfTrue,  b evaluates to false (contradiction) *)
      rewrite H in H5. discriminate.
  - (* E_IfFalse, b evaluates to true (contradiction) *)
      rewrite H in H5. discriminate.
  - (* E_IfFalse, b evaluates to false *)
      apply IHE1. assumption.
  - (* E_WhileFalse, b evaluates to false *)
    reflexivity.
  - (* E_WhileFalse, b evaluates to true (contradiction) *)
    rewrite H in H2. discriminate.
  - (* E_WhileTrue, b evaluates to false (contradiction) *)
    rewrite H in H4. discriminate.
  - (* E_WhileTrue, b evaluates to true *)
    rewrite (IHE1_1 st'0 H3) in *.
    apply IHE1_2. assumption.  Qed.


(* REASONING ABOUT IMP PROGRAMS *)

Theorem plus2_spec : forall st n st',
  st X = n ->
  st =[ plus2 ]=> st' ->
  st' X = 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. clear Heval. simpl.
  apply t_update_eq.  Qed.

(** **** Exercise: 3 stars, standard, optional (XtimesYinZ_spec)

    State and prove a specification of [XtimesYinZ]. *)

(* FILL IN HERE *)
Theorem XtimesYinZ_spec : forall st m n st',
  st X = m ->
  st Y = n ->
  st =[ XtimesYinZ ]=> st' ->
  st' Z = m * n.
Proof.
  intros st m n st' HX HY Heval.
  inversion Heval. subst. clear Heval. simpl. apply t_update_eq.
Qed.

Theorem loop_never_stops : forall st st',
  ~(st =[ loop ]=> st').
Proof.
  intros st st' contra. unfold loop in contra.
  remember <{ while true do skip end }> as loopdef
           eqn:Heqloopdef.
  induction contra; inversion Heqloopdef; subst; try discriminate.
  apply IHcontra2. reflexivity.
Qed.

Fixpoint no_whiles (c : com) : bool :=
  match c with 
  | <{ skip }> => 
      true 
  | <{ _ := _ }> => 
      true
  | <{ c1 ; c2}> => 
      andb (no_whiles c1)(no_whiles c2)
  | <{ if _ then ct else cf end}> => 
      andb (no_whiles ct)(no_whiles cf)
  | <{ while _ do _ end}> => 
      false
  end.

Inductive no_whilesR : com -> Prop := 
  | no_whiles_Skip : no_whilesR <{ skip }>
  | no_whiles_Asgn : forall x a, no_whilesR <{ x := a }>
  | no_whiles_Seq : forall c1 c2 (H1 : no_whilesR c1)(H2 : no_whilesR c2), no_whilesR <{ c1 ; c2}>
  | no_whiles_If : forall b c1 c2 (H1 : no_whilesR c1)(H2 : no_whilesR c2), no_whilesR<{if b then c1 else c2 end}>
  .

Theorem no_whiles_eqv : 
  forall c, no_whiles c = true <-> no_whilesR c.
Proof.
  intros.
  split.
  - induction c;
      try constructor;
      try (inversion H as [H1]; apply andb_true_iff in H1);
      try (destruct H1 as [H1 _]; apply IHc1; apply H1);
      try (destruct H1 as [_ H2]; apply IHc2; apply H2);
      discriminate.
  - intros H.
    induction H;
      try reflexivity;
      apply andb_true_iff;
      split;
      assumption.
Qed.

Theorem no_whiles_terminating :
  forall c, no_whilesR c -> forall st, exists st', st =[ c ]=> st'.
Proof.
  intros c H.
  induction c.
  - intros. exists st. constructor.
  - intros. exists (x !-> (aeval st a) ; st). constructor. reflexivity.
  - intros. inversion H as [| | c1' c2' H1 H2|]. subst. clear H.
    assert (H: exists st1, st =[ c1 ]=> st1). { apply IHc1. assumption. }
    clear H1. destruct H as [st1 H1].
    assert (H: exists st2, st1 =[ c2 ]=> st2). { apply IHc2. assumption. }
    clear H2. destruct H as [st2 H2].
    exists st2. apply E_Seq with (st':=st1); assumption.
  - intros. inversion H as [| | | b' c1' c2' H1 H2]. subst. clear H.
    assert (H: exists st1, st =[ c1 ]=> st1). { apply IHc1. assumption. }
    clear H1. destruct H as [st1 H1].
    assert (H: exists st2, st =[ c2 ]=> st2). { apply IHc2. assumption. }
    clear H2. destruct H as [st2 H2].
    destruct (beval st b) eqn:Hbeval.
    + exists st1. apply E_IfTrue; assumption.
    + exists st2. apply E_IfFalse; assumption.
  - inversion H.
Qed.

(* ADDITIONAL EXERCISES *)

Inductive sinstr : Type :=
| SPush (n : nat)
| SLoad (x : string)
| SPlus
| SMinus
| SMult.

Fixpoint s_execute(st : state)(stack : list nat) (prog : list sinstr) : list nat :=
  match prog with 
  | SPush n :: prog => s_execute st (n :: stack) prog
  | SLoad x :: prog => s_execute st (st x :: stack) prog 
  | SPlus :: prog   => match stack with 
                        | n2 :: n1 :: stack => s_execute st (n1 + n2 :: stack) prog 
                        | _ => s_execute st stack prog
                        end
  | SMinus :: prog => match stack with 
                        | n2 :: n1 :: stack => s_execute st (n1 - n2 :: stack ) prog 
                        | _ => s_execute st stack prog 
                        end 
  | SMult :: prog => match stack with 
                        | n2 :: n1 :: stack => s_execute st (n1*n2 :: stack) prog 
                        | _ => s_execute st stack prog 
                        end 
  | [] => stack 
  end.

Check s_execute.

Example s_execute1 : 
  s_execute empty_st [] [SPush 5; SPush 3; SPush 1; SMinus]
  = [2; 5].
Proof. reflexivity. Qed.

Example s_execute2 : 
  s_execute (X !-> 3) [3;4] [SPush 4; SLoad X; SMult; SPlus]
  = [15;4].
Proof. reflexivity. Qed.

Fixpoint s_compile (e : aexp) : list sinstr := 
  match e with 
  | ANum n => [SPush n]
  | AId x => [SLoad x]
  | APlus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SPlus]
  | AMinus a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMinus]
  | AMult a1 a2 => s_compile a1 ++ s_compile a2 ++ [SMult]
  end.

Example s_compile1 : 
  s_compile <{ X - (2*Y)}> 
  = [SLoad X; SPush 2; SLoad Y; SMult; SMinus].
Proof. reflexivity. Qed.

Theorem execute_app : forall st p1 p2 stack,
  s_execute st stack (p1 ++ p2) = s_execute st (s_execute st stack p1) p2.
Proof.
  intros st p1 p2.
  induction p1 as [ | s p1].
  - simpl. reflexivity.
  - intros stack. 
    destruct s;
    try (apply IHp1);
    (destruct stack; [apply IHp1 | destruct stack; try (apply IHp1)]).
Qed.

Lemma s_compile_correct_aux : forall st e stack,
  s_execute st stack (s_compile e) = aeval st e :: stack.
Proof.
  intros st e.
  induction e; intros;
  try (simpl; rewrite execute_app; rewrite execute_app; rewrite IHe1; rewrite IHe2);
  reflexivity.
Qed.

Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [] (s_compile e) = [ aeval st e ].
Proof.
  intros.
  apply s_compile_correct_aux.
Qed.

Fixpoint beval_short_circuit (st : state)(b : bexp) : bool :=
  match b with 
  | <{true}>       => true
  | <{false}>      => false
  | <{a1 = a2}>    => (aeval st a1) =? (aeval st a2)
  | <{ a1 <> a2}>  => negb ( (aeval st a1) =? (aeval st a2))
  | <{a1 <= a2}>   => (aeval st a1) <=? (aeval st a2)
  | <{a1 > a2}>    => negb((aeval st a1) <=? (aeval st a2))
  | <{~ b1}>        => negb (beval st b1)
  | <{b1 && b2}>   => match beval st b1 with 
                      | false => false
                      | true => beval st b2
                      end
  end.

Module BreakImp.

Inductive com : Type :=
| CSkip 
| CBreak 
| CAsgn (x : string)(a : aexp)
| CSeq (c1 c2 : com)
| CIf (b : bexp)(c1 c2 : com)
| CWhile (b : bexp) (c : com).

Notation "'break'" := CBreak (in custom com at level 0) : com_scope.
Notation "'skip'" := CSkip
  (in custom com at level 0) : com_scope.
Notation "x := y" := (CAsgn x y)
  (in custom com at level 0, x constr at level 0, y at level 85, no associativity,
    format "x := y") : com_scope.
Notation "x ; y" := (CSeq x y)
  (in custom com at level 90,
    right associativity,
    format "'[v' x ; '/' y ']'") : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" := (CIf x y z)
  (in custom com at level 89, x at level 99, y at level 99, z at level 99,
    format "'[v' 'if' x 'then' '/ ' y '/' 'else' '/ ' z '/' 'end' ']'") : com_scope.
Notation "'while' x 'do' y 'end'" := (CWhile x y)
  (in custom com at level 89, x at level 99, y at level 99,
    format "'[v' 'while' x 'do' '/ ' y '/' 'end' ']'") : com_scope.

Inductive result : Type :=
  | SContinue
  | SBreak.

Reserved Notation "st '=[' c ']=>' st' '/' s"
  (at level 40, c custom com at level 99, st' constr at next level).

Inductive ceval : com -> state -> result -> state -> Prop :=
  | E_Skip : forall st, 
        st =[ CSkip ]=> st / SContinue
  | E_Break : forall st,
        st =[ break ]=> st / SBreak
  | E_Asgn : forall st a n x,
        aeval st a = n -> 
        st =[ x := a ]=> ( x !-> n ; st) / SContinue
  | E_Seq1 : forall c1 c2 st st',
        st  =[ c1 ]=> st' / SBreak  ->
        st  =[ c1 ; c2 ]=> st' / SBreak
  | E_Seq2 : forall c1 c2 st st' st'' s,
        st  =[ c1 ]=> st' / SContinue  ->
        st' =[ c2 ]=> st'' / s  ->
        st  =[ c1 ; c2 ]=> st'' / s
  | E_IfTrue : forall st st' b c1 c2 s,
        beval st b = true ->
        st =[ c1 ]=> st' / s ->
        st =[ if b then c1 else c2 end]=> st' / s
  | E_IfFalse : forall st st' b c1 c2 s,
        beval st b = false ->
        st =[ c2 ]=> st' / s ->
        st =[ if b then c1 else c2 end]=> st' / s
  | E_WhileFalse : forall b st c,
        beval st b = false ->
        st =[ while b do c end ]=> st / SContinue
  | E_WhileTrue1 : forall st st' b c,
        beval st b = true ->
        st  =[ c ]=> st' / SBreak ->
        st  =[ while b do c end ]=> st' / SContinue
  | E_WhileTrue2 : forall st st' st'' b c,
        beval st b = true ->
        st  =[ c ]=> st' / SContinue ->
        st' =[ while b do c end ]=> st'' / SContinue ->
        st  =[ while b do c end ]=> st'' / SContinue

  where "st '=[' c ']=>' st' '/' s" := (ceval c st s st').


Theorem break_ignore : forall c st st' s,
  st =[ break; c ]=> st' / s ->
  st = st'.
Proof.
  intros.
  inversion H as [| | | c1 c2 st0 st'0 Hbreak | c1 c2 st0 st'0 st''0 s' Hbreak | | | | | ];
  inversion Hbreak.
  reflexivity.
Qed.

Theorem while_continue : forall b c st st' s,
  st =[ while b do c end ]=> st' / s -> 
  s = SContinue.
Proof.
  intros.
  inversion H; reflexivity.
Qed.

Theorem while_stops_on_break : forall b c st st', 
  beval st b = true -> 
  st =[ c ]=> st' / SBreak -> 
  st =[ while b do c end ]=> st' / SContinue.
Proof.
  intros.
  inversion H0; subst; constructor; assumption. 
Qed.

Theorem seq_continue : forall c1 c2 st st' st'',
  st =[ c1 ]=> st' / SContinue -> 
  st' =[ c2 ]=> st'' / SContinue ->
  st =[ c1 ; c2 ]=> st'' / SContinue.
Proof.
  intros. 
  apply E_Seq2 with (st' := st'); assumption.
Qed.

Theorem seq_stops_on_break : forall c1 c2 st st',
  st =[ c1 ]=> st' / SBreak -> 
  st =[ c1 ; c2 ]=> st' / SBreak.
Proof.
  intros. 
  apply E_Seq1; assumption.
Qed.


Theorem while_break_true : forall b c st st',
  st =[ while b do c end ]=> st' / SContinue -> 
  beval st' b = true -> 
  exists st'', st'' =[ c ]=> st' / SBreak.
Proof.
  intros b c st st' H E'.
  remember <{ while b do c end}> as whiledef eqn:Hwhiledef.
  induction H as [| | | | | | | b' st c' contra HH| |st st' st'' b' c' _ _ _ _ IH];
    try discriminate;
    injection Hwhiledef as Hb Hc;
    subst.
  - rewrite contra in E'. discriminate.
  - exists st. assumption.
  - apply IH. 
    + reflexivity.
    + assumption.
Qed. 

Theorem ceval_deterministic: forall (c:com) st st1 st2 s1 s2,
     st =[ c ]=> st1 / s1 ->
     st =[ c ]=> st2 / s2 ->
     st1 = st2 /\ s1 = s2.
Proof.
  intros c st st1 st2 s1 s2 E1 E2.
  generalize dependent st2.
  generalize dependent s2.
  induction E1;
    intros s2 st2 E2;
    inversion E2 as [ | | | | | | | | | ];
    subst;
    try (split; reflexivity);
    try (apply IHE1; assumption);
    try (rewrite H in H0; discriminate).
  + destruct (IHE1 SContinue st'0).
    * assumption.
    * discriminate. 
  + destruct (IHE1_1 SBreak st2).
    * assumption.
    * discriminate.
  + destruct (IHE1_1 SContinue st'0).
    * assumption.
    * subst. apply IHE1_2. assumption.
  + split.
    * apply IHE1 with SBreak. assumption.
    * reflexivity.
  + destruct (IHE1 SContinue st'0).
    * assumption.
    * discriminate.
  + destruct (IHE1_1 SBreak st2).
    * assumption.
    * discriminate.
  + destruct (IHE1_1 SContinue st'0).
    * assumption.
    * subst. apply IHE1_2. assumption.
Qed.

End BreakImp.

Module ForImp.

Inductive com : Type :=
  | CSkip
  | CBreak
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com)
  | CFor (b : bexp) (pre post c : com).

Notation "'break'" := CBreak (in custom com at level 0).
Notation "'skip'"  :=
         CSkip (in custom com at level 0) : com_scope.
Notation "x := y"  :=
         (CAsgn x y)
            (in custom com at level 0, x constr at level 0,
             y at level 85, no associativity) : com_scope.
Notation "x ; y" :=
         (CSeq x y)
           (in custom com at level 90, right associativity) : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" :=
         (CIf x y z)
           (in custom com at level 89, x at level 99,
            y at level 99, z at level 99) : com_scope.
Notation "'while' x 'do' y 'end'" :=
         (CWhile x y)
            (in custom com at level 89, x at level 99, y at level 99) : com_scope.
Notation "'for' pre b post 'do' c 'end'" :=
         (CFor b pre post c)
            (in custom com at level 89, pre at level 99, b at level 99, post at level 99, c at level 99) : com_scope.

Inductive result : Type :=
  | SContinue
  | SBreak.

Reserved Notation "st '=[' c ']=>' st' '/' s"
     (at level 40, c custom com at level 99, st' constr at next level).

Inductive ceval : com -> state -> result -> state -> Prop :=
  | E_Skip : forall st,
      st =[ skip ]=> st / SContinue
  | E_Break : forall st,
      st =[ break ]=> st / SBreak
  | E_Asgn  : forall st a n x,
      aeval st a = n ->
      st =[ x := a ]=> (x !-> n ; st) / SContinue
  | E_Seq1 : forall c1 c2 st st',
      st  =[ c1 ]=> st' / SBreak  ->
      st  =[ c1 ; c2 ]=> st' / SBreak
  | E_Seq2 : forall c1 c2 st st' st'' s,
      st  =[ c1 ]=> st' / SContinue  ->
      st' =[ c2 ]=> st'' / s  ->
      st  =[ c1 ; c2 ]=> st'' / s
  | E_IfTrue : forall st st' b c1 c2 s,
      beval st b = true ->
      st =[ c1 ]=> st' / s ->
      st =[ if b then c1 else c2 end]=> st' / s
  | E_IfFalse : forall st st' b c1 c2 s,
      beval st b = false ->
      st =[ c2 ]=> st' / s ->
      st =[ if b then c1 else c2 end]=> st' / s
  | E_WhileFalse : forall b st c,
      beval st b = false ->
      st =[ while b do c end ]=> st / SContinue
  | E_WhileTrue1 : forall st st' b c,
      beval st b = true ->
      st  =[ c ]=> st' / SBreak ->
      st  =[ while b do c end ]=> st' / SContinue
  | E_WhileTrue2 : forall st st' st'' b c,
      beval st b = true ->
      st  =[ c ]=> st' / SContinue ->
      st' =[ while b do c end ]=> st'' / SContinue ->
      st  =[ while b do c end ]=> st'' / SContinue
  | E_For : forall b st st' pre post c s,
      st =[ pre ; while b do (c ; post) end ]=> st' / s ->
      st =[ CFor b pre post c ]=> st' / s

  where "st '=[' c ']=>' st' '/' s" := (ceval c st s st').

Theorem ceval_deterministic: forall (c:com) st st1 st2 s1 s2,
     st =[ c ]=> st1 / s1 ->
     st =[ c ]=> st2 / s2 ->
     st1 = st2 /\ s1 = s2.
Proof.
  intros c st st1 st2 s1 s2 E1 E2.
  generalize dependent st2.
  generalize dependent s2.
  induction E1;
    intros s2 st2 E2;
    inversion E2 as [ | | | | | | | | | | ];
    subst;
    try (split; reflexivity);
    try (apply IHE1; assumption);
    try (rewrite H in H0; discriminate).
  + destruct (IHE1 SContinue st'0).
    * assumption.
    * discriminate.
  + destruct (IHE1_1 SBreak st2).
    * assumption.
    * discriminate.
  + destruct (IHE1_1 SContinue st'0).
    * assumption.
    * subst. apply IHE1_2. assumption.
  + split.
    * apply IHE1 with SBreak. assumption.
    * reflexivity.
  + destruct (IHE1 SContinue st'0).
    * assumption.
    * discriminate.
  + destruct (IHE1_1 SBreak st2).
    * assumption.
    * discriminate.
  + destruct (IHE1_1 SContinue st'0).
    * assumption.
    * subst. apply IHE1_2. assumption.
Qed.

End ForImp.