]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/factorization.ma
fix
[helm.git] / helm / 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 set "baseuri" "cic:/matita/nat/factorization".
16
17 include "nat/ord.ma".
18 include "nat/gcd.ma".
19 include "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: \forall n:nat. (S O) < n \to
28 nth_prime (max_prime_factor n) \divides n.
29 intros.apply divides_b_true_to_divides.
30 apply lt_O_nth_prime_n.
31 apply (f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n).
32 cut (\exists i. nth_prime i = smallest_factor n).
33 elim Hcut.
34 apply (ex_intro nat ? a).
35 split.
36 apply (trans_le a (nth_prime a)).
37 apply le_n_fn.
38 exact lt_nth_prime_n_nth_prime_Sn.
39 rewrite > H1. apply le_smallest_factor_n.
40 rewrite > H1.
41 change with (divides_b (smallest_factor n) n = true).
42 apply divides_to_divides_b_true.
43 apply (trans_lt ? (S O)).unfold lt. apply le_n.
44 apply lt_SO_smallest_factor.assumption.
45 apply divides_smallest_factor_n.
46 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
47 apply prime_to_nth_prime.
48 apply prime_smallest_factor_n.assumption.
49 qed.
50
51 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to 
52 max_prime_factor n \le max_prime_factor m.
53 intros.change with
54 ((max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) \le
55 (max m (\lambda p:nat.eqb (m \mod (nth_prime p)) O))).
56 apply f_m_to_le_max.
57 apply (trans_le ? n).
58 apply le_max_n.apply divides_to_le.assumption.assumption.
59 change with (divides_b (nth_prime (max_prime_factor n)) m = true).
60 apply divides_to_divides_b_true.
61 cut (prime (nth_prime (max_prime_factor n))).
62 apply lt_O_nth_prime_n.apply prime_nth_prime.
63 cut (nth_prime (max_prime_factor n) \divides n).
64 apply (transitive_divides ? n).
65 apply divides_max_prime_factor_n.
66 assumption.assumption.
67 apply divides_b_true_to_divides.
68 apply lt_O_nth_prime_n.
69 apply divides_to_divides_b_true.
70 apply lt_O_nth_prime_n.
71 apply divides_max_prime_factor_n.
72 assumption.
73 qed.
74
75 theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to
76 p = max_prime_factor n \to 
77 (pair nat nat q r) = p_ord n (nth_prime p) \to
78 (S O) < r \to max_prime_factor r < p.
79 intros.
80 rewrite > H1.
81 cut (max_prime_factor r \lt max_prime_factor n \lor
82     max_prime_factor r = max_prime_factor n).
83 elim Hcut.assumption.
84 absurd (nth_prime (max_prime_factor n) \divides r).
85 rewrite < H4.
86 apply divides_max_prime_factor_n.
87 assumption.
88 change with (nth_prime (max_prime_factor n) \divides r \to False).
89 intro.
90 cut (r \mod (nth_prime (max_prime_factor n)) \neq O).
91 apply Hcut1.apply divides_to_mod_O.
92 apply lt_O_nth_prime_n.assumption.
93 apply (p_ord_aux_to_not_mod_O n n ? q r).
94 apply lt_SO_nth_prime_n.assumption.
95 apply le_n.
96 rewrite < H1.assumption.
97 apply (le_to_or_lt_eq (max_prime_factor r)  (max_prime_factor n)).
98 apply divides_to_max_prime_factor.
99 assumption.assumption.
100 apply (witness r n ((nth_prime p) \sup q)).
101 rewrite < sym_times.
102 apply (p_ord_aux_to_exp n n ? q r).
103 apply lt_O_nth_prime_n.assumption.
104 qed.
105
106 theorem p_ord_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to
107 max_prime_factor n \le p \to 
108 (pair nat nat q r) = p_ord n (nth_prime p) \to
109 (S O) < r \to max_prime_factor r < p.
110 intros.
111 cut (max_prime_factor n < p \lor max_prime_factor n = p).
112 elim Hcut.apply (le_to_lt_to_lt ? (max_prime_factor n)).
113 apply divides_to_max_prime_factor.assumption.assumption.
114 apply (witness r n ((nth_prime p) \sup q)).
115 rewrite > sym_times.
116 apply (p_ord_aux_to_exp n n).
117 apply lt_O_nth_prime_n.
118 assumption.assumption.
119 apply (p_ord_to_lt_max_prime_factor n ? q).
120 assumption.apply sym_eq.assumption.assumption.assumption.
121 apply (le_to_or_lt_eq ? p H1).
122 qed.
123
124 (* datatypes and functions *)
125
126 inductive nat_fact : Set \def
127     nf_last : nat \to nat_fact   
128   | nf_cons : nat \to nat_fact \to nat_fact.
129
130 inductive nat_fact_all : Set \def
131     nfa_zero : nat_fact_all
132   | nfa_one : nat_fact_all
133   | nfa_proper : nat_fact \to nat_fact_all.
134
135 let rec factorize_aux p n acc \def
136   match p with 
137   [ O \Rightarrow acc
138   | (S p1) \Rightarrow 
139     match p_ord n (nth_prime p1) with
140     [ (pair q r) \Rightarrow 
141       factorize_aux p1 r (nf_cons q acc)]].
142   
143 definition factorize : nat \to nat_fact_all \def \lambda n:nat.
144   match n with
145     [ O \Rightarrow nfa_zero
146     | (S n1) \Rightarrow
147       match n1 with
148       [ O \Rightarrow nfa_one
149     | (S n2) \Rightarrow 
150       let p \def (max (S(S n2)) (\lambda p:nat.eqb ((S(S n2)) \mod (nth_prime p)) O)) in
151       match p_ord (S(S n2)) (nth_prime p) with
152       [ (pair q r) \Rightarrow 
153            nfa_proper (factorize_aux p r (nf_last (pred q)))]]].
154            
155 let rec defactorize_aux f i \def
156   match f with
157   [ (nf_last n) \Rightarrow (nth_prime i) \sup (S n)
158   | (nf_cons n g) \Rightarrow 
159       (nth_prime i) \sup n *(defactorize_aux g (S i))].
160       
161 definition defactorize : nat_fact_all \to nat \def
162 \lambda f : nat_fact_all. 
163 match f with 
164 [ nfa_zero \Rightarrow O
165 | nfa_one \Rightarrow (S O)
166 | (nfa_proper g) \Rightarrow defactorize_aux g O]. 
167
168 theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat.
169 O < defactorize_aux f i.
170 intro.elim f.simplify.unfold lt. 
171 rewrite > times_n_SO.
172 apply le_times.
173 change with (O < nth_prime i).
174 apply lt_O_nth_prime_n.
175 change with (O < exp (nth_prime i) n).
176 apply lt_O_exp.
177 apply lt_O_nth_prime_n.
178 simplify.unfold lt.
179 rewrite > times_n_SO.
180 apply le_times.
181 change with (O < exp (nth_prime i) n).
182 apply lt_O_exp.
183 apply lt_O_nth_prime_n.
184 change with (O < defactorize_aux n1 (S i)).
185 apply H.
186 qed.
187
188 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
189 S O < defactorize_aux f i.
190 intro.elim f.simplify.unfold lt.
191 rewrite > times_n_SO.
192 apply le_times.
193 change with (S O < nth_prime i).
194 apply lt_SO_nth_prime_n.
195 change with (O < exp (nth_prime i) n).
196 apply lt_O_exp.
197 apply lt_O_nth_prime_n.
198 simplify.unfold lt.
199 rewrite > times_n_SO.
200 rewrite > sym_times.
201 apply le_times.
202 change with (O < exp (nth_prime i) n).
203 apply lt_O_exp.
204 apply lt_O_nth_prime_n.
205 change with (S O < defactorize_aux n1 (S i)).
206 apply H.
207 qed.
208
209 theorem defactorize_aux_factorize_aux : 
210 \forall p,n:nat.\forall acc:nat_fact.O < n \to
211 ((n=(S O) \land p=O) \lor max_prime_factor n < p) \to
212 defactorize_aux (factorize_aux p n acc) O = n*(defactorize_aux acc p).
213 intro.elim p.simplify.
214 elim H1.elim H2.rewrite > H3.
215 rewrite > sym_times. apply times_n_SO.
216 apply False_ind.apply (not_le_Sn_O (max_prime_factor n) H2).
217 simplify.
218 (* generalizing the goal: I guess there exists a better way *)
219 cut (\forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to
220 defactorize_aux match (p_ord_aux n1 n1 (nth_prime n)) with
221 [(pair q r)  \Rightarrow (factorize_aux n r (nf_cons q acc))] O =
222 n1*defactorize_aux acc (S n)).
223 apply (Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n)))
224 (snd ? ? (p_ord_aux n1 n1 (nth_prime n)))).
225 apply sym_eq.apply eq_pair_fst_snd.
226 intros.
227 rewrite < H3.
228 simplify.
229 cut (n1 = r * (nth_prime n) \sup q).
230 rewrite > H.
231 simplify.rewrite < assoc_times.
232 rewrite < Hcut.reflexivity.
233 cut (O < r \lor O = r).
234 elim Hcut1.assumption.absurd (n1 = O).
235 rewrite > Hcut.rewrite < H4.reflexivity.
236 unfold Not. intro.apply (not_le_Sn_O O).
237 rewrite < H5 in \vdash (? ? %).assumption.
238 apply le_to_or_lt_eq.apply le_O_n.
239 cut ((S O) < r \lor (S O) \nlt r).
240 elim Hcut1.
241 right.
242 apply (p_ord_to_lt_max_prime_factor1 n1 ? q r).
243 assumption.elim H2.
244 elim H5.
245 apply False_ind.
246 apply (not_eq_O_S n).apply sym_eq.assumption.
247 apply le_S_S_to_le.
248 exact H5.
249 assumption.assumption.
250 cut (r=(S O)).
251 apply (nat_case n).
252 left.split.assumption.reflexivity.
253 intro.right.rewrite > Hcut2.
254 simplify.unfold lt.apply le_S_S.apply le_O_n.
255 cut (r \lt (S O) \or r=(S O)).
256 elim Hcut2.absurd (O=r).
257 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
258 unfold Not.intro.
259 cut (O=n1).
260 apply (not_le_Sn_O O).
261 rewrite > Hcut3 in \vdash (? ? %).
262 assumption.rewrite > Hcut. 
263 rewrite < H6.reflexivity.
264 assumption.
265 apply (le_to_or_lt_eq r (S O)).
266 apply not_lt_to_le.assumption.
267 apply (decidable_lt (S O) r).
268 rewrite > sym_times.
269 apply (p_ord_aux_to_exp n1 n1).
270 apply lt_O_nth_prime_n.assumption.
271 qed.
272
273 theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
274 intro.
275 apply (nat_case n).reflexivity.
276 intro.apply (nat_case m).reflexivity.
277 intro.change with  
278 (let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
279 defactorize (match p_ord (S(S m1)) (nth_prime p) with
280 [ (pair q r) \Rightarrow 
281    nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
282 intro.
283 (* generalizing the goal; find a better way *)
284 cut (\forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to
285 defactorize (match p_ord (S(S m1)) (nth_prime p) with
286 [ (pair q r) \Rightarrow 
287    nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
288 apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
289 (snd ? ? (p_ord (S(S m1)) (nth_prime p)))).
290 apply sym_eq.apply eq_pair_fst_snd.
291 intros.
292 rewrite < H.
293 change with 
294 (defactorize_aux (factorize_aux p r (nf_last (pred q))) O = (S(S m1))).
295 cut ((S(S m1)) = (nth_prime p) \sup q *r).
296 cut (O<r).
297 rewrite > defactorize_aux_factorize_aux.
298 change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
299 cut ((S (pred q)) = q).
300 rewrite > Hcut2.
301 rewrite > sym_times.
302 apply sym_eq.
303 apply (p_ord_aux_to_exp (S(S m1))).
304 apply lt_O_nth_prime_n.
305 assumption.
306 (* O < q *)
307 apply sym_eq. apply S_pred.
308 cut (O < q \lor O = q).
309 elim Hcut2.assumption.
310 absurd (nth_prime p \divides S (S m1)).
311 apply (divides_max_prime_factor_n (S (S m1))).
312 unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
313 cut ((S(S m1)) = r).
314 rewrite > Hcut3 in \vdash (? (? ? %)).
315 change with (nth_prime p \divides r \to False).
316 intro.
317 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
318 apply lt_SO_nth_prime_n.
319 unfold lt.apply le_S_S.apply le_O_n.apply le_n.
320 assumption.
321 apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
322 rewrite > times_n_SO in \vdash (? ? ? %).
323 rewrite < sym_times.
324 rewrite > (exp_n_O (nth_prime p)).
325 rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
326 assumption.
327 apply le_to_or_lt_eq.apply le_O_n.assumption.
328 (* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
329 cut ((S O) < r \lor S O \nlt r).
330 elim Hcut2.
331 right. 
332 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
333 unfold lt.apply le_S_S. apply le_O_n.
334 apply le_n.
335 assumption.assumption.
336 cut (r=(S O)).
337 apply (nat_case p).
338 left.split.assumption.reflexivity.
339 intro.right.rewrite > Hcut3.
340 simplify.unfold lt.apply le_S_S.apply le_O_n.
341 cut (r \lt (S O) \or r=(S O)).
342 elim Hcut3.absurd (O=r).
343 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
344 unfold Not.intro.
345 apply (not_le_Sn_O O).
346 rewrite > H3 in \vdash (? ? %).assumption.assumption.
347 apply (le_to_or_lt_eq r (S O)).
348 apply not_lt_to_le.assumption.
349 apply (decidable_lt (S O) r).
350 (* O < r *)
351 cut (O < r \lor O = r).
352 elim Hcut1.assumption. 
353 apply False_ind.
354 apply (not_eq_O_S (S m1)).
355 rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
356 apply le_to_or_lt_eq.apply le_O_n.
357 (* prova del cut *)
358 goal 20.
359 apply (p_ord_aux_to_exp (S(S m1))).
360 apply lt_O_nth_prime_n.
361 assumption.
362 (* fine prova cut *)
363 qed.
364
365 let rec max_p f \def
366 match f with
367 [ (nf_last n) \Rightarrow O
368 | (nf_cons n g) \Rightarrow S (max_p g)].
369
370 let rec max_p_exponent f \def
371 match f with
372 [ (nf_last n) \Rightarrow n
373 | (nf_cons n g) \Rightarrow max_p_exponent g].
374
375 theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat. 
376 nth_prime ((max_p f)+i) \divides defactorize_aux f i.
377 intro.
378 elim f.simplify.apply (witness ? ? ((nth_prime i) \sup n)).
379 reflexivity.
380 change with 
381 (nth_prime (S(max_p n1)+i) \divides
382 (nth_prime i) \sup n *(defactorize_aux n1 (S i))).
383 elim (H (S i)).
384 rewrite > H1.
385 rewrite < sym_times.
386 rewrite > assoc_times.
387 rewrite < plus_n_Sm.
388 apply (witness ? ? (n2* (nth_prime i) \sup n)).
389 reflexivity.
390 qed.
391
392 theorem divides_exp_to_divides: 
393 \forall p,n,m:nat. prime p \to 
394 p \divides n \sup m \to p \divides n.
395 intros 3.elim m.simplify in H1.
396 apply (transitive_divides p (S O)).assumption.
397 apply divides_SO_n.
398 cut (p \divides n \lor p \divides n \sup n1).
399 elim Hcut.assumption.
400 apply H.assumption.assumption.
401 apply divides_times_to_divides.assumption.
402 exact H2.
403 qed.
404
405 theorem divides_exp_to_eq: 
406 \forall p,q,m:nat. prime p \to prime q \to
407 p \divides q \sup m \to p = q.
408 intros.
409 unfold prime in H1.
410 elim H1.apply H4.
411 apply (divides_exp_to_divides p q m).
412 assumption.assumption.
413 unfold prime in H.elim H.assumption.
414 qed.
415
416 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
417 i < j \to nth_prime i \ndivides defactorize_aux f j.
418 intro.elim f.
419 change with
420 (nth_prime i \divides (nth_prime j) \sup (S n) \to False).
421 intro.absurd ((nth_prime i) = (nth_prime j)).
422 apply (divides_exp_to_eq ? ? (S n)).
423 apply prime_nth_prime.apply prime_nth_prime.
424 assumption.
425 change with ((nth_prime i) = (nth_prime j) \to False).
426 intro.cut (i = j).
427 apply (not_le_Sn_n i).rewrite > Hcut in \vdash (? ? %).assumption.
428 apply (injective_nth_prime ? ? H2).
429 change with 
430 (nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False).
431 intro.
432 cut (nth_prime i \divides (nth_prime j) \sup n
433 \lor nth_prime i \divides defactorize_aux n1 (S j)).
434 elim Hcut.
435 absurd ((nth_prime i) = (nth_prime j)).
436 apply (divides_exp_to_eq ? ? n).
437 apply prime_nth_prime.apply prime_nth_prime.
438 assumption.
439 change with ((nth_prime i) = (nth_prime j) \to False).
440 intro.
441 cut (i = j).
442 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
443 apply (injective_nth_prime ? ? H4).
444 apply (H i (S j)).
445 apply (trans_lt ? j).assumption.unfold lt.apply le_n.
446 assumption.
447 apply divides_times_to_divides.
448 apply prime_nth_prime.assumption.
449 qed.
450
451 lemma not_eq_nf_last_nf_cons: \forall g:nat_fact.\forall n,m,i:nat.
452 \lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i).
453 intros.
454 change with 
455 (exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False).
456 intro.
457 cut (S(max_p g)+i= i).
458 apply (not_le_Sn_n i).
459 rewrite < Hcut in \vdash (? ? %).
460 simplify.apply le_S_S.
461 apply le_plus_n.
462 apply injective_nth_prime.
463 (* uffa, perche' semplifica ? *)
464 change with (nth_prime (S(max_p g)+i)= nth_prime i).
465 apply (divides_exp_to_eq ? ? (S n)).
466 apply prime_nth_prime.apply prime_nth_prime.
467 rewrite > H.
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.
471 qed.
472
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).
475 intros.
476 simplify.unfold Not.rewrite < plus_n_O.
477 intro.
478 apply (not_divides_defactorize_aux f i (S i) ?).
479 unfold lt.apply le_n.
480 rewrite > H.
481 rewrite > assoc_times.
482 apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
483 reflexivity.
484 qed.
485
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.
488 intro.
489 elim f.
490 generalize in match H.
491 elim g.
492 apply eq_f.
493 apply inj_S. apply (inj_exp_r (nth_prime i)).
494 apply lt_SO_nth_prime_n.
495 assumption.
496 apply False_ind.
497 apply (not_eq_nf_last_nf_cons n2 n n1 i H2).
498 generalize in match H1.
499 elim g.
500 apply False_ind.
501 apply (not_eq_nf_last_nf_cons n1 n2 n i).
502 apply sym_eq. assumption.
503 simplify in H3.
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)).
509 intro.
510 elim n4. apply eq_f.
511 apply (H n3 (S i)).
512 simplify in H4.
513 rewrite > plus_n_O.
514 rewrite > (plus_n_O (defactorize_aux n3 (S i))).assumption.
515 apply False_ind.
516 apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).assumption.
517 intros.
518 apply False_ind.
519 apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i).
520 apply sym_eq.assumption.
521 intros.
522 cut (nf_cons n4 n1 = nf_cons m n3).
523 cut (n4=m).
524 cut (n1=n3).
525 rewrite > Hcut1.rewrite > Hcut2.reflexivity.
526 change with 
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.
531 change with 
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.
540 qed.
541
542 theorem injective_defactorize_aux: \forall i:nat.
543 injective nat_fact nat (\lambda f.defactorize_aux f i).
544 change with (\forall i:nat.\forall f,g:nat_fact.
545 defactorize_aux f i = defactorize_aux g i \to f = g).
546 intros.
547 apply (eq_defactorize_aux_to_eq f g i H).
548 qed.
549
550 theorem injective_defactorize: 
551 injective nat_fact_all nat defactorize.
552 change with (\forall f,g:nat_fact_all.
553 defactorize f = defactorize g \to f = g).
554 intro.elim f.
555 generalize in match H.elim g.
556 (* zero - zero *)
557 reflexivity.
558 (* zero - one *)
559 simplify in H1.
560 apply False_ind.
561 apply (not_eq_O_S O H1).
562 (* zero - proper *)
563 simplify in H1.
564 apply False_ind.
565 apply (not_le_Sn_n O).
566 rewrite > H1 in \vdash (? ? %).
567 change with (O < defactorize_aux n O).
568 apply lt_O_defactorize_aux.
569 generalize in match H.
570 elim g.
571 (* one - zero *)
572 simplify in H1.
573 apply False_ind.
574 apply (not_eq_O_S O).apply sym_eq. assumption.
575 (* one - one *)
576 reflexivity.
577 (* one - proper *)
578 simplify in H1.
579 apply False_ind.
580 apply (not_le_Sn_n (S O)).
581 rewrite > H1 in \vdash (? ? %).
582 change with ((S O) < defactorize_aux n O).
583 apply lt_SO_defactorize_aux.
584 generalize in match H.elim g.
585 (* proper - zero *)
586 simplify in H1.
587 apply False_ind.
588 apply (not_le_Sn_n O).
589 rewrite < H1 in \vdash (? ? %).
590 change with (O < defactorize_aux n O).
591 apply lt_O_defactorize_aux.
592 (* proper - one *)
593 simplify in H1.
594 apply False_ind.
595 apply (not_le_Sn_n (S O)).
596 rewrite < H1 in \vdash (? ? %).
597 change with ((S O) < defactorize_aux n O).
598 apply lt_SO_defactorize_aux.
599 (* proper - proper *)
600 apply eq_f.
601 apply (injective_defactorize_aux O).
602 exact H1.
603 qed.
604
605 theorem factorize_defactorize: 
606 \forall f,g: nat_fact_all. factorize (defactorize f) = f.
607 intros.
608 apply injective_defactorize.
609 (* uffa: perche' semplifica ??? *)
610 change with (defactorize(factorize (defactorize f)) = (defactorize f)).
611 apply defactorize_factorize.
612 qed.
613