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