helm/software/matita/contribs/procedural/Coq/Lists/Streams.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Streams.v,v 1.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
  34
  35 (* UNEXPORTED
  36 Set Implicit Arguments.
  37 *)
  38
  39 (*#* Streams *)
  40
  41 (* UNEXPORTED
  42 Section Streams
  43 *)
  44
  45 (* UNEXPORTED
  46 cic:/Coq/Lists/Streams/Streams/A.var
  47 *)
  48
  49 inline procedural "cic:/Coq/Lists/Streams/Stream.ind".
  50
  51 inline procedural "cic:/Coq/Lists/Streams/hd.con" as definition.
  52
  53 inline procedural "cic:/Coq/Lists/Streams/tl.con" as definition.
  54
  55 inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl.con" as definition.
  56
  57 inline procedural "cic:/Coq/Lists/Streams/Str_nth.con" as definition.
  58
  59 inline procedural "cic:/Coq/Lists/Streams/unfold_Stream.con" as lemma.
  60
  61 inline procedural "cic:/Coq/Lists/Streams/tl_nth_tl.con" as lemma.
  62
  63 (* UNEXPORTED
  64 Hint Resolve tl_nth_tl: datatypes v62.
  65 *)
  66
  67 inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl_plus.con" as lemma.
  68
  69 inline procedural "cic:/Coq/Lists/Streams/Str_nth_plus.con" as lemma.
  70
  71 (*#* Extensional Equality between two streams  *)
  72
  73 inline procedural "cic:/Coq/Lists/Streams/EqSt.ind".
  74
  75 (*#* A coinduction principle *)
  76
  77 (* UNEXPORTED
  78 Ltac coinduction proof :=
  79   cofix proof; intros; constructor;
  80    [ clear proof | try (apply proof; clear proof) ].
  81 *)
  82
  83 (*#* Extensional equality is an equivalence relation *)
  84
  85 inline procedural "cic:/Coq/Lists/Streams/EqSt_reflex.con" as theorem.
  86
  87 inline procedural "cic:/Coq/Lists/Streams/sym_EqSt.con" as theorem.
  88
  89 inline procedural "cic:/Coq/Lists/Streams/trans_EqSt.con" as theorem.
  90
  91 (*#* The definition given is equivalent to require the elements at each
  92     position to be equal *)
  93
  94 inline procedural "cic:/Coq/Lists/Streams/eqst_ntheq.con" as theorem.
  95
  96 inline procedural "cic:/Coq/Lists/Streams/ntheq_eqst.con" as theorem.
  97
  98 (* UNEXPORTED
  99 Section Stream_Properties
 100 *)
 101
 102 (* UNEXPORTED
 103 cic:/Coq/Lists/Streams/Streams/Stream_Properties/P.var
 104 *)
 105
 106 (*i
 107 Inductive Exists : Stream -> Prop :=
 108   | Here    : forall x:Stream, P x -> Exists x
 109   | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
 110 i*)
 111
 112 inline procedural "cic:/Coq/Lists/Streams/Exists.ind".
 113
 114 inline procedural "cic:/Coq/Lists/Streams/ForAll.ind".
 115
 116 (* UNEXPORTED
 117 Section Co_Induction_ForAll
 118 *)
 119
 120 (* UNEXPORTED
 121 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/Inv.var
 122 *)
 123
 124 (* UNEXPORTED
 125 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvThenP.var
 126 *)
 127
 128 (* UNEXPORTED
 129 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvIsStable.var
 130 *)
 131
 132 inline procedural "cic:/Coq/Lists/Streams/ForAll_coind.con" as theorem.
 133
 134 (* UNEXPORTED
 135 End Co_Induction_ForAll
 136 *)
 137
 138 (* UNEXPORTED
 139 End Stream_Properties
 140 *)
 141
 142 (* UNEXPORTED
 143 End Streams
 144 *)
 145
 146 (* UNEXPORTED
 147 Section Map
 148 *)
 149
 150 (* UNEXPORTED
 151 cic:/Coq/Lists/Streams/Map/A.var
 152 *)
 153
 154 (* UNEXPORTED
 155 cic:/Coq/Lists/Streams/Map/B.var
 156 *)
 157
 158 (* UNEXPORTED
 159 cic:/Coq/Lists/Streams/Map/f.var
 160 *)
 161
 162 inline procedural "cic:/Coq/Lists/Streams/map.con" as definition.
 163
 164 (* UNEXPORTED
 165 End Map
 166 *)
 167
 168 (* UNEXPORTED
 169 Section Constant_Stream
 170 *)
 171
 172 (* UNEXPORTED
 173 cic:/Coq/Lists/Streams/Constant_Stream/A.var
 174 *)
 175
 176 (* UNEXPORTED
 177 cic:/Coq/Lists/Streams/Constant_Stream/a.var
 178 *)
 179
 180 inline procedural "cic:/Coq/Lists/Streams/const.con" as definition.
 181
 182 (* UNEXPORTED
 183 End Constant_Stream
 184 *)
 185
 186 (* UNEXPORTED
 187 Unset Implicit Arguments.
 188 *)
 189