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 include "Init/Prelude.ma".
  20
  21 (*#***********************************************************************)
  22
  23 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  24
  25 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  26
  27 (*   \VV/  **************************************************************)
  28
  29 (*    //   *      This file is distributed under the terms of the       *)
  30
  31 (*         *       GNU Lesser General Public License Version 2.1        *)
  32
  33 (*#***********************************************************************)
  34
  35 (*i $Id: Streams.v,v 1.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
  36
  37 (* UNEXPORTED
  38 Set Implicit Arguments.
  39 *)
  40
  41 (*#* Streams *)
  42
  43 (* UNEXPORTED
  44 Section Streams
  45 *)
  46
  47 (* UNEXPORTED
  48 cic:/Coq/Lists/Streams/Streams/A.var
  49 *)
  50
  51 inline procedural "cic:/Coq/Lists/Streams/Stream.ind".
  52
  53 inline procedural "cic:/Coq/Lists/Streams/hd.con" as definition.
  54
  55 inline procedural "cic:/Coq/Lists/Streams/tl.con" as definition.
  56
  57 inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl.con" as definition.
  58
  59 inline procedural "cic:/Coq/Lists/Streams/Str_nth.con" as definition.
  60
  61 inline procedural "cic:/Coq/Lists/Streams/unfold_Stream.con" as lemma.
  62
  63 inline procedural "cic:/Coq/Lists/Streams/tl_nth_tl.con" as lemma.
  64
  65 (* UNEXPORTED
  66 Hint Resolve tl_nth_tl: datatypes v62.
  67 *)
  68
  69 inline procedural "cic:/Coq/Lists/Streams/Str_nth_tl_plus.con" as lemma.
  70
  71 inline procedural "cic:/Coq/Lists/Streams/Str_nth_plus.con" as lemma.
  72
  73 (*#* Extensional Equality between two streams  *)
  74
  75 inline procedural "cic:/Coq/Lists/Streams/EqSt.ind".
  76
  77 (*#* A coinduction principle *)
  78
  79 (* UNEXPORTED
  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 inline procedural "cic:/Coq/Lists/Streams/EqSt_reflex.con" as theorem.
  88
  89 inline procedural "cic:/Coq/Lists/Streams/sym_EqSt.con" as theorem.
  90
  91 inline procedural "cic:/Coq/Lists/Streams/trans_EqSt.con" as theorem.
  92
  93 (*#* The definition given is equivalent to require the elements at each
  94     position to be equal *)
  95
  96 inline procedural "cic:/Coq/Lists/Streams/eqst_ntheq.con" as theorem.
  97
  98 inline procedural "cic:/Coq/Lists/Streams/ntheq_eqst.con" as theorem.
  99
 100 (* UNEXPORTED
 101 Section Stream_Properties
 102 *)
 103
 104 (* UNEXPORTED
 105 cic:/Coq/Lists/Streams/Streams/Stream_Properties/P.var
 106 *)
 107
 108 (*i
 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.
 112 i*)
 113
 114 inline procedural "cic:/Coq/Lists/Streams/Exists.ind".
 115
 116 inline procedural "cic:/Coq/Lists/Streams/ForAll.ind".
 117
 118 (* UNEXPORTED
 119 Section Co_Induction_ForAll
 120 *)
 121
 122 (* UNEXPORTED
 123 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/Inv.var
 124 *)
 125
 126 (* UNEXPORTED
 127 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvThenP.var
 128 *)
 129
 130 (* UNEXPORTED
 131 cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvIsStable.var
 132 *)
 133
 134 inline procedural "cic:/Coq/Lists/Streams/ForAll_coind.con" as theorem.
 135
 136 (* UNEXPORTED
 137 End Co_Induction_ForAll
 138 *)
 139
 140 (* UNEXPORTED
 141 End Stream_Properties
 142 *)
 143
 144 (* UNEXPORTED
 145 End Streams
 146 *)
 147
 148 (* UNEXPORTED
 149 Section Map
 150 *)
 151
 152 (* UNEXPORTED
 153 cic:/Coq/Lists/Streams/Map/A.var
 154 *)
 155
 156 (* UNEXPORTED
 157 cic:/Coq/Lists/Streams/Map/B.var
 158 *)
 159
 160 (* UNEXPORTED
 161 cic:/Coq/Lists/Streams/Map/f.var
 162 *)
 163
 164 inline procedural "cic:/Coq/Lists/Streams/map.con" as definition.
 165
 166 (* UNEXPORTED
 167 End Map
 168 *)
 169
 170 (* UNEXPORTED
 171 Section Constant_Stream
 172 *)
 173
 174 (* UNEXPORTED
 175 cic:/Coq/Lists/Streams/Constant_Stream/A.var
 176 *)
 177
 178 (* UNEXPORTED
 179 cic:/Coq/Lists/Streams/Constant_Stream/a.var
 180 *)
 181
 182 inline procedural "cic:/Coq/Lists/Streams/const.con" as definition.
 183
 184 (* UNEXPORTED
 185 End Constant_Stream
 186 *)
 187
 188 (* UNEXPORTED
 189 Unset Implicit Arguments.
 190 *)
 191