Code from class

[Jay McCarthy]

I added an example of doing coinduction in a proof.

Jay


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

(* XXX End of class 2 *)
CoInductive co_ceval_small_to_the_end : com -> state -> Set :=
| cESE_done :
forall c st,
(forall c' st', ~ ceval_small c st c' st') ->
co_ceval_small_to_the_end c st
| cESE_trans :
forall c c' st st',
ceval_small c st c' st' ->
co_ceval_small_to_the_end c' st' ->
co_ceval_small_to_the_end c st.

(* XXX Make a list where the tail has to be bigger than front *)

CoInductive NListBT : nat -> Set :=
| NListBT_nil :
forall n,
NListBT n
| NListBT_cons :
forall (n m:nat),
m > n ->
NListBT m ->
NListBT n.

Program CoFixpoint nlist_from (n:nat) : (NListBT n) :=
NListBT_cons n (n + 4) _ (nlist_from (n + 4)).
Obligation 1.
omega.
Qed.

Print nlist_from_obligation_1.

(* Fails:
Theorem nlist_from_exists:
forall n,
NListBT n.
Proof.
intros n.
cofix. exact nlist_from_exists.
Qed.
*)

Theorem nlist_from_exists:
forall n,
NListBT n.
Proof.
cofix.
intros n.
apply NListBT_cons with (m:=n + 4).
omega.
apply nlist_from_exists.
Qed.

Print nlist_from_exists.

CoFixpoint co_eval_small_to_the_end_interp (c:com) (st:state)
: co_ceval_small_to_the_end c st :=
match (ceval_small_dec c st) with
| inleft (exist (c', st') SMALL) =>
cESE_trans c c' st st' SMALL (co_eval_small_to_the_end_interp c' st')
| inright DONE =>
cESE_done c st DONE
end.

Print loop.

Check co_eval_small_to_the_end_interp loop empty_state.
Eval compute in (co_eval_small_to_the_end_interp loop empty_state).

Extraction co_eval_small_to_the_end_interp.

CoInductive IList (X:Set) : Set :=
| IList_cons : X -> IList X -> IList X.

CoFixpoint nats_f_from (X:Set) (f:nat -> X) (i:nat) : IList X :=
IList_cons X (f i) (nats_f_from X f (S i)).

Definition nats_f (X:Set) (f:nat -> X) := nats_f_from X f 0.

Definition nats := nats_f nat (fun x => x).

(*
CoFixpoint filter (X:Set) (f:X -> bool) (l:IList X) : IList X :=
match l with
| IList_cons x rst =>
if f x then
IList_cons X x (filter X f rst)
else
(filter X f rst)
end.
*)

(* (first (filter odd? (filter even? nats))) *)

Theorem ceval_small_big:
forall c st st',
ceval c st st' <->
ceval_small_to_the_end c st st'.
Proof.
split.

Case "Forward".
intros CE.
ceval_cases (induction CE) SCase.

Case "Backwards".

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