matita/library_auto/auto/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 set "baseuri" "cic:/matita/library_auto/nat/factorization".
  16
  17 include "auto/nat/ord.ma".
  18 include "auto/nat/gcd.ma".
  19 include "auto/nat/nth_prime.ma".
  20
  21 (* the following factorization algorithm looks for the largest prime
  22    factor. *)
  23 definition max_prime_factor \def \lambda n:nat.
  24 (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)).
  25
  26 (* max_prime_factor is indeed a factor *)
  27 theorem divides_max_prime_factor_n:
  28   \forall n:nat. (S O) < n
  29   \to nth_prime (max_prime_factor n) \divides n.
  30 intros.
  31 apply divides_b_true_to_divides
  32 [ apply lt_O_nth_prime_n
  33 | apply (f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
  34   cut (\exists i. nth_prime i = smallest_factor n)
  35   [ elim Hcut.
  36     apply (ex_intro nat ? a).
  37     split
  38     [ apply (trans_le a (nth_prime a))
  39       [ auto
  40         (*apply le_n_fn.
  41         exact lt_nth_prime_n_nth_prime_Sn*)
  42       | rewrite > H1.
  43         apply le_smallest_factor_n
  44       ]
  45     | rewrite > H1.
  46       (*CSC: simplify here does something nasty! *)
  47       change with (divides_b (smallest_factor n) n = true).
  48       apply divides_to_divides_b_true
  49       [ auto
  50         (*apply (trans_lt ? (S O))
  51         [ unfold lt.
  52           apply le_n
  53         | apply lt_SO_smallest_factor.
  54           assumption
  55         ]*)
  56       | auto
  57         (*letin x \def le.
  58         auto new*)
  59          (*
  60        apply divides_smallest_factor_n;
  61         apply (trans_lt ? (S O));
  62         [ unfold lt; apply le_n;
  63         | assumption; ] *)
  64       ]
  65     ]
  66   | auto
  67     (*
  68     apply prime_to_nth_prime;
  69     apply prime_smallest_factor_n;
  70     assumption; *)
  71   ]
  72 ]
  73 qed.
  74
  75 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to
  76 max_prime_factor n \le max_prime_factor m.
  77 intros.
  78 unfold max_prime_factor.
  79 apply f_m_to_le_max
  80 [ auto
  81   (*apply (trans_le ? n)
  82   [ apply le_max_n
  83   | apply divides_to_le;assumption
  84   ]*)
  85 | change with (divides_b (nth_prime (max_prime_factor n)) m = true).
  86   apply divides_to_divides_b_true
  87   [ auto
  88     (*cut (prime (nth_prime (max_prime_factor n)))
  89     [ apply lt_O_nth_prime_n
  90     | apply prime_nth_prime
  91     ]*)
  92   | auto
  93     (*cut (nth_prime (max_prime_factor n) \divides n)
  94     [ auto
  95     | auto
  96     ] *)
  97   (*
  98     [ apply (transitive_divides ? n);
  99       [ apply divides_max_prime_factor_n.
 100         assumption.
 101       | assumption.
 102       ]
 103     | apply divides_b_true_to_divides;
 104       [ apply lt_O_nth_prime_n.
 105       | apply divides_to_divides_b_true;
 106         [ apply lt_O_nth_prime_n.
 107         | apply divides_max_prime_factor_n.
 108           assumption.
 109         ]
 110       ]
 111     ]
 112   *)
 113   ]
 114 ]
 115 qed.
 116
 117 theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to
 118 p = max_prime_factor n \to
 119 (pair nat nat q r) = p_ord n (nth_prime p) \to
 120 (S O) < r \to max_prime_factor r < p.
 121 intros.
 122 rewrite > H1.
 123 cut (max_prime_factor r \lt max_prime_factor n \lor
 124     max_prime_factor r = max_prime_factor n)
 125 [ elim Hcut
 126   [ assumption
 127   | absurd (nth_prime (max_prime_factor n) \divides r)
 128     [ rewrite < H4.
 129       auto
 130       (*apply divides_max_prime_factor_n.
 131       assumption*)
 132     | unfold Not.
 133       intro.
 134       cut (r \mod (nth_prime (max_prime_factor n)) \neq O)
 135       [ auto
 136         (*unfold Not in Hcut1.
 137         auto new*)
 138         (*
 139         apply Hcut1.apply divides_to_mod_O;
 140         [ apply lt_O_nth_prime_n.
 141         | assumption.
 142         ]
 143         *)
 144       | letin z \def le.
 145         cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
 146         [ 2: rewrite < H1.
 147           assumption
 148         | letin x \def le.
 149           auto width = 4 new
 150         ]
 151       (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
 152       ]
 153       (*
 154         apply (p_ord_aux_to_not_mod_O n n ? q r);
 155         [ apply lt_SO_nth_prime_n.
 156         | assumption.
 157         | apply le_n.
 158         | rewrite < H1.assumption.
 159         ]
 160       ].
 161       *)
 162     ]
 163   ]
 164 | apply (le_to_or_lt_eq (max_prime_factor r)  (max_prime_factor n)).
 165   apply divides_to_max_prime_factor
 166   [ assumption
 167   | assumption
 168   | apply (witness r n ((nth_prime p) \sup q)).
 169     rewrite < sym_times.
 170     apply (p_ord_aux_to_exp n n ? q r)
 171     [ apply lt_O_nth_prime_n
 172     | assumption
 173     ]
 174   ]
 175 ]
 176 qed.
 177
 178 theorem p_ord_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to
 179 max_prime_factor n \le p \to
 180 (pair nat nat q r) = p_ord n (nth_prime p) \to
 181 (S O) < r \to max_prime_factor r < p.
 182 intros.
 183 cut (max_prime_factor n < p \lor max_prime_factor n = p)
 184 [ elim Hcut
 185   [ apply (le_to_lt_to_lt ? (max_prime_factor n))
 186     [ apply divides_to_max_prime_factor
 187       [ assumption
 188       | assumption
 189       | apply (witness r n ((nth_prime p) \sup q)).
 190         rewrite > sym_times.
 191         (*qui auto non chiude il goal*)
 192         apply (p_ord_aux_to_exp n n)
 193         [ apply lt_O_nth_prime_n.
 194         | assumption
 195         ]
 196       ]
 197     | assumption
 198     ]
 199   | apply (p_ord_to_lt_max_prime_factor n ? q);auto
 200     (*[ assumption
 201     | apply sym_eq.
 202       assumption
 203     | assumption
 204     | assumption
 205     ]*)
 206   ]
 207 | apply (le_to_or_lt_eq ? p H1)
 208 ]
 209 qed.
 210
 211 (* datatypes and functions *)
 212
 213 inductive nat_fact : Set \def
 214     nf_last : nat \to nat_fact
 215   | nf_cons : nat \to nat_fact \to nat_fact.
 216
 217 inductive nat_fact_all : Set \def
 218     nfa_zero : nat_fact_all
 219   | nfa_one : nat_fact_all
 220   | nfa_proper : nat_fact \to nat_fact_all.
 221
 222 let rec factorize_aux p n acc \def
 223   match p with
 224   [ O \Rightarrow acc
 225   | (S p1) \Rightarrow
 226     match p_ord n (nth_prime p1) with
 227     [ (pair q r) \Rightarrow
 228       factorize_aux p1 r (nf_cons q acc)]].
 229
 230 definition factorize : nat \to nat_fact_all \def \lambda n:nat.
 231   match n with
 232     [ O \Rightarrow nfa_zero
 233     | (S n1) \Rightarrow
 234       match n1 with
 235       [ O \Rightarrow nfa_one
 236     | (S n2) \Rightarrow
 237       let p \def (max (S(S n2)) (\lambda p:nat.eqb ((S(S n2)) \mod (nth_prime p)) O)) in
 238       match p_ord (S(S n2)) (nth_prime p) with
 239       [ (pair q r) \Rightarrow
 240            nfa_proper (factorize_aux p r (nf_last (pred q)))]]].
 241
 242 let rec defactorize_aux f i \def
 243   match f with
 244   [ (nf_last n) \Rightarrow (nth_prime i) \sup (S n)
 245   | (nf_cons n g) \Rightarrow
 246       (nth_prime i) \sup n *(defactorize_aux g (S i))].
 247
 248 definition defactorize : nat_fact_all \to nat \def
 249 \lambda f : nat_fact_all.
 250 match f with
 251 [ nfa_zero \Rightarrow O
 252 | nfa_one \Rightarrow (S O)
 253 | (nfa_proper g) \Rightarrow defactorize_aux g O].
 254
 255 theorem lt_O_defactorize_aux:
 256  \forall f:nat_fact.
 257  \forall i:nat.
 258  O < defactorize_aux f i.
 259 intro.
 260 elim f
 261 [1,2:
 262   simplify;
 263   unfold lt;
 264   rewrite > times_n_SO;auto
 265   (*apply le_times
 266   [ change with (O < nth_prime i).
 267     apply lt_O_nth_prime_n
 268   |2,3:
 269     change with (O < exp (nth_prime i) n);
 270     apply lt_O_exp;
 271     apply lt_O_nth_prime_n
 272   | change with (O < defactorize_aux n1 (S i)).
 273     apply H
 274   ] *)
 275 ]
 276 qed.
 277
 278 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 279 S O < defactorize_aux f i.
 280 intro.
 281 elim f
 282 [ simplify.
 283   unfold lt.
 284   rewrite > times_n_SO.
 285   auto
 286   (*apply le_times
 287   [ change with (S O < nth_prime i).
 288     apply lt_SO_nth_prime_n
 289   | change with (O < exp (nth_prime i) n).
 290     apply lt_O_exp.
 291     apply lt_O_nth_prime_n
 292   ]*)
 293 | simplify.
 294   unfold lt.
 295   rewrite > times_n_SO.
 296   rewrite > sym_times.
 297   auto
 298   (*apply le_times
 299   [ change with (O < exp (nth_prime i) n).
 300     apply lt_O_exp.
 301     apply lt_O_nth_prime_n
 302   | change with (S O < defactorize_aux n1 (S i)).
 303     apply H
 304   ]*)
 305 ]
 306 qed.
 307
 308 theorem defactorize_aux_factorize_aux :
 309 \forall p,n:nat.\forall acc:nat_fact.O < n \to
 310 ((n=(S O) \land p=O) \lor max_prime_factor n < p) \to
 311 defactorize_aux (factorize_aux p n acc) O = n*(defactorize_aux acc p).
 312 intro.
 313 elim p
 314 [ simplify.
 315   elim H1
 316   [ elim H2.
 317     auto
 318     (*rewrite > H3.
 319     rewrite > sym_times.
 320     apply times_n_SO*)
 321   | apply False_ind.
 322     apply (not_le_Sn_O (max_prime_factor n) H2)
 323   ]
 324 | simplify.
 325   (* generalizing the goal: I guess there exists a better way *)
 326   cut (\forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to
 327   defactorize_aux match (p_ord_aux n1 n1 (nth_prime n)) with
 328   [(pair q r)  \Rightarrow (factorize_aux n r (nf_cons q acc))] O =
 329   n1*defactorize_aux acc (S n))
 330   [ (*invocando auto in questo punto, dopo circa 7 minuti l'esecuzione non era ancora terminata
 331       ne' con un errore ne' chiudendo il goal
 332      *)
 333     apply (Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n)))
 334     (snd ? ? (p_ord_aux n1 n1 (nth_prime n)))).
 335     auto
 336     (*apply sym_eq.apply eq_pair_fst_snd*)
 337   | intros.
 338     rewrite < H3.
 339     simplify.
 340     cut (n1 = r * (nth_prime n) \sup q)
 341     [ rewrite > H
 342       [ simplify.
 343         auto
 344         (*rewrite < assoc_times.
 345         rewrite < Hcut.
 346         reflexivity.*)
 347       | auto
 348         (*cut (O < r \lor O = r)
 349         [ elim Hcut1
 350           [ assumption
 351           | absurd (n1 = O)
 352             [ rewrite > Hcut.
 353               rewrite < H4.
 354               reflexivity
 355             | unfold Not.
 356               intro.
 357               apply (not_le_Sn_O O).
 358               rewrite < H5 in \vdash (? ? %).
 359               assumption
 360             ]
 361           ]
 362         | apply le_to_or_lt_eq.
 363           apply le_O_n
 364         ]*)
 365       | cut ((S O) < r \lor (S O) \nlt r)
 366         [ elim Hcut1
 367           [ right.
 368             apply (p_ord_to_lt_max_prime_factor1 n1 ? q r)
 369             [ assumption
 370             | elim H2
 371               [ elim H5.
 372                 apply False_ind.
 373                 apply (not_eq_O_S n).
 374                 auto
 375                 (*apply sym_eq.
 376                 assumption*)
 377               | auto
 378                 (*apply le_S_S_to_le.
 379                 exact H5*)
 380               ]
 381             | assumption
 382             | assumption
 383             ]
 384           | cut (r=(S O))
 385             [ apply (nat_case n)
 386               [ auto
 387                 (*left.
 388                 split
 389                 [ assumption
 390                 | reflexivity
 391                 ]*)
 392               | intro.
 393                 right.
 394                 rewrite > Hcut2.
 395                 auto
 396                 (*simplify.
 397                 unfold lt.
 398                 apply le_S_S.
 399                 apply le_O_n*)
 400               ]
 401             | cut (r < (S O) ∨ r=(S O))
 402               [ elim Hcut2
 403                 [ absurd (O=r)
 404                   [ auto
 405                     (*apply le_n_O_to_eq.
 406                     apply le_S_S_to_le.
 407                     exact H5*)
 408                   | unfold Not.
 409                     intro.
 410                     auto
 411                     (*cut (O=n1)
 412                     [ apply (not_le_Sn_O O).
 413                       rewrite > Hcut3 in ⊢ (? ? %).
 414                       assumption
 415                     | rewrite > Hcut.
 416                       rewrite < H6.
 417                       reflexivity
 418                     ]*)
 419                   ]
 420                 | assumption
 421                 ]
 422               | auto
 423                 (*apply (le_to_or_lt_eq r (S O)).
 424                 apply not_lt_to_le.
 425                 assumption*)
 426               ]
 427             ]
 428           ]
 429         | apply (decidable_lt (S O) r)
 430         ]
 431       ]
 432     | rewrite > sym_times.
 433       apply (p_ord_aux_to_exp n1 n1)
 434       [ apply lt_O_nth_prime_n
 435       | assumption
 436       ]
 437     ]
 438   ]
 439 ]
 440 qed.
 441
 442 theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
 443 intro.
 444 apply (nat_case n)
 445 [ reflexivity
 446 | intro.
 447   apply (nat_case m)
 448   [ reflexivity
 449   | intro.(*CSC: simplify here does something really nasty *)
 450     change with
 451     (let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
 452     defactorize (match p_ord (S(S m1)) (nth_prime p) with
 453     [ (pair q r) \Rightarrow
 454        nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
 455     intro.
 456     (* generalizing the goal; find a better way *)
 457     cut (\forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to
 458     defactorize (match p_ord (S(S m1)) (nth_prime p) with
 459     [ (pair q r) \Rightarrow
 460       nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)))
 461     [ (*invocando auto qui, dopo circa 300 secondi non si ottiene alcun risultato*)
 462       apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
 463       (snd ? ? (p_ord (S(S m1)) (nth_prime p)))).
 464       auto
 465       (*apply sym_eq.
 466       apply eq_pair_fst_snd*)
 467     | intros.
 468       rewrite < H.
 469       simplify.
 470       cut ((S(S m1)) = (nth_prime p) \sup q *r)
 471       [ cut (O<r)
 472         [ rewrite > defactorize_aux_factorize_aux
 473           [ (*CSC: simplify here does something really nasty *)
 474             change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
 475             cut ((S (pred q)) = q)
 476             [ (*invocando auto qui, dopo circa 300 secondi non si ottiene ancora alcun risultato*)
 477               rewrite > Hcut2.
 478               auto
 479               (*rewrite > sym_times.
 480               apply sym_eq.
 481               apply (p_ord_aux_to_exp (S(S m1)))
 482               [ apply lt_O_nth_prime_n
 483               | assumption
 484               ]*)
 485             | (* O < q *)
 486               apply sym_eq.
 487               apply S_pred.
 488               cut (O < q \lor O = q)
 489               [ elim Hcut2
 490                 [ assumption
 491                 | absurd (nth_prime p \divides S (S m1))
 492                   [ apply (divides_max_prime_factor_n (S (S m1))).
 493                     auto
 494                     (*unfold lt.
 495                     apply le_S_S.
 496                     apply le_S_S.
 497                     apply le_O_n.*)
 498                   | cut ((S(S m1)) = r)
 499                     [ rewrite > Hcut3 in \vdash (? (? ? %)).
 500                       (*CSC: simplify here does something really nasty *)
 501                       change with (nth_prime p \divides r \to False).
 502                       intro.
 503                       apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r)                      [ apply lt_SO_nth_prime_n
 504                       | auto
 505                         (*unfold lt.
 506                         apply le_S_S.
 507                         apply le_O_n*)
 508                       | apply le_n
 509                       | assumption
 510                       | (*invocando auto qui, dopo circa 300 secondi non si ottiene ancora alcun risultato*)
 511                         apply divides_to_mod_O
 512                         [ apply lt_O_nth_prime_n
 513                         | assumption
 514                         ]
 515                       ]
 516                     | rewrite > times_n_SO in \vdash (? ? ? %).
 517                       rewrite < sym_times.
 518                       rewrite > (exp_n_O (nth_prime p)).
 519                       rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
 520                       assumption
 521                     ]
 522                   ]
 523                 ]
 524               | auto
 525                 (*apply le_to_or_lt_eq.
 526                 apply le_O_n*)
 527               ]
 528             ]
 529           | assumption
 530           | (* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
 531             cut ((S O) < r \lor S O \nlt r)
 532             [ elim Hcut2
 533               [ right.
 534                 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r);auto
 535                 (*[ unfold lt.
 536                   apply le_S_S.
 537                   apply le_O_n
 538                 | apply le_n
 539                 | assumption
 540                 | assumption
 541                 ]*)
 542               | cut (r=(S O))
 543                 [ apply (nat_case p)
 544                   [ auto
 545                     (*left.
 546                     split
 547                     [ assumption
 548                     | reflexivity
 549                     ]*)
 550                   | intro.
 551                     right.
 552                     rewrite > Hcut3.
 553                     auto
 554                     (*simplify.
 555                     unfold lt.
 556                     apply le_S_S.
 557                     apply le_O_n*)
 558                   ]
 559                 | cut (r \lt (S O) \or r=(S O))
 560                   [ elim Hcut3
 561                     [ absurd (O=r);auto
 562                       (*[ apply le_n_O_to_eq.
 563                         apply le_S_S_to_le.
 564                         exact H2
 565                       | unfold Not.
 566                         intro.
 567                         apply (not_le_Sn_O O).
 568                         rewrite > H3 in \vdash (? ? %).
 569                         assumption
 570                       ]*)
 571                     | assumption
 572                     ]
 573                   | auto
 574                     (*apply (le_to_or_lt_eq r (S O)).
 575                     apply not_lt_to_le.
 576                     assumption*)
 577                   ]
 578                 ]
 579               ]
 580             | apply (decidable_lt (S O) r)
 581             ]
 582           ]
 583         | (* O < r *)
 584           cut (O < r \lor O = r)
 585           [ elim Hcut1
 586             [ assumption
 587             | apply False_ind.
 588               apply (not_eq_O_S (S m1)).
 589               rewrite > Hcut.
 590               rewrite < H1.
 591               auto
 592               (*rewrite < times_n_O.
 593               reflexivity*)
 594             ]
 595           | auto
 596             (*apply le_to_or_lt_eq.
 597             apply le_O_n*)
 598           ]
 599         ]
 600       | (* prova del cut *)
 601         goal 20.
 602         apply (p_ord_aux_to_exp (S(S m1)));auto
 603         (*[ apply lt_O_nth_prime_n
 604         | assumption
 605         ]*)
 606         (* fine prova cut *)
 607       ]
 608     ]
 609   ]
 610 ]
 611 qed.
 612
 613 let rec max_p f \def
 614 match f with
 615 [ (nf_last n) \Rightarrow O
 616 | (nf_cons n g) \Rightarrow S (max_p g)].
 617
 618 let rec max_p_exponent f \def
 619 match f with
 620 [ (nf_last n) \Rightarrow n
 621 | (nf_cons n g) \Rightarrow max_p_exponent g].
 622
 623 theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat.
 624 nth_prime ((max_p f)+i) \divides defactorize_aux f i.
 625 intro.
 626 elim f
 627 [ simplify.
 628   auto
 629   (*apply (witness ? ? ((nth_prime i) \sup n)).
 630   reflexivity*)
 631 | change with
 632   (nth_prime (S(max_p n1)+i) \divides
 633   (nth_prime i) \sup n *(defactorize_aux n1 (S i))).
 634   elim (H (S i)).
 635   rewrite > H1.
 636   rewrite < sym_times.
 637   rewrite > assoc_times.
 638   auto
 639   (*rewrite < plus_n_Sm.
 640   apply (witness ? ? (n2* (nth_prime i) \sup n)).
 641   reflexivity*)
 642 ]
 643 qed.
 644
 645 theorem divides_exp_to_divides:
 646 \forall p,n,m:nat. prime p \to
 647 p \divides n \sup m \to p \divides n.
 648 intros 3.
 649 elim m
 650 [ simplify in H1.
 651   auto
 652   (*apply (transitive_divides p (S O))
 653   [ assumption
 654   | apply divides_SO_n
 655   ]*)
 656 | cut (p \divides n \lor p \divides n \sup n1)
 657   [ elim Hcut
 658     [ assumption
 659     | auto
 660       (*apply H;assumption*)
 661     ]
 662   | auto
 663     (*apply divides_times_to_divides
 664     [ assumption
 665     | exact H2
 666     ]*)
 667   ]
 668 ]
 669 qed.
 670
 671 theorem divides_exp_to_eq:
 672 \forall p,q,m:nat. prime p \to prime q \to
 673 p \divides q \sup m \to p = q.
 674 intros.
 675 unfold prime in H1.
 676 elim H1.
 677 apply H4
 678 [ apply (divides_exp_to_divides p q m);assumption
 679 | (*invocando auto in questo punto, dopo piu' di 8 minuti la computazione non
 680    * era ancora terminata.
 681    *)
 682   unfold prime in H.
 683   (*invocando auto anche in questo punto, dopo piu' di 10 minuti la computazione
 684    * non era ancora terminata.
 685    *)
 686   elim H.
 687   assumption
 688 ]
 689 qed.
 690
 691 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
 692 i < j \to nth_prime i \ndivides defactorize_aux f j.
 693 intro.
 694 elim f
 695 [ change with
 696   (nth_prime i \divides (nth_prime j) \sup (S n) \to False).
 697   intro.
 698   absurd ((nth_prime i) = (nth_prime j))
 699   [ apply (divides_exp_to_eq ? ? (S n));auto
 700     (*[ apply prime_nth_prime
 701     | apply prime_nth_prime
 702     | assumption
 703     ]*)
 704   | unfold Not.
 705     intro.
 706     cut (i = j)
 707     [ apply (not_le_Sn_n i).
 708       rewrite > Hcut in \vdash (? ? %).
 709       assumption
 710     | apply (injective_nth_prime ? ? H2)
 711     ]
 712   ]
 713 | unfold Not.
 714   simplify.
 715   intro.
 716   cut (nth_prime i \divides (nth_prime j) \sup n
 717   \lor nth_prime i \divides defactorize_aux n1 (S j))
 718   [ elim Hcut
 719     [ absurd ((nth_prime i) = (nth_prime j))
 720       [ apply (divides_exp_to_eq ? ? n);auto
 721         (*[ apply prime_nth_prime
 722         | apply prime_nth_prime
 723         | assumption
 724         ]*)
 725       | unfold Not.
 726         intro.
 727         cut (i = j)
 728         [ apply (not_le_Sn_n i).
 729           rewrite > Hcut1 in \vdash (? ? %).
 730           assumption
 731         | apply (injective_nth_prime ? ? H4)
 732         ]
 733       ]
 734     | apply (H i (S j))
 735       [ auto
 736         (*apply (trans_lt ? j)
 737         [ assumption
 738         | unfold lt.
 739           apply le_n
 740         ]*)
 741       | assumption
 742       ]
 743     ]
 744   | auto
 745     (*apply divides_times_to_divides.
 746     apply prime_nth_prime.
 747     assumption*)
 748   ]
 749 ]
 750 qed.
 751
 752 lemma not_eq_nf_last_nf_cons: \forall g:nat_fact.\forall n,m,i:nat.
 753 \lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i).
 754 intros.
 755 change with
 756 (exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False).
 757 intro.
 758 cut (S(max_p g)+i= i)
 759 [ apply (not_le_Sn_n i).
 760   rewrite < Hcut in \vdash (? ? %). (*chiamando auto qui da uno strano errore  "di tipo"*)
 761   simplify.
 762   auto
 763   (*apply le_S_S.
 764   apply le_plus_n*)
 765 | apply injective_nth_prime.
 766   apply (divides_exp_to_eq ? ? (S n))
 767   [ apply prime_nth_prime
 768   | apply prime_nth_prime
 769   | rewrite > H.
 770     change with (divides (nth_prime ((max_p (nf_cons m g))+i))
 771     (defactorize_aux (nf_cons m g) i)).
 772     apply divides_max_p_defactorize
 773   ]
 774 ]
 775 qed.
 776
 777 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
 778 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
 779 intros.
 780 simplify.
 781 unfold Not.
 782 rewrite < plus_n_O.
 783 intro.
 784 apply (not_divides_defactorize_aux f i (S i) ?)
 785 [ auto
 786   (*unfold lt.
 787   apply le_n*)
 788 | auto
 789   (*rewrite > H.
 790   rewrite > assoc_times.
 791   apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
 792   reflexivity*)
 793 ]
 794 qed.
 795
 796 theorem eq_defactorize_aux_to_eq: \forall f,g:nat_fact.\forall i:nat.
 797 defactorize_aux f i = defactorize_aux g i \to f = g.
 798 intro.
 799 elim f
 800 [ generalize in match H.
 801   elim g
 802   [ apply eq_f.
 803     apply inj_S.
 804     apply (inj_exp_r (nth_prime i))
 805     [ apply lt_SO_nth_prime_n
 806     | (*qui auto non conclude il goal attivo*)
 807       assumption
 808     ]
 809   | apply False_ind.
 810     (*auto chiamato qui NON conclude il goal attivo*)
 811     apply (not_eq_nf_last_nf_cons n2 n n1 i H2)
 812   ]
 813 | generalize in match H1.
 814   elim g
 815   [ apply False_ind.
 816     apply (not_eq_nf_last_nf_cons n1 n2 n i).
 817     auto
 818     (*apply sym_eq.
 819     assumption*)
 820   | simplify in H3.
 821     generalize in match H3.
 822     apply (nat_elim2 (\lambda n,n2.
 823     ((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
 824     ((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
 825     nf_cons n n1 = nf_cons n2 n3))
 826     [ intro.
 827       elim n4
 828       [ auto
 829         (*apply eq_f.
 830         apply (H n3 (S i))
 831         simplify in H4.
 832         rewrite > plus_n_O.
 833         rewrite > (plus_n_O (defactorize_aux n3 (S i))).
 834         assumption*)
 835       | apply False_ind.
 836         apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).
 837         (*auto chiamato qui NON chiude il goal attivo*)
 838         assumption
 839       ]
 840     | intros.
 841       apply False_ind.
 842       apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i).
 843       apply sym_eq.
 844       (*auto chiamato qui non chiude il goal*)
 845       assumption
 846     | intros.
 847       cut (nf_cons n4 n1 = nf_cons m n3)
 848       [ cut (n4=m)
 849         [ cut (n1=n3)
 850           [ auto
 851             (*rewrite > Hcut1.
 852             rewrite > Hcut2.
 853             reflexivity*)
 854           | change with
 855             (match nf_cons n4 n1 with
 856             [ (nf_last m) \Rightarrow n1
 857             | (nf_cons m g) \Rightarrow g ] = n3).
 858             rewrite > Hcut.
 859             auto
 860             (*simplify.
 861             reflexivity*)
 862           ]
 863         | change with
 864           (match nf_cons n4 n1 with
 865           [ (nf_last m) \Rightarrow m
 866           | (nf_cons m g) \Rightarrow m ] = m).
 867           (*invocando auto qui, dopo circa 8 minuti la computazione non era ancora terminata*)
 868           rewrite > Hcut.
 869           auto
 870           (*simplify.
 871           reflexivity*)
 872         ]
 873       | apply H4.
 874         simplify in H5.
 875         apply (inj_times_r1 (nth_prime i))
 876         [ apply lt_O_nth_prime_n
 877         | rewrite < assoc_times.
 878           rewrite < assoc_times.
 879           assumption
 880         ]
 881       ]
 882     ]
 883   ]
 884 ]
 885 qed.
 886
 887 theorem injective_defactorize_aux: \forall i:nat.
 888 injective nat_fact nat (\lambda f.defactorize_aux f i).
 889 simplify.
 890 intros.
 891 apply (eq_defactorize_aux_to_eq x y i H).
 892 qed.
 893
 894 theorem injective_defactorize:
 895 injective nat_fact_all nat defactorize.
 896 unfold injective.
 897 change with (\forall f,g.defactorize f = defactorize g \to f=g).
 898 intro.
 899 elim f
 900 [ generalize in match H.
 901   elim g
 902   [ (* zero - zero *)
 903     reflexivity
 904   | (* zero - one *)
 905     simplify in H1.
 906     apply False_ind.
 907     apply (not_eq_O_S O H1)
 908   | (* zero - proper *)
 909     simplify in H1.
 910     apply False_ind.
 911     apply (not_le_Sn_n O).
 912     rewrite > H1 in \vdash (? ? %).
 913     auto
 914     (*change with (O < defactorize_aux n O).
 915     apply lt_O_defactorize_aux*)
 916   ]
 917 | generalize in match H.
 918   elim g
 919   [ (* one - zero *)
 920     simplify in H1.
 921     apply False_ind.
 922     auto
 923     (*apply (not_eq_O_S O).
 924     apply sym_eq.
 925     assumption*)
 926   | (* one - one *)
 927     reflexivity
 928   | (* one - proper *)
 929     simplify in H1.
 930     apply False_ind.
 931     apply (not_le_Sn_n (S O)).
 932     rewrite > H1 in \vdash (? ? %).
 933     auto
 934     (*change with ((S O) < defactorize_aux n O).
 935     apply lt_SO_defactorize_aux*)
 936   ]
 937 | generalize in match H.
 938   elim g
 939   [ (* proper - zero *)
 940     simplify in H1.
 941     apply False_ind.
 942     apply (not_le_Sn_n O).
 943     rewrite < H1 in \vdash (? ? %).
 944     auto
 945     (*change with (O < defactorize_aux n O).
 946     apply lt_O_defactorize_aux.*)
 947   | (* proper - one *)
 948     simplify in H1.
 949     apply False_ind.
 950     apply (not_le_Sn_n (S O)).
 951     rewrite < H1 in \vdash (? ? %).
 952     auto
 953     (*change with ((S O) < defactorize_aux n O).
 954     apply lt_SO_defactorize_aux.*)
 955   | (* proper - proper *)
 956     apply eq_f.
 957     apply (injective_defactorize_aux O).
 958     (*invocata qui la tattica auto NON chiude il goal, chiuso invece
 959      *da exact H1
 960      *)
 961     exact H1
 962   ]
 963 ]
 964 qed.
 965
 966 theorem factorize_defactorize:
 967 \forall f,g: nat_fact_all. factorize (defactorize f) = f.
 968 intros.
 969 auto.
 970 (*apply injective_defactorize.
 971 apply defactorize_factorize.
 972 *)
 973 qed.