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