← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Lists/Streams.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Lists/Streams.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Streams.v 9967 2007-07-11 15:25:03Z roconnor $ i*)
 
10
 
 
11
Set Implicit Arguments.
 
12
 
 
13
(** Streams *)
 
14
 
 
15
Section Streams.
 
16
 
 
17
Variable A : Type.
 
18
 
 
19
CoInductive Stream : Type :=
 
20
    Cons : A -> Stream -> Stream.
 
21
 
 
22
 
 
23
Definition hd (x:Stream) := match x with
 
24
                            | Cons a _ => a
 
25
                            end.
 
26
 
 
27
Definition tl (x:Stream) := match x with
 
28
                            | Cons _ s => s
 
29
                            end.
 
30
 
 
31
 
 
32
Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream :=
 
33
  match n with
 
34
  | O => s
 
35
  | S m => Str_nth_tl m (tl s)
 
36
  end.
 
37
 
 
38
Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).
 
39
 
 
40
 
 
41
Lemma unfold_Stream :
 
42
 forall x:Stream, x = match x with
 
43
                      | Cons a s => Cons a s
 
44
                      end. 
 
45
Proof.
 
46
  intro x.
 
47
  case x.
 
48
  trivial.
 
49
Qed.
 
50
 
 
51
Lemma tl_nth_tl :
 
52
 forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).
 
53
Proof.
 
54
  simple induction n; simpl in |- *; auto.
 
55
Qed.
 
56
Hint Resolve tl_nth_tl: datatypes v62.
 
57
 
 
58
Lemma Str_nth_tl_plus :
 
59
 forall (n m:nat) (s:Stream),
 
60
   Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.
 
61
simple induction n; simpl in |- *; intros; auto with datatypes.
 
62
rewrite <- H.
 
63
rewrite tl_nth_tl; trivial with datatypes.
 
64
Qed.
 
65
 
 
66
Lemma Str_nth_plus :
 
67
 forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.
 
68
intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus;
 
69
 trivial with datatypes.
 
70
Qed.
 
71
 
 
72
(** Extensional Equality between two streams  *)
 
73
 
 
74
CoInductive EqSt (s1 s2: Stream) : Prop :=
 
75
    eqst :
 
76
        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
 
77
 
 
78
(** A coinduction principle *)
 
79
 
 
80
Ltac coinduction proof :=
 
81
  cofix proof; intros; constructor;
 
82
   [ clear proof | try (apply proof; clear proof) ].
 
83
 
 
84
 
 
85
(** Extensional equality is an equivalence relation *)
 
86
 
 
87
Theorem EqSt_reflex : forall s:Stream, EqSt s s.
 
88
coinduction EqSt_reflex.
 
89
reflexivity.
 
90
Qed.
 
91
 
 
92
Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.
 
93
coinduction Eq_sym.
 
94
case H; intros; symmetry  in |- *; assumption.
 
95
case H; intros; assumption.
 
96
Qed.
 
97
 
 
98
 
 
99
Theorem trans_EqSt :
 
100
 forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.
 
101
coinduction Eq_trans.
 
102
transitivity (hd s2).
 
103
case H; intros; assumption.
 
104
case H0; intros; assumption.
 
105
apply (Eq_trans (tl s1) (tl s2) (tl s3)).
 
106
case H; trivial with datatypes.
 
107
case H0; trivial with datatypes.
 
108
Qed.
 
109
 
 
110
(** The definition given is equivalent to require the elements at each
 
111
    position to be equal *)
 
112
 
 
113
Theorem eqst_ntheq :
 
114
 forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
 
115
unfold Str_nth in |- *; simple induction n.
 
116
intros s1 s2 H; case H; trivial with datatypes.
 
117
intros m hypind.
 
118
simpl in |- *.
 
119
intros s1 s2 H.
 
120
apply hypind.
 
121
case H; trivial with datatypes.
 
122
Qed.
 
123
 
 
124
Theorem ntheq_eqst :
 
125
 forall s1 s2:Stream,
 
126
   (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.
 
127
coinduction Equiv2.
 
128
apply (H 0).
 
129
intros n; apply (H (S n)).
 
130
Qed.
 
131
 
 
132
Section Stream_Properties.
 
133
 
 
134
Variable P : Stream -> Prop.
 
135
 
 
136
(*i
 
137
Inductive Exists : Stream -> Prop :=
 
138
  | Here    : forall x:Stream, P x -> Exists x
 
139
  | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
 
140
i*)
 
141
 
 
142
Inductive Exists ( x: Stream ) : Prop :=
 
143
  | Here : P x -> Exists x
 
144
  | Further : Exists (tl x) -> Exists x.
 
145
 
 
146
CoInductive ForAll (x: Stream) : Prop :=
 
147
    HereAndFurther : P x -> ForAll (tl x) -> ForAll x.
 
148
 
 
149
Lemma ForAll_Str_nth_tl : forall m x, ForAll x -> ForAll (Str_nth_tl m x).
 
150
Proof.
 
151
induction m.
 
152
 tauto.
 
153
intros x [_ H].
 
154
simpl.
 
155
apply IHm.
 
156
assumption.
 
157
Qed.
 
158
 
 
159
Section Co_Induction_ForAll.
 
160
Variable Inv : Stream -> Prop.
 
161
Hypothesis InvThenP : forall x:Stream, Inv x -> P x.
 
162
Hypothesis InvIsStable : forall x:Stream, Inv x -> Inv (tl x).
 
163
 
 
164
Theorem ForAll_coind : forall x:Stream, Inv x -> ForAll x.
 
165
coinduction ForAll_coind; auto.
 
166
Qed.
 
167
End Co_Induction_ForAll.
 
168
 
 
169
End Stream_Properties.
 
170
 
 
171
End Streams.
 
172
 
 
173
Section Map.
 
174
Variables A B : Type.
 
175
Variable f : A -> B.
 
176
CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)).
 
177
 
 
178
Lemma Str_nth_tl_map : forall n s, Str_nth_tl n (map s)= map (Str_nth_tl n s).
 
179
Proof.
 
180
induction n.
 
181
reflexivity.
 
182
simpl.
 
183
intros s.
 
184
apply IHn.
 
185
Qed.
 
186
 
 
187
Lemma Str_nth_map : forall n s, Str_nth n (map s)= f (Str_nth n s).
 
188
Proof.
 
189
intros n s.
 
190
unfold Str_nth.
 
191
rewrite Str_nth_tl_map.
 
192
reflexivity.
 
193
Qed.
 
194
 
 
195
Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P
 
196
(map s)) S <-> ForAll P (map S).
 
197
Proof.
 
198
intros P S.
 
199
split; generalize S; clear S; cofix; intros S; constructor;
 
200
destruct H as [H0 H]; firstorder.
 
201
Qed.
 
202
 
 
203
Lemma Exists_map : forall (P:Stream B -> Prop) (S:Stream A), Exists (fun s => P
 
204
(map s)) S -> Exists P (map S).
 
205
Proof.
 
206
intros P S H.
 
207
(induction H;[left|right]); firstorder.
 
208
Defined.
 
209
 
 
210
End Map.
 
211
 
 
212
Section Constant_Stream.
 
213
Variable A : Type.
 
214
Variable a : A.
 
215
CoFixpoint const  : Stream A := Cons a const.
 
216
End Constant_Stream.
 
217
 
 
218
Section Zip.
 
219
 
 
220
Variable A B C : Type.
 
221
Variable f: A -> B -> C.
 
222
 
 
223
CoFixpoint zipWith (a:Stream A) (b:Stream B) : Stream C :=
 
224
Cons (f (hd a) (hd b)) (zipWith (tl a) (tl b)).
 
225
 
 
226
Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), 
 
227
 Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b).
 
228
Proof.
 
229
induction n.
 
230
reflexivity.
 
231
intros [x xs] [y ys].
 
232
unfold Str_nth in *.
 
233
simpl in *.
 
234
apply IHn.
 
235
Qed.
 
236
 
 
237
Lemma Str_nth_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth n (zipWith a
 
238
 b)= f (Str_nth n a) (Str_nth n b).
 
239
Proof.
 
240
intros.
 
241
unfold Str_nth.
 
242
rewrite Str_nth_tl_zipWith.
 
243
reflexivity.
 
244
Qed.
 
245
 
 
246
End Zip.
 
247
 
 
248
Unset Implicit Arguments.