1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 include "Init/Prelude.ma".
21 (*#***********************************************************************)
23 (* v * The Coq Proof Assistant / The Coq Development Team *)
25 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
27 (* \VV/ **************************************************************)
29 (* // * This file is distributed under the terms of the *)
31 (* * GNU Lesser General Public License Version 2.1 *)
33 (*#***********************************************************************)
35 (*i $Id: Streams.v,v 1.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
38 Set Implicit Arguments.
48 cic:/Coq/Lists/Streams/Streams/A.var
51 inline procedural "cic:/Coq/Lists/Streams/Stream.ind".
53 inline procedural "cic:/Coq/Lists/Streams/hd.con" as definition.
55 inline procedural "cic:/Coq/Lists/Streams/tl.con" as definition.
57 inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl.con" as definition.
59 inline procedural "cic:/Coq/Lists/Streams/Str_nth.con" as definition.
61 inline procedural "cic:/Coq/Lists/Streams/unfold_Stream.con" as lemma.
63 inline procedural "cic:/Coq/Lists/Streams/tl_nth_tl.con" as lemma.
66 Hint Resolve tl_nth_tl: datatypes v62.
69 inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl_plus.con" as lemma.
71 inline procedural "cic:/Coq/Lists/Streams/Str_nth_plus.con" as lemma.
73 (*#* Extensional Equality between two streams *)
75 inline procedural "cic:/Coq/Lists/Streams/EqSt.ind".
77 (*#* A coinduction principle *)
80 Ltac coinduction proof :=
81 cofix proof; intros; constructor;
82 [ clear proof | try (apply proof; clear proof) ].
85 (*#* Extensional equality is an equivalence relation *)
87 inline procedural "cic:/Coq/Lists/Streams/EqSt_reflex.con" as theorem.
89 inline procedural "cic:/Coq/Lists/Streams/sym_EqSt.con" as theorem.
91 inline procedural "cic:/Coq/Lists/Streams/trans_EqSt.con" as theorem.
93 (*#* The definition given is equivalent to require the elements at each
94 position to be equal *)
96 inline procedural "cic:/Coq/Lists/Streams/eqst_ntheq.con" as theorem.
98 inline procedural "cic:/Coq/Lists/Streams/ntheq_eqst.con" as theorem.
101 Section Stream_Properties
105 cic:/Coq/Lists/Streams/Streams/Stream_Properties/P.var
109 Inductive Exists : Stream -> Prop :=
110 | Here : forall x:Stream, P x -> Exists x
111 | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
114 inline procedural "cic:/Coq/Lists/Streams/Exists.ind".
116 inline procedural "cic:/Coq/Lists/Streams/ForAll.ind".
119 Section Co_Induction_ForAll
123 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/Inv.var
127 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvThenP.var
131 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvIsStable.var
134 inline procedural "cic:/Coq/Lists/Streams/ForAll_coind.con" as theorem.
137 End Co_Induction_ForAll
141 End Stream_Properties
153 cic:/Coq/Lists/Streams/Map/A.var
157 cic:/Coq/Lists/Streams/Map/B.var
161 cic:/Coq/Lists/Streams/Map/f.var
164 inline procedural "cic:/Coq/Lists/Streams/map.con" as definition.
171 Section Constant_Stream
175 cic:/Coq/Lists/Streams/Constant_Stream/A.var
179 cic:/Coq/Lists/Streams/Constant_Stream/a.var
182 inline procedural "cic:/Coq/Lists/Streams/const.con" as definition.
189 Unset Implicit Arguments.