(* G54DTP Dependently Typed Programming.
Inductive and Coinductive predicates on streams.
Venanzio Capretta, March 2011.
*)
Require Import Arith.
Require Import Streams.
(* Streams are infinite sequences of elements. *)
Print Stream.
Set Implicit Arguments.
CoFixpoint s0: Stream nat := Cons 4 (Cons 2 (Cons 3 s0)).
(* Unfolding a stream n times: useful in proofs. *)
Fixpoint sunf (A:Set)(s:Stream A)(n:nat): Stream A :=
match n with
O => s
| S n' => match s with
Cons a s' => Cons a (sunf s' n')
end
end.
Eval simpl in (sunf s0 10).
Section StreamPredicates.
Variable A:Set.
Variable P:A -> Prop.
(* (Sometime s) is true if there is an element of the stream s
that satisfies the predicate P.
*)
Inductive Sometime: Stream A -> Prop :=
st_head: forall (a:A)(s:Stream A), P a -> Sometime (Cons a s)
| st_tail: forall (a:A)(s:Stream A), Sometime s ->
Sometime (Cons a s).
(* (Forever s) is satisfied if all elements of the stream s
satisfy the predicate P.
*)
CoInductive ForEver: Stream A -> Prop :=
forever: forall (a:A)(s:Stream A), P a -> ForEver s ->
ForEver (Cons a s).
(* (Eventually s) is satisfied if P is satisfied
after a certain point.
*)
Inductive Eventually: Stream A -> Prop :=
ev_now: forall s, ForEver s -> Eventually s
| ev_later: forall (a:A)(s:Stream A), Eventually s ->
Eventually (Cons a s).
End StreamPredicates.
(* When we close the session, variables become arguments. *)
Check Sometime.
Check ForEver.
Check Eventually.
Require Import Even.
Check even.
Lemma evs0: Sometime even s0.
Proof.
rewrite unfold_Stream; simpl.
apply st_head.
repeat (apply even_S; apply odd_S).
exact even_O.
Qed.
(* A different way to prove the same statement. *)
Lemma evs0': Sometime even s0.
Proof.
rewrite unfold_Stream; simpl.
apply st_tail.
apply st_head.
repeat (apply even_S; apply odd_S).
exact even_O.
Qed.
CoFixpoint s1:= Cons 1 (Cons 5 s1).
Lemma ods1: ForEver odd s1.
Proof.
cofix.
rewrite unfold_Stream; simpl.
apply forever.
apply odd_S; apply even_O.
apply forever.
repeat (apply odd_S; apply even_S).
apply odd_S; apply even_O.
apply ods1.
Qed.
Definition s2 := Cons 2 (Cons 0 s1).
Lemma evods2: Eventually odd s2.
Proof.
rewrite unfold_Stream; simpl.
apply ev_later.
apply ev_later.
apply ev_now.
exact ods1.
Qed.