helm/matita/library/nat/gcd.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/gcd".
  16
  17 include "nat/primes.ma".
  18
  19 let rec gcd_aux p m n: nat \def
  20 match divides_b n m with
  21 [ true \Rightarrow n
  22 | false \Rightarrow
  23   match p with
  24   [O \Rightarrow n
  25   |(S q) \Rightarrow gcd_aux q n (mod m n)]].
  26
  27 definition gcd : nat \to nat \to nat \def
  28 \lambda n,m:nat.
  29   match leb n m with
  30   [ true \Rightarrow
  31     match n with
  32     [ O \Rightarrow m
  33     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
  34   | false \Rightarrow
  35     match m with
  36     [ O \Rightarrow n
  37     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
  38
  39 theorem divides_mod: \forall p,m,n:nat. O < n \to divides p m \to divides p n \to
  40 divides p (mod m n).
  41 intros.elim H1.elim H2.
  42 apply witness ? ? (n2 - n1*(div m n)).
  43 rewrite > distr_times_minus.
  44 rewrite < H3.
  45 rewrite < assoc_times.
  46 rewrite < H4.
  47 apply sym_eq.
  48 apply plus_to_minus.
  49 rewrite > div_mod m n in \vdash (? ? %).
  50 rewrite > sym_times.
  51 apply eq_plus_to_le ? ? (mod m n).
  52 reflexivity.
  53 assumption.
  54 rewrite > sym_times.
  55 apply div_mod.assumption.
  56 qed.
  57
  58 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
  59 divides p (mod m n) \to divides p n \to divides p m.
  60 intros.elim H1.elim H2.
  61 apply witness p m ((n1*(div m n))+n2).
  62 rewrite > distr_times_plus.
  63 rewrite < H3.
  64 rewrite < assoc_times.
  65 rewrite < H4.rewrite < sym_times.
  66 apply div_mod.assumption.
  67 qed.
  68
  69 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
  70 divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n.
  71 intro.elim p.
  72 absurd O < n.assumption.apply le_to_not_lt.assumption.
  73 cut (divides n1 m) \lor \not (divides n1 m).
  74 change with
  75 (divides
  76 (match divides_b n1 m with
  77 [ true \Rightarrow n1
  78 | false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land
  79 (divides
  80 (match divides_b n1 m with
  81 [ true \Rightarrow n1
  82 | false \Rightarrow gcd_aux n n1 (mod m n1)]) n1).
  83 elim Hcut.rewrite > divides_to_divides_b_true.
  84 simplify.
  85 split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
  86 assumption.assumption.
  87 rewrite > not_divides_to_divides_b_false.
  88 change with
  89 (divides (gcd_aux n n1 (mod m n1)) m) \land
  90 (divides (gcd_aux n n1 (mod m n1)) n1).
  91 cut (divides (gcd_aux n n1 (mod m n1)) n1) \land
  92 (divides (gcd_aux n n1 (mod m n1)) (mod m n1)).
  93 elim Hcut1.
  94 split.apply divides_mod_to_divides ? ? n1.
  95 assumption.assumption.assumption.assumption.
  96 apply H.
  97 cut O \lt mod m n1 \lor O = mod m n1.
  98 elim Hcut1.assumption.
  99 apply False_ind.apply H4.apply mod_O_to_divides.
 100 assumption.apply sym_eq.assumption.
 101 apply le_to_or_lt_eq.apply le_O_n.
 102 apply lt_to_le.
 103 apply lt_mod_m_m.assumption.
 104 apply le_S_S_to_le.
 105 apply trans_le ? n1.
 106 change with mod m n1 < n1.
 107 apply lt_mod_m_m.assumption.assumption.
 108 assumption.assumption.
 109 apply decidable_divides n1 m.assumption.
 110 qed.
 111
 112 theorem divides_gcd_nm: \forall n,m.
 113 divides (gcd n m) m \land divides (gcd n m) n.
 114 intros.
 115 change with
 116 divides
 117 (match leb n m with
 118   [ true \Rightarrow
 119     match n with
 120     [ O \Rightarrow m
 121     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 122   | false \Rightarrow
 123     match m with
 124     [ O \Rightarrow n
 125     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m
 126 \land
 127  divides
 128 (match leb n m with
 129   [ true \Rightarrow
 130     match n with
 131     [ O \Rightarrow m
 132     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 133   | false \Rightarrow
 134     match m with
 135     [ O \Rightarrow n
 136     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n.
 137 apply leb_elim n m.
 138 apply nat_case1 n.
 139 simplify.intros.split.
 140 apply witness m m (S O).apply times_n_SO.
 141 apply witness m O O.apply times_n_O.
 142 intros.change with
 143 divides (gcd_aux (S m1) m (S m1)) m
 144 \land
 145 divides (gcd_aux (S m1) m (S m1)) (S m1).
 146 apply divides_gcd_aux_mn.
 147 simplify.apply le_S_S.apply le_O_n.
 148 assumption.apply le_n.
 149 simplify.intro.
 150 apply nat_case1 m.
 151 simplify.intros.split.
 152 apply witness n O O.apply times_n_O.
 153 apply witness n n (S O).apply times_n_SO.
 154 intros.change with
 155 divides (gcd_aux (S m1) n (S m1)) (S m1)
 156 \land
 157 divides (gcd_aux (S m1) n (S m1)) n.
 158 cut divides (gcd_aux (S m1) n (S m1)) n
 159 \land
 160 divides (gcd_aux (S m1) n (S m1)) (S m1).
 161 elim Hcut.split.assumption.assumption.
 162 apply divides_gcd_aux_mn.
 163 simplify.apply le_S_S.apply le_O_n.
 164 apply not_lt_to_le.simplify.intro.apply H.
 165 rewrite > H1.apply trans_le ? (S n).
 166 apply le_n_Sn.assumption.apply le_n.
 167 qed.
 168
 169 theorem divides_gcd_n: \forall n,m.
 170 divides (gcd n m) n.
 171 intros.
 172 exact proj2  ? ? (divides_gcd_nm n m).
 173 qed.
 174
 175 theorem divides_gcd_m: \forall n,m.
 176 divides (gcd n m) m.
 177 intros.
 178 exact proj1 ? ? (divides_gcd_nm n m).
 179 qed.
 180
 181 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 182 divides d m \to divides d n \to divides d (gcd_aux p m n).
 183 intro.elim p.
 184 absurd O < n.assumption.apply le_to_not_lt.assumption.
 185 change with
 186 divides d
 187 (match divides_b n1 m with
 188 [ true \Rightarrow n1
 189 | false \Rightarrow gcd_aux n n1 (mod m n1)]).
 190 cut divides n1 m \lor \not (divides n1 m).
 191 elim Hcut.
 192 rewrite > divides_to_divides_b_true.
 193 simplify.assumption.
 194 assumption.assumption.
 195 rewrite > not_divides_to_divides_b_false.
 196 change with divides d (gcd_aux n n1 (mod m n1)).
 197 apply H.
 198 cut O \lt mod m n1 \lor O = mod m n1.
 199 elim Hcut1.assumption.
 200 absurd divides n1 m.apply mod_O_to_divides.
 201 assumption.apply sym_eq.assumption.assumption.
 202 apply le_to_or_lt_eq.apply le_O_n.
 203 apply lt_to_le.
 204 apply lt_mod_m_m.assumption.
 205 apply le_S_S_to_le.
 206 apply trans_le ? n1.
 207 change with mod m n1 < n1.
 208 apply lt_mod_m_m.assumption.assumption.
 209 assumption.
 210 apply divides_mod.assumption.assumption.assumption.
 211 assumption.assumption.
 212 apply decidable_divides n1 m.assumption.
 213 qed.
 214
 215 theorem divides_d_gcd: \forall m,n,d.
 216 divides d m \to divides d n \to divides d (gcd n m).
 217 intros.
 218 change with
 219 divides d (
 220 match leb n m with
 221   [ true \Rightarrow
 222     match n with
 223     [ O \Rightarrow m
 224     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 225   | false \Rightarrow
 226     match m with
 227     [ O \Rightarrow n
 228     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
 229 apply leb_elim n m.
 230 apply nat_case1 n.simplify.intros.assumption.
 231 intros.
 232 change with divides d (gcd_aux (S m1) m (S m1)).
 233 apply divides_gcd_aux.
 234 simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
 235 rewrite < H2.assumption.
 236 apply nat_case1 m.simplify.intros.assumption.
 237 intros.
 238 change with divides d (gcd_aux (S m1) n (S m1)).
 239 apply divides_gcd_aux.
 240 simplify.apply le_S_S.apply le_O_n.
 241 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 242 rewrite < H2.assumption.
 243 qed.
 244
 245 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 246 ex nat (\lambda a. ex nat (\lambda b.
 247 a*n - b*m = (gcd_aux p m n) \lor b*m - a*n = (gcd_aux p m n))).
 248 intro.
 249 elim p.
 250 absurd O < n.assumption.apply le_to_not_lt.assumption.
 251 cut O < m.
 252 cut (divides n1 m) \lor \not (divides n1 m).
 253 change with
 254 ex nat (\lambda a. ex nat (\lambda b.
 255 a*n1 - b*m = match divides_b n1 m with
 256 [ true \Rightarrow n1
 257 | false \Rightarrow gcd_aux n n1 (mod m n1)]
 258 \lor
 259 b*m - a*n1 = match divides_b n1 m with
 260 [ true \Rightarrow n1
 261 | false \Rightarrow gcd_aux n n1 (mod m n1)])).
 262 elim Hcut1.
 263 rewrite > divides_to_divides_b_true.
 264 simplify.
 265 apply ex_intro ? ? (S O).
 266 apply ex_intro ? ? O.
 267 left.simplify.rewrite < plus_n_O.
 268 apply sym_eq.apply minus_n_O.
 269 assumption.assumption.
 270 rewrite > not_divides_to_divides_b_false.
 271 change with
 272 ex nat (\lambda a. ex nat (\lambda b.
 273 a*n1 - b*m = gcd_aux n n1 (mod m n1)
 274 \lor
 275 b*m - a*n1 = gcd_aux n n1 (mod m n1))).
 276 cut
 277 ex nat (\lambda a. ex nat (\lambda b.
 278 a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
 279 \lor
 280 b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))).
 281 elim Hcut2.elim H5.elim H6.
 282 (* first case *)
 283 rewrite < H7.
 284 apply ex_intro ? ? (a1+a*(div m n1)).
 285 apply ex_intro ? ? a.
 286 right.
 287 rewrite < sym_plus.
 288 rewrite < sym_times n1.
 289 rewrite > distr_times_plus.
 290 rewrite > sym_times n1.
 291 rewrite > sym_times n1.
 292 rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?).
 293 rewrite > assoc_times.
 294 rewrite < sym_plus.
 295 rewrite > distr_times_plus.
 296 rewrite < eq_minus_minus_minus_plus.
 297 rewrite < sym_plus.
 298 rewrite < plus_minus.
 299 rewrite < minus_n_n.reflexivity.
 300 apply le_n.
 301 assumption.
 302 (* second case *)
 303 rewrite < H7.
 304 apply ex_intro ? ? (a1+a*(div m n1)).
 305 apply ex_intro ? ? a.
 306 left.
 307 rewrite > sym_times.
 308 rewrite > distr_times_plus.
 309 rewrite > sym_times.
 310 rewrite > sym_times n1.
 311 rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
 312 rewrite > distr_times_plus.
 313 rewrite > assoc_times.
 314 rewrite < eq_minus_minus_minus_plus.
 315 rewrite < sym_plus.
 316 rewrite < plus_minus.
 317 rewrite < minus_n_n.reflexivity.
 318 apply le_n.
 319 assumption.
 320 apply H n1 (mod m n1).
 321 cut O \lt mod m n1 \lor O = mod m n1.
 322 elim Hcut2.assumption.
 323 absurd divides n1 m.apply mod_O_to_divides.
 324 assumption.
 325 symmetry.assumption.assumption.
 326 apply le_to_or_lt_eq.apply le_O_n.
 327 apply lt_to_le.
 328 apply lt_mod_m_m.assumption.
 329 apply le_S_S_to_le.
 330 apply trans_le ? n1.
 331 change with mod m n1 < n1.
 332 apply lt_mod_m_m.
 333 assumption.assumption.assumption.assumption.
 334 apply decidable_divides n1 m.assumption.
 335 apply lt_to_le_to_lt ? n1.assumption.assumption.
 336 qed.
 337
 338 theorem eq_minus_gcd: \forall m,n.
 339 ex nat (\lambda a. ex nat (\lambda b.
 340 a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))).
 341 intros.
 342 change with
 343 ex nat (\lambda a. ex nat (\lambda b.
 344 a*n - b*m =
 345 match leb n m with
 346   [ true \Rightarrow
 347     match n with
 348     [ O \Rightarrow m
 349     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 350   | false \Rightarrow
 351     match m with
 352     [ O \Rightarrow n
 353     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
 354 \lor b*m - a*n =
 355 match leb n m with
 356   [ true \Rightarrow
 357     match n with
 358     [ O \Rightarrow m
 359     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 360   | false \Rightarrow
 361     match m with
 362     [ O \Rightarrow n
 363     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
 364 )).
 365 apply leb_elim n m.
 366 apply nat_case1 n.
 367 simplify.intros.
 368 apply ex_intro ? ? O.
 369 apply ex_intro ? ? (S O).
 370 right.simplify.
 371 rewrite < plus_n_O.
 372 apply sym_eq.apply minus_n_O.
 373 intros.
 374 change with
 375 ex nat (\lambda a. ex nat (\lambda b.
 376 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 377 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))).
 378 apply eq_minus_gcd_aux.
 379 simplify. apply le_S_S.apply le_O_n.
 380 assumption.apply le_n.
 381 apply nat_case1 m.
 382 simplify.intros.
 383 apply ex_intro ? ? (S O).
 384 apply ex_intro ? ? O.
 385 left.simplify.
 386 rewrite < plus_n_O.
 387 apply sym_eq.apply minus_n_O.
 388 intros.
 389 change with
 390 ex nat (\lambda a. ex nat (\lambda b.
 391 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 392 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))).
 393 cut
 394 ex nat (\lambda a. ex nat (\lambda b.
 395 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 396 \lor
 397 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))).
 398 elim Hcut.elim H2.elim H3.
 399 apply ex_intro ? ? a1.
 400 apply ex_intro ? ? a.
 401 right.assumption.
 402 apply ex_intro ? ? a1.
 403 apply ex_intro ? ? a.
 404 left.assumption.
 405 apply eq_minus_gcd_aux.
 406 simplify. apply le_S_S.apply le_O_n.
 407 apply lt_to_le.apply not_le_to_lt.assumption.
 408 apply le_n.
 409 qed.
 410
 411 (* some properties of gcd *)
 412
 413 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 414 intro.simplify.reflexivity.
 415 qed.
 416
 417 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 418 m = O \land n = O.
 419 intros.cut divides O n \land divides O m.
 420 elim Hcut.elim H2.split.
 421 assumption.elim H1.assumption.
 422 rewrite < H.
 423 apply divides_gcd_nm.
 424 qed.
 425
 426 theorem symmetric_gcd: symmetric nat gcd.
 427 change with
 428 \forall n,m:nat. gcd n m = gcd m n.
 429 intros.
 430 cut O < (gcd n m) \lor O = (gcd n m).
 431 elim Hcut.
 432 cut O < (gcd m n) \lor O = (gcd m n).
 433 elim Hcut1.
 434 apply antisym_le.
 435 apply divides_to_le.assumption.
 436 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 437 apply divides_to_le.assumption.
 438 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 439 rewrite < H1.
 440 cut m=O \land n=O.
 441 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
 442 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 443 apply le_to_or_lt_eq.apply le_O_n.
 444 rewrite < H.
 445 cut n=O \land m=O.
 446 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
 447 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 448 apply le_to_or_lt_eq.apply le_O_n.
 449 qed.
 450
 451 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 452 symmetric_gcd.
 453
 454 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 455 intro.
 456 apply antisym_le.apply divides_to_le.simplify.apply le_n.
 457 apply divides_gcd_n.
 458 cut O < gcd (S O) n \lor O = gcd (S O) n.
 459 elim Hcut.assumption.
 460 apply False_ind.
 461 apply not_eq_O_S O.
 462 cut (S O)=O \land n=O.
 463 elim Hcut1.apply sym_eq.assumption.
 464 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 465 apply le_to_or_lt_eq.apply le_O_n.
 466 qed.
 467
 468 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to
 469 gcd n m = (S O).
 470 intros.simplify in H.change with gcd n m = (S O).
 471 elim H.
 472 apply antisym_le.
 473 apply not_lt_to_le.
 474 change with (S (S O)) \le gcd n m \to False.intro.
 475 apply H1.rewrite < H3 (gcd n m).
 476 apply divides_gcd_m.
 477 apply divides_gcd_n.assumption.
 478 cut O < gcd n m \lor O = gcd n m.
 479 elim Hcut.assumption.
 480 apply False_ind.
 481 apply not_le_Sn_O (S O).
 482 cut n=O \land m=O.
 483 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
 484 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 485 apply le_to_or_lt_eq.apply le_O_n.
 486 qed.
 487
 488 (* esempio di sfarfallalmento !!! *)
 489 (*
 490 theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
 491 divides n p \lor divides n q.
 492 intros.
 493 cut divides n p \lor \not (divides n p).
 494 elim Hcut.left.assumption.
 495 right.
 496 cut ex nat (\lambda a. ex nat (\lambda b.
 497 a*n - b*p = (S O) \lor b*p - a*n = (S O))).
 498 elim Hcut1.elim H3.*)
 499
 500 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
 501 divides n p \lor divides n q.
 502 intros.
 503 cut divides n p \lor \not (divides n p).
 504 elim Hcut.
 505 left.assumption.
 506 right.
 507 cut ex nat (\lambda a. ex nat (\lambda b.
 508 a*n - b*p = (S O) \lor b*p - a*n = (S O))).
 509 elim Hcut1.elim H3.elim H4.
 510 (* first case *)
 511 rewrite > times_n_SO q.rewrite < H5.
 512 rewrite > distr_times_minus.
 513 rewrite > sym_times q (a1*p).
 514 rewrite > assoc_times a1.
 515 elim H1.rewrite > H6.
 516 rewrite < sym_times n.rewrite < assoc_times.
 517 rewrite > sym_times q.rewrite > assoc_times.
 518 rewrite < assoc_times a1.rewrite < sym_times n.
 519 rewrite > assoc_times n.
 520 rewrite < distr_times_minus.
 521 apply witness ? ? (q*a-a1*n2).reflexivity.
 522 (* second case *)
 523 rewrite > times_n_SO q.rewrite < H5.
 524 rewrite > distr_times_minus.
 525 rewrite > sym_times q (a1*p).
 526 rewrite > assoc_times a1.
 527 elim H1.rewrite > H6.
 528 rewrite < sym_times.rewrite > assoc_times.
 529 rewrite < assoc_times q.
 530 rewrite < sym_times n.
 531 rewrite < distr_times_minus.
 532 apply witness ? ? (n2*a1-q*a).reflexivity.
 533 (* end second case *)
 534 rewrite < prime_to_gcd_SO n p.
 535 apply eq_minus_gcd.
 536 assumption.assumption.
 537 apply decidable_divides n p.
 538 apply trans_lt ? (S O).simplify.apply le_n.
 539 simplify in H.elim H. assumption.
 540 qed.