Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 170 insertions, 0 deletions

diff --git a/theories7/Lists/Streams.v b/theories7/Lists/Streams.v
new file mode 100755
index 00000000..ccfc4895
--- /dev/null
+++ b/theories7/Lists/Streams.v
@@ -0,0 +1,170 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Streams.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*)
+
+Set Implicit Arguments.
+
+(** Streams *)
+
+Section Streams.
+
+Variable A : Set.
+
+CoInductive Set Stream   := Cons : A->Stream->Stream.
+
+
+Definition hd  := 
+  [x:Stream] Cases x of (Cons a _) => a end.
+
+Definition tl  := 
+  [x:Stream] Cases x of (Cons _ s) => s end.
+
+
+Fixpoint Str_nth_tl [n:nat] : Stream->Stream := 
+  [s:Stream] Cases n of
+	          O    => s
+		|(S m) => (Str_nth_tl m (tl s))
+	    end.
+
+Definition Str_nth : nat->Stream->A := [n:nat][s:Stream](hd (Str_nth_tl n s)).
+
+
+Lemma unfold_Stream :(x:Stream)x=(Cases x of (Cons a s) => (Cons a s) end). 
+Proof.
+  Intro x.
+  Case x.
+  Trivial.
+Qed.
+
+Lemma tl_nth_tl : (n:nat)(s:Stream)(tl (Str_nth_tl n s))=(Str_nth_tl n (tl s)).
+Proof.
+  Induction n; Simpl; Auto.
+Qed.
+Hints Resolve tl_nth_tl : datatypes v62.
+
+Lemma Str_nth_tl_plus 
+: (n,m:nat)(s:Stream)(Str_nth_tl n (Str_nth_tl m s))=(Str_nth_tl (plus n m) s).
+Induction n; Simpl; Intros; Auto with datatypes.
+Rewrite <- H.
+Rewrite tl_nth_tl; Trivial with datatypes.
+Qed.
+
+Lemma Str_nth_plus 
+  : (n,m:nat)(s:Stream)(Str_nth n (Str_nth_tl m s))=(Str_nth (plus n m) s).
+Intros; Unfold Str_nth; Rewrite Str_nth_tl_plus; Trivial with datatypes.
+Qed.
+
+(** Extensional Equality between two streams  *)
+
+CoInductive EqSt  : Stream->Stream->Prop := 
+	    eqst : (s1,s2:Stream)
+		   ((hd s1)=(hd s2))->
+		   (EqSt (tl s1) (tl s2))
+                    ->(EqSt s1 s2).
+
+(** A coinduction principle *)
+
+Tactic Definition CoInduction proof := 
+  Cofix proof; Intros; Constructor;
+    [Clear proof | Try (Apply proof;Clear proof)].
+
+
+(** Extensional equality is an equivalence relation *)
+
+Theorem  EqSt_reflex : (s:Stream)(EqSt s s).
+CoInduction EqSt_reflex.
+Reflexivity.
+Qed.
+
+Theorem sym_EqSt : 
+ (s1:Stream)(s2:Stream)(EqSt s1 s2)->(EqSt s2 s1).
+(CoInduction Eq_sym).
+Case H;Intros;Symmetry;Assumption.
+Case H;Intros;Assumption.
+Qed.
+
+
+Theorem trans_EqSt : 
+ (s1,s2,s3:Stream)(EqSt s1 s2)->(EqSt s2 s3)->(EqSt s1 s3).
+(CoInduction Eq_trans).
+Transitivity (hd s2).
+Case H; Intros; Assumption.
+Case H0; Intros; Assumption.
+Apply (Eq_trans (tl s1) (tl s2) (tl s3)).
+Case H;  Trivial with datatypes.
+Case H0; Trivial with datatypes.
+Qed.
+
+(** The definition given is equivalent to require the elements at each
+    position to be equal *)
+
+Theorem eqst_ntheq :
+  (n:nat)(s1,s2:Stream)(EqSt s1 s2)->(Str_nth n s1)=(Str_nth n s2).
+Unfold Str_nth; Induction n.
+Intros s1 s2 H; Case H; Trivial with datatypes.
+Intros m hypind.
+Simpl.
+Intros s1 s2 H.
+Apply hypind.
+Case H; Trivial with datatypes.
+Qed.
+
+Theorem ntheq_eqst : 
+  (s1,s2:Stream)((n:nat)(Str_nth n s1)=(Str_nth n s2))->(EqSt s1 s2).
+(CoInduction Equiv2).
+Apply (H O).
+Intros n; Apply (H (S n)).
+Qed.
+
+Section Stream_Properties.
+
+Variable P : Stream->Prop.
+
+(*i
+Inductive Exists : Stream -> Prop :=
+  | Here    : forall x:Stream, P x -> Exists x
+  | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
+i*)
+
+Inductive   Exists :  Stream -> Prop :=
+   Here    : (x:Stream)(P x) ->(Exists x) |
+   Further : (x:Stream)(Exists (tl x))->(Exists x).
+
+CoInductive ForAll : Stream  -> Prop :=
+    forall : (x:Stream)(P x)->(ForAll (tl x))->(ForAll x).
+
+
+Section Co_Induction_ForAll.
+Variable   Inv        :  Stream -> Prop.
+Hypothesis InvThenP   : (x:Stream)(Inv x)->(P x).
+Hypothesis InvIsStable: (x:Stream)(Inv x)->(Inv (tl x)).
+
+Theorem ForAll_coind : (x:Stream)(Inv x)->(ForAll x).
+(CoInduction ForAll_coind);Auto.
+Qed.
+End Co_Induction_ForAll.
+
+End Stream_Properties.
+
+End Streams.
+
+Section Map.
+Variables A,B : Set.
+Variable  f   : A->B.
+CoFixpoint map : (Stream A)->(Stream B) :=
+ [s:(Stream A)](Cons (f (hd s)) (map (tl s))).
+End Map.
+
+Section Constant_Stream.
+Variable A : Set.
+Variable a : A.
+CoFixpoint const : (Stream A) := (Cons a const).
+End Constant_Stream.
+
+Unset Implicit Arguments.