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         apply (p_ord_aux_to_exp (S(S m1)));auto
 602         (*[ apply lt_O_nth_prime_n
 603         | assumption
 604         ]*)
 605         (* fine prova cut *)
 606       ]
 607     ]
 608   ]
 609 ]
 610 qed.
 611
 612 let rec max_p f \def
 613 match f with
 614 [ (nf_last n) \Rightarrow O
 615 | (nf_cons n g) \Rightarrow S (max_p g)].
 616
 617 let rec max_p_exponent f \def
 618 match f with
 619 [ (nf_last n) \Rightarrow n
 620 | (nf_cons n g) \Rightarrow max_p_exponent g].
 621
 622 theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat.
 623 nth_prime ((max_p f)+i) \divides defactorize_aux f i.
 624 intro.
 625 elim f
 626 [ simplify.
 627   auto
 628   (*apply (witness ? ? ((nth_prime i) \sup n)).
 629   reflexivity*)
 630 | change with
 631   (nth_prime (S(max_p n1)+i) \divides
 632   (nth_prime i) \sup n *(defactorize_aux n1 (S i))).
 633   elim (H (S i)).
 634   rewrite > H1.
 635   rewrite < sym_times.
 636   rewrite > assoc_times.
 637   auto
 638   (*rewrite < plus_n_Sm.
 639   apply (witness ? ? (n2* (nth_prime i) \sup n)).
 640   reflexivity*)
 641 ]
 642 qed.
 643
 644 theorem divides_exp_to_divides:
 645 \forall p,n,m:nat. prime p \to
 646 p \divides n \sup m \to p \divides n.
 647 intros 3.
 648 elim m
 649 [ simplify in H1.
 650   auto
 651   (*apply (transitive_divides p (S O))
 652   [ assumption
 653   | apply divides_SO_n
 654   ]*)
 655 | cut (p \divides n \lor p \divides n \sup n1)
 656   [ elim Hcut
 657     [ assumption
 658     | auto
 659       (*apply H;assumption*)
 660     ]
 661   | auto
 662     (*apply divides_times_to_divides
 663     [ assumption
 664     | exact H2
 665     ]*)
 666   ]
 667 ]
 668 qed.
 669
 670 theorem divides_exp_to_eq:
 671 \forall p,q,m:nat. prime p \to prime q \to
 672 p \divides q \sup m \to p = q.
 673 intros.
 674 unfold prime in H1.
 675 elim H1.
 676 apply H4
 677 [ apply (divides_exp_to_divides p q m);assumption
 678 | (*invocando auto in questo punto, dopo piu' di 8 minuti la computazione non
 679    * era ancora terminata.
 680    *)
 681   unfold prime in H.
 682   (*invocando auto anche in questo punto, dopo piu' di 10 minuti la computazione
 683    * non era ancora terminata.
 684    *)
 685   elim H.
 686   assumption
 687 ]
 688 qed.
 689
 690 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
 691 i < j \to nth_prime i \ndivides defactorize_aux f j.
 692 intro.
 693 elim f
 694 [ change with
 695   (nth_prime i \divides (nth_prime j) \sup (S n) \to False).
 696   intro.
 697   absurd ((nth_prime i) = (nth_prime j))
 698   [ apply (divides_exp_to_eq ? ? (S n));auto
 699     (*[ apply prime_nth_prime
 700     | apply prime_nth_prime
 701     | assumption
 702     ]*)
 703   | unfold Not.
 704     intro.
 705     cut (i = j)
 706     [ apply (not_le_Sn_n i).
 707       rewrite > Hcut in \vdash (? ? %).
 708       assumption
 709     | apply (injective_nth_prime ? ? H2)
 710     ]
 711   ]
 712 | unfold Not.
 713   simplify.
 714   intro.
 715   cut (nth_prime i \divides (nth_prime j) \sup n
 716   \lor nth_prime i \divides defactorize_aux n1 (S j))
 717   [ elim Hcut
 718     [ absurd ((nth_prime i) = (nth_prime j))
 719       [ apply (divides_exp_to_eq ? ? n);auto
 720         (*[ apply prime_nth_prime
 721         | apply prime_nth_prime
 722         | assumption
 723         ]*)
 724       | unfold Not.
 725         intro.
 726         cut (i = j)
 727         [ apply (not_le_Sn_n i).
 728           rewrite > Hcut1 in \vdash (? ? %).
 729           assumption
 730         | apply (injective_nth_prime ? ? H4)
 731         ]
 732       ]
 733     | apply (H i (S j))
 734       [ auto
 735         (*apply (trans_lt ? j)
 736         [ assumption
 737         | unfold lt.
 738           apply le_n
 739         ]*)
 740       | assumption
 741       ]
 742     ]
 743   | auto
 744     (*apply divides_times_to_divides.
 745     apply prime_nth_prime.
 746     assumption*)
 747   ]
 748 ]
 749 qed.
 750
 751 lemma not_eq_nf_last_nf_cons: \forall g:nat_fact.\forall n,m,i:nat.
 752 \lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i).
 753 intros.
 754 change with
 755 (exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False).
 756 intro.
 757 cut (S(max_p g)+i= i)
 758 [ apply (not_le_Sn_n i).
 759   rewrite < Hcut in \vdash (? ? %). (*chiamando auto qui da uno strano errore  "di tipo"*)
 760   simplify.
 761   auto
 762   (*apply le_S_S.
 763   apply le_plus_n*)
 764 | apply injective_nth_prime.
 765   apply (divides_exp_to_eq ? ? (S n))
 766   [ apply prime_nth_prime
 767   | apply prime_nth_prime
 768   | rewrite > H.
 769     change with (divides (nth_prime ((max_p (nf_cons m g))+i))
 770     (defactorize_aux (nf_cons m g) i)).
 771     apply divides_max_p_defactorize
 772   ]
 773 ]
 774 qed.
 775
 776 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
 777 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
 778 intros.
 779 simplify.
 780 unfold Not.
 781 rewrite < plus_n_O.
 782 intro.
 783 apply (not_divides_defactorize_aux f i (S i) ?)
 784 [ auto
 785   (*unfold lt.
 786   apply le_n*)
 787 | auto
 788   (*rewrite > H.
 789   rewrite > assoc_times.
 790   apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
 791   reflexivity*)
 792 ]
 793 qed.
 794
 795 theorem eq_defactorize_aux_to_eq: \forall f,g:nat_fact.\forall i:nat.
 796 defactorize_aux f i = defactorize_aux g i \to f = g.
 797 intro.
 798 elim f
 799 [ generalize in match H.
 800   elim g
 801   [ apply eq_f.
 802     apply inj_S.
 803     apply (inj_exp_r (nth_prime i))
 804     [ apply lt_SO_nth_prime_n
 805     | (*qui auto non conclude il goal attivo*)
 806       assumption
 807     ]
 808   | apply False_ind.
 809     (*auto chiamato qui NON conclude il goal attivo*)
 810     apply (not_eq_nf_last_nf_cons n2 n n1 i H2)
 811   ]
 812 | generalize in match H1.
 813   elim g
 814   [ apply False_ind.
 815     apply (not_eq_nf_last_nf_cons n1 n2 n i).
 816     auto
 817     (*apply sym_eq.
 818     assumption*)
 819   | simplify in H3.
 820     generalize in match H3.
 821     apply (nat_elim2 (\lambda n,n2.
 822     ((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
 823     ((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
 824     nf_cons n n1 = nf_cons n2 n3))
 825     [ intro.
 826       elim n4
 827       [ auto
 828         (*apply eq_f.
 829         apply (H n3 (S i))
 830         simplify in H4.
 831         rewrite > plus_n_O.
 832         rewrite > (plus_n_O (defactorize_aux n3 (S i))).
 833         assumption*)
 834       | apply False_ind.
 835         apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).
 836         (*auto chiamato qui NON chiude il goal attivo*)
 837         assumption
 838       ]
 839     | intros.
 840       apply False_ind.
 841       apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i).
 842       apply sym_eq.
 843       (*auto chiamato qui non chiude il goal*)
 844       assumption
 845     | intros.
 846       cut (nf_cons n4 n1 = nf_cons m n3)
 847       [ cut (n4=m)
 848         [ cut (n1=n3)
 849           [ auto
 850             (*rewrite > Hcut1.
 851             rewrite > Hcut2.
 852             reflexivity*)
 853           | change with
 854             (match nf_cons n4 n1 with
 855             [ (nf_last m) \Rightarrow n1
 856             | (nf_cons m g) \Rightarrow g ] = n3).
 857             rewrite > Hcut.
 858             auto
 859             (*simplify.
 860             reflexivity*)
 861           ]
 862         | change with
 863           (match nf_cons n4 n1 with
 864           [ (nf_last m) \Rightarrow m
 865           | (nf_cons m g) \Rightarrow m ] = m).
 866           (*invocando auto qui, dopo circa 8 minuti la computazione non era ancora terminata*)
 867           rewrite > Hcut.
 868           auto
 869           (*simplify.
 870           reflexivity*)
 871         ]
 872       | apply H4.
 873         simplify in H5.
 874         apply (inj_times_r1 (nth_prime i))
 875         [ apply lt_O_nth_prime_n
 876         | rewrite < assoc_times.
 877           rewrite < assoc_times.
 878           assumption
 879         ]
 880       ]
 881     ]
 882   ]
 883 ]
 884 qed.
 885
 886 theorem injective_defactorize_aux: \forall i:nat.
 887 injective nat_fact nat (\lambda f.defactorize_aux f i).
 888 simplify.
 889 intros.
 890 apply (eq_defactorize_aux_to_eq x y i H).
 891 qed.
 892
 893 theorem injective_defactorize:
 894 injective nat_fact_all nat defactorize.
 895 unfold injective.
 896 change with (\forall f,g.defactorize f = defactorize g \to f=g).
 897 intro.
 898 elim f
 899 [ generalize in match H.
 900   elim g
 901   [ (* zero - zero *)
 902     reflexivity
 903   | (* zero - one *)
 904     simplify in H1.
 905     apply False_ind.
 906     apply (not_eq_O_S O H1)
 907   | (* zero - proper *)
 908     simplify in H1.
 909     apply False_ind.
 910     apply (not_le_Sn_n O).
 911     rewrite > H1 in \vdash (? ? %).
 912     auto
 913     (*change with (O < defactorize_aux n O).
 914     apply lt_O_defactorize_aux*)
 915   ]
 916 | generalize in match H.
 917   elim g
 918   [ (* one - zero *)
 919     simplify in H1.
 920     apply False_ind.
 921     auto
 922     (*apply (not_eq_O_S O).
 923     apply sym_eq.
 924     assumption*)
 925   | (* one - one *)
 926     reflexivity
 927   | (* one - proper *)
 928     simplify in H1.
 929     apply False_ind.
 930     apply (not_le_Sn_n (S O)).
 931     rewrite > H1 in \vdash (? ? %).
 932     auto
 933     (*change with ((S O) < defactorize_aux n O).
 934     apply lt_SO_defactorize_aux*)
 935   ]
 936 | generalize in match H.
 937   elim g
 938   [ (* proper - zero *)
 939     simplify in H1.
 940     apply False_ind.
 941     apply (not_le_Sn_n O).
 942     rewrite < H1 in \vdash (? ? %).
 943     auto
 944     (*change with (O < defactorize_aux n O).
 945     apply lt_O_defactorize_aux.*)
 946   | (* proper - one *)
 947     simplify in H1.
 948     apply False_ind.
 949     apply (not_le_Sn_n (S O)).
 950     rewrite < H1 in \vdash (? ? %).
 951     auto
 952     (*change with ((S O) < defactorize_aux n O).
 953     apply lt_SO_defactorize_aux.*)
 954   | (* proper - proper *)
 955     apply eq_f.
 956     apply (injective_defactorize_aux O).
 957     (*invocata qui la tattica auto NON chiude il goal, chiuso invece
 958      *da exact H1
 959      *)
 960     exact H1
 961   ]
 962 ]
 963 qed.
 964
 965 theorem factorize_defactorize:
 966 \forall f,g: nat_fact_all. factorize (defactorize f) = f.
 967 intros.
 968 auto.
 969 (*apply injective_defactorize.
 970 apply defactorize_factorize.
 971 *)
 972 qed.