1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/factorization".
19 include "nat/nth_prime.ma".
21 (* the following factorization algorithm looks for the largest prime
23 definition max_prime_factor \def \lambda n:nat.
24 (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)).
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; apply divides_b_true_to_divides;
31 [ apply lt_O_nth_prime_n;
32 | apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
33 cut (\exists i. nth_prime i = smallest_factor n);
35 apply (ex_intro nat ? a);
37 [ apply (trans_le a (nth_prime a));
39 exact lt_nth_prime_n_nth_prime_Sn;
41 apply le_smallest_factor_n; ]
43 (*CSC: simplify here does something nasty! *)
44 change with (divides_b (smallest_factor n) n = true);
45 apply divides_to_divides_b_true;
46 [ apply (trans_lt ? (S O));
47 [ unfold lt; apply le_n;
48 | apply lt_SO_smallest_factor; assumption; ]
49 | apply divides_smallest_factor_n;
50 apply (trans_lt ? (S O));
51 [ unfold lt; apply le_n;
53 | apply prime_to_nth_prime;
54 apply prime_smallest_factor_n;
58 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to
59 max_prime_factor n \le max_prime_factor m.
60 intros.unfold max_prime_factor.
63 apply le_max_n.apply divides_to_le.assumption.assumption.
64 change with (divides_b (nth_prime (max_prime_factor n)) m = true).
65 apply divides_to_divides_b_true.
66 cut (prime (nth_prime (max_prime_factor n))).
67 apply lt_O_nth_prime_n.apply prime_nth_prime.
68 cut (nth_prime (max_prime_factor n) \divides n).
69 apply (transitive_divides ? n).
70 apply divides_max_prime_factor_n.
71 assumption.assumption.
72 apply divides_b_true_to_divides.
73 apply lt_O_nth_prime_n.
74 apply divides_to_divides_b_true.
75 apply lt_O_nth_prime_n.
76 apply divides_max_prime_factor_n.
80 theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to
81 p = max_prime_factor n \to
82 (pair nat nat q r) = p_ord n (nth_prime p) \to
83 (S O) < r \to max_prime_factor r < p.
86 cut (max_prime_factor r \lt max_prime_factor n \lor
87 max_prime_factor r = max_prime_factor n).
89 absurd (nth_prime (max_prime_factor n) \divides r).
91 apply divides_max_prime_factor_n.
92 assumption.unfold Not.
94 cut (r \mod (nth_prime (max_prime_factor n)) \neq O).
95 apply Hcut1.apply divides_to_mod_O.
96 apply lt_O_nth_prime_n.assumption.
97 apply (p_ord_aux_to_not_mod_O n n ? q r).
98 apply lt_SO_nth_prime_n.assumption.
100 rewrite < H1.assumption.
101 apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)).
102 apply divides_to_max_prime_factor.
103 assumption.assumption.
104 apply (witness r n ((nth_prime p) \sup q)).
106 apply (p_ord_aux_to_exp n n ? q r).
107 apply lt_O_nth_prime_n.assumption.
110 theorem p_ord_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to
111 max_prime_factor n \le p \to
112 (pair nat nat q r) = p_ord n (nth_prime p) \to
113 (S O) < r \to max_prime_factor r < p.
115 cut (max_prime_factor n < p \lor max_prime_factor n = p).
116 elim Hcut.apply (le_to_lt_to_lt ? (max_prime_factor n)).
117 apply divides_to_max_prime_factor.assumption.assumption.
118 apply (witness r n ((nth_prime p) \sup q)).
120 apply (p_ord_aux_to_exp n n).
121 apply lt_O_nth_prime_n.
122 assumption.assumption.
123 apply (p_ord_to_lt_max_prime_factor n ? q).
124 assumption.apply sym_eq.assumption.assumption.assumption.
125 apply (le_to_or_lt_eq ? p H1).
128 (* datatypes and functions *)
130 inductive nat_fact : Set \def
131 nf_last : nat \to nat_fact
132 | nf_cons : nat \to nat_fact \to nat_fact.
134 inductive nat_fact_all : Set \def
135 nfa_zero : nat_fact_all
136 | nfa_one : nat_fact_all
137 | nfa_proper : nat_fact \to nat_fact_all.
139 let rec factorize_aux p n acc \def
143 match p_ord n (nth_prime p1) with
144 [ (pair q r) \Rightarrow
145 factorize_aux p1 r (nf_cons q acc)]].
147 definition factorize : nat \to nat_fact_all \def \lambda n:nat.
149 [ O \Rightarrow nfa_zero
152 [ O \Rightarrow nfa_one
154 let p \def (max (S(S n2)) (\lambda p:nat.eqb ((S(S n2)) \mod (nth_prime p)) O)) in
155 match p_ord (S(S n2)) (nth_prime p) with
156 [ (pair q r) \Rightarrow
157 nfa_proper (factorize_aux p r (nf_last (pred q)))]]].
159 let rec defactorize_aux f i \def
161 [ (nf_last n) \Rightarrow (nth_prime i) \sup (S n)
162 | (nf_cons n g) \Rightarrow
163 (nth_prime i) \sup n *(defactorize_aux g (S i))].
165 definition defactorize : nat_fact_all \to nat \def
166 \lambda f : nat_fact_all.
168 [ nfa_zero \Rightarrow O
169 | nfa_one \Rightarrow (S O)
170 | (nfa_proper g) \Rightarrow defactorize_aux g O].
172 theorem lt_O_defactorize_aux:
175 O < defactorize_aux f i.
179 rewrite > times_n_SO;
181 [ change with (O < nth_prime i);
182 apply lt_O_nth_prime_n;
184 change with (O < exp (nth_prime i) n);
186 apply lt_O_nth_prime_n;
187 | change with (O < defactorize_aux n1 (S i));
191 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
192 S O < defactorize_aux f i.
193 intro.elim f.simplify.unfold lt.
194 rewrite > times_n_SO.
196 change with (S O < nth_prime i).
197 apply lt_SO_nth_prime_n.
198 change with (O < exp (nth_prime i) n).
200 apply lt_O_nth_prime_n.
202 rewrite > times_n_SO.
205 change with (O < exp (nth_prime i) n).
207 apply lt_O_nth_prime_n.
208 change with (S O < defactorize_aux n1 (S i)).
212 theorem defactorize_aux_factorize_aux :
213 \forall p,n:nat.\forall acc:nat_fact.O < n \to
214 ((n=(S O) \land p=O) \lor max_prime_factor n < p) \to
215 defactorize_aux (factorize_aux p n acc) O = n*(defactorize_aux acc p).
216 intro.elim p.simplify.
217 elim H1.elim H2.rewrite > H3.
218 rewrite > sym_times. apply times_n_SO.
219 apply False_ind.apply (not_le_Sn_O (max_prime_factor n) H2).
221 (* generalizing the goal: I guess there exists a better way *)
222 cut (\forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to
223 defactorize_aux match (p_ord_aux n1 n1 (nth_prime n)) with
224 [(pair q r) \Rightarrow (factorize_aux n r (nf_cons q acc))] O =
225 n1*defactorize_aux acc (S n)).
226 apply (Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n)))
227 (snd ? ? (p_ord_aux n1 n1 (nth_prime n)))).
228 apply sym_eq.apply eq_pair_fst_snd.
232 cut (n1 = r * (nth_prime n) \sup q).
234 simplify.rewrite < assoc_times.
235 rewrite < Hcut.reflexivity.
236 cut (O < r \lor O = r).
237 elim Hcut1.assumption.absurd (n1 = O).
238 rewrite > Hcut.rewrite < H4.reflexivity.
239 unfold Not. intro.apply (not_le_Sn_O O).
240 rewrite < H5 in \vdash (? ? %).assumption.
241 apply le_to_or_lt_eq.apply le_O_n.
242 cut ((S O) < r \lor (S O) \nlt r).
245 apply (p_ord_to_lt_max_prime_factor1 n1 ? q r).
249 apply (not_eq_O_S n).apply sym_eq.assumption.
252 assumption.assumption.
255 left.split.assumption.reflexivity.
256 intro.right.rewrite > Hcut2.
257 simplify.unfold lt.apply le_S_S.apply le_O_n.
258 cut (r \lt (S O) \or r=(S O)).
259 elim Hcut2.absurd (O=r).
260 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
263 apply (not_le_Sn_O O).
264 rewrite > Hcut3 in \vdash (? ? %).
265 assumption.rewrite > Hcut.
266 rewrite < H6.reflexivity.
268 apply (le_to_or_lt_eq r (S O)).
269 apply not_lt_to_le.assumption.
270 apply (decidable_lt (S O) r).
272 apply (p_ord_aux_to_exp n1 n1).
273 apply lt_O_nth_prime_n.assumption.
276 theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
278 apply (nat_case n).reflexivity.
279 intro.apply (nat_case m).reflexivity.
280 intro.(*CSC: simplify here does something really nasty *)
282 (let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
283 defactorize (match p_ord (S(S m1)) (nth_prime p) with
284 [ (pair q r) \Rightarrow
285 nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
287 (* generalizing the goal; find a better way *)
288 cut (\forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to
289 defactorize (match p_ord (S(S m1)) (nth_prime p) with
290 [ (pair q r) \Rightarrow
291 nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
292 apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
293 (snd ? ? (p_ord (S(S m1)) (nth_prime p)))).
294 apply sym_eq.apply eq_pair_fst_snd.
298 cut ((S(S m1)) = (nth_prime p) \sup q *r).
300 rewrite > defactorize_aux_factorize_aux.
301 (*CSC: simplify here does something really nasty *)
302 change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
303 cut ((S (pred q)) = q).
307 apply (p_ord_aux_to_exp (S(S m1))).
308 apply lt_O_nth_prime_n.
311 apply sym_eq. apply S_pred.
312 cut (O < q \lor O = q).
313 elim Hcut2.assumption.
314 absurd (nth_prime p \divides S (S m1)).
315 apply (divides_max_prime_factor_n (S (S m1))).
316 unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
318 rewrite > Hcut3 in \vdash (? (? ? %)).
319 (*CSC: simplify here does something really nasty *)
320 change with (nth_prime p \divides r \to False).
322 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
323 apply lt_SO_nth_prime_n.
324 unfold lt.apply le_S_S.apply le_O_n.apply le_n.
326 apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
327 rewrite > times_n_SO in \vdash (? ? ? %).
329 rewrite > (exp_n_O (nth_prime p)).
330 rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
332 apply le_to_or_lt_eq.apply le_O_n.assumption.
333 (* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
334 cut ((S O) < r \lor S O \nlt r).
337 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
338 unfold lt.apply le_S_S. apply le_O_n.
340 assumption.assumption.
343 left.split.assumption.reflexivity.
344 intro.right.rewrite > Hcut3.
345 simplify.unfold lt.apply le_S_S.apply le_O_n.
346 cut (r \lt (S O) \or r=(S O)).
347 elim Hcut3.absurd (O=r).
348 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
350 apply (not_le_Sn_O O).
351 rewrite > H3 in \vdash (? ? %).assumption.assumption.
352 apply (le_to_or_lt_eq r (S O)).
353 apply not_lt_to_le.assumption.
354 apply (decidable_lt (S O) r).
356 cut (O < r \lor O = r).
357 elim Hcut1.assumption.
359 apply (not_eq_O_S (S m1)).
360 rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
361 apply le_to_or_lt_eq.apply le_O_n.
364 apply (p_ord_aux_to_exp (S(S m1))).
365 apply lt_O_nth_prime_n.
372 [ (nf_last n) \Rightarrow O
373 | (nf_cons n g) \Rightarrow S (max_p g)].
375 let rec max_p_exponent f \def
377 [ (nf_last n) \Rightarrow n
378 | (nf_cons n g) \Rightarrow max_p_exponent g].
380 theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat.
381 nth_prime ((max_p f)+i) \divides defactorize_aux f i.
383 elim f.simplify.apply (witness ? ? ((nth_prime i) \sup n)).
386 (nth_prime (S(max_p n1)+i) \divides
387 (nth_prime i) \sup n *(defactorize_aux n1 (S i))).
391 rewrite > assoc_times.
393 apply (witness ? ? (n2* (nth_prime i) \sup n)).
397 theorem divides_exp_to_divides:
398 \forall p,n,m:nat. prime p \to
399 p \divides n \sup m \to p \divides n.
400 intros 3.elim m.simplify in H1.
401 apply (transitive_divides p (S O)).assumption.
403 cut (p \divides n \lor p \divides n \sup n1).
404 elim Hcut.assumption.
405 apply H.assumption.assumption.
406 apply divides_times_to_divides.assumption.
410 theorem divides_exp_to_eq:
411 \forall p,q,m:nat. prime p \to prime q \to
412 p \divides q \sup m \to p = q.
416 apply (divides_exp_to_divides p q m).
417 assumption.assumption.
418 unfold prime in H.elim H.assumption.
421 theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
422 i < j \to nth_prime i \ndivides defactorize_aux f j.
425 (nth_prime i \divides (nth_prime j) \sup (S n) \to False).
426 intro.absurd ((nth_prime i) = (nth_prime j)).
427 apply (divides_exp_to_eq ? ? (S n)).
428 apply prime_nth_prime.apply prime_nth_prime.
429 assumption.unfold Not.
431 apply (not_le_Sn_n i).rewrite > Hcut in \vdash (? ? %).assumption.
432 apply (injective_nth_prime ? ? H2).
435 cut (nth_prime i \divides (nth_prime j) \sup n
436 \lor nth_prime i \divides defactorize_aux n1 (S j)).
438 absurd ((nth_prime i) = (nth_prime j)).
439 apply (divides_exp_to_eq ? ? n).
440 apply prime_nth_prime.apply prime_nth_prime.
441 assumption.unfold Not.
444 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
445 apply (injective_nth_prime ? ? H4).
447 apply (trans_lt ? j).assumption.unfold lt.apply le_n.
449 apply divides_times_to_divides.
450 apply prime_nth_prime.assumption.
453 lemma not_eq_nf_last_nf_cons: \forall g:nat_fact.\forall n,m,i:nat.
454 \lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i).
457 (exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False).
459 cut (S(max_p g)+i= i).
460 apply (not_le_Sn_n i).
461 rewrite < Hcut in \vdash (? ? %).
462 simplify.apply le_S_S.
464 apply injective_nth_prime.
465 apply (divides_exp_to_eq ? ? (S n)).
466 apply prime_nth_prime.apply prime_nth_prime.
468 change with (divides (nth_prime ((max_p (nf_cons m g))+i))
469 (defactorize_aux (nf_cons m g) i)).
470 apply divides_max_p_defactorize.
473 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
474 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
476 simplify.unfold Not.rewrite < plus_n_O.
478 apply (not_divides_defactorize_aux f i (S i) ?).
479 unfold lt.apply le_n.
481 rewrite > assoc_times.
482 apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
486 theorem eq_defactorize_aux_to_eq: \forall f,g:nat_fact.\forall i:nat.
487 defactorize_aux f i = defactorize_aux g i \to f = g.
490 generalize in match H.
493 apply inj_S. apply (inj_exp_r (nth_prime i)).
494 apply lt_SO_nth_prime_n.
497 apply (not_eq_nf_last_nf_cons n2 n n1 i H2).
498 generalize in match H1.
501 apply (not_eq_nf_last_nf_cons n1 n2 n i).
502 apply sym_eq. assumption.
504 generalize in match H3.
505 apply (nat_elim2 (\lambda n,n2.
506 ((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
507 ((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
508 nf_cons n n1 = nf_cons n2 n3)).
514 rewrite > (plus_n_O (defactorize_aux n3 (S i))).assumption.
516 apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).assumption.
519 apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i).
520 apply sym_eq.assumption.
522 cut (nf_cons n4 n1 = nf_cons m n3).
525 rewrite > Hcut1.rewrite > Hcut2.reflexivity.
527 (match nf_cons n4 n1 with
528 [ (nf_last m) \Rightarrow n1
529 | (nf_cons m g) \Rightarrow g ] = n3).
530 rewrite > Hcut.simplify.reflexivity.
532 (match nf_cons n4 n1 with
533 [ (nf_last m) \Rightarrow m
534 | (nf_cons m g) \Rightarrow m ] = m).
535 rewrite > Hcut.simplify.reflexivity.
536 apply H4.simplify in H5.
537 apply (inj_times_r1 (nth_prime i)).
538 apply lt_O_nth_prime_n.
539 rewrite < assoc_times.rewrite < assoc_times.assumption.
542 theorem injective_defactorize_aux: \forall i:nat.
543 injective nat_fact nat (\lambda f.defactorize_aux f i).
546 apply (eq_defactorize_aux_to_eq x y i H).
549 theorem injective_defactorize:
550 injective nat_fact_all nat defactorize.
552 change with (\forall f,g.defactorize f = defactorize g \to f=g).
554 generalize in match H.elim g.
560 apply (not_eq_O_S O H1).
564 apply (not_le_Sn_n O).
565 rewrite > H1 in \vdash (? ? %).
566 change with (O < defactorize_aux n O).
567 apply lt_O_defactorize_aux.
568 generalize in match H.
573 apply (not_eq_O_S O).apply sym_eq. assumption.
579 apply (not_le_Sn_n (S O)).
580 rewrite > H1 in \vdash (? ? %).
581 change with ((S O) < defactorize_aux n O).
582 apply lt_SO_defactorize_aux.
583 generalize in match H.elim g.
587 apply (not_le_Sn_n O).
588 rewrite < H1 in \vdash (? ? %).
589 change with (O < defactorize_aux n O).
590 apply lt_O_defactorize_aux.
594 apply (not_le_Sn_n (S O)).
595 rewrite < H1 in \vdash (? ? %).
596 change with ((S O) < defactorize_aux n O).
597 apply lt_SO_defactorize_aux.
598 (* proper - proper *)
600 apply (injective_defactorize_aux O).
604 theorem factorize_defactorize:
605 \forall f,g: nat_fact_all. factorize (defactorize f) = f.
607 apply injective_defactorize.
608 apply defactorize_factorize.