Library Coq.Lists.Streams

Set Implicit Arguments.

CoInductive Stream (A : Type) :=
  Cons : A -> Stream A -> Stream A.

Section Streams.
  Variable A : Type.

  Notation Stream := (Stream A).

Definition hd (x:Stream) := match x with
                            | Cons a _ => a
                            end.

Definition tl (x:Stream) := match x with
                            | Cons _ s => s
                            end.

Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream :=
  match n with
  | O => s
  | S m => Str_nth_tl m (tl s)
  end.

Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).

Lemma unfold_Stream :
 forall x:Stream, x = match x with
                      | Cons a s => Cons a s
                      end.

Lemma tl_nth_tl :
 forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).
#[local]
Hint Resolve tl_nth_tl: datatypes.

Lemma Str_nth_tl_plus :
 forall (n m:nat) (s:Stream),
   Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.

Lemma Str_nth_plus :
 forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.

CoInductive EqSt (s1 s2: Stream) : Prop :=
    eqst :
        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.

Ltac coinduction proof :=
  cofix proof; intros; constructor;
   [ clear proof | try (apply proof; clear proof) ].

Theorem EqSt_reflex : forall s:Stream, EqSt s s.

Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.

Theorem trans_EqSt :
 forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.

Theorem eqst_ntheq :
 forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.

Theorem ntheq_eqst :
 forall s1 s2:Stream,
   (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.

Section Stream_Properties.

Variable P : Stream -> Prop.


Inductive Exists ( x: Stream ) : Prop :=
  | Here : P x -> Exists x
  | Further : Exists (tl x) -> Exists x.

CoInductive ForAll (x: Stream) : Prop :=
    HereAndFurther : P x -> ForAll (tl x) -> ForAll x.

Lemma ForAll_Str_nth_tl : forall m x, ForAll x -> ForAll (Str_nth_tl m x).

Section Co_Induction_ForAll.
Variable Inv : Stream -> Prop.
Hypothesis InvThenP : forall x:Stream, Inv x -> P x.
Hypothesis InvIsStable : forall x:Stream, Inv x -> Inv (tl x).

Theorem ForAll_coind : forall x:Stream, Inv x -> ForAll x.
End Co_Induction_ForAll.

End Stream_Properties.

End Streams.

Section Map.
Variables A B : Type.
Variable f : A -> B.
CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)).

Lemma Str_nth_tl_map : forall n s, Str_nth_tl n (map s)= map (Str_nth_tl n s).

Lemma Str_nth_map : forall n s, Str_nth n (map s)= f (Str_nth n s).

Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P
(map s)) S <-> ForAll P (map S).

Lemma Exists_map : forall (P:Stream B -> Prop) (S:Stream A), Exists (fun s => P
(map s)) S -> Exists P (map S).

End Map.

Section Constant_Stream.
Variable A : Type.
Variable a : A.
CoFixpoint const : Stream A := Cons a const.
End Constant_Stream.

Section Zip.

Variable A B C : Type.
Variable f: A -> B -> C.

CoFixpoint zipWith (a:Stream A) (b:Stream B) : Stream C :=
Cons (f (hd a) (hd b)) (zipWith (tl a) (tl b)).

Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B),
 Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b).

Lemma Str_nth_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth n (zipWith a
 b)= f (Str_nth n a) (Str_nth n b).

End Zip.

Unset Implicit Arguments.