helm/software/matita/contribs/procedural/Coq/Bool/Bool.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: Bool.v,v 1.29.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)
  36
  37 (*#* Booleans  *)
  38
  39 (*#* The type [bool] is defined in the prelude as
  40     [Inductive bool : Set := true : bool | false : bool] *)
  41
  42 (*#* Interpretation of booleans as Proposition *)
  43
  44 inline procedural "cic:/Coq/Bool/Bool/Is_true.con" as definition.
  45
  46 (* UNEXPORTED
  47 Hint Unfold Is_true: bool.
  48 *)
  49
  50 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_left.con" as lemma.
  51
  52 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_right.con" as lemma.
  53
  54 (* UNEXPORTED
  55 Hint Immediate Is_true_eq_right Is_true_eq_left: bool.
  56 *)
  57
  58 (*#******************)
  59
  60 (*#* Discrimination *)
  61
  62 (*#******************)
  63
  64 inline procedural "cic:/Coq/Bool/Bool/diff_true_false.con" as lemma.
  65
  66 (* UNEXPORTED
  67 Hint Resolve diff_true_false: bool v62.
  68 *)
  69
  70 inline procedural "cic:/Coq/Bool/Bool/diff_false_true.con" as lemma.
  71
  72 (* UNEXPORTED
  73 Hint Resolve diff_false_true: bool v62.
  74 *)
  75
  76 inline procedural "cic:/Coq/Bool/Bool/eq_true_false_abs.con" as lemma.
  77
  78 (* UNEXPORTED
  79 Hint Resolve eq_true_false_abs: bool.
  80 *)
  81
  82 inline procedural "cic:/Coq/Bool/Bool/not_true_is_false.con" as lemma.
  83
  84 inline procedural "cic:/Coq/Bool/Bool/not_false_is_true.con" as lemma.
  85
  86 (*#*********************)
  87
  88 (*#* Order on booleans *)
  89
  90 (*#*********************)
  91
  92 inline procedural "cic:/Coq/Bool/Bool/leb.con" as definition.
  93
  94 (* UNEXPORTED
  95 Hint Unfold leb: bool v62.
  96 *)
  97
  98 (*#************)
  99
 100 (*#* Equality *)
 101
 102 (*#************)
 103
 104 inline procedural "cic:/Coq/Bool/Bool/eqb.con" as definition.
 105
 106 inline procedural "cic:/Coq/Bool/Bool/eqb_refl.con" as lemma.
 107
 108 inline procedural "cic:/Coq/Bool/Bool/eqb_eq.con" as lemma.
 109
 110 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_true.con" as lemma.
 111
 112 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_true2.con" as lemma.
 113
 114 inline procedural "cic:/Coq/Bool/Bool/eqb_subst.con" as lemma.
 115
 116 inline procedural "cic:/Coq/Bool/Bool/eqb_reflx.con" as lemma.
 117
 118 inline procedural "cic:/Coq/Bool/Bool/eqb_prop.con" as lemma.
 119
 120 (*#***********************)
 121
 122 (*#* Logical combinators *)
 123
 124 (*#***********************)
 125
 126 inline procedural "cic:/Coq/Bool/Bool/ifb.con" as definition.
 127
 128 inline procedural "cic:/Coq/Bool/Bool/andb.con" as definition.
 129
 130 inline procedural "cic:/Coq/Bool/Bool/orb.con" as definition.
 131
 132 inline procedural "cic:/Coq/Bool/Bool/implb.con" as definition.
 133
 134 inline procedural "cic:/Coq/Bool/Bool/xorb.con" as definition.
 135
 136 inline procedural "cic:/Coq/Bool/Bool/negb.con" as definition.
 137
 138 (* NOTATION
 139 Infix "||" := orb (at level 50, left associativity) : bool_scope.
 140 *)
 141
 142 (* NOTATION
 143 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
 144 *)
 145
 146 (* UNEXPORTED
 147 Open Scope bool_scope.
 148 *)
 149
 150 (* UNEXPORTED
 151 Delimit Scope bool_scope with bool.
 152 *)
 153
 154 (* UNEXPORTED
 155 Bind Scope bool_scope with bool.
 156 *)
 157
 158 (*#*************************)
 159
 160 (*#* Lemmas about [negb]   *)
 161
 162 (*#*************************)
 163
 164 inline procedural "cic:/Coq/Bool/Bool/negb_intro.con" as lemma.
 165
 166 inline procedural "cic:/Coq/Bool/Bool/negb_elim.con" as lemma.
 167
 168 inline procedural "cic:/Coq/Bool/Bool/negb_orb.con" as lemma.
 169
 170 inline procedural "cic:/Coq/Bool/Bool/negb_andb.con" as lemma.
 171
 172 inline procedural "cic:/Coq/Bool/Bool/negb_sym.con" as lemma.
 173
 174 inline procedural "cic:/Coq/Bool/Bool/no_fixpoint_negb.con" as lemma.
 175
 176 inline procedural "cic:/Coq/Bool/Bool/eqb_negb1.con" as lemma.
 177
 178 inline procedural "cic:/Coq/Bool/Bool/eqb_negb2.con" as lemma.
 179
 180 inline procedural "cic:/Coq/Bool/Bool/if_negb.con" as lemma.
 181
 182 (*#***************************)
 183
 184 (*#* A few lemmas about [or] *)
 185
 186 (*#***************************)
 187
 188 inline procedural "cic:/Coq/Bool/Bool/orb_prop.con" as lemma.
 189
 190 inline procedural "cic:/Coq/Bool/Bool/orb_prop2.con" as lemma.
 191
 192 inline procedural "cic:/Coq/Bool/Bool/orb_true_intro.con" as lemma.
 193
 194 (* UNEXPORTED
 195 Hint Resolve orb_true_intro: bool v62.
 196 *)
 197
 198 inline procedural "cic:/Coq/Bool/Bool/orb_b_true.con" as lemma.
 199
 200 (* UNEXPORTED
 201 Hint Resolve orb_b_true: bool v62.
 202 *)
 203
 204 inline procedural "cic:/Coq/Bool/Bool/orb_true_b.con" as lemma.
 205
 206 inline procedural "cic:/Coq/Bool/Bool/orb_true_elim.con" as definition.
 207
 208 inline procedural "cic:/Coq/Bool/Bool/orb_false_intro.con" as lemma.
 209
 210 (* UNEXPORTED
 211 Hint Resolve orb_false_intro: bool v62.
 212 *)
 213
 214 inline procedural "cic:/Coq/Bool/Bool/orb_b_false.con" as lemma.
 215
 216 (* UNEXPORTED
 217 Hint Resolve orb_b_false: bool v62.
 218 *)
 219
 220 inline procedural "cic:/Coq/Bool/Bool/orb_false_b.con" as lemma.
 221
 222 (* UNEXPORTED
 223 Hint Resolve orb_false_b: bool v62.
 224 *)
 225
 226 inline procedural "cic:/Coq/Bool/Bool/orb_false_elim.con" as lemma.
 227
 228 inline procedural "cic:/Coq/Bool/Bool/orb_neg_b.con" as lemma.
 229
 230 (* UNEXPORTED
 231 Hint Resolve orb_neg_b: bool v62.
 232 *)
 233
 234 inline procedural "cic:/Coq/Bool/Bool/orb_comm.con" as lemma.
 235
 236 inline procedural "cic:/Coq/Bool/Bool/orb_assoc.con" as lemma.
 237
 238 (* UNEXPORTED
 239 Hint Resolve orb_comm orb_assoc orb_b_false orb_false_b: bool v62.
 240 *)
 241
 242 (*#****************************)
 243
 244 (*#* A few lemmas about [and] *)
 245
 246 (*#****************************)
 247
 248 inline procedural "cic:/Coq/Bool/Bool/andb_prop.con" as lemma.
 249
 250 (* UNEXPORTED
 251 Hint Resolve andb_prop: bool v62.
 252 *)
 253
 254 inline procedural "cic:/Coq/Bool/Bool/andb_true_eq.con" as definition.
 255
 256 inline procedural "cic:/Coq/Bool/Bool/andb_prop2.con" as lemma.
 257
 258 (* UNEXPORTED
 259 Hint Resolve andb_prop2: bool v62.
 260 *)
 261
 262 inline procedural "cic:/Coq/Bool/Bool/andb_true_intro.con" as lemma.
 263
 264 (* UNEXPORTED
 265 Hint Resolve andb_true_intro: bool v62.
 266 *)
 267
 268 inline procedural "cic:/Coq/Bool/Bool/andb_true_intro2.con" as lemma.
 269
 270 (* UNEXPORTED
 271 Hint Resolve andb_true_intro2: bool v62.
 272 *)
 273
 274 inline procedural "cic:/Coq/Bool/Bool/andb_false_intro1.con" as lemma.
 275
 276 inline procedural "cic:/Coq/Bool/Bool/andb_false_intro2.con" as lemma.
 277
 278 inline procedural "cic:/Coq/Bool/Bool/andb_b_false.con" as lemma.
 279
 280 inline procedural "cic:/Coq/Bool/Bool/andb_false_b.con" as lemma.
 281
 282 inline procedural "cic:/Coq/Bool/Bool/andb_b_true.con" as lemma.
 283
 284 inline procedural "cic:/Coq/Bool/Bool/andb_true_b.con" as lemma.
 285
 286 inline procedural "cic:/Coq/Bool/Bool/andb_false_elim.con" as definition.
 287
 288 (* UNEXPORTED
 289 Hint Resolve andb_false_elim: bool v62.
 290 *)
 291
 292 inline procedural "cic:/Coq/Bool/Bool/andb_neg_b.con" as lemma.
 293
 294 (* UNEXPORTED
 295 Hint Resolve andb_neg_b: bool v62.
 296 *)
 297
 298 inline procedural "cic:/Coq/Bool/Bool/andb_comm.con" as lemma.
 299
 300 inline procedural "cic:/Coq/Bool/Bool/andb_assoc.con" as lemma.
 301
 302 (* UNEXPORTED
 303 Hint Resolve andb_comm andb_assoc: bool v62.
 304 *)
 305
 306 (*#******************************)
 307
 308 (*#* Properties of [xorb]       *)
 309
 310 (*#******************************)
 311
 312 inline procedural "cic:/Coq/Bool/Bool/xorb_false.con" as lemma.
 313
 314 inline procedural "cic:/Coq/Bool/Bool/false_xorb.con" as lemma.
 315
 316 inline procedural "cic:/Coq/Bool/Bool/xorb_true.con" as lemma.
 317
 318 inline procedural "cic:/Coq/Bool/Bool/true_xorb.con" as lemma.
 319
 320 inline procedural "cic:/Coq/Bool/Bool/xorb_nilpotent.con" as lemma.
 321
 322 inline procedural "cic:/Coq/Bool/Bool/xorb_comm.con" as lemma.
 323
 324 inline procedural "cic:/Coq/Bool/Bool/xorb_assoc.con" as lemma.
 325
 326 inline procedural "cic:/Coq/Bool/Bool/xorb_eq.con" as lemma.
 327
 328 inline procedural "cic:/Coq/Bool/Bool/xorb_move_l_r_1.con" as lemma.
 329
 330 inline procedural "cic:/Coq/Bool/Bool/xorb_move_l_r_2.con" as lemma.
 331
 332 inline procedural "cic:/Coq/Bool/Bool/xorb_move_r_l_1.con" as lemma.
 333
 334 inline procedural "cic:/Coq/Bool/Bool/xorb_move_r_l_2.con" as lemma.
 335
 336 (*#******************************)
 337
 338 (*#* De Morgan's law            *)
 339
 340 (*#******************************)
 341
 342 inline procedural "cic:/Coq/Bool/Bool/demorgan1.con" as lemma.
 343
 344 inline procedural "cic:/Coq/Bool/Bool/demorgan2.con" as lemma.
 345
 346 inline procedural "cic:/Coq/Bool/Bool/demorgan3.con" as lemma.
 347
 348 inline procedural "cic:/Coq/Bool/Bool/demorgan4.con" as lemma.
 349
 350 inline procedural "cic:/Coq/Bool/Bool/absoption_andb.con" as lemma.
 351
 352 inline procedural "cic:/Coq/Bool/Bool/absoption_orb.con" as lemma.
 353
 354 (*#* Misc. equalities between booleans (to be used by Auto) *)
 355
 356 inline procedural "cic:/Coq/Bool/Bool/bool_1.con" as lemma.
 357
 358 inline procedural "cic:/Coq/Bool/Bool/bool_2.con" as lemma.
 359
 360 inline procedural "cic:/Coq/Bool/Bool/bool_3.con" as lemma.
 361
 362 inline procedural "cic:/Coq/Bool/Bool/bool_4.con" as lemma.
 363
 364 inline procedural "cic:/Coq/Bool/Bool/bool_5.con" as lemma.
 365
 366 inline procedural "cic:/Coq/Bool/Bool/bool_6.con" as lemma.
 367
 368 (* UNEXPORTED
 369 Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.
 370 *)
 371