Require Export Imp.

Example ceval_example3:
    (IFB BLe (ANum 2) (ANum 3) THEN Y ::= ANum 1 ELSE Y ::= ANum 2 FI) 
    / empty_state ==> (update empty_state Y 1).
Proof.
  Admitted.

(* Hint:  sequencing is right associative *)
Example ceval_example2:
    (X ::= ANum 0; Y ::= ANum 1; Z ::= ANum 2) / empty_state ==>
    (update (update (update empty_state X 0) Y 1) Z 2).
Proof. 
  (* FILL IN HERE *) Admitted.

Lemma swap : forall n m : nat,
  (Z ::= AId X; X ::= AId Y; Y ::= AId X)
  / (update (update empty_state X n) Y m) ==>
  (update (update (update (update (update empty_state X n) Y m) Z n) X m) Y n).
Proof.
  Admitted.

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

Definition aequiv (a1 a2 : aexp) : Prop :=
  forall (st:state), 
    aeval st a1 = aeval st a2.

Definition bequiv (b1 b2 : bexp) : Prop :=
  forall (st:state), 
    beval st b1 = beval st b2.

Definition cequiv (c1 c2 : com) : Prop :=
  forall (st st':state), 
    (c1 / st ==> st') <-> (c2 / st ==> st').

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

Theorem aequiv_example:
  aequiv (AMinus (AId X) (AId X)) (ANum 0).
Proof.
  Admitted.

Theorem skip_left: forall c,
  cequiv 
     (SKIP; c) 
     c.
Proof. 
  Admitted.

Theorem IFB_true_simple: forall c1 c2,
  cequiv 
    (IFB BTrue THEN c1 ELSE c2 FI) 
    c1.
Proof. 
  Admitted.

Theorem IFB_true: forall b c1 c2,
     bequiv b BTrue  ->
     cequiv 
       (IFB b THEN c1 ELSE c2 FI) 
       c1.
Proof.
  Admitted.

Theorem loop_unrolling: forall b c,
  cequiv
    (WHILE b DO c END)
    (IFB b THEN (c; WHILE b DO c END) ELSE SKIP FI).
Proof.
  Admitted.

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

Theorem identity_assignment_first_try : forall (x:id),
  cequiv
    (x ::= AId x)
    SKIP.
Proof. 
   unfold cequiv.  intros. split; intro H.
     Case "->". 
       inversion H; subst.  simpl.
       replace (update st x (st x)) with st.  
       constructor. 
Admitted.

Axiom functional_extensionality : forall {X Y: Type} {f g : X -> Y},
    (forall (x: X), f x = g x) ->  f = g.

Theorem identity_assignment : forall (x:id),
  cequiv
    (x ::= AId x)
    SKIP.
Proof. 
   unfold cequiv.  intros. split; intro H.
     Case "->". 
       inversion H; subst. simpl.
       replace (update st x (st x)) with st.  
       constructor. 
       apply functional_extensionality. intro. rewrite update_same; reflexivity.  
     Case "<-".
       inversion H; subst. 
       assert (st' = (update st' x (st' x))).
          apply functional_extensionality. intro. rewrite update_same; reflexivity.
       rewrite H0 at 2. 
       constructor. reflexivity.
Qed.

Theorem assign_aequiv : forall x e,
  aequiv (AId x) e -> 
  cequiv SKIP (x ::= e).
Proof.
  Admitted.

Theorem CAss_congruence : forall i a1 a1',
  aequiv a1 a1' ->
  cequiv (CAss i a1) (CAss i a1').
Proof.
  Admitted.