]> matita.cs.unibo.it Git - helm.git/blob - matita/library_auto/auto/nat/factorization.ma
debian package for matita
[helm.git] / 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.