Updated extra code

[Jay McCarthy]

Inductive ceval_small : com -> state -> com -> state -> Prop :=
| ES_Ass : forall st a1 n X,
aeval st a1 = n ->
ceval_small (X ::= a1) (st)
(SKIP) (update st X n)
| ES_Seq_c1 : forall c1 c1' c2 st st',
ceval_small (c1) (st)
(c1') (st') ->
ceval_small (c1 ; c2) (st)
(c1' ; c2) (st')
| ES_Seq_c2 : forall c2 st,
ceval_small (SKIP ; c2) (st)
c2 (st)
| ES_IfTrue : forall st b1 c1 c2,
beval st b1 = true ->
ceval_small (IFB b1 THEN c1 ELSE c2 FI) st
c1 st
| ES_IfFalse : forall st b1 c1 c2,
beval st b1 = false ->
ceval_small (IFB b1 THEN c1 ELSE c2 FI) st
c2 st
| ES_WhileEnd : forall b1 st c1,
beval st b1 = false ->
ceval_small (WHILE b1 DO c1 END) st
(SKIP) st
| ES_WhileLoop : forall st b1 c1,
beval st b1 = true ->
ceval_small (WHILE b1 DO c1 END) st
(c1 ; (WHILE b1 DO c1 END)) st.

Theorem ceval_small_dec:
forall c st,
{ p | let (c',st') := (p:com*state) in ceval_small c st c' st' }
+ { forall c' st', ~ ceval_small c st c' st' }.
Proof.
com_cases (induction c) Case; intros st.

Case "SKIP".
right. intros c' st' H.
inversion H.

Case "::=".
left. exists (SKIP, update st i (aeval st a)).
apply ES_Ass. reflexivity.

Case ";".
com_cases (destruct c1) SCase.
SCase "SKIP".
left. exists (c2, st). apply ES_Seq_c2.

SCase "::=".
destruct (IHc1 st) as [ [[c1' st'] IHc1st] | FAILED ].
left. exists ((c1';c2), st'). apply ES_Seq_c1. apply IHc1st.
right. intros c' st' H. unfold not in FAILED.
(* XXX After class 1 *)
inversion H. apply FAILED in H5. auto.

SCase ";".
destruct (IHc1 st) as [ [[c1' st'] IHc1st] | FAILED ].
left. exists ((c1';c2), st'). apply ES_Seq_c1. apply IHc1st.
right. intros c' st' H. unfold not in FAILED.
inversion H. apply FAILED in H5. auto.

SCase "IFB".
destruct (IHc1 st) as [ [[c1' st'] IHc1st] | FAILED ].
left. exists ((c1';c2), st'). apply ES_Seq_c1. apply IHc1st.
right. intros c' st' H. unfold not in FAILED.
inversion H. apply FAILED in H5. auto.

SCase "WHILE".
destruct (IHc1 st) as [ [[c1' st'] IHc1st] | FAILED ].
left. exists ((c1';c2), st'). apply ES_Seq_c1. apply IHc1st.
right. intros c' st' H. unfold not in FAILED.
inversion H. apply FAILED in H5. auto.

Case "IFB".
clear IHc1 IHc2.
left. remember (beval st b) as beval_res.
destruct beval_res.
exists (c1, st). apply ES_IfTrue. symmetry. auto.
exists (c2, st). apply ES_IfFalse. symmetry. auto.

Case "WHILE".
clear IHc.
left. remember (beval st b) as beval_res.
destruct beval_res.
exists ((c ; WHILE b DO c END), st). apply ES_WhileLoop.
symmetry. auto.
exists (SKIP, st). apply ES_WhileEnd.
symmetry. auto.
Qed.

Set Extraction AccessOpaque.
Extraction ceval_small_dec.

(*
let rec ceval_big c st =
(match (ceval_small_dec c st) with
| Inleft (Pair (c', st')) ->
ceval_big c' st'
| InRight ->
st).
*)

Inductive ceval_small_to_the_end : com -> state -> state -> Prop :=
| ESE_skip :
forall st,
ceval_small_to_the_end SKIP st st
| ESE_trans :
forall c c' st st' st'',
ceval_small c st c' st' ->
ceval_small_to_the_end c' st' st'' ->
ceval_small_to_the_end c st st''.

(* No members:
Inductive None : Set :=
| N1 : (forall n:Prop, n -> nat) -> None.
*)

CoInductive co_ceval_small_to_the_end : com -> state -> state -> Prop :=
| cESE_skip :
forall st,
co_ceval_small_to_the_end SKIP st st
| cESE_trans :
forall c c' st st' st'',
ceval_small c st c' st' ->
co_ceval_small_to_the_end c' st' st'' ->
co_ceval_small_to_the_end c st st''.


--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93