weblib/arithmetics/gcd.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/primes.ma".
  13
  14 let rec gcd_aux p m n: nat ≝
  15 match p with
  16   [O ⇒ m
  17   |S q ⇒
  18     match dividesb n m with
  19     [ true ⇒ n
  20     | false ⇒ gcd_aux q n (m \mod n)]].
  21
  22 definition gcd : nat → nat → nat ≝ λn,m:nat.
  23   match leb n m with
  24   [ true ⇒ gcd_aux n m n
  25   | false ⇒ gcd_aux m n m ].
  26
  27 theorem commutative_gcd: ∀n,m. gcd n m = gcd m n.
  28 #n #m normalize @leb_elim
  29   [#lenm cases(le_to_or_lt_eq … lenm)
  30     [#ltnm >not_le_to_leb_false // @lt_to_not_le //
  31     |#eqnm >eqnm (cases (leb m m)) //
  32     ]
  33   |#notlenm >le_to_leb_true // @(transitive_le ? (S m)) //
  34    @not_le_to_lt //
  35   ]
  36 qed.
  37
  38 theorem gcd_O_l: ∀m. gcd O m = m.
  39 // qed.
  40
  41 theorem divides_mod: ∀p,m,n:nat. O < n →
  42   p ∣ m → p ∣ n → p ∣ (m \mod n).
  43 #p #m #n #posn * #qm #eqm * #qn #eqn
  44 @(quotient ?? (qm - qn*(m / n))) >distributive_times_minus
  45 <eqm <associative_times <eqn @sym_eq @plus_to_minus /2/
  46 qed.
  47
  48 theorem divides_mod_to_divides: ∀p,m,n:nat. O < n →
  49   p ∣ (m \mod n) → p ∣ n → p ∣ m.
  50 #p #m #n #posn * #q1 #eq1 * #q2 #eq2
  51 @(quotient p m ((q2*(m / n))+q1)) >distributive_times_plus
  52 <eq1 <associative_times <eq2 /2/
  53 qed.
  54
  55 lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m →
  56   gcd_aux p m n = n.
  57 #p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm normalize
  58 >divides_to_dividesb_true normalize //
  59 qed.
  60
  61 theorem divides_to_gcd: ∀m,n. O < n → n ∣ m →
  62   gcd n m = n.
  63 #m #n #posn (cases m)
  64  [>commutative_gcd //
  65  |#l #divn (cut (n ≤ (S l))) [@divides_to_le //] #len normalize
  66   >le_to_leb_true // normalize @divides_to_gcd_aux //
  67  ]
  68 qed.
  69
  70 lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m →
  71   gcd_aux (S p) m n = gcd_aux p n (m \mod n).
  72 #p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false
  73 normalize // qed.
  74
  75 theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →
  76   gcd_aux p m n ∣ m ∧ gcd_aux p m n ∣ n.
  77 #p (elim p)
  78   [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
  79   |#q #Hind #m #n #posn #lenm #lenS cases(decidable_divides n m)
  80     [#divnm >(divides_to_gcd_aux … posn divnm) // % //
  81     |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
  82      cut (gcd_aux q n (m \mod n) ∣ n ∧
  83           gcd_aux q n (m \mod n) ∣ mod m n)
  84       [cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
  85        @Hind
  86         [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
  87          @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
  88         |/2/
  89         |@le_S_S_to_le @(transitive_le … ltmod lenS)
  90         ]
  91       |* #H #H1 % [@(divides_mod_to_divides … posn H1) // |//]
  92       ]
  93     ]
  94   ]
  95 qed.
  96
  97 theorem divides_gcd_nm: ∀n,m.
  98   gcd n m ∣ m ∧ gcd n m ∣ n.
  99 #n #m cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO /2/]
 100 #posn cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO /2/]
 101 #posm normalize @leb_elim normalize
 102   [#lenm @divides_gcd_aux_mn //
 103   |#notlt normalize cut (∀A,B. A∧B → B∧A) [#A #B * /2/] #sym_and
 104    @sym_and @divides_gcd_aux_mn // @(transitive_le ? (S m)) //
 105    @not_le_to_lt //
 106   ]
 107 qed.
 108
 109 theorem divides_gcd_l: ∀n,m. gcd n m ∣ n.
 110 #n #m @(proj2  ? ? (divides_gcd_nm n m)).
 111 qed.
 112
 113 theorem divides_gcd_r: \forall n,m. gcd n m ∣ m.
 114 #n #m @(proj1 ? ? (divides_gcd_nm n m)).
 115 qed.
 116
 117 theorem divides_times_gcd_aux: ∀p,m,n,d,c.
 118   O < c → O < n → n ≤ m → n ≤ p →
 119     d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd_aux p m n.
 120 #p (elim p)
 121   [#m #n #d #c #_ #posn #_ #lenO @False_ind @(absurd … lenO) /2/
 122   |#q #Hind #m #n #d #c #posc #posn #lenm #lenS #dcm #dcn
 123    cases(decidable_divides n m)
 124     [#divnm >(divides_to_gcd_aux … posn divnm) //
 125     |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
 126      cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
 127      @Hind //
 128       [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
 129        @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
 130       |/2/
 131       |@le_S_S_to_le @(transitive_le … ltmod lenS)
 132       |<times_mod // < (commutative_times c m)
 133        <(commutative_times c n) @divides_mod //
 134        >(times_n_O 0) @lt_times //
 135       ]
 136     ]
 137   ]
 138 qed.
 139
 140 (*a particular case of the previous theorem, with c=1 *)
 141 theorem divides_gcd_aux: ∀p,m,n,d. O < n → n ≤ m → n ≤ p →
 142   d ∣ m \to d ∣ n \to d ∣ gcd_aux p m n.
 143   (* bell'esempio di smart application *)
 144 /2/ qed.
 145
 146 theorem divides_d_times_gcd: ∀m,n,d,c. O < c →
 147   d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd n m.
 148 #m #n #d #c #posc #dcm #dcn
 149 cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO @dcm] #posn
 150 cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO <commutative_gcd @dcn] #posm
 151 normalize @leb_elim normalize
 152   [#lenm @divides_times_gcd_aux //
 153   |#nlenm @divides_times_gcd_aux //
 154    @(transitive_le ? (S m)) // @not_le_to_lt //
 155   ]
 156 qed.
 157
 158 (* a particular case of the previous theorem, with c=1 *)
 159 theorem divides_d_gcd: ∀m,n,d.
 160  d ∣ m → d ∣ n → d ∣ gcd n m.
 161 #m #n #d #divdn #divdn applyS (divides_d_times_gcd m n d 1) //
 162 qed.
 163
 164 theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m →  n ≤ p →
 165   ∃a,b. a*n - b*m = gcd_aux p m n ∨ b*m - a*n = gcd_aux p m n.
 166 #p (elim p)
 167   [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
 168   |#q #Hind #m #n #posn #lenm #lenS
 169    cut (0 < m) [@lt_to_le_to_lt //] #posm
 170    cases(decidable_divides n m)
 171     [#divnm >(divides_to_gcd_aux … posn divnm) //
 172      @(ex_intro ?? 1) @(ex_intro ?? 0) %1 //
 173     |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
 174      cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
 175      lapply (Hind n (m \mod n) ???)
 176       [@le_S_S_to_le @(transitive_le … ltmod lenS)
 177       |/2/
 178       |cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
 179        @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
 180       ]
 181      * #a * #b * #H
 182       [(* first case *)
 183        <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %2
 184        <commutative_plus >distributive_times_plus_r
 185        >(div_mod m n) in ⊢(? ? (? % ?) ?)
 186        >associative_times <commutative_plus >distributive_times_plus
 187        <minus_plus <commutative_plus <plus_minus //
 188       |(* second case *)
 189         <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
 190         >distributive_times_plus_r
 191         >(div_mod m n) in ⊢ (? ? (? ? %) ?)
 192         >distributive_times_plus >associative_times
 193         <minus_plus <commutative_plus <plus_minus //
 194       ]
 195     ]
 196   ]
 197 qed.
 198
 199 theorem eq_minus_gcd:
 200   ∀m,n.∃ a,b.a*n - b*m = gcd n m ∨ b*m - a*n = gcd n m.
 201   #m #n cases(le_to_or_lt_eq …(le_O_n n))
 202   [|#eqn0 >eqn0 @(ex_intro ?? O) @(ex_intro ? ? 1) %2 applyS minus_n_O]
 203 #posn cases(le_to_or_lt_eq …(le_O_n m))
 204   [|#eqm0 >eqm0 @(ex_intro ?? 1) @(ex_intro ? ? 0) %1 applyS minus_n_O]
 205 #posm normalize @leb_elim normalize
 206   [#lenm @eq_minus_gcd_aux //
 207   |#nlenm lapply(eq_minus_gcd_aux m n m posm ? (le_n m))
 208     [@(transitive_le … (not_le_to_lt … nlenm)) //]
 209    * #a * #b * #H @(ex_intro ?? b) @(ex_intro ?? a) [%2 // |%1 //]
 210   ]
 211 qed.
 212
 213 (* some properties of gcd *)
 214
 215 theorem gcd_O_to_eq_O:∀m,n:nat.
 216   gcd m n = O → m = O ∧ n = O.
 217 #m #n #H cut (O ∣ n ∧ O ∣ m)
 218   [<H @divides_gcd_nm| * * #q1 #H1 * #q2 #H2 % // ]
 219 qed.
 220
 221 theorem lt_O_gcd:∀m,n:nat. O < n → O < gcd m n.
 222 #m #n #posn @(nat_case (gcd m n)) //
 223 #H (cases (gcd_O_to_eq_O m n H)) //
 224 qed.
 225
 226 theorem gcd_n_n: ∀n.gcd n n = n.
 227 #n (cases n) //
 228 #m @le_to_le_to_eq
 229   [@divides_to_le //
 230   |@divides_to_le (*/2/*) [@lt_O_gcd // |@divides_d_gcd // ]
 231   ]
 232 qed.
 233
 234 (* some properties or relative primes - i.e. gcd = 1 *)
 235 theorem gcd_1_to_lt_O: ∀i,n. 1 < n → gcd i n = 1 → O < i.
 236 #i #n #lt1n #gcd1 cases (le_to_or_lt_eq ?? (le_O_n i)) //
 237 #iO @False_ind @(absurd … gcd1) <iO normalize
 238 @sym_not_eq @lt_to_not_eq //
 239 qed.
 240
 241 theorem gcd_1_to_lt_n: ∀i,n. 1 < n →
 242   i ≤ n → gcd i n = 1 → i < n.
 243 #i #n #lt1n #lein #gcd1 cases (le_to_or_lt_eq ?? lein) //
 244 (* impressive *)
 245 qed.
 246
 247 theorem  gcd_n_times_nm: ∀n,m. O < m → gcd n (n*m) = n.
 248 #n #m #posm @(nat_case n) //
 249 #l #eqn @le_to_le_to_eq
 250   [@divides_to_le //
 251   |@divides_to_le
 252     [@lt_O_gcd >(times_n_O O) @lt_times // |@divides_d_gcd /2/]
 253   ]
 254 qed.
 255
 256 theorem le_gcd_times: ∀m,n,p. O< p → gcd m n ≤ gcd m (n*p).
 257 #m #n #p #posp @(nat_case n) //
 258 #l #eqn @divides_to_le [@lt_O_gcd >(times_n_O O) @lt_times //]
 259 @divides_d_gcd [@(transitive_divides ? (S l)) /2/ |//]
 260 qed.
 261
 262 theorem gcd_times_SO_to_gcd_SO: ∀m,n,p:nat. O < n → O < p →
 263   gcd m (n*p) = 1 → gcd m n = 1.
 264 #m #n #p #posn #posp #gcd1 @le_to_le_to_eq
 265   [<gcd1 @le_gcd_times // | @lt_O_gcd //]
 266 qed.
 267
 268 (* for the "converse" of the previous result see the end  of this development *)
 269
 270 theorem eq_gcd_SO_to_not_divides: ∀n,m. 1 < n →
 271   gcd n m = 1 → n ∤ m.
 272 #n #m #lt1n #gcd1 @(not_to_not … (gcd n m = n))
 273   [#divnm @divides_to_gcd /2/ | /2/]
 274 qed.
 275
 276 theorem gcd_SO_n: ∀n:nat. gcd 1 n = 1.
 277 #n @le_to_le_to_eq
 278   [@divides_to_le // |>commutative_gcd @lt_O_gcd //]
 279 qed.
 280
 281 theorem divides_gcd_mod: ∀m,n:nat. O < n →
 282   gcd m n ∣ gcd n (m \mod n).
 283 #m #n #posn @divides_d_gcd [@divides_mod // | //]
 284 qed.
 285
 286 theorem divides_mod_gcd: ∀m,n:nat. O < n →
 287   gcd n (m \mod n) ∣ gcd m n.
 288 #m #n #posn @divides_d_gcd
 289   [@divides_gcd_l |@(divides_mod_to_divides ?? n) //]
 290 qed.
 291
 292 theorem gcd_mod: ∀m,n:nat. O < n →
 293   gcd n (m \mod n) = gcd m n.
 294 #m #n #posn @antisymmetric_divides
 295   [@divides_mod_gcd // | @divides_gcd_mod //]
 296 qed.
 297
 298 (* gcd and primes *)
 299
 300 theorem prime_to_gcd_1: ∀n,m:nat. prime n → n ∤ m →
 301   gcd n m = 1.
 302 (* bella dimostrazione *)
 303 #n #m * #lt1n #primen #ndivnm @le_to_le_to_eq
 304   [@not_lt_to_le @(not_to_not … (primen (gcd n m) (divides_gcd_l …)))
 305    @(not_to_not ? (n ∣m)) //
 306   |@lt_O_gcd @not_eq_to_le_to_lt // @(not_to_not ? (n ∣ m)) //
 307   ]
 308 qed.
 309
 310 (* primes and divides *)
 311 theorem divides_times_to_divides: ∀p,n,m:nat.prime p →
 312   p ∣ n*m → p ∣ n ∨ p ∣ m.
 313 #p #n #m #primp * #c #nm
 314 cases (decidable_divides p n) /2/ #ndivpn %2
 315 cut (∃a,b. a*n - b*p = 1 ∨ b*p - a*n = 1)
 316   [<(prime_to_gcd_1 … primp ndivpn) >commutative_gcd @eq_minus_gcd]
 317 * #a * #b * #H
 318   [@(quotient ?? (a*c-b*m)) >distributive_times_minus <associative_times
 319    >(commutative_times p) >associative_times <nm <associative_times
 320    <associative_times <commutative_times >(commutative_times (p*b))
 321    <distributive_times_minus //
 322   |@(quotient ?? (b*m -a*c)) >distributive_times_minus <(associative_times p)
 323    <(associative_times p) <(commutative_times a) >(associative_times a)
 324    <nm <(associative_times a) <commutative_times >(commutative_times (a*n))
 325    <distributive_times_minus //
 326   ]
 327 qed.
 328
 329 theorem divides_exp_to_divides:
 330 ∀p,n,m:nat. prime p → p ∣n^m → p ∣ n.
 331 #p #n #m #primep (elim m) normalize /2/
 332 #l #Hind #H cases(divides_times_to_divides  … primep H) /2/
 333 qed.
 334
 335 theorem divides_exp_to_eq:
 336 ∀p,q,m:nat. prime p → prime q →
 337   p ∣ q^m → p = q.
 338 #p #q #m #H * #lt1q #primeq #H @primeq /2/
 339 qed.
 340
 341 (* relative primes *)
 342 theorem eq_gcd_times_1: ∀p,n,m:nat. O < n → O < m →
 343  gcd p n = 1 → gcd p m = 1 → gcd p (n*m) = 1.
 344 #p #n #m #posn #posm #primepn #primepm
 345 @le_to_le_to_eq [|@lt_O_gcd >(times_n_O 0) @lt_times //]
 346 @not_lt_to_le % #lt1gcd
 347 cut (smallest_factor (gcd p (n*m)) ∣ n ∨
 348      smallest_factor (gcd p (n*m)) ∣ m)
 349   [@divides_times_to_divides
 350     [@prime_smallest_factor_n //
 351     |@(transitive_divides ? (gcd p (n*m))) //
 352      @divides_smallest_factor_n /2/
 353     ]
 354   |* #H
 355     [@(absurd ?? (lt_to_not_le …(lt_SO_smallest_factor … lt1gcd)))
 356      <primepn @divides_to_le // @divides_d_gcd //
 357      @(transitive_divides … (divides_smallest_factor_n …))
 358        [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
 359     |@(absurd ?? (lt_to_not_le … (lt_SO_smallest_factor …lt1gcd)))
 360      <primepm @divides_to_le // @divides_d_gcd //
 361      @(transitive_divides … (divides_smallest_factor_n …))
 362        [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
 363   ]
 364 qed.
 365
 366
 367 theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
 368 gcd p n = 1 → p ∣ (n*m) → p ∣ m.
 369 #p #m #n #posn #gcd1 * #c #nm
 370 cases(eq_minus_gcd m p) #a * #b * #H >gcd1 in H #H
 371   [@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times
 372    <associative_times <nm >(commutative_times m) >commutative_times
 373    >associative_times <distributive_times_minus //
 374   |@(quotient ?? (c*b-a*n)) >distributive_times_minus <associative_times
 375    <associative_times <nm >(commutative_times m) <(commutative_times n)
 376    >associative_times <distributive_times_minus //
 377   ]
 378 qed.
 379
 380 (*
 381 theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
 382 divides p n \to divides q n \to divides (p*q) n.
 383 intros.elim H3.
 384 rewrite > H5 in H4.
 385 elim (divides_times_to_divides ? ? ? H1 H4)
 386   [elim H.apply False_ind.
 387    apply H2.apply sym_eq.apply H8
 388     [assumption
 389     |apply prime_to_lt_SO.assumption
 390     ]
 391   |elim H6.
 392    apply (witness ? ? n1).
 393    rewrite > assoc_times.
 394    rewrite < H7.assumption
 395   ]
 396 qed.
 397 *)
 398
 399 theorem divides_to_divides_times: ∀p,q,n. prime p  → p ∤ q →
 400  p ∣ n → q ∣ n → p*q ∣ n.
 401 #p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn in divpn)
 402 #divpn cases(divides_times_to_divides ??? primep divpn) #H
 403   [@False_ind /2/
 404   |cases H #c #eqb @(quotient ?? c) >eqb <associative_times //
 405   ]
 406 qed.