diff options
Diffstat (limited to 'theories/Lists/Streams.v')
-rw-r--r-- | theories/Lists/Streams.v | 84 |
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. |