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 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/iteration2.ma".
17 include "nat/primes.ma".
20 let rec sigma_p n p (g:nat \to nat) \def
25 [true \Rightarrow (g k)+(sigma_p k p g)
26 |false \Rightarrow sigma_p k p g]
29 theorem true_to_sigma_p_Sn:
30 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
31 p n = true \to sigma_p (S n) p g =
32 (g n)+(sigma_p n p g).
34 rewrite > H.reflexivity.
37 theorem false_to_sigma_p_Sn:
38 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
39 p n = false \to sigma_p (S n) p g = sigma_p n p g.
41 rewrite > H.reflexivity.
44 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
45 \forall g1,g2: nat \to nat.\forall n.
46 (\forall x. x < n \to p1 x = p2 x) \to
47 (\forall x. x < n \to g1 x = g2 x) \to
48 sigma_p n p1 g1 = sigma_p n p2 g2.
51 |apply (bool_elim ? (p1 n1))
53 rewrite > (true_to_sigma_p_Sn ? ? ? H3).
54 rewrite > true_to_sigma_p_Sn
58 [intros.apply H1.apply le_S.assumption
59 |intros.apply H2.apply le_S.assumption
62 |rewrite < H3.apply sym_eq.apply H1.apply le_n
65 rewrite > (false_to_sigma_p_Sn ? ? ? H3).
66 rewrite > false_to_sigma_p_Sn
68 [intros.apply H1.apply le_S.assumption
69 |intros.apply H2.apply le_S.assumption
71 |rewrite < H3.apply sym_eq.apply H1.apply le_n
77 theorem sigma_p_false:
78 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
80 elim n[reflexivity|simplify.assumption]
83 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
84 \forall g: nat \to nat.
86 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
90 |apply (bool_elim ? (p (n1+n)))
92 simplify in \vdash (? ? (? % ? ?) ?).
93 rewrite > (true_to_sigma_p_Sn ? ? ? H1).
94 rewrite > (true_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1).
96 rewrite < H.reflexivity
98 simplify in \vdash (? ? (? % ? ?) ?).
99 rewrite > (false_to_sigma_p_Sn ? ? ? H1).
100 rewrite > (false_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1).
106 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
107 \forall p:nat \to bool.
108 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
109 p i = false) \to sigma_p m p g = sigma_p n p g.
118 apply H3[apply H4|apply le_S.assumption]
127 \forall p1,p2:nat \to bool.
128 \forall g: nat \to nat \to nat.
130 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
131 (\lambda x.g (div x m) (mod x m)) =
133 (\lambda x.sigma_p m p2 (g x)).
136 [simplify.reflexivity
137 |apply (bool_elim ? (p1 n1))
139 rewrite > (true_to_sigma_p_Sn ? ? ? H1).
140 simplify in \vdash (? ? (? % ? ?) ?);
141 rewrite > sigma_p_plus.
147 rewrite > (div_plus_times ? ? ? H2).
148 rewrite > (mod_plus_times ? ? ? H2).
153 rewrite > (div_plus_times ? ? ? H2).
154 rewrite > (mod_plus_times ? ? ? H2).
156 simplify.reflexivity.
161 rewrite > (false_to_sigma_p_Sn ? ? ? H1).
162 simplify in \vdash (? ? (? % ? ?) ?);
163 rewrite > sigma_p_plus.
165 apply (trans_eq ? ? (O+(sigma_p n1 p1 (\lambda x:nat.sigma_p m p2 (g x)))))
167 [rewrite > (eq_sigma_p ? (\lambda x.false) ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
171 rewrite > (div_plus_times ? ? ? H2).
172 rewrite > (mod_plus_times ? ? ? H2).
185 lemma sigma_p_gi: \forall g: nat \to nat.
186 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
187 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
191 apply (not_le_Sn_O i).
193 |apply (bool_elim ? (p n1));intro
194 [elim (le_to_or_lt_eq i n1)
195 [rewrite > true_to_sigma_p_Sn
196 [rewrite > true_to_sigma_p_Sn
197 [rewrite < assoc_plus.
198 rewrite < sym_plus in \vdash (? ? ? (? % ?)).
199 rewrite > assoc_plus.
202 |apply H[assumption|assumption]
204 |rewrite > H3.simplify.
205 change with (notb (eqb n1 i) = notb false).
207 apply not_eq_to_eqb_false.
209 apply (lt_to_not_eq ? ? H4).
210 apply sym_eq.assumption
214 |rewrite > true_to_sigma_p_Sn
218 |rewrite > false_to_sigma_p_Sn
223 change with (notb false = notb (eqb x n1)).
226 apply not_eq_to_eqb_false.
227 apply (lt_to_not_eq ? ? H5)
233 rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
239 |apply le_S_S_to_le.assumption
241 |rewrite > false_to_sigma_p_Sn
242 [elim (le_to_or_lt_eq i n1)
243 [rewrite > false_to_sigma_p_Sn
244 [apply H[assumption|assumption]
245 |rewrite > H3.reflexivity
248 apply not_eq_true_false.
252 |apply le_S_S_to_le.assumption
260 theorem eq_sigma_p_gh:
261 \forall g,h,h1: nat \to nat.\forall n,n1.
262 \forall p1,p2:nat \to bool.
263 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
264 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
265 (\forall i. i < n \to p1 i = true \to h i < n1) \to
266 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
267 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
268 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
269 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
272 [generalize in match H5.
275 |apply (bool_elim ? (p2 n2));intro
277 apply (not_le_Sn_O (h1 n2)).
279 [apply le_n|assumption]
280 |rewrite > false_to_sigma_p_Sn
283 apply H7[apply le_S.apply H9|assumption]
288 |apply (bool_elim ? (p1 n1));intro
289 [rewrite > true_to_sigma_p_Sn
290 [rewrite > (sigma_p_gi g n2 (h n1))
297 change with ((\not eqb (h i) (h n1))= \not false).
299 apply not_eq_to_eqb_false.
301 apply (lt_to_not_eq ? ? H8).
304 [apply eq_f.assumption|apply le_n|assumption]
305 |apply le_S.assumption
308 |apply le_S.assumption
312 apply H2[apply le_S.assumption|assumption]
314 apply H3[apply le_S.assumption|assumption]
318 |generalize in match H9.
320 [reflexivity|assumption]
325 |generalize in match H9.
327 [reflexivity|assumption]
330 elim (le_to_or_lt_eq (h1 j) n1)
332 |generalize in match H9.
338 [reflexivity|assumption|auto]
339 |apply eqb_false_to_not_eq.
340 generalize in match H11.
342 [apply sym_eq.assumption|reflexivity]
346 apply not_eq_true_false.
347 apply sym_eq.assumption
352 |generalize in match H9.
354 [reflexivity|assumption]
359 |apply H3[apply le_n|assumption]
360 |apply H1[apply le_n|assumption]
364 |rewrite > false_to_sigma_p_Sn
366 [intros.apply H1[apply le_S.assumption|assumption]
367 |intros.apply H2[apply le_S.assumption|assumption]
368 |intros.apply H3[apply le_S.assumption|assumption]
369 |intros.apply H4[assumption|assumption]
370 |intros.apply H5[assumption|assumption]
372 elim (le_to_or_lt_eq (h1 j) n1)
377 [reflexivity|assumption|assumption]
379 apply not_eq_true_false.
383 [reflexivity|assumption|assumption]
386 apply H6[assumption|assumption]
395 definition p_ord_times \def
398 [pair q r \Rightarrow r*m+q].
400 theorem eq_p_ord_times: \forall p,m,x.
401 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
402 intros.unfold p_ord_times. unfold ord_rem.
408 theorem div_p_ord_times:
409 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
410 intros.rewrite > eq_p_ord_times.
411 apply div_plus_times.
415 theorem mod_p_ord_times:
416 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
417 intros.rewrite > eq_p_ord_times.
418 apply mod_plus_times.
422 theorem sigma_p_divides:
423 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
424 \forall g: nat \to nat.
425 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
426 sigma_p (S n) (\lambda x.divides_b x n)
427 (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
432 (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n)
433 (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))))
435 apply (eq_sigma_p_gh g ? (p_ord_times p (S m)))
437 lapply (divides_b_true_to_lt_O ? ? H H4).
438 apply divides_to_divides_b_true
439 [rewrite > (times_n_O O).
442 |apply lt_O_exp.assumption
445 [apply divides_b_true_to_divides.assumption
446 |apply (witness ? ? (p \sup (m-i \mod (S m)))).
447 rewrite < exp_plus_times.
450 apply plus_minus_m_m.
455 lapply (divides_b_true_to_lt_O ? ? H H4).
457 rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
458 [change with ((i/S m)*S m+i \mod S m=i).
465 apply (trans_divides ? (i/ S m))
467 apply divides_b_true_to_divides;assumption]
474 change with ((i/S m) < S n).
475 apply (lt_times_to_lt_l m).
476 apply (le_to_lt_to_lt ? i)
487 [rewrite > div_p_ord_times
488 [apply divides_to_divides_b_true
491 |apply (divides_b_true_to_lt_O ? ? ? H4).
492 rewrite > (times_n_O O).
494 [assumption|apply lt_O_exp.assumption]
496 |cut (n = ord_rem (n*(exp p m)) p)
498 apply divides_to_divides_ord_rem
499 [apply (divides_b_true_to_lt_O ? ? ? H4).
500 rewrite > (times_n_O O).
502 [assumption|apply lt_O_exp.assumption]
503 |rewrite > (times_n_O O).
505 [assumption|apply lt_O_exp.assumption]
507 |apply divides_b_true_to_divides.
511 rewrite > (p_ord_exp1 p ? m n)
521 |cut (m = ord (n*(exp p m)) p)
524 apply divides_to_le_ord
525 [apply (divides_b_true_to_lt_O ? ? ? H4).
526 rewrite > (times_n_O O).
528 [assumption|apply lt_O_exp.assumption]
529 |rewrite > (times_n_O O).
531 [assumption|apply lt_O_exp.assumption]
533 |apply divides_b_true_to_divides.
537 rewrite > (p_ord_exp1 p ? m n)
547 [rewrite > div_p_ord_times
548 [rewrite > mod_p_ord_times
549 [rewrite > sym_times.
553 |apply (divides_b_true_to_lt_O ? ? ? H4).
554 rewrite > (times_n_O O).
556 [assumption|apply lt_O_exp.assumption]
558 |cut (m = ord (n*(exp p m)) p)
561 apply divides_to_le_ord
562 [apply (divides_b_true_to_lt_O ? ? ? H4).
563 rewrite > (times_n_O O).
565 [assumption|apply lt_O_exp.assumption]
566 |rewrite > (times_n_O O).
568 [assumption|apply lt_O_exp.assumption]
570 |apply divides_b_true_to_divides.
574 rewrite > (p_ord_exp1 p ? m n)
584 |cut (m = ord (n*(exp p m)) p)
587 apply divides_to_le_ord
588 [apply (divides_b_true_to_lt_O ? ? ? H4).
589 rewrite > (times_n_O O).
591 [assumption|apply lt_O_exp.assumption]
592 |rewrite > (times_n_O O).
594 [assumption|apply lt_O_exp.assumption]
596 |apply divides_b_true_to_divides.
600 rewrite > (p_ord_exp1 p ? m n)
609 rewrite > eq_p_ord_times.
611 apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
614 cut (m = ord (n*(p \sup m)) p)
616 apply divides_to_le_ord
617 [apply (divides_b_true_to_lt_O ? ? ? H4).
618 rewrite > (times_n_O O).
620 [assumption|apply lt_O_exp.assumption]
621 |rewrite > (times_n_O O).
623 [assumption|apply lt_O_exp.assumption]
625 |apply divides_b_true_to_divides.
630 rewrite > (p_ord_exp1 p ? m n)
637 |change with (S (ord_rem j p)*S m \le S n*S m).
640 cut (n = ord_rem (n*(p \sup m)) p)
645 |rewrite > (times_n_O O).
647 [assumption|apply lt_O_exp.assumption]
649 |apply divides_to_divides_ord_rem
650 [apply (divides_b_true_to_lt_O ? ? ? H4).
651 rewrite > (times_n_O O).
653 [assumption|apply lt_O_exp.assumption]
654 |rewrite > (times_n_O O).
656 [assumption|apply lt_O_exp.assumption]
658 |apply divides_b_true_to_divides.
664 rewrite > (p_ord_exp1 p ? m n)
675 elim (divides_b (x/S m) n);reflexivity
679 |elim H1.apply lt_to_le.assumption