diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:11:51 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-21 01:11:51 +0000 |
commit | 0940e93d753c2df977e44d40f5b9d9652e881def (patch) | |
tree | 918eaeeae94c5875ee45d2bead6b7cd91f09e9f2 /theories/Lists/Streams.v | |
parent | e7c6f94b15d15dbf0d15f08982f04076abdd0fa7 (diff) |
theories/Lists
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@508 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/Streams.v')
-rwxr-xr-x | theories/Lists/Streams.v | 165 |
1 files changed, 165 insertions, 0 deletions
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v new file mode 100755 index 000000000..6b7ffca5e --- /dev/null +++ b/theories/Lists/Streams.v @@ -0,0 +1,165 @@ + +(* $Id$ *) + +Implicit Arguments On. + +Section Streams. (* The set of streams : definition *) + +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. +Save. +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. +Save. + +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. +Save. + +(* 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] := + [ <:tactic:<( 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. + +(* +Inductive Exists : Stream -> Prop := + Here : (x:Stream)(P x) ->(Exists x) | + Further : (x:Stream)~(P x)->(Exists (tl x))->(Exists x). +*) + +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. +Variables A : Set. +Variable a : A. +CoFixpoint const : (Stream A) := (Cons a const). +End Constant_Stream. + + + +Implicit Arguments Off. |