Extra stuff from today

[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.

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''.

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.

 left. exists (c2, st). apply ES_Seq_c2.

 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 Here *)

Theorem ceval_small_big:

 forall c st st',

   ceval c st st' <->

   ceval_small_to_the_end c st st'.

Proof.

Admitted.

--
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