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