helm/software/matita/contribs/procedural/Coq/ZArith/Znumtheory.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: Znumtheory.v,v 1.5.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
  34
  35 include "ZArith/ZArith_base.ma".
  36
  37 include "ZArith/Zcomplements.ma".
  38
  39 include "ZArith/Zdiv.ma".
  40
  41 (* UNEXPORTED
  42 Open Local Scope Z_scope.
  43 *)
  44
  45 (*#* This file contains some notions of number theory upon Z numbers:
  46      - a divisibility predicate [Zdivide]
  47      - a gcd predicate [gcd]
  48      - Euclid algorithm [euclid]
  49      - an efficient [Zgcd] function
  50      - a relatively prime predicate [rel_prime]
  51      - a prime predicate [prime]
  52 *)
  53
  54 (*#* * Divisibility *)
  55
  56 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide.ind".
  57
  58 (*#* Syntax for divisibility *)
  59
  60 (* NOTATION
  61 Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
  62 *)
  63
  64 (*#* Results concerning divisibility*)
  65
  66 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_refl.con" as lemma.
  67
  68 inline procedural "cic:/Coq/ZArith/Znumtheory/Zone_divide.con" as lemma.
  69
  70 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_0.con" as lemma.
  71
  72 (* UNEXPORTED
  73 Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith.
  74 *)
  75
  76 inline procedural "cic:/Coq/ZArith/Znumtheory/Zmult_divide_compat_l.con" as lemma.
  77
  78 inline procedural "cic:/Coq/ZArith/Znumtheory/Zmult_divide_compat_r.con" as lemma.
  79
  80 (* UNEXPORTED
  81 Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r: zarith.
  82 *)
  83
  84 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_plus_r.con" as lemma.
  85
  86 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_opp_r.con" as lemma.
  87
  88 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_opp_r_rev.con" as lemma.
  89
  90 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_opp_l.con" as lemma.
  91
  92 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_opp_l_rev.con" as lemma.
  93
  94 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_minus_l.con" as lemma.
  95
  96 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_mult_l.con" as lemma.
  97
  98 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_mult_r.con" as lemma.
  99
 100 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_factor_r.con" as lemma.
 101
 102 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_factor_l.con" as lemma.
 103
 104 (* UNEXPORTED
 105 Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
 106   Zdivide_opp_l_rev Zdivide_minus_l Zdivide_mult_l Zdivide_mult_r
 107   Zdivide_factor_r Zdivide_factor_l: zarith.
 108 *)
 109
 110 (*#* Auxiliary result. *)
 111
 112 inline procedural "cic:/Coq/ZArith/Znumtheory/Zmult_one.con" as lemma.
 113
 114 (*#* Only [1] and [-1] divide [1]. *)
 115
 116 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_1.con" as lemma.
 117
 118 (*#* If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *)
 119
 120 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_antisym.con" as lemma.
 121
 122 (*#* If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
 123
 124 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_bounds.con" as lemma.
 125
 126 (*#* * Greatest common divisor (gcd). *)
 127
 128 (*#* There is no unicity of the gcd; hence we define the predicate [gcd a b d]
 129      expressing that [d] is a gcd of [a] and [b].
 130      (We show later that the [gcd] is actually unique if we discard its sign.) *)
 131
 132 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd.ind".
 133
 134 (*#* Trivial properties of [gcd] *)
 135
 136 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_sym.con" as lemma.
 137
 138 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_0.con" as lemma.
 139
 140 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_minus.con" as lemma.
 141
 142 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_opp.con" as lemma.
 143
 144 (* UNEXPORTED
 145 Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
 146 *)
 147
 148 (*#* * Extended Euclid algorithm. *)
 149
 150 (*#* Euclid's algorithm to compute the [gcd] mainly relies on
 151     the following property. *)
 152
 153 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_for_euclid.con" as lemma.
 154
 155 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_for_euclid2.con" as lemma.
 156
 157 (*#* We implement the extended version of Euclid's algorithm,
 158     i.e. the one computing Bezout's coefficients as it computes
 159     the [gcd]. We follow the algorithm given in Knuth's
 160     "Art of Computer Programming", vol 2, page 325. *)
 161
 162 (* UNEXPORTED
 163 Section extended_euclid_algorithm
 164 *)
 165
 166 (* UNEXPORTED
 167 cic:/Coq/ZArith/Znumtheory/extended_euclid_algorithm/a.var
 168 *)
 169
 170 (* UNEXPORTED
 171 cic:/Coq/ZArith/Znumtheory/extended_euclid_algorithm/b.var
 172 *)
 173
 174 (*#* The specification of Euclid's algorithm is the existence of
 175     [u], [v] and [d] such that [ua+vb=d] and [(gcd a b d)]. *)
 176
 177 inline procedural "cic:/Coq/ZArith/Znumtheory/Euclid.ind".
 178
 179 (*#* The recursive part of Euclid's algorithm uses well-founded
 180     recursion of non-negative integers. It maintains 6 integers
 181     [u1,u2,u3,v1,v2,v3] such that the following invariant holds:
 182     [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)].
 183     *)
 184
 185 inline procedural "cic:/Coq/ZArith/Znumtheory/euclid_rec.con" as lemma.
 186
 187 (*#* We get Euclid's algorithm by applying [euclid_rec] on
 188     [1,0,a,0,1,b] when [b>=0] and [1,0,a,0,-1,-b] when [b<0]. *)
 189
 190 inline procedural "cic:/Coq/ZArith/Znumtheory/euclid.con" as lemma.
 191
 192 (* UNEXPORTED
 193 End extended_euclid_algorithm
 194 *)
 195
 196 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_uniqueness_apart_sign.con" as theorem.
 197
 198 (*#* * Bezout's coefficients *)
 199
 200 inline procedural "cic:/Coq/ZArith/Znumtheory/Bezout.ind".
 201
 202 (*#* Existence of Bezout's coefficients for the [gcd] of [a] and [b] *)
 203
 204 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_bezout.con" as lemma.
 205
 206 (*#* gcd of [ca] and [cb] is [c gcd(a,b)]. *)
 207
 208 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_mult.con" as lemma.
 209
 210 (*#* We could obtain a [Zgcd] function via [euclid]. But we propose
 211   here a more direct version of a [Zgcd], with better extraction
 212   (no bezout coeffs). *)
 213
 214 inline procedural "cic:/Coq/ZArith/Znumtheory/Zgcd_pos.con" as definition.
 215
 216 inline procedural "cic:/Coq/ZArith/Znumtheory/Zgcd_spec.con" as definition.
 217
 218 inline procedural "cic:/Coq/ZArith/Znumtheory/Zgcd.con" as definition.
 219
 220 inline procedural "cic:/Coq/ZArith/Znumtheory/Zgcd_is_pos.con" as lemma.
 221
 222 inline procedural "cic:/Coq/ZArith/Znumtheory/Zgcd_is_gcd.con" as lemma.
 223
 224 (*#* * Relative primality *)
 225
 226 inline procedural "cic:/Coq/ZArith/Znumtheory/rel_prime.con" as definition.
 227
 228 (*#* Bezout's theorem: [a] and [b] are relatively prime if and
 229     only if there exist [u] and [v] such that [ua+vb = 1]. *)
 230
 231 inline procedural "cic:/Coq/ZArith/Znumtheory/rel_prime_bezout.con" as lemma.
 232
 233 inline procedural "cic:/Coq/ZArith/Znumtheory/bezout_rel_prime.con" as lemma.
 234
 235 (*#* Gauss's theorem: if [a] divides [bc] and if [a] and [b] are
 236     relatively prime, then [a] divides [c]. *)
 237
 238 inline procedural "cic:/Coq/ZArith/Znumtheory/Gauss.con" as theorem.
 239
 240 (*#* If [a] is relatively prime to [b] and [c], then it is to [bc] *)
 241
 242 inline procedural "cic:/Coq/ZArith/Znumtheory/rel_prime_mult.con" as lemma.
 243
 244 inline procedural "cic:/Coq/ZArith/Znumtheory/rel_prime_cross_prod.con" as lemma.
 245
 246 (*#* After factorization by a gcd, the original numbers are relatively prime. *)
 247
 248 inline procedural "cic:/Coq/ZArith/Znumtheory/Zis_gcd_rel_prime.con" as lemma.
 249
 250 (*#* * Primality *)
 251
 252 inline procedural "cic:/Coq/ZArith/Znumtheory/prime.ind".
 253
 254 (*#* The sole divisors of a prime number [p] are [-1], [1], [p] and [-p]. *)
 255
 256 inline procedural "cic:/Coq/ZArith/Znumtheory/prime_divisors.con" as lemma.
 257
 258 (*#* A prime number is relatively prime with any number it does not divide *)
 259
 260 inline procedural "cic:/Coq/ZArith/Znumtheory/prime_rel_prime.con" as lemma.
 261
 262 (* UNEXPORTED
 263 Hint Resolve prime_rel_prime: zarith.
 264 *)
 265
 266 (*#* [Zdivide] can be expressed using [Zmod]. *)
 267
 268 inline procedural "cic:/Coq/ZArith/Znumtheory/Zmod_divide.con" as lemma.
 269
 270 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_mod.con" as lemma.
 271
 272 (*#* [Zdivide] is hence decidable *)
 273
 274 inline procedural "cic:/Coq/ZArith/Znumtheory/Zdivide_dec.con" as lemma.
 275
 276 (*#* If a prime [p] divides [ab] then it divides either [a] or [b] *)
 277
 278 inline procedural "cic:/Coq/ZArith/Znumtheory/prime_mult.con" as lemma.
 279