helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.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: BinInt.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
  34
  35 (*#**********************************************************)
  36
  37 (*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *)
  38
  39 (*#**********************************************************)
  40
  41 include "NArith/BinPos.ma".
  42
  43 include "NArith/Pnat.ma".
  44
  45 include "NArith/BinNat.ma".
  46
  47 include "Arith/Plus.ma".
  48
  49 include "Arith/Mult.ma".
  50
  51 (*#*********************************************************************)
  52
  53 (*#* Binary integer numbers *)
  54
  55 inline procedural "cic:/Coq/ZArith/BinInt/Z.ind".
  56
  57 (*#* Declare Scope Z_scope with Key Z *)
  58
  59 (* UNEXPORTED
  60 Delimit Scope Z_scope with Z.
  61 *)
  62
  63 (*#* Automatically open scope positive_scope for the constructors of Z *)
  64
  65 (* UNEXPORTED
  66 Bind Scope Z_scope with Z.
  67 *)
  68
  69 (* UNEXPORTED
  70 Arguments Scope Zpos [positive_scope].
  71 *)
  72
  73 (* UNEXPORTED
  74 Arguments Scope Zneg [positive_scope].
  75 *)
  76
  77 (*#* Subtraction of positive into Z *)
  78
  79 inline procedural "cic:/Coq/ZArith/BinInt/Zdouble_plus_one.con" as definition.
  80
  81 inline procedural "cic:/Coq/ZArith/BinInt/Zdouble_minus_one.con" as definition.
  82
  83 inline procedural "cic:/Coq/ZArith/BinInt/Zdouble.con" as definition.
  84
  85 inline procedural "cic:/Coq/ZArith/BinInt/ZPminus.con" as definition.
  86
  87 (*#* Addition on integers *)
  88
  89 inline procedural "cic:/Coq/ZArith/BinInt/Zplus.con" as definition.
  90
  91 (* NOTATION
  92 Infix "+" := Zplus : Z_scope.
  93 *)
  94
  95 (*#* Opposite *)
  96
  97 inline procedural "cic:/Coq/ZArith/BinInt/Zopp.con" as definition.
  98
  99 (* NOTATION
 100 Notation "- x" := (Zopp x) : Z_scope.
 101 *)
 102
 103 (*#* Successor on integers *)
 104
 105 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc.con" as definition.
 106
 107 (*#* Predecessor on integers *)
 108
 109 inline procedural "cic:/Coq/ZArith/BinInt/Zpred.con" as definition.
 110
 111 (*#* Subtraction on integers *)
 112
 113 inline procedural "cic:/Coq/ZArith/BinInt/Zminus.con" as definition.
 114
 115 (* NOTATION
 116 Infix "-" := Zminus : Z_scope.
 117 *)
 118
 119 (*#* Multiplication on integers *)
 120
 121 inline procedural "cic:/Coq/ZArith/BinInt/Zmult.con" as definition.
 122
 123 (* NOTATION
 124 Infix "*" := Zmult : Z_scope.
 125 *)
 126
 127 (*#* Comparison of integers *)
 128
 129 inline procedural "cic:/Coq/ZArith/BinInt/Zcompare.con" as definition.
 130
 131 (* NOTATION
 132 Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
 133 *)
 134
 135 (* UNEXPORTED
 136 Ltac elim_compare com1 com2 :=
 137   case (Dcompare (com1 ?= com2)%Z);
 138    [ idtac | let x := fresh "H" in
 139              (intro x; case x; clear x) ].
 140 *)
 141
 142 (*#* Sign function *)
 143
 144 inline procedural "cic:/Coq/ZArith/BinInt/Zsgn.con" as definition.
 145
 146 (*#* Direct, easier to handle variants of successor and addition *)
 147
 148 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc'.con" as definition.
 149
 150 inline procedural "cic:/Coq/ZArith/BinInt/Zpred'.con" as definition.
 151
 152 inline procedural "cic:/Coq/ZArith/BinInt/Zplus'.con" as definition.
 153
 154 (* UNEXPORTED
 155 Open Local Scope Z_scope.
 156 *)
 157
 158 (*#*********************************************************************)
 159
 160 (*#* Inductive specification of Z *)
 161
 162 inline procedural "cic:/Coq/ZArith/BinInt/Zind.con" as theorem.
 163
 164 (*#*********************************************************************)
 165
 166 (*#* Properties of opposite on binary integer numbers *)
 167
 168 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_neg.con" as theorem.
 169
 170 (*#* [opp] is involutive *)
 171
 172 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_involutive.con" as theorem.
 173
 174 (*#* Injectivity of the opposite *)
 175
 176 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_inj.con" as theorem.
 177
 178 (*#*********************************************************************)
 179
 180 (* Properties of the direct definition of successor and predecessor *)
 181
 182 inline procedural "cic:/Coq/ZArith/BinInt/Zpred'_succ'.con" as lemma.
 183
 184 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc'_discr.con" as lemma.
 185
 186 (*#*********************************************************************)
 187
 188 (*#* Other properties of binary integer numbers *)
 189
 190 inline procedural "cic:/Coq/ZArith/BinInt/ZL0.con" as lemma.
 191
 192 (*#*********************************************************************)
 193
 194 (*#* Properties of the addition on integers *)
 195
 196 (*#* zero is left neutral for addition *)
 197
 198 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_l.con" as theorem.
 199
 200 (*#* zero is right neutral for addition *)
 201
 202 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_r.con" as theorem.
 203
 204 (*#* addition is commutative *)
 205
 206 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_comm.con" as theorem.
 207
 208 (*#* opposite distributes over addition *)
 209
 210 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_plus_distr.con" as theorem.
 211
 212 (*#* opposite is inverse for addition *)
 213
 214 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_opp_r.con" as theorem.
 215
 216 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_opp_l.con" as theorem.
 217
 218 (* UNEXPORTED
 219 Hint Local Resolve Zplus_0_l Zplus_0_r.
 220 *)
 221
 222 (*#* addition is associative *)
 223
 224 inline procedural "cic:/Coq/ZArith/BinInt/weak_assoc.con" as lemma.
 225
 226 (* UNEXPORTED
 227 Hint Local Resolve weak_assoc.
 228 *)
 229
 230 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_assoc.con" as theorem.
 231
 232 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_assoc_reverse.con" as lemma.
 233
 234 (*#* Associativity mixed with commutativity *)
 235
 236 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_permute.con" as theorem.
 237
 238 (*#* addition simplifies *)
 239
 240 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_reg_l.con" as theorem.
 241
 242 (*#* addition and successor permutes *)
 243
 244 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_succ_l.con" as lemma.
 245
 246 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_succ_r.con" as lemma.
 247
 248 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_succ_comm.con" as lemma.
 249
 250 (*#* Misc properties, usually redundant or non natural *)
 251
 252 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con" as lemma.
 253
 254 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_simpl_l.con" as lemma.
 255
 256 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_simpl_l_reverse.con" as lemma.
 257
 258 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con" as lemma.
 259
 260 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_opp_expand.con" as lemma.
 261
 262 (*#*********************************************************************)
 263
 264 (*#* Properties of successor and predecessor on binary integer numbers *)
 265
 266 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_discr.con" as theorem.
 267
 268 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_succ_morphism.con" as theorem.
 269
 270 (*#* successor and predecessor are inverse functions *)
 271
 272 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_pred.con" as theorem.
 273
 274 (* UNEXPORTED
 275 Hint Immediate Zsucc_pred: zarith.
 276 *)
 277
 278 inline procedural "cic:/Coq/ZArith/BinInt/Zpred_succ.con" as theorem.
 279
 280 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_inj.con" as theorem.
 281
 282 (*#* Misc properties, usually redundant or non natural *)
 283
 284 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_eq_compat.con" as lemma.
 285
 286 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_inj_contrapositive.con" as lemma.
 287
 288 (*#*********************************************************************)
 289
 290 (*#* Properties of subtraction on binary integer numbers *)
 291
 292 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_0_r.con" as lemma.
 293
 294 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_0_l_reverse.con" as lemma.
 295
 296 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_diag.con" as lemma.
 297
 298 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_diag_reverse.con" as lemma.
 299
 300 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_minus_eq.con" as lemma.
 301
 302 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus.con" as lemma.
 303
 304 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_minus.con" as lemma.
 305
 306 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_succ_l.con" as lemma.
 307
 308 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_l.con" as lemma.
 309
 310 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_l_reverse.con" as lemma.
 311
 312 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_r.con" as lemma.
 313
 314 (*#* Misc redundant properties *)
 315
 316 inline procedural "cic:/Coq/ZArith/BinInt/Zeq_minus.con" as lemma.
 317
 318 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_eq.con" as lemma.
 319
 320 (*#*********************************************************************)
 321
 322 (*#* Properties of multiplication on binary integer numbers *)
 323
 324 (*#* One is neutral for multiplication *)
 325
 326 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_1_l.con" as theorem.
 327
 328 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_1_r.con" as theorem.
 329
 330 (*#* Zero property of multiplication *)
 331
 332 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_0_l.con" as theorem.
 333
 334 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_0_r.con" as theorem.
 335
 336 (* UNEXPORTED
 337 Hint Local Resolve Zmult_0_l Zmult_0_r.
 338 *)
 339
 340 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_0_r_reverse.con" as lemma.
 341
 342 (*#* Commutativity of multiplication *)
 343
 344 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_comm.con" as theorem.
 345
 346 (*#* Associativity of multiplication *)
 347
 348 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_assoc.con" as theorem.
 349
 350 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_assoc_reverse.con" as lemma.
 351
 352 (*#* Associativity mixed with commutativity *)
 353
 354 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_permute.con" as theorem.
 355
 356 (*#* Z is integral *)
 357
 358 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_integral_l.con" as theorem.
 359
 360 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_integral.con" as theorem.
 361
 362 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_1_inversion_l.con" as lemma.
 363
 364 (*#* Multiplication and Opposite *)
 365
 366 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_mult_distr_l.con" as theorem.
 367
 368 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_mult_distr_r.con" as theorem.
 369
 370 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_mult_distr_l_reverse.con" as lemma.
 371
 372 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_opp_comm.con" as theorem.
 373
 374 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_opp_opp.con" as theorem.
 375
 376 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_eq_mult_neg_1.con" as theorem.
 377
 378 (*#* Distributivity of multiplication over addition *)
 379
 380 inline procedural "cic:/Coq/ZArith/BinInt/weak_Zmult_plus_distr_r.con" as lemma.
 381
 382 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_plus_distr_r.con" as theorem.
 383
 384 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_plus_distr_l.con" as theorem.
 385
 386 (*#* Distributivity of multiplication over subtraction *)
 387
 388 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_minus_distr_r.con" as lemma.
 389
 390 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con" as lemma.
 391
 392 (*#* Simplification of multiplication for non-zero integers *)
 393
 394 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_reg_l.con" as lemma.
 395
 396 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_reg_r.con" as lemma.
 397
 398 (*#* Addition and multiplication by 2 *)
 399
 400 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con" as lemma.
 401
 402 (*#* Multiplication and successor *)
 403
 404 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_r.con" as lemma.
 405
 406 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_r_reverse.con" as lemma.
 407
 408 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_l.con" as lemma.
 409
 410 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_l_reverse.con" as lemma.
 411
 412 (*#* Misc redundant properties *)
 413
 414 inline procedural "cic:/Coq/ZArith/BinInt/Z_eq_mult.con" as lemma.
 415
 416 (*#*********************************************************************)
 417
 418 (*#* Relating binary positive numbers and binary integers *)
 419
 420 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_xI.con" as lemma.
 421
 422 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_xO.con" as lemma.
 423
 424 inline procedural "cic:/Coq/ZArith/BinInt/Zneg_xI.con" as lemma.
 425
 426 inline procedural "cic:/Coq/ZArith/BinInt/Zneg_xO.con" as lemma.
 427
 428 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_plus_distr.con" as lemma.
 429
 430 inline procedural "cic:/Coq/ZArith/BinInt/Zneg_plus_distr.con" as lemma.
 431
 432 (*#*********************************************************************)
 433
 434 (*#* Order relations *)
 435
 436 inline procedural "cic:/Coq/ZArith/BinInt/Zlt.con" as definition.
 437
 438 inline procedural "cic:/Coq/ZArith/BinInt/Zgt.con" as definition.
 439
 440 inline procedural "cic:/Coq/ZArith/BinInt/Zle.con" as definition.
 441
 442 inline procedural "cic:/Coq/ZArith/BinInt/Zge.con" as definition.
 443
 444 inline procedural "cic:/Coq/ZArith/BinInt/Zne.con" as definition.
 445
 446 (* NOTATION
 447 Infix "<=" := Zle : Z_scope.
 448 *)
 449
 450 (* NOTATION
 451 Infix "<" := Zlt : Z_scope.
 452 *)
 453
 454 (* NOTATION
 455 Infix ">=" := Zge : Z_scope.
 456 *)
 457
 458 (* NOTATION
 459 Infix ">" := Zgt : Z_scope.
 460 *)
 461
 462 (* NOTATION
 463 Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
 464 *)
 465
 466 (* NOTATION
 467 Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
 468 *)
 469
 470 (* NOTATION
 471 Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
 472 *)
 473
 474 (* NOTATION
 475 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 476 *)
 477
 478 (*#*********************************************************************)
 479
 480 (*#* Absolute value on integers *)
 481
 482 inline procedural "cic:/Coq/ZArith/BinInt/Zabs_nat.con" as definition.
 483
 484 inline procedural "cic:/Coq/ZArith/BinInt/Zabs.con" as definition.
 485
 486 (*#*********************************************************************)
 487
 488 (*#* From [nat] to [Z] *)
 489
 490 inline procedural "cic:/Coq/ZArith/BinInt/Z_of_nat.con" as definition.
 491
 492 include "NArith/BinNat.ma".
 493
 494 inline procedural "cic:/Coq/ZArith/BinInt/Zabs_N.con" as definition.
 495
 496 inline procedural "cic:/Coq/ZArith/BinInt/Z_of_N.con" as definition.
 497