diff options
Diffstat (limited to 'theories7/Lists/Streams.v')
| -rwxr-xr-x | theories7/Lists/Streams.v | 170 |
1 files changed, 0 insertions, 170 deletions
diff --git a/theories7/Lists/Streams.v b/theories7/Lists/Streams.v deleted file mode 100755 index ccfc4895..00000000 --- a/theories7/Lists/Streams.v +++ /dev/null @@ -1,170 +0,0 @@ -(************************************************************************) -(* 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. |