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