helm/software/matita/library/nat/factorization.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 include "nat/ord.ma".
  16
  17 (* the following factorization algorithm looks for the largest prime
  18    factor. *)
  19 definition max_prime_factor \def \lambda n:nat.
  20 (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)).
  21
  22 theorem lt_SO_max_prime: \forall m. S O <  m \to
  23 S O < max m (λi:nat.primeb i∧divides_b i m).
  24 intros.
  25 apply (lt_to_le_to_lt ? (smallest_factor m))
  26   [apply lt_SO_smallest_factor.assumption
  27   |apply f_m_to_le_max
  28     [apply le_smallest_factor_n
  29     |apply true_to_true_to_andb_true
  30       [apply prime_to_primeb_true.
  31        apply prime_smallest_factor_n.
  32        assumption
  33       |apply divides_to_divides_b_true
  34         [apply lt_O_smallest_factor.apply lt_to_le.assumption
  35         |apply divides_smallest_factor_n.
  36          apply lt_to_le.assumption
  37         ]
  38       ]
  39     ]
  40   ]
  41 qed.
  42 (* max_prime_factor is indeed a factor *)
  43 theorem divides_max_prime_factor_n:
  44   \forall n:nat. (S O) < n
  45   \to nth_prime (max_prime_factor n) \divides n.
  46 intros.
  47 apply divides_b_true_to_divides.
  48 apply (f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
  49 cut (\exists i. nth_prime i = smallest_factor n);
  50   [ elim Hcut.
  51     apply (ex_intro nat ? a);
  52     split;
  53     [ apply (trans_le a (nth_prime a));
  54       [ apply le_n_fn;
  55         exact lt_nth_prime_n_nth_prime_Sn;
  56       | rewrite > H1;
  57         apply le_smallest_factor_n; ]
  58     | rewrite > H1;
  59       change with (divides_b (smallest_factor n) n = true);
  60       apply divides_to_divides_b_true;
  61       [ apply (trans_lt ? (S O));
  62         [ unfold lt; apply le_n;
  63         | apply lt_SO_smallest_factor; assumption; ]
  64       | apply divides_smallest_factor_n;
  65         autobatch; ] ]
  66   | apply prime_to_nth_prime;
  67     autobatch.
  68     (*
  69     apply prime_to_nth_prime;
  70     apply prime_smallest_factor_n;
  71     assumption; *) ]
  72 qed.
  73
  74 lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
  75  \exists p.p \leq m \land prime p \land p \divides n.
  76 intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
  77   [split
  78      [apply divides_to_le
  79         [apply lt_to_le;assumption
  80         |apply divides_max_prime_factor_n;assumption]
  81      |apply prime_nth_prime;]
  82   |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n;
  83    assumption]
  84 qed.
  85
  86 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to
  87 max_prime_factor n \le max_prime_factor m.
  88 intros.unfold max_prime_factor.
  89 apply f_m_to_le_max.
  90 apply (trans_le ? n).
  91 apply le_max_n.apply divides_to_le.assumption.assumption.
  92 change with (divides_b (nth_prime (max_prime_factor n)) m = true).
  93 apply divides_to_divides_b_true.
  94 cut (prime (nth_prime (max_prime_factor n))).
  95 apply lt_O_nth_prime_n.apply prime_nth_prime.
  96 cut (nth_prime (max_prime_factor n) \divides n).
  97 autobatch.
  98 autobatch.
  99 (*
 100   [ apply (transitive_divides ? n);
 101     [ apply divides_max_prime_factor_n.
 102       assumption.
 103     | assumption.
 104     ]
 105   | apply divides_b_true_to_divides;
 106     [ apply lt_O_nth_prime_n.
 107     | apply divides_to_divides_b_true;
 108       [ apply lt_O_nth_prime_n.
 109       | apply divides_max_prime_factor_n.
 110         assumption.
 111       ]
 112     ]
 113   ]
 114 *)
 115 qed.
 116
 117 theorem divides_to_max_prime_factor1 : \forall n,m. O < n \to O < m \to n \divides m \to
 118 max_prime_factor n \le max_prime_factor m.
 119 intros 3.
 120 elim (le_to_or_lt_eq ? ? H)
 121   [apply divides_to_max_prime_factor
 122     [assumption|assumption|assumption]
 123   |rewrite < H1.
 124    simplify.apply le_O_n.
 125   ]
 126 qed.
 127
 128 theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
 129   (S O) < n \to
 130   p = max_prime_factor n \to
 131   p_ord n (nth_prime p) \neq pair nat nat O r.
 132 intros.unfold Not.intro.
 133 apply (p_ord_O_to_not_divides ? ? ? ? H2)
 134   [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 135   |rewrite > H1.
 136    apply divides_max_prime_factor_n.
 137    assumption
 138   ]
 139 qed.
 140
 141 theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to
 142 p = max_prime_factor n \to
 143 (pair nat nat q r) = p_ord n (nth_prime p) \to
 144 (S O) < r \to max_prime_factor r < p.
 145 intros.
 146 rewrite > H1.
 147 cut (max_prime_factor r \lt max_prime_factor n \lor
 148     max_prime_factor r = max_prime_factor n).
 149 elim Hcut.assumption.
 150 absurd (nth_prime (max_prime_factor n) \divides r).
 151 rewrite < H4.
 152 apply divides_max_prime_factor_n.
 153 assumption.unfold Not.
 154 intro.
 155 cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
 156   [ apply Hcut1; autobatch depth=2;
 157     (*
 158     apply Hcut1.apply divides_to_mod_O;
 159     [ apply lt_O_nth_prime_n.
 160     | assumption.
 161     ]
 162     *)
 163   | unfold p_ord in H2; lapply depth=0 le_n; autobatch width = 4 depth = 2;
 164     (*apply (p_ord_aux_to_not_mod_O n n ? q r);
 165     [ apply lt_SO_nth_prime_n.
 166     | assumption.
 167     | apply le_n.
 168     | rewrite < H1.assumption.
 169     ]*)
 170   ].
 171
 172 apply (le_to_or_lt_eq (max_prime_factor r)  (max_prime_factor n)).
 173 apply divides_to_max_prime_factor.
 174 assumption.assumption.
 175 apply (witness r n ((nth_prime p) \sup q)).
 176 rewrite < sym_times.
 177 apply (p_ord_aux_to_exp n n ? q r).
 178 apply lt_O_nth_prime_n.assumption.
 179 qed.
 180
 181 theorem p_ord_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to
 182 max_prime_factor n \le p \to
 183 (pair nat nat q r) = p_ord n (nth_prime p) \to
 184 (S O) < r \to max_prime_factor r < p.
 185 intros.
 186 cut (max_prime_factor n < p \lor max_prime_factor n = p).
 187 elim Hcut.apply (le_to_lt_to_lt ? (max_prime_factor n)).
 188 apply divides_to_max_prime_factor.assumption.assumption.
 189 apply (witness r n ((nth_prime p) \sup q)).
 190 rewrite > sym_times.
 191 apply (p_ord_aux_to_exp n n).
 192 apply lt_O_nth_prime_n.
 193 assumption.assumption.
 194 apply (p_ord_to_lt_max_prime_factor n ? q).
 195 assumption.apply sym_eq.assumption.assumption.assumption.
 196 apply (le_to_or_lt_eq ? p H1).
 197 qed.
 198
 199 lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
 200 O < n \to n=S O \lor max_prime_factor n < p \to
 201 (nth_prime p \ndivides n).
 202 intros.unfold Not.intro.
 203 elim H1
 204   [rewrite > H3 in H2.
 205    apply (le_to_not_lt (nth_prime p) (S O))
 206     [apply divides_to_le[apply le_n|assumption]
 207     |apply lt_SO_nth_prime_n
 208     ]
 209   |apply (not_le_Sn_n p).
 210    change with (p < p).
 211    apply (le_to_lt_to_lt ? ? ? ? H3).
 212    unfold max_prime_factor.
 213    apply  f_m_to_le_max
 214     [apply (trans_le ? (nth_prime p))
 215       [apply lt_to_le.
 216        apply lt_n_nth_prime_n
 217       |apply divides_to_le;assumption
 218       ]
 219     |apply eq_to_eqb_true.
 220      apply divides_to_mod_O
 221       [apply lt_O_nth_prime_n|assumption]
 222     ]
 223   ]
 224 qed.
 225
 226 (* datatypes and functions *)
 227
 228 inductive nat_fact : Set \def
 229     nf_last : nat \to nat_fact
 230   | nf_cons : nat \to nat_fact \to nat_fact.
 231
 232 inductive nat_fact_all : Set \def
 233     nfa_zero : nat_fact_all
 234   | nfa_one : nat_fact_all
 235   | nfa_proper : nat_fact \to nat_fact_all.
 236
 237 let rec factorize_aux p n acc \def
 238   match p with
 239   [ O \Rightarrow acc
 240   | (S p1) \Rightarrow
 241     match p_ord n (nth_prime p1) with
 242     [ (pair q r) \Rightarrow
 243       factorize_aux p1 r (nf_cons q acc)]].
 244
 245 definition factorize : nat \to nat_fact_all \def \lambda n:nat.
 246   match n with
 247     [ O \Rightarrow nfa_zero
 248     | (S n1) \Rightarrow
 249       match n1 with
 250       [ O \Rightarrow nfa_one
 251     | (S n2) \Rightarrow
 252       let p \def (max (S(S n2)) (\lambda p:nat.eqb ((S(S n2)) \mod (nth_prime p)) O)) in
 253       match p_ord (S(S n2)) (nth_prime p) with
 254       [ (pair q r) \Rightarrow
 255            nfa_proper (factorize_aux p r (nf_last (pred q)))]]].
 256
 257 let rec defactorize_aux f i \def
 258   match f with
 259   [ (nf_last n) \Rightarrow (nth_prime i) \sup (S n)
 260   | (nf_cons n g) \Rightarrow
 261       (nth_prime i) \sup n *(defactorize_aux g (S i))].
 262
 263 definition defactorize : nat_fact_all \to nat \def
 264 \lambda f : nat_fact_all.
 265 match f with
 266 [ nfa_zero \Rightarrow O
 267 | nfa_one \Rightarrow (S O)
 268 | (nfa_proper g) \Rightarrow defactorize_aux g O].
 269
 270 theorem lt_O_defactorize_aux:
 271  \forall f:nat_fact.
 272  \forall i:nat.
 273  O < defactorize_aux f i.
 274 intro; elim f;
 275 [1,2:
 276   simplify; unfold lt;
 277   rewrite > times_n_SO;
 278   apply le_times;
 279   [ change with (O < nth_prime i);
 280     apply lt_O_nth_prime_n;
 281   |2,3:
 282     change with (O < exp (nth_prime i) n);
 283     apply lt_O_exp;
 284     apply lt_O_nth_prime_n;
 285   | change with (O < defactorize_aux n1 (S i));
 286     apply H; ] ]
 287 qed.
 288
 289 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 290 S O < defactorize_aux f i.
 291 intro.elim f.simplify.unfold lt.
 292 rewrite > times_n_SO.
 293 apply le_times.
 294 change with (S O < nth_prime i).
 295 apply lt_SO_nth_prime_n.
 296 change with (O < exp (nth_prime i) n).
 297 apply lt_O_exp.
 298 apply lt_O_nth_prime_n.
 299 simplify.unfold lt.
 300 rewrite > times_n_SO.
 301 rewrite > sym_times.
 302 apply le_times.
 303 change with (O < exp (nth_prime i) n).
 304 apply lt_O_exp.
 305 apply lt_O_nth_prime_n.
 306 change with (S O < defactorize_aux n1 (S i)).
 307 apply H.
 308 qed.
 309
 310 theorem defactorize_aux_factorize_aux :
 311 \forall p,n:nat.\forall acc:nat_fact.O < n \to
 312 ((n=(S O) \land p=O) \lor max_prime_factor n < p) \to
 313 defactorize_aux (factorize_aux p n acc) O = n*(defactorize_aux acc p).
 314 intro.elim p.simplify.
 315 elim H1.elim H2.rewrite > H3.
 316 rewrite > sym_times. apply times_n_SO.
 317 apply False_ind.apply (not_le_Sn_O (max_prime_factor n) H2).
 318 simplify.
 319 (* generalizing the goal: I guess there exists a better way *)
 320 cut (\forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to
 321 defactorize_aux match (p_ord_aux n1 n1 (nth_prime n)) with
 322 [(pair q r)  \Rightarrow (factorize_aux n r (nf_cons q acc))] O =
 323 n1*defactorize_aux acc (S n)).
 324 apply (Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n)))
 325 (snd ? ? (p_ord_aux n1 n1 (nth_prime n)))).
 326 apply sym_eq.apply eq_pair_fst_snd.
 327 intros.
 328 rewrite < H3.
 329 simplify.
 330 cut (n1 = r * (nth_prime n) \sup q).
 331 rewrite > H.
 332 simplify.rewrite < assoc_times.
 333 rewrite < Hcut.reflexivity.
 334 cut (O < r \lor O = r).
 335 elim Hcut1.assumption.absurd (n1 = O).
 336 rewrite > Hcut.rewrite < H4.reflexivity.
 337 unfold Not. intro.apply (not_le_Sn_O O).
 338 rewrite < H5 in \vdash (? ? %).assumption.
 339 apply le_to_or_lt_eq.apply le_O_n.
 340 cut ((S O) < r \lor (S O) \nlt r).
 341 elim Hcut1.
 342 right.
 343 apply (p_ord_to_lt_max_prime_factor1 n1 ? q r).
 344 assumption.elim H2.
 345 elim H5.
 346 apply False_ind.
 347 apply (not_eq_O_S n).apply sym_eq.assumption.
 348 apply le_S_S_to_le.
 349 exact H5.
 350 assumption.assumption.
 351 cut (r=(S O)).
 352 apply (nat_case n).
 353 left.split.assumption.reflexivity.
 354 intro.right.rewrite > Hcut2.
 355 simplify.unfold lt.apply le_S_S.apply le_O_n.
 356 cut (r < (S O) ∨ r=(S O)).
 357 elim Hcut2.absurd (O=r).
 358 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
 359 unfold Not.intro.
 360 cut (O=n1).
 361 apply (not_le_Sn_O O).
 362 rewrite > Hcut3 in ⊢ (? ? %).
 363 assumption.rewrite > Hcut.
 364 rewrite < H6.reflexivity.
 365 assumption.
 366 apply (le_to_or_lt_eq r (S O)).
 367 apply not_lt_to_le.assumption.
 368 apply (decidable_lt (S O) r).
 369 rewrite > sym_times.
 370 apply (p_ord_aux_to_exp n1 n1).
 371 apply lt_O_nth_prime_n.assumption.
 372 qed.
 373
 374 theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
 375 intro.
 376 apply (nat_case n).reflexivity.
 377 intro.apply (nat_case m).reflexivity.
 378 intro.
 379 change with
 380 (let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
 381 defactorize (match p_ord (S(S m1)) (nth_prime p) with
 382 [ (pair q r) \Rightarrow
 383    nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
 384 intro.
 385 (* generalizing the goal; find a better way *)
 386 cut (\forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to
 387 defactorize (match p_ord (S(S m1)) (nth_prime p) with
 388 [ (pair q r) \Rightarrow
 389    nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
 390 apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
 391 (snd ? ? (p_ord (S(S m1)) (nth_prime p)))).
 392 apply sym_eq.apply eq_pair_fst_snd.
 393 intros.
 394 rewrite < H.
 395 simplify.
 396 cut ((S(S m1)) = (nth_prime p) \sup q *r).
 397 cut (O<r).
 398 rewrite > defactorize_aux_factorize_aux.
 399 change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
 400 cut ((S (pred q)) = q).
 401 rewrite > Hcut2.
 402 rewrite > sym_times.
 403 apply sym_eq.
 404 apply (p_ord_aux_to_exp (S(S m1))).
 405 apply lt_O_nth_prime_n.
 406 assumption.
 407 (* O < q *)
 408 apply sym_eq. apply S_pred.
 409 cut (O < q \lor O = q).
 410 elim Hcut2.assumption.
 411 absurd (nth_prime p \divides S (S m1)).
 412 apply (divides_max_prime_factor_n (S (S m1))).
 413 unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
 414 cut ((S(S m1)) = r).
 415 rewrite > Hcut3 in \vdash (? (? ? %)).
 416 change with (nth_prime p \divides r \to False).
 417 intro.
 418 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
 419 apply lt_SO_nth_prime_n.
 420 unfold lt.apply le_S_S.apply le_O_n.apply le_n.
 421 assumption.
 422 apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
 423 rewrite > times_n_SO in \vdash (? ? ? %).
 424 rewrite < sym_times.
 425 rewrite > (exp_n_O (nth_prime p)).
 426 rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
 427 assumption.
 428 apply le_to_or_lt_eq.apply le_O_n.assumption.
 429 (* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
 430 cut ((S O) < r \lor S O \nlt r).
 431 elim Hcut2.
 432 right.
 433 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
 434 unfold lt.apply le_S_S. apply le_O_n.
 435 apply le_n.
 436 assumption.assumption.
 437 cut (r=(S O)).
 438 apply (nat_case p).
 439 left.split.assumption.reflexivity.
 440 intro.right.rewrite > Hcut3.
 441 simplify.unfold lt.apply le_S_S.apply le_O_n.
 442 cut (r \lt (S O) \or r=(S O)).
 443 elim Hcut3.absurd (O=r).
 444 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
 445 unfold Not.intro.
 446 apply (not_le_Sn_O O).
 447 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 448 apply (le_to_or_lt_eq r (S O)).
 449 apply not_lt_to_le.assumption.
 450 apply (decidable_lt (S O) r).
 451 (* O < r *)
 452 cut (O < r \lor O = r).
 453 elim Hcut1.assumption.
 454 apply False_ind.
 455 apply (not_eq_O_S (S m1)).
 456 rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
 457 apply le_to_or_lt_eq.apply le_O_n.
 458 (* prova del cut *)
 459 apply (p_ord_aux_to_exp (S(S m1))).
 460 apply lt_O_nth_prime_n.
 461 assumption.
 462 (* fine prova cut *)
 463 qed.
 464
 465 let rec max_p f \def
 466 match f with
 467 [ (nf_last n) \Rightarrow O
 468 | (nf_cons n g) \Rightarrow S (max_p g)].
 469
 470 let rec max_p_exponent f \def
 471 match f with
 472 [ (nf_last n) \Rightarrow n
 473 | (nf_cons n g) \Rightarrow max_p_exponent g].
 474
 475 theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat.
 476 nth_prime ((max_p f)+i) \divides defactorize_aux f i.
 477 intro.
 478 elim f.simplify.apply (witness ? ? ((nth_prime i) \sup n)).
 479 reflexivity.
 480 change with
 481 (nth_prime (S(max_p n1)+i) \divides
 482 (nth_prime i) \sup n *(defactorize_aux n1 (S i))).
 483 elim (H (S i)).
 484 rewrite > H1.
 485 rewrite < sym_times.
 486 rewrite > assoc_times.
 487 rewrite < plus_n_Sm.
 488 apply (witness ? ? (n2* (nth_prime i) \sup n)).
 489 reflexivity.
 490 qed.
 491
 492 lemma eq_p_max: \forall n,p,r:nat. O < n \to
 493 O < r \to
 494 r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
 495 p = max_prime_factor (r*(nth_prime p)\sup n).
 496 intros.
 497 apply sym_eq.
 498 unfold max_prime_factor.
 499 apply max_spec_to_max.
 500 split
 501   [split
 502     [rewrite > times_n_SO in \vdash (? % ?).
 503      rewrite > sym_times.
 504      apply le_times
 505       [assumption
 506       |apply lt_to_le.
 507        apply (lt_to_le_to_lt ? (nth_prime p))
 508         [apply lt_n_nth_prime_n
 509         |rewrite > exp_n_SO in \vdash (? % ?).
 510          apply le_exp
 511           [apply lt_O_nth_prime_n
 512           |assumption
 513           ]
 514         ]
 515       ]
 516     |apply eq_to_eqb_true.
 517      apply divides_to_mod_O
 518       [apply lt_O_nth_prime_n
 519       |apply (lt_O_n_elim ? H).
 520        intro.
 521        apply (witness ? ? ((r*(nth_prime p) \sup m))).
 522        rewrite < assoc_times.
 523        rewrite < sym_times in \vdash (? ? ? (? % ?)).
 524        rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
 525        rewrite > assoc_times.
 526        rewrite < exp_plus_times.
 527        reflexivity
 528       ]
 529     ]
 530   |intros.
 531    apply not_eq_to_eqb_false.
 532    unfold Not.intro.
 533    lapply (mod_O_to_divides ? ? ? H5)
 534     [apply lt_O_nth_prime_n
 535     |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
 536       [elim H2
 537         [rewrite > H6 in Hletin.
 538          simplify in Hletin.
 539          rewrite < plus_n_O in Hletin.
 540          apply Hcut.assumption
 541         |elim (divides_times_to_divides ? ? ? ? Hletin)
 542           [apply (lt_to_not_le ? ? H3).
 543            apply lt_to_le.
 544            apply (le_to_lt_to_lt ? ? ? ? H6).
 545            apply f_m_to_le_max
 546             [apply (trans_le ? (nth_prime i))
 547               [apply lt_to_le.
 548                apply lt_n_nth_prime_n
 549               |apply divides_to_le[assumption|assumption]
 550               ]
 551             |apply eq_to_eqb_true.
 552              apply divides_to_mod_O
 553               [apply lt_O_nth_prime_n|assumption]
 554             ]
 555           |apply prime_nth_prime
 556           |apply Hcut.assumption
 557           ]
 558         ]
 559       |unfold Not.intro.
 560        apply (lt_to_not_eq ? ? H3).
 561        apply sym_eq.
 562        elim (prime_nth_prime p).
 563        apply injective_nth_prime.
 564        apply H8
 565         [apply (divides_exp_to_divides ? ? ? ? H6).
 566          apply prime_nth_prime.
 567         |apply lt_SO_nth_prime_n
 568         ]
 569       ]
 570     ]
 571   ]
 572 qed.
 573
 574 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
 575 i < j \to nth_prime i \ndivides defactorize_aux f j.
 576 intro.elim f.
 577 change with
 578 (nth_prime i \divides (nth_prime j) \sup (S n) \to False).
 579 intro.absurd ((nth_prime i) = (nth_prime j)).
 580 apply (divides_exp_to_eq ? ? (S n)).
 581 apply prime_nth_prime.apply prime_nth_prime.
 582 assumption.unfold Not.
 583 intro.cut (i = j).
 584 apply (not_le_Sn_n i).rewrite > Hcut in \vdash (? ? %).assumption.
 585 apply (injective_nth_prime ? ? H2).
 586 unfold Not.simplify.
 587 intro.
 588 cut (nth_prime i \divides (nth_prime j) \sup n
 589 \lor nth_prime i \divides defactorize_aux n1 (S j)).
 590 elim Hcut.
 591 absurd ((nth_prime i) = (nth_prime j)).
 592 apply (divides_exp_to_eq ? ? n).
 593 apply prime_nth_prime.apply prime_nth_prime.
 594 assumption.unfold Not.
 595 intro.
 596 cut (i = j).
 597 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
 598 apply (injective_nth_prime ? ? H4).
 599 apply (H i (S j)).
 600 apply (trans_lt ? j).assumption.unfold lt.apply le_n.
 601 assumption.
 602 apply divides_times_to_divides.
 603 apply prime_nth_prime.assumption.
 604 qed.
 605
 606 lemma not_eq_nf_last_nf_cons: \forall g:nat_fact.\forall n,m,i:nat.
 607 \lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i).
 608 intros.
 609 change with
 610 (exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False).
 611 intro.
 612 cut (S(max_p g)+i= i).
 613 apply (not_le_Sn_n i).
 614 rewrite < Hcut in \vdash (? ? %).
 615 simplify.apply le_S_S.
 616 apply le_plus_n.
 617 apply injective_nth_prime.
 618 apply (divides_exp_to_eq ? ? (S n)).
 619 apply prime_nth_prime.apply prime_nth_prime.
 620 rewrite > H.
 621 change with (divides (nth_prime ((max_p (nf_cons m g))+i))
 622 (defactorize_aux (nf_cons m g) i)).
 623 apply divides_max_p_defactorize.
 624 qed.
 625
 626 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
 627 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
 628 intros.
 629 simplify.unfold Not.rewrite < plus_n_O.
 630 intro.
 631 apply (not_divides_defactorize_aux f i (S i) ?).
 632 unfold lt.apply le_n.
 633 rewrite > H.
 634 rewrite > assoc_times.
 635 apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
 636 reflexivity.
 637 qed.
 638
 639 theorem eq_defactorize_aux_to_eq: \forall f,g:nat_fact.\forall i:nat.
 640 defactorize_aux f i = defactorize_aux g i \to f = g.
 641 intro.
 642 elim f.
 643 elim g in H ⊢ %.
 644 apply eq_f.
 645 apply inj_S. apply (inj_exp_r (nth_prime i)).
 646 apply lt_SO_nth_prime_n.
 647 assumption.
 648 apply False_ind.
 649 apply (not_eq_nf_last_nf_cons n2 n n1 i H1).
 650 elim g in H1 ⊢ %.
 651 apply False_ind.
 652 apply (not_eq_nf_last_nf_cons n1 n2 n i).
 653 apply sym_eq. assumption.
 654 simplify in H2.
 655 generalize in match H2.
 656 apply (nat_elim2 (\lambda n,n2.
 657 ((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
 658 ((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
 659 nf_cons n n1 = nf_cons n2 n3)).
 660 intro.
 661 elim n4. apply eq_f.
 662 apply (H n3 (S i)).
 663 simplify in H4.
 664 rewrite > plus_n_O.
 665 rewrite > (plus_n_O (defactorize_aux n3 (S i))).assumption.
 666 apply False_ind.
 667 apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).assumption.
 668 intros.
 669 apply False_ind.
 670 apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i).
 671 apply sym_eq.assumption.
 672 intros.
 673 cut (nf_cons n4 n1 = nf_cons m n3).
 674 cut (n4=m).
 675 cut (n1=n3).
 676 rewrite > Hcut1.rewrite > Hcut2.reflexivity.
 677 change with
 678 (match nf_cons n4 n1 with
 679 [ (nf_last m) \Rightarrow n1
 680 | (nf_cons m g) \Rightarrow g ] = n3).
 681 rewrite > Hcut.simplify.reflexivity.
 682 change with
 683 (match nf_cons n4 n1 with
 684 [ (nf_last m) \Rightarrow m
 685 | (nf_cons m g) \Rightarrow m ] = m).
 686 rewrite > Hcut.simplify.reflexivity.
 687 apply H3.simplify in H4.
 688 apply (inj_times_r1 (nth_prime i)).
 689 apply lt_O_nth_prime_n.
 690 rewrite < assoc_times.rewrite < assoc_times.assumption.
 691 qed.
 692
 693 theorem injective_defactorize_aux: \forall i:nat.
 694 injective nat_fact nat (\lambda f.defactorize_aux f i).
 695 simplify.
 696 intros.
 697 apply (eq_defactorize_aux_to_eq x y i H).
 698 qed.
 699
 700 theorem injective_defactorize:
 701 injective nat_fact_all nat defactorize.
 702 unfold injective.
 703 change with (\forall f,g.defactorize f = defactorize g \to f=g).
 704 intro.elim f.
 705 elim g in H ⊢ %.
 706 (* zero - zero *)
 707 reflexivity.
 708 (* zero - one *)
 709 simplify in H1.
 710 apply False_ind.
 711 apply (not_eq_O_S O H).
 712 (* zero - proper *)
 713 simplify in H1.
 714 apply False_ind.
 715 apply (not_le_Sn_n O).
 716 rewrite > H in \vdash (? ? %).
 717 change with (O < defactorize_aux n O).
 718 apply lt_O_defactorize_aux.
 719 elim g in H ⊢ %.
 720 (* one - zero *)
 721 simplify in H1.
 722 apply False_ind.
 723 apply (not_eq_O_S O).apply sym_eq. assumption.
 724 (* one - one *)
 725 reflexivity.
 726 (* one - proper *)
 727 simplify in H1.
 728 apply False_ind.
 729 apply (not_le_Sn_n (S O)).
 730 rewrite > H in \vdash (? ? %).
 731 change with ((S O) < defactorize_aux n O).
 732 apply lt_SO_defactorize_aux.
 733 elim g in H ⊢ %.
 734 (* proper - zero *)
 735 simplify in H1.
 736 apply False_ind.
 737 apply (not_le_Sn_n O).
 738 rewrite < H in \vdash (? ? %).
 739 change with (O < defactorize_aux n O).
 740 apply lt_O_defactorize_aux.
 741 (* proper - one *)
 742 simplify in H1.
 743 apply False_ind.
 744 apply (not_le_Sn_n (S O)).
 745 rewrite < H in \vdash (? ? %).
 746 change with ((S O) < defactorize_aux n O).
 747 apply lt_SO_defactorize_aux.
 748 (* proper - proper *)
 749 apply eq_f.
 750 apply (injective_defactorize_aux O).
 751 exact H.
 752 qed.
 753
 754 theorem factorize_defactorize:
 755 \forall f: nat_fact_all. factorize (defactorize f) = f.
 756 intros.
 757 apply injective_defactorize.
 758 apply defactorize_factorize.
 759 qed.