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 rewrite > sym_times.
  55 apply div_mod.assumption. 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 rewrite > not_divides_to_divides_b_false.
  87 change with
  88 (divides (gcd_aux n n1 (mod m n1)) m) \land
  89 (divides (gcd_aux n n1 (mod m n1)) n1).
  90 cut (divides (gcd_aux n n1 (mod m n1)) n1) \land
  91 (divides (gcd_aux n n1 (mod m n1)) (mod m n1)).
  92 elim Hcut1.
  93 split.apply divides_mod_to_divides ? ? n1.
  94 assumption.assumption.assumption.assumption.
  95 apply H.
  96 cut O \lt mod m n1 \lor O = mod m n1.
  97 elim Hcut1.assumption.
  98 apply False_ind.apply H4.apply mod_O_to_divides.
  99 assumption.apply sym_eq.assumption.
 100 apply le_to_or_lt_eq.apply le_O_n.
 101 apply lt_to_le.
 102 apply lt_mod_m_m.assumption.
 103 apply le_S_S_to_le.
 104 apply trans_le ? n1.
 105 change with mod m n1 < n1.
 106 apply lt_mod_m_m.assumption.assumption.
 107 apply decidable_divides n1 m.assumption.
 108 apply lt_to_le_to_lt ? n1.assumption.reflexivity.
 109 assumption.
 110 assumption.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 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 apply decidable_divides n1 m.assumption.
 212 apply lt_to_le_to_lt ? n1.assumption.reflexivity.
 213 assumption.assumption.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 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 (* second case *)
 301 rewrite < H7.
 302 apply ex_intro ? ? (a1+a*(div m n1)).
 303 apply ex_intro ? ? a.
 304 left.
 305 rewrite > sym_times.
 306 rewrite > distr_times_plus.
 307 rewrite > sym_times.
 308 rewrite > sym_times n1.
 309 rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
 310 rewrite > distr_times_plus.
 311 rewrite > assoc_times.
 312 rewrite < eq_minus_minus_minus_plus.
 313 rewrite < sym_plus.
 314 rewrite < plus_minus.
 315 rewrite < minus_n_n.reflexivity.
 316 (* end second case *)
 317 apply H n1 (mod m n1).
 318 (* a lot of trivialities left *)
 319 cut O \lt mod m n1 \lor O = mod m n1.
 320 elim Hcut2.assumption.
 321 absurd divides n1 m.apply mod_O_to_divides.
 322 assumption.apply sym_eq.assumption.assumption.
 323 apply le_to_or_lt_eq.apply le_O_n.
 324 apply lt_to_le.
 325 apply lt_mod_m_m.assumption.
 326 apply le_S_S_to_le.
 327 apply trans_le ? n1.
 328 change with mod m n1 < n1.
 329 apply lt_mod_m_m.assumption.assumption.
 330 apply decidable_divides n1 m.assumption.
 331 apply lt_to_le_to_lt ? n1.assumption.assumption.
 332 assumption.assumption.assumption.assumption.assumption.
 333 apply le_n.assumption.
 334 apply le_n.
 335 qed.
 336
 337 theorem eq_minus_gcd: \forall m,n.
 338 ex nat (\lambda a. ex nat (\lambda b.
 339 a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))).
 340 intros.
 341 change with
 342 ex nat (\lambda a. ex nat (\lambda b.
 343 a*n - b*m =
 344 match leb n m with
 345   [ true \Rightarrow
 346     match n with
 347     [ O \Rightarrow m
 348     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 349   | false \Rightarrow
 350     match m with
 351     [ O \Rightarrow n
 352     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
 353 \lor b*m - a*n =
 354 match leb n m with
 355   [ true \Rightarrow
 356     match n with
 357     [ O \Rightarrow m
 358     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
 359   | false \Rightarrow
 360     match m with
 361     [ O \Rightarrow n
 362     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
 363 )).
 364 apply leb_elim n m.
 365 apply nat_case1 n.
 366 simplify.intros.
 367 apply ex_intro ? ? O.
 368 apply ex_intro ? ? (S O).
 369 right.simplify.
 370 rewrite < plus_n_O.
 371 apply sym_eq.apply minus_n_O.
 372 intros.
 373 change with
 374 ex nat (\lambda a. ex nat (\lambda b.
 375 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
 376 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))).
 377 apply eq_minus_gcd_aux.
 378 simplify. apply le_S_S.apply le_O_n.
 379 assumption.apply le_n.
 380 apply nat_case1 m.
 381 simplify.intros.
 382 apply ex_intro ? ? (S O).
 383 apply ex_intro ? ? O.
 384 left.simplify.
 385 rewrite < plus_n_O.
 386 apply sym_eq.apply minus_n_O.
 387 intros.
 388 change with
 389 ex nat (\lambda a. ex nat (\lambda b.
 390 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
 391 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))).
 392 cut
 393 ex nat (\lambda a. ex nat (\lambda b.
 394 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 395 \lor
 396 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))).
 397 elim Hcut.elim H2.elim H3.
 398 apply ex_intro ? ? a1.
 399 apply ex_intro ? ? a.
 400 right.assumption.
 401 apply ex_intro ? ? a1.
 402 apply ex_intro ? ? a.
 403 left.assumption.
 404 apply eq_minus_gcd_aux.
 405 simplify. apply le_S_S.apply le_O_n.
 406 apply lt_to_le.apply not_le_to_lt.assumption.
 407 apply le_n.
 408 qed.
 409
 410 (* some properties of gcd *)
 411
 412 theorem gcd_O_n: \forall n:nat. gcd O n = n.
 413 intro.simplify.reflexivity.
 414 qed.
 415
 416 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
 417 m = O \land n = O.
 418 intros.cut divides O n \land divides O m.
 419 elim Hcut.elim H2.split.
 420 assumption.elim H1.assumption.
 421 rewrite < H.
 422 apply divides_gcd_nm.
 423 qed.
 424
 425 theorem symmetric_gcd: symmetric nat gcd.
 426 change with
 427 \forall n,m:nat. gcd n m = gcd m n.
 428 intros.
 429 cut O < (gcd n m) \lor O = (gcd n m).
 430 elim Hcut.
 431 cut O < (gcd m n) \lor O = (gcd m n).
 432 elim Hcut1.
 433 apply antisym_le.
 434 apply divides_to_le.assumption.
 435 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 436 apply divides_to_le.assumption.
 437 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
 438 rewrite < H1.
 439 cut m=O \land n=O.
 440 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
 441 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 442 apply le_to_or_lt_eq.apply le_O_n.
 443 rewrite < H.
 444 cut n=O \land m=O.
 445 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
 446 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 447 apply le_to_or_lt_eq.apply le_O_n.
 448 qed.
 449
 450 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
 451 symmetric_gcd.
 452
 453 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 454 intro.
 455 apply antisym_le.apply divides_to_le.simplify.apply le_n.
 456 apply divides_gcd_n.
 457 cut O < gcd (S O) n \lor O = gcd (S O) n.
 458 elim Hcut.assumption.
 459 apply False_ind.
 460 apply not_eq_O_S O.
 461 cut (S O)=O \land n=O.
 462 elim Hcut1.apply sym_eq.assumption.
 463 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 464 apply le_to_or_lt_eq.apply le_O_n.
 465 qed.
 466
 467 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to
 468 gcd n m = (S O).
 469 intros.simplify in H.change with gcd n m = (S O).
 470 elim H.
 471 apply antisym_le.
 472 apply not_lt_to_le.
 473 change with (S (S O)) \le gcd n m \to False.intro.
 474 apply H1.rewrite < H3 (gcd n m).
 475 apply divides_gcd_m.
 476 cut O < gcd n m \lor O = gcd n m.
 477 elim Hcut.assumption.
 478 apply False_ind.
 479 apply not_le_Sn_O (S O).
 480 cut n=O \land m=O.
 481 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
 482 apply gcd_O_to_eq_O.apply sym_eq.assumption.
 483 apply le_to_or_lt_eq.apply le_O_n.
 484 apply divides_gcd_n.assumption.
 485 qed.
 486
 487 (* esempio di sfarfallalmento !!! *)
 488 (*
 489 theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
 490 divides n p \lor divides n q.
 491 intros.
 492 cut divides n p \lor \not (divides n p).
 493 elim Hcut.left.assumption.
 494 right.
 495 cut ex nat (\lambda a. ex nat (\lambda b.
 496 a*n - b*p = (S O) \lor b*p - a*n = (S O))).
 497 elim Hcut1.elim H3.*)
 498
 499 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
 500 divides n p \lor divides n q.
 501 intros.
 502 cut divides n p \lor \not (divides n p).
 503 elim Hcut.
 504 left.assumption.
 505 right.
 506 cut ex nat (\lambda a. ex nat (\lambda b.
 507 a*n - b*p = (S O) \lor b*p - a*n = (S O))).
 508 elim Hcut1.elim H3.elim H4.
 509 (* first case *)
 510 rewrite > times_n_SO q.rewrite < H5.
 511 rewrite > distr_times_minus.
 512 rewrite > sym_times q (a1*p).
 513 rewrite > assoc_times a1.
 514 elim H1.rewrite > H6.
 515 rewrite < sym_times n.rewrite < assoc_times.
 516 rewrite > sym_times q.rewrite > assoc_times.
 517 rewrite < assoc_times a1.rewrite < sym_times n.
 518 rewrite > assoc_times n.
 519 rewrite < distr_times_minus.
 520 apply witness ? ? (q*a-a1*n2).reflexivity.
 521 (* second case *)
 522 rewrite > times_n_SO q.rewrite < H5.
 523 rewrite > distr_times_minus.
 524 rewrite > sym_times q (a1*p).
 525 rewrite > assoc_times a1.
 526 elim H1.rewrite > H6.
 527 rewrite < sym_times.rewrite > assoc_times.
 528 rewrite < assoc_times q.
 529 rewrite < sym_times n.
 530 rewrite < distr_times_minus.
 531 apply witness ? ? (n2*a1-q*a).reflexivity.
 532 (* end second case *)
 533 rewrite < prime_to_gcd_SO n p.
 534 apply eq_minus_gcd.
 535 apply decidable_divides n p.
 536 apply trans_lt ? (S O).simplify.apply le_n.
 537 simplify in H.elim H. assumption.
 538 assumption.assumption.
 539 qed.