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/library_autobatch/nat/primes".
17 include "auto/nat/div_and_mod.ma".
18 include "auto/nat/minimization.ma".
19 include "auto/nat/sigma_and_pi.ma".
20 include "auto/nat/factorial.ma".
22 inductive divides (n,m:nat) : Prop \def
23 witness : \forall p:nat.m = times n p \to divides n m.
25 interpretation "divides" 'divides n m = (divides n m).
26 interpretation "not divides" 'ndivides n m = (Not (divides n m)).
28 theorem reflexive_divides : reflexive nat divides.
31 exact (witness x x (S O) (times_n_SO x)).
34 theorem divides_to_div_mod_spec :
35 \forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O.
41 | apply (lt_O_n_elim n H).
50 theorem div_mod_spec_to_divides :
51 \forall n,m,p. div_mod_spec m n p O \to n \divides m.
55 (*apply (witness n m p).
57 rewrite > (plus_n_O (p*n)).
61 theorem divides_to_mod_O:
62 \forall n,m. O < n \to n \divides m \to (m \mod n) = O.
64 apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O)
66 (*apply div_mod_spec_div_mod.
69 (*apply divides_to_div_mod_spec;assumption*)
73 theorem mod_O_to_divides:
74 \forall n,m. O< n \to (m \mod n) = O \to n \divides m.
76 apply (witness n m (m / n)).
77 rewrite > (plus_n_O (n * (m / n))).
81 (* Andrea: perche' hint non lo trova ?*)
86 theorem divides_n_O: \forall n:nat. n \divides O.
89 (*apply (witness n O O).
93 theorem divides_n_n: \forall n:nat. n \divides n.
96 apply (witness n n (S O)).
100 theorem divides_SO_n: \forall n:nat. (S O) \divides n.
103 (*apply (witness (S O) n n).
108 theorem divides_plus: \forall n,p,q:nat.
109 n \divides p \to n \divides q \to n \divides p+q.
113 apply (witness n (p+q) (n2+n1)).
118 apply distr_times_plus.*)
121 theorem divides_minus: \forall n,p,q:nat.
122 divides n p \to divides n q \to divides n (p-q).
126 apply (witness n (p-q) (n2-n1)).
131 apply distr_times_minus.*)
134 theorem divides_times: \forall n,m,p,q:nat.
135 n \divides p \to m \divides q \to n*m \divides p*q.
139 apply (witness (n*m) (p*q) (n2*n1)).
142 apply (trans_eq nat ? (n*(m*(n2*n1))))
143 [ apply (trans_eq nat ? (n*(n2*(m*n1))))
146 apply (trans_eq nat ? ((n2*m)*n1))
150 | rewrite > (sym_times n2 m).
160 theorem transitive_divides: transitive ? divides.
165 apply (witness x z (n2*n)).
172 variant trans_divides: \forall n,m,p.
173 n \divides m \to m \divides p \to n \divides p \def transitive_divides.
175 theorem eq_mod_to_divides:\forall n,m,p. O< p \to
176 mod n p = mod m p \to divides p (n-m).
178 cut (n \le m \or \not n \le m)
183 apply (witness p O O).
186 (*apply eq_minus_n_m_O.
189 | apply (witness p (n-m) ((div n p)-(div m p))).
190 rewrite > distr_times_minus.
192 rewrite > (sym_times p).
193 cut ((div n p)*p = n - (mod n p))
195 rewrite > eq_minus_minus_minus_plus.
211 | apply (decidable_le n m)
215 theorem antisymmetric_divides: antisymmetric nat divides.
216 unfold antisymmetric.
234 (*rewrite < times_n_O.
237 apply antisymmetric_le
239 rewrite > times_n_SO in \vdash (? % ?).
246 rewrite > times_n_SO in \vdash (? % ?).
258 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
263 [ apply (lt_O_n_elim n2 Hcut).
266 (*rewrite < sym_times.
270 | elim (le_to_or_lt_eq O n2)
277 apply (not_le_Sn_n O)
284 theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n.
287 elim (le_to_or_lt_eq O n (le_O_n n))
296 exact (not_le_Sn_n O)*)
301 (* boolean divides *)
302 definition divides_b : nat \to nat \to bool \def
303 \lambda n,m :nat. (eqb (m \mod n) O).
305 theorem divides_b_to_Prop :
306 \forall n,m:nat. O < n \to
307 match divides_b n m with
308 [ true \Rightarrow n \divides m
309 | false \Rightarrow n \ndivides m].
316 (*apply mod_O_to_divides;assumption*)
323 apply divides_to_mod_O;assumption*)
327 theorem divides_b_true_to_divides :
328 \forall n,m:nat. O < n \to
329 (divides_b n m = true ) \to n \divides m.
333 [ true \Rightarrow n \divides m
334 | false \Rightarrow n \ndivides m].
336 apply divides_b_to_Prop.
340 theorem divides_b_false_to_not_divides :
341 \forall n,m:nat. O < n \to
342 (divides_b n m = false ) \to n \ndivides m.
346 [ true \Rightarrow n \divides m
347 | false \Rightarrow n \ndivides m].
349 apply divides_b_to_Prop.
353 theorem decidable_divides: \forall n,m:nat.O < n \to
354 decidable (n \divides m).
358 (match divides_b n m with
359 [ true \Rightarrow n \divides m
360 | false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m)
362 apply divides_b_to_Prop.
364 | elim (divides_b n m)
366 (*qui autobatch non chiude il goal, chiuso dalla sola apply H1*)
369 (*qui autobatch non chiude il goal, chiuso dalla sola apply H1*)
375 theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
376 n \divides m \to divides_b n m = true.
378 cut (match (divides_b n m) with
379 [ true \Rightarrow n \divides m
380 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = true))
382 apply divides_b_to_Prop.
384 | elim (divides_b n m)
386 | absurd (n \divides m)
388 | (*qui autobatch non chiude il goal, chiuso dalla sola applicazione di assumption*)
395 theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
396 \lnot(n \divides m) \to (divides_b n m) = false.
398 cut (match (divides_b n m) with
399 [ true \Rightarrow n \divides m
400 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = false))
402 apply divides_b_to_Prop.
404 | elim (divides_b n m)
405 [ absurd (n \divides m)
406 [ (*qui autobatch non chiude il goal, chiuso dalla sola tattica assumption*)
416 theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat.
417 m \le i \to i \le n+m \to f i \divides pi n f m.
425 | apply antisymmetric_le
431 cut (i < S n1+m \lor i = S n1 + m)
433 [ apply (transitive_divides ? (pi n1 f m))
436 (*apply le_S_S_to_le.
439 (*apply (witness ? ? (f (S n1+m))).
444 apply (witness ? ? (pi n1 f m)).
448 (*apply le_to_or_lt_eq.
455 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat.
456 i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
457 intros.cut (pi n f) \mod (f i) = O.
459 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
460 rewrite > Hcut.assumption.
461 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
462 apply divides_f_pi_f.assumption.
466 (* divides and fact *)
467 theorem divides_fact : \forall n,i:nat.
468 O < i \to i \le n \to i \divides n!.
474 (*apply (le_n_O_elim i H1).
475 apply (not_le_Sn_O O)*)
477 | change with (i \divides (S n1)*n1!).
478 apply (le_n_Sm_elim i n1 H2)
480 apply (transitive_divides ? n1!)
486 (*apply (witness ? ? (S n1)).
492 apply (witness ? ? n1!).
498 theorem mod_S_fact: \forall n,i:nat.
499 (S O) < i \to i \le n \to (S n!) \mod i = (S O).
505 (*apply (trans_lt O (S O))
513 apply divides_to_mod_O
514 [ apply ltn_to_ltO [| apply H]
516 [ apply ltn_to_ltO [| apply H]
523 theorem not_divides_S_fact: \forall n,i:nat.
524 (S O) < i \to i \le n \to i \ndivides S n!.
526 apply divides_b_false_to_not_divides
528 (*apply (trans_lt O (S O))
533 rewrite > mod_S_fact;autobatch
543 definition prime : nat \to Prop \def
544 \lambda n:nat. (S O) < n \land
545 (\forall m:nat. m \divides n \to (S O) < m \to m = n).
547 theorem not_prime_O: \lnot (prime O).
552 apply (not_le_Sn_O (S O) H1).
555 theorem not_prime_SO: \lnot (prime (S O)).
560 apply (not_le_Sn_n (S O) H1).
563 (* smallest factor *)
564 definition smallest_factor : nat \to nat \def
570 [ O \Rightarrow (S O)
571 | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
574 theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
575 normalize.reflexivity.
578 theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)).
579 normalize.reflexivity.
582 theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
583 simplify.reflexivity.
586 theorem lt_SO_smallest_factor:
587 \forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
593 apply (not_le_Sn_O (S O) H)*)
597 (*intro. apply False_ind.
598 apply (not_le_Sn_n (S O) H)*)
601 (S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
602 apply (lt_to_le_to_lt ? (S (S O)))
603 [ apply (le_n (S(S O)))
604 | cut ((S(S O)) = (S(S m1)) - m1)
610 (*rewrite < sym_plus.
619 theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
625 apply (not_le_Sn_n O H)*)
634 apply (trans_lt ? (S O))
638 | apply lt_SO_smallest_factor.
648 theorem divides_smallest_factor_n :
649 \forall n:nat. O < n \to smallest_factor n \divides n.
655 apply (not_le_Sn_O O H)*)
661 apply (witness ? ? (S O)).
665 apply divides_b_true_to_divides
666 [ apply (lt_O_smallest_factor ? H)
668 (eqb ((S(S m1)) \mod (min_aux m1 (S(S m1))
669 (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
670 apply f_min_aux_true.
671 apply (ex_intro nat ? (S(S m1))).
681 | apply (trans_lt ? (S O))
695 theorem le_smallest_factor_n :
696 \forall n:nat. smallest_factor n \le n.
712 | apply divides_smallest_factor_n.
721 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
722 (S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
727 apply (not_le_Sn_O (S O) H)
732 apply (not_le_Sn_n (S O) H)
734 apply divides_b_false_to_not_divides
736 (*apply (trans_lt O (S O))
741 apply (lt_min_aux_to_false
742 (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i)
743 [ cut ((S(S O)) = (S(S m1)-m1))
749 (*rewrite < sym_plus.
760 theorem prime_smallest_factor_n :
761 \forall n:nat. (S O) < n \to prime (smallest_factor n).
763 change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land
764 (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n))).
767 [ apply lt_SO_smallest_factor.
770 cut (le m (smallest_factor n))
771 [ elim (le_to_or_lt_eq m (smallest_factor n) Hcut)
772 [ absurd (m \divides n)
773 [ apply (transitive_divides m (smallest_factor n))
775 | apply divides_smallest_factor_n.
777 (*apply (trans_lt ? (S O))
783 | apply lt_smallest_factor_to_not_divides;autobatch
791 | apply divides_to_le
792 [ apply (trans_lt O (S O))
794 | apply lt_SO_smallest_factor.
803 theorem prime_to_smallest_factor: \forall n. prime n \to
804 smallest_factor n = n.
810 apply (not_prime_O H)*)
816 apply (not_prime_SO H)*)
819 ((S O) < (S(S m1)) \land
820 (\forall m:nat. m \divides S(S m1) \to (S O) < m \to m = (S(S m1))) \to
821 smallest_factor (S(S m1)) = (S(S m1))).
826 [ apply divides_smallest_factor_n.
827 apply (trans_lt ? (S O))
832 | apply lt_SO_smallest_factor.
839 (* a number n > O is prime iff its smallest factor is n *)
840 definition primeb \def \lambda n:nat.
842 [ O \Rightarrow false
845 [ O \Rightarrow false
846 | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]].
849 theorem example4 : primeb (S(S(S O))) = true.
850 normalize.reflexivity.
853 theorem example5 : primeb (S(S(S(S(S(S O)))))) = false.
854 normalize.reflexivity.
857 theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true.
858 normalize.reflexivity.
861 theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true.
862 normalize.reflexivity.
865 theorem primeb_to_Prop: \forall n.
867 [ true \Rightarrow prime n
868 | false \Rightarrow \lnot (prime n)].
877 apply (not_le_Sn_O (S O) H1)*)
886 apply (not_le_Sn_n (S O) H1)*)
889 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
890 [ true \Rightarrow prime (S(S m1))
891 | false \Rightarrow \lnot (prime (S(S m1)))].
892 apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1)))
896 apply prime_smallest_factor_n.
903 change with (prime (S(S m1)) \to False).
907 apply prime_to_smallest_factor.
914 theorem primeb_true_to_prime : \forall n:nat.
915 primeb n = true \to prime n.
919 [ true \Rightarrow prime n
920 | false \Rightarrow \lnot (prime n)].
922 (*qui autobatch non chiude il goal*)
923 apply primeb_to_Prop.
926 theorem primeb_false_to_not_prime : \forall n:nat.
927 primeb n = false \to \lnot (prime n).
931 [ true \Rightarrow prime n
932 | false \Rightarrow \lnot (prime n)].
934 (*qui autobatch non chiude il goal*)
935 apply primeb_to_Prop.
938 theorem decidable_prime : \forall n:nat.decidable (prime n).
943 [ true \Rightarrow prime n
944 | false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n))
946 (*qui autobatch non chiude il goal*)
950 (*qui autobatch non chiude il goal*)
953 (*qui autobatch non chiude il goal*)
959 theorem prime_to_primeb_true: \forall n:nat.
960 prime n \to primeb n = true.
962 cut (match (primeb n) with
963 [ true \Rightarrow prime n
964 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = true))
966 (*qui autobatch non chiude il goal*)
972 | (*qui autobatch non chiude il goal*)
979 theorem not_prime_to_primeb_false: \forall n:nat.
980 \lnot(prime n) \to primeb n = false.
982 cut (match (primeb n) with
983 [ true \Rightarrow prime n
984 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = false))
986 (*qui autobatch non chiude il goal*)
990 [ (*qui autobatch non chiude il goal*)