helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.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: TheoryList.v,v 1.15.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
  34
  35 (*#* Some programs and results about lists following CAML Manual *)
  36
  37 include "Lists/List.ma".
  38
  39 (* UNEXPORTED
  40 Set Implicit Arguments.
  41 *)
  42
  43 (* UNEXPORTED
  44 Section Lists
  45 *)
  46
  47 (* UNEXPORTED
  48 cic:/Coq/Lists/TheoryList/Lists/A.var
  49 *)
  50
  51 (*#*********************)
  52
  53 (*#* The null function *)
  54
  55 (*#*********************)
  56
  57 inline procedural "cic:/Coq/Lists/TheoryList/Isnil.con" as definition.
  58
  59 inline procedural "cic:/Coq/Lists/TheoryList/Isnil_nil.con" as lemma.
  60
  61 (* UNEXPORTED
  62 Hint Resolve Isnil_nil.
  63 *)
  64
  65 inline procedural "cic:/Coq/Lists/TheoryList/not_Isnil_cons.con" as lemma.
  66
  67 (* UNEXPORTED
  68 Hint Resolve Isnil_nil not_Isnil_cons.
  69 *)
  70
  71 inline procedural "cic:/Coq/Lists/TheoryList/Isnil_dec.con" as lemma.
  72
  73 (*#***********************)
  74
  75 (*#* The Uncons function *)
  76
  77 (*#***********************)
  78
  79 inline procedural "cic:/Coq/Lists/TheoryList/Uncons.con" as lemma.
  80
  81 (*#*******************************)
  82
  83 (*#* The head function           *)
  84
  85 (*#*******************************)
  86
  87 inline procedural "cic:/Coq/Lists/TheoryList/Hd.con" as lemma.
  88
  89 inline procedural "cic:/Coq/Lists/TheoryList/Tl.con" as lemma.
  90
  91 (*#***************************************)
  92
  93 (*#* Length of lists                     *)
  94
  95 (*#***************************************)
  96
  97 (* length is defined in List *)
  98
  99 inline procedural "cic:/Coq/Lists/TheoryList/Length_l.con" as definition.
 100
 101 (* A tail recursive version *)
 102
 103 inline procedural "cic:/Coq/Lists/TheoryList/Length_l_pf.con" as lemma.
 104
 105 inline procedural "cic:/Coq/Lists/TheoryList/Length.con" as lemma.
 106
 107 (*#******************************)
 108
 109 (*#* Members of lists           *)
 110
 111 (*#******************************)
 112
 113 inline procedural "cic:/Coq/Lists/TheoryList/In_spec.ind".
 114
 115 (* UNEXPORTED
 116 Hint Resolve in_hd in_tl.
 117 *)
 118
 119 (* UNEXPORTED
 120 Hint Unfold In.
 121 *)
 122
 123 (* UNEXPORTED
 124 Hint Resolve in_cons.
 125 *)
 126
 127 inline procedural "cic:/Coq/Lists/TheoryList/In_In_spec.con" as theorem.
 128
 129 inline procedural "cic:/Coq/Lists/TheoryList/AllS.ind".
 130
 131 (* UNEXPORTED
 132 Hint Resolve allS_nil allS_cons.
 133 *)
 134
 135 (* UNEXPORTED
 136 cic:/Coq/Lists/TheoryList/Lists/eqA_dec.var
 137 *)
 138
 139 inline procedural "cic:/Coq/Lists/TheoryList/mem.con" as definition.
 140
 141 (* UNEXPORTED
 142 Hint Unfold In.
 143 *)
 144
 145 inline procedural "cic:/Coq/Lists/TheoryList/Mem.con" as lemma.
 146
 147 (*#********************************)
 148
 149 (*#* Index of elements            *)
 150
 151 (*#********************************)
 152
 153 include "Arith/Le.ma".
 154
 155 include "Arith/Lt.ma".
 156
 157 inline procedural "cic:/Coq/Lists/TheoryList/nth_spec.ind".
 158
 159 (* UNEXPORTED
 160 Hint Resolve nth_spec_O nth_spec_S.
 161 *)
 162
 163 inline procedural "cic:/Coq/Lists/TheoryList/fst_nth_spec.ind".
 164
 165 (* UNEXPORTED
 166 Hint Resolve fst_nth_O fst_nth_S.
 167 *)
 168
 169 inline procedural "cic:/Coq/Lists/TheoryList/fst_nth_nth.con" as lemma.
 170
 171 (* UNEXPORTED
 172 Hint Immediate fst_nth_nth.
 173 *)
 174
 175 inline procedural "cic:/Coq/Lists/TheoryList/nth_lt_O.con" as lemma.
 176
 177 inline procedural "cic:/Coq/Lists/TheoryList/nth_le_length.con" as lemma.
 178
 179 inline procedural "cic:/Coq/Lists/TheoryList/Nth_func.con" as definition.
 180
 181 inline procedural "cic:/Coq/Lists/TheoryList/Nth.con" as lemma.
 182
 183 inline procedural "cic:/Coq/Lists/TheoryList/Item.con" as lemma.
 184
 185 include "Arith/Minus.ma".
 186
 187 include "Bool/DecBool.ma".
 188
 189 inline procedural "cic:/Coq/Lists/TheoryList/index_p.con" as definition.
 190
 191 inline procedural "cic:/Coq/Lists/TheoryList/Index_p.con" as lemma.
 192
 193 inline procedural "cic:/Coq/Lists/TheoryList/Index.con" as lemma.
 194
 195 (* UNEXPORTED
 196 Section Find_sec
 197 *)
 198
 199 (* UNEXPORTED
 200 cic:/Coq/Lists/TheoryList/Lists/Find_sec/R.var
 201 *)
 202
 203 (* UNEXPORTED
 204 cic:/Coq/Lists/TheoryList/Lists/Find_sec/P.var
 205 *)
 206
 207 inline procedural "cic:/Coq/Lists/TheoryList/InR.ind".
 208
 209 (* UNEXPORTED
 210 Hint Resolve inR_hd inR_tl.
 211 *)
 212
 213 inline procedural "cic:/Coq/Lists/TheoryList/InR_inv.con" as definition.
 214
 215 inline procedural "cic:/Coq/Lists/TheoryList/InR_INV.con" as lemma.
 216
 217 inline procedural "cic:/Coq/Lists/TheoryList/InR_cons_inv.con" as lemma.
 218
 219 inline procedural "cic:/Coq/Lists/TheoryList/InR_or_app.con" as lemma.
 220
 221 inline procedural "cic:/Coq/Lists/TheoryList/InR_app_or.con" as lemma.
 222
 223 (* UNEXPORTED
 224 cic:/Coq/Lists/TheoryList/Lists/Find_sec/RS_dec.var
 225 *)
 226
 227 inline procedural "cic:/Coq/Lists/TheoryList/find.con" as definition.
 228
 229 inline procedural "cic:/Coq/Lists/TheoryList/Find.con" as lemma.
 230
 231 (* UNEXPORTED
 232 cic:/Coq/Lists/TheoryList/Lists/Find_sec/B.var
 233 *)
 234
 235 (* UNEXPORTED
 236 cic:/Coq/Lists/TheoryList/Lists/Find_sec/T.var
 237 *)
 238
 239 (* UNEXPORTED
 240 cic:/Coq/Lists/TheoryList/Lists/Find_sec/TS_dec.var
 241 *)
 242
 243 inline procedural "cic:/Coq/Lists/TheoryList/try_find.con" as definition.
 244
 245 inline procedural "cic:/Coq/Lists/TheoryList/Try_find.con" as lemma.
 246
 247 (* UNEXPORTED
 248 End Find_sec
 249 *)
 250
 251 (* UNEXPORTED
 252 Section Assoc_sec
 253 *)
 254
 255 (* UNEXPORTED
 256 cic:/Coq/Lists/TheoryList/Lists/Assoc_sec/B.var
 257 *)
 258
 259 inline procedural "cic:/Coq/Lists/TheoryList/assoc.con" as definition.
 260
 261 inline procedural "cic:/Coq/Lists/TheoryList/AllS_assoc.ind".
 262
 263 (* UNEXPORTED
 264 Hint Resolve allS_assoc_nil allS_assoc_cons.
 265 *)
 266
 267 (* The specification seems too weak: it is enough to return b if the
 268    list has at least an element (a,b); probably the intention is to have
 269    the specification
 270
 271    (a:A)(l:(list A*B)){b:B|(In_spec (a,b) l)}+{(AllS_assoc [a':A]~(a=a') l)}.
 272 *)
 273
 274 inline procedural "cic:/Coq/Lists/TheoryList/Assoc.con" as lemma.
 275
 276 (* UNEXPORTED
 277 End Assoc_sec
 278 *)
 279
 280 (* UNEXPORTED
 281 End Lists
 282 *)
 283
 284 (* UNEXPORTED
 285 Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons:
 286   datatypes.
 287 *)
 288
 289 (* UNEXPORTED
 290 Hint Immediate fst_nth_nth: datatypes.
 291 *)
 292