helm/software/matita/contribs/procedural/Coq/Relations/Relation_Operators.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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
  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: Relation_Operators.v,v 1.8 2003/11/29 17:28:41 herbelin Exp $ i*)
  34
  35 (*#***************************************************************************)
  36
  37 (*                      Bruno Barras, Cristina Cornes                       *)
  38
  39 (*                                                                          *)
  40
  41 (*  Some of these definitons were taken from :                              *)
  42
  43 (*     Constructing Recursion Operators in Type Theory                      *)
  44
  45 (*     L. Paulson  JSC (1986) 2, 325-355                                    *)
  46
  47 (*#***************************************************************************)
  48
  49 include "Relations/Relation_Definitions.ma".
  50
  51 include "Lists/List.ma".
  52
  53 (*#* Some operators to build relations *)
  54
  55 (* UNEXPORTED
  56 Section Transitive_Closure
  57 *)
  58
  59 (* UNEXPORTED
  60 cic:/Coq/Relations/Relation_Operators/Transitive_Closure/A.var
  61 *)
  62
  63 (* UNEXPORTED
  64 cic:/Coq/Relations/Relation_Operators/Transitive_Closure/R.var
  65 *)
  66
  67 inline procedural "cic:/Coq/Relations/Relation_Operators/clos_trans.ind".
  68
  69 (* UNEXPORTED
  70 End Transitive_Closure
  71 *)
  72
  73 (* UNEXPORTED
  74 Section Reflexive_Transitive_Closure
  75 *)
  76
  77 (* UNEXPORTED
  78 cic:/Coq/Relations/Relation_Operators/Reflexive_Transitive_Closure/A.var
  79 *)
  80
  81 (* UNEXPORTED
  82 cic:/Coq/Relations/Relation_Operators/Reflexive_Transitive_Closure/R.var
  83 *)
  84
  85 inline procedural "cic:/Coq/Relations/Relation_Operators/clos_refl_trans.ind".
  86
  87 (* UNEXPORTED
  88 End Reflexive_Transitive_Closure
  89 *)
  90
  91 (* UNEXPORTED
  92 Section Reflexive_Symetric_Transitive_Closure
  93 *)
  94
  95 (* UNEXPORTED
  96 cic:/Coq/Relations/Relation_Operators/Reflexive_Symetric_Transitive_Closure/A.var
  97 *)
  98
  99 (* UNEXPORTED
 100 cic:/Coq/Relations/Relation_Operators/Reflexive_Symetric_Transitive_Closure/R.var
 101 *)
 102
 103 inline procedural "cic:/Coq/Relations/Relation_Operators/clos_refl_sym_trans.ind".
 104
 105 (* UNEXPORTED
 106 End Reflexive_Symetric_Transitive_Closure
 107 *)
 108
 109 (* UNEXPORTED
 110 Section Transposee
 111 *)
 112
 113 (* UNEXPORTED
 114 cic:/Coq/Relations/Relation_Operators/Transposee/A.var
 115 *)
 116
 117 (* UNEXPORTED
 118 cic:/Coq/Relations/Relation_Operators/Transposee/R.var
 119 *)
 120
 121 inline procedural "cic:/Coq/Relations/Relation_Operators/transp.con" as definition.
 122
 123 (* UNEXPORTED
 124 End Transposee
 125 *)
 126
 127 (* UNEXPORTED
 128 Section Union
 129 *)
 130
 131 (* UNEXPORTED
 132 cic:/Coq/Relations/Relation_Operators/Union/A.var
 133 *)
 134
 135 (* UNEXPORTED
 136 cic:/Coq/Relations/Relation_Operators/Union/R1.var
 137 *)
 138
 139 (* UNEXPORTED
 140 cic:/Coq/Relations/Relation_Operators/Union/R2.var
 141 *)
 142
 143 inline procedural "cic:/Coq/Relations/Relation_Operators/union.con" as definition.
 144
 145 (* UNEXPORTED
 146 End Union
 147 *)
 148
 149 (* UNEXPORTED
 150 Section Disjoint_Union
 151 *)
 152
 153 (* UNEXPORTED
 154 cic:/Coq/Relations/Relation_Operators/Disjoint_Union/A.var
 155 *)
 156
 157 (* UNEXPORTED
 158 cic:/Coq/Relations/Relation_Operators/Disjoint_Union/B.var
 159 *)
 160
 161 (* UNEXPORTED
 162 cic:/Coq/Relations/Relation_Operators/Disjoint_Union/leA.var
 163 *)
 164
 165 (* UNEXPORTED
 166 cic:/Coq/Relations/Relation_Operators/Disjoint_Union/leB.var
 167 *)
 168
 169 inline procedural "cic:/Coq/Relations/Relation_Operators/le_AsB.ind".
 170
 171 (* UNEXPORTED
 172 End Disjoint_Union
 173 *)
 174
 175 (* UNEXPORTED
 176 Section Lexicographic_Product
 177 *)
 178
 179 (* Lexicographic order on dependent pairs *)
 180
 181 (* UNEXPORTED
 182 cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/A.var
 183 *)
 184
 185 (* UNEXPORTED
 186 cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/B.var
 187 *)
 188
 189 (* UNEXPORTED
 190 cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/leA.var
 191 *)
 192
 193 (* UNEXPORTED
 194 cic:/Coq/Relations/Relation_Operators/Lexicographic_Product/leB.var
 195 *)
 196
 197 inline procedural "cic:/Coq/Relations/Relation_Operators/lexprod.ind".
 198
 199 (* UNEXPORTED
 200 End Lexicographic_Product
 201 *)
 202
 203 (* UNEXPORTED
 204 Section Symmetric_Product
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/Coq/Relations/Relation_Operators/Symmetric_Product/A.var
 209 *)
 210
 211 (* UNEXPORTED
 212 cic:/Coq/Relations/Relation_Operators/Symmetric_Product/B.var
 213 *)
 214
 215 (* UNEXPORTED
 216 cic:/Coq/Relations/Relation_Operators/Symmetric_Product/leA.var
 217 *)
 218
 219 (* UNEXPORTED
 220 cic:/Coq/Relations/Relation_Operators/Symmetric_Product/leB.var
 221 *)
 222
 223 inline procedural "cic:/Coq/Relations/Relation_Operators/symprod.ind".
 224
 225 (* UNEXPORTED
 226 End Symmetric_Product
 227 *)
 228
 229 (* UNEXPORTED
 230 Section Swap
 231 *)
 232
 233 (* UNEXPORTED
 234 cic:/Coq/Relations/Relation_Operators/Swap/A.var
 235 *)
 236
 237 (* UNEXPORTED
 238 cic:/Coq/Relations/Relation_Operators/Swap/R.var
 239 *)
 240
 241 inline procedural "cic:/Coq/Relations/Relation_Operators/swapprod.ind".
 242
 243 (* UNEXPORTED
 244 End Swap
 245 *)
 246
 247 (* UNEXPORTED
 248 Section Lexicographic_Exponentiation
 249 *)
 250
 251 (* UNEXPORTED
 252 cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/A.var
 253 *)
 254
 255 (* UNEXPORTED
 256 cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/leA.var
 257 *)
 258
 259 inline procedural "cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/Nil.con" "Lexicographic_Exponentiation__" as definition.
 260
 261 inline procedural "cic:/Coq/Relations/Relation_Operators/Lexicographic_Exponentiation/List.con" "Lexicographic_Exponentiation__" as definition.
 262
 263 inline procedural "cic:/Coq/Relations/Relation_Operators/Ltl.ind".
 264
 265 inline procedural "cic:/Coq/Relations/Relation_Operators/Desc.ind".
 266
 267 inline procedural "cic:/Coq/Relations/Relation_Operators/Pow.con" as definition.
 268
 269 inline procedural "cic:/Coq/Relations/Relation_Operators/lex_exp.con" as definition.
 270
 271 (* UNEXPORTED
 272 End Lexicographic_Exponentiation
 273 *)
 274
 275 (* UNEXPORTED
 276 Hint Unfold transp union: sets v62.
 277 *)
 278
 279 (* UNEXPORTED
 280 Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62.
 281 *)
 282
 283 (* UNEXPORTED
 284 Hint Immediate rst_sym: sets v62.
 285 *)
 286