1 files changed, 78 insertions, 6 deletions

diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 7bc6a09d..49990502 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Streams.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Streams.v 9967 2007-07-11 15:25:03Z roconnor $ i*)
 
 Set Implicit Arguments.
 
@@ -14,9 +14,9 @@ Set Implicit Arguments.
 
 Section Streams.
 
-Variable A : Set.
+Variable A : Type.
 
-CoInductive Stream : Set :=
+CoInductive Stream : Type :=
     Cons : A -> Stream -> Stream.
 
 
@@ -146,6 +146,15 @@ Inductive Exists ( x: Stream ) : Prop :=
 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).
+Proof.
+induction m.
+ tauto.
+intros x [_ H].
+simpl.
+apply IHm.
+assumption.
+Qed.
 
 Section Co_Induction_ForAll.
 Variable Inv : Stream -> Prop.
@@ -162,15 +171,78 @@ End Stream_Properties.
 End Streams.
 
 Section Map.
-Variables A B : Set.
+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).
+Proof.
+induction n.
+reflexivity.
+simpl.
+intros s.
+apply IHn.
+Qed.
+
+Lemma Str_nth_map : forall n s, Str_nth n (map s)= f (Str_nth n s).
+Proof.
+intros n s.
+unfold Str_nth.
+rewrite Str_nth_tl_map.
+reflexivity.
+Qed.
+
+Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P
+(map s)) S <-> ForAll P (map S).
+Proof.
+intros P S.
+split; generalize S; clear S; cofix; intros S; constructor;
+destruct H as [H0 H]; firstorder.
+Qed.
+
+Lemma Exists_map : forall (P:Stream B -> Prop) (S:Stream A), Exists (fun s => P
+(map s)) S -> Exists P (map S).
+Proof.
+intros P S H.
+(induction H;[left|right]); firstorder.
+Defined.
+
 End Map.
 
 Section Constant_Stream.
-Variable A : Set.
+Variable A : Type.
 Variable a : A.
 CoFixpoint const  : Stream A := Cons a const.
 End Constant_Stream.
 
-Unset Implicit Arguments.
\ No newline at end of file
+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).
+Proof.
+induction n.
+reflexivity.
+intros [x xs] [y ys].
+unfold Str_nth in *.
+simpl in *.
+apply IHn.
+Qed.
+
+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).
+Proof.
+intros.
+unfold Str_nth.
+rewrite Str_nth_tl_zipWith.
+reflexivity.
+Qed.
+
+End Zip.
+
+Unset Implicit Arguments.