]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/primes.ma
exercises ready
[helm.git] / helm / software / matita / library / nat / primes.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/div_and_mod.ma".
16 include "nat/minimization.ma".
17 include "nat/sigma_and_pi.ma".
18 include "nat/factorial.ma".
19
20 inductive divides (n,m:nat) : Prop \def
21 witness : \forall p:nat.m = times n p \to divides n m.
22
23 interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m).
24 interpretation "not divides" 'ndivides n m =
25  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
26
27 theorem reflexive_divides : reflexive nat divides.
28 unfold reflexive.
29 intros.
30 exact (witness x x (S O) (times_n_SO x)).
31 qed.
32
33 theorem divides_to_div_mod_spec :
34 \forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O.
35 intros.elim H1.rewrite > H2.
36 constructor 1.assumption.
37 apply (lt_O_n_elim n H).intros.
38 rewrite < plus_n_O.
39 rewrite > div_times.apply sym_times.
40 qed.
41
42 theorem div_mod_spec_to_divides :
43 \forall n,m,p. div_mod_spec m n p O \to n \divides m.
44 intros.elim H.
45 apply (witness n m p).
46 rewrite < sym_times.
47 rewrite > (plus_n_O (p*n)).assumption.
48 qed.
49
50 theorem divides_to_mod_O:
51 \forall n,m. O < n \to n \divides m \to (m \mod n) = O.
52 intros.apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O).
53 apply div_mod_spec_div_mod.assumption.
54 apply divides_to_div_mod_spec.assumption.assumption.
55 qed.
56
57 theorem mod_O_to_divides:
58 \forall n,m. O< n \to (m \mod n) = O \to  n \divides m.
59 intros.
60 apply (witness n m (m / n)).
61 rewrite > (plus_n_O (n * (m / n))).
62 rewrite < H1.
63 rewrite < sym_times.
64 (* Andrea: perche' hint non lo trova ?*)
65 apply div_mod.
66 assumption.
67 qed.
68
69 theorem divides_n_O: \forall n:nat. n \divides O.
70 intro. apply (witness n O O).apply times_n_O.
71 qed.
72
73 theorem divides_n_n: \forall n:nat. n \divides n.
74 intro. apply (witness n n (S O)).apply times_n_SO.
75 qed.
76
77 theorem divides_SO_n: \forall n:nat. (S O) \divides n.
78 intro. apply (witness (S O) n n). simplify.apply plus_n_O.
79 qed.
80
81 theorem divides_plus: \forall n,p,q:nat. 
82 n \divides p \to n \divides q \to n \divides p+q.
83 intros.
84 elim H.elim H1. apply (witness n (p+q) (n1+n2)).
85 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
86 qed.
87
88 theorem divides_minus: \forall n,p,q:nat. 
89 divides n p \to divides n q \to divides n (p-q).
90 intros.
91 elim H.elim H1. apply (witness n (p-q) (n1-n2)).
92 rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
93 qed.
94
95 theorem divides_times: \forall n,m,p,q:nat. 
96 n \divides p \to m \divides q \to n*m \divides p*q.
97 intros.
98 elim H.elim H1. apply (witness (n*m) (p*q) (n1*n2)).
99 rewrite > H2.rewrite > H3.
100 apply (trans_eq nat ? (n*(m*(n1*n2)))).
101 apply (trans_eq nat ? (n*(n1*(m*n2)))).
102 apply assoc_times.
103 apply eq_f.
104 apply (trans_eq nat ? ((n1*m)*n2)).
105 apply sym_eq. apply assoc_times.
106 rewrite > (sym_times n1 m).apply assoc_times.
107 apply sym_eq. apply assoc_times.
108 qed.
109
110 theorem transitive_divides: transitive ? divides.
111 unfold.
112 intros.
113 elim H.elim H1. apply (witness x z (n1*n)).
114 rewrite > H3.rewrite > H2.
115 apply assoc_times.
116 qed.
117
118 variant trans_divides: \forall n,m,p. 
119  n \divides m \to m \divides p \to n \divides p \def transitive_divides.
120
121 theorem eq_mod_to_divides:\forall n,m,p. O< p \to
122 mod n p = mod m p \to divides p (n-m).
123 intros.
124 cut (n \le m \or \not n \le m).
125 elim Hcut.
126 cut (n-m=O).
127 rewrite > Hcut1.
128 apply (witness p O O).
129 apply times_n_O.
130 apply eq_minus_n_m_O.
131 assumption.
132 apply (witness p (n-m) ((div n p)-(div m p))).
133 rewrite > distr_times_minus.
134 rewrite > sym_times.
135 rewrite > (sym_times p).
136 cut ((div n p)*p = n - (mod n p)).
137 rewrite > Hcut1.
138 rewrite > eq_minus_minus_minus_plus.
139 rewrite > sym_plus.
140 rewrite > H1.
141 rewrite < div_mod.reflexivity.
142 assumption.
143 apply sym_eq.
144 apply plus_to_minus.
145 rewrite > sym_plus.
146 apply div_mod.
147 assumption.
148 apply (decidable_le n m).
149 qed.
150
151 theorem antisymmetric_divides: antisymmetric nat divides.
152 unfold antisymmetric.intros.elim H. elim H1.
153 apply (nat_case1 n1).intro.
154 rewrite > H3.rewrite > H2.rewrite > H4.
155 rewrite < times_n_O.reflexivity.
156 intros.
157 apply (nat_case1 n).intro.
158 rewrite > H2.rewrite > H3.rewrite > H5.
159 rewrite < times_n_O.reflexivity.
160 intros.
161 apply antisymmetric_le.
162 rewrite > H2.rewrite > times_n_SO in \vdash (? % ?).
163 apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n.
164 rewrite > H3.rewrite > times_n_SO in \vdash (? % ?).
165 apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n.
166 qed.
167
168 (* divides le *)
169 theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
170 intros. elim H1.rewrite > H2.cut (O < n1).
171 apply (lt_O_n_elim n1 Hcut).intro.rewrite < sym_times.
172 simplify.rewrite < sym_plus.
173 apply le_plus_n.
174 elim (le_to_or_lt_eq O n1).
175 assumption.
176 absurd (O<m).assumption.
177 rewrite > H2.rewrite < H3.rewrite < times_n_O.
178 apply (not_le_Sn_n O).
179 apply le_O_n.
180 qed.
181
182 theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n.
183 intros.elim H1.
184 elim (le_to_or_lt_eq O n (le_O_n n)).
185 assumption.
186 rewrite < H3.absurd (O < m).assumption.
187 rewrite > H2.rewrite < H3.
188 simplify.exact (not_le_Sn_n O).
189 qed.
190
191 (*a variant of or_div_mod *)
192 theorem or_div_mod1: \forall n,q. O < q \to
193 (divides q (S n)) \land S n = (S (div n q)) * q \lor
194 (\lnot (divides q (S n)) \land S n= (div n q) * q + S (n\mod q)).
195 intros.elim (or_div_mod n q H);elim H1
196   [left.split
197     [apply (witness ? ? (S (n/q))).
198      rewrite > sym_times.assumption
199     |assumption
200     ]
201   |right.split
202     [intro.
203      apply (not_eq_O_S (n \mod q)).
204      (* come faccio a fare unfold nelleipotesi ? *)
205      cut ((S n) \mod q = O)
206       [rewrite < Hcut.
207        apply (div_mod_spec_to_eq2 (S n) q (div (S n) q) (mod (S n) q) (div n q) (S (mod n q)))
208         [apply div_mod_spec_div_mod.
209          assumption
210         |apply div_mod_spec_intro;assumption
211         ]
212       |apply divides_to_mod_O;assumption
213       ]
214     |assumption
215     ]
216   ]
217 qed.
218
219 theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
220 intro.
221 elim (le_to_or_lt_eq O n (le_O_n n))
222   [rewrite > plus_n_O.
223    rewrite < (divides_to_mod_O ? ? H H1).
224    apply sym_eq.
225    apply div_mod.
226    assumption
227   |elim H1.
228    generalize in match H2.
229    rewrite < H.
230    simplify.
231    intro.
232    rewrite > H3.
233    reflexivity
234   ]
235 qed.
236
237 theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
238 intros.
239 apply (witness ? ? d).
240 apply sym_eq.
241 apply divides_to_div.
242 assumption.
243 qed.
244
245 theorem div_div: \forall n,d:nat. O < n \to divides d n \to 
246 n/(n/d) = d.
247 intros.
248 apply (inj_times_l1 (n/d))
249   [apply (lt_times_n_to_lt d)
250     [apply (divides_to_lt_O ? ? H H1).
251     |rewrite > divides_to_div;assumption
252     ]
253   |rewrite > divides_to_div
254     [rewrite > sym_times.
255      rewrite > divides_to_div
256       [reflexivity
257       |assumption
258       ]
259     |apply (witness ? ? d).
260      apply sym_eq.
261      apply divides_to_div.
262      assumption
263     ]
264   ]
265 qed.
266
267 theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat.
268 O \lt b \to c \divides b \to a * (b /c) = (a*b)/c.
269 intros.
270 elim H1.
271 rewrite > H2.
272 rewrite > (sym_times c n1).
273 cut(O \lt c)
274 [ rewrite > (lt_O_to_div_times n1 c)
275   [ rewrite < assoc_times.
276     rewrite > (lt_O_to_div_times (a *n1) c)
277     [ reflexivity
278     | assumption
279     ]
280   | assumption
281   ]  
282 | apply (divides_to_lt_O c b);
283     assumption.
284 ]
285 qed.
286
287 theorem eq_div_plus: \forall n,m,d. O < d \to
288 divides d n \to divides d m \to
289 (n + m ) / d = n/d + m/d.
290 intros.
291 elim H1.
292 elim H2.
293 rewrite > H3.rewrite > H4.
294 rewrite < distr_times_plus.
295 rewrite > sym_times.
296 rewrite > sym_times in âŠ¢ (? ? ? (? (? % ?) ?)).
297 rewrite > sym_times in âŠ¢ (? ? ? (? ? (? % ?))).
298 rewrite > lt_O_to_div_times
299   [rewrite > lt_O_to_div_times
300     [rewrite > lt_O_to_div_times
301       [reflexivity
302       |assumption
303       ]
304     |assumption
305     ]
306   |assumption
307   ]
308 qed.
309
310 (* boolean divides *)
311 definition divides_b : nat \to nat \to bool \def
312 \lambda n,m :nat. (eqb (m \mod n) O).
313
314 theorem divides_b_to_Prop :
315 \forall n,m:nat. O < n \to
316 match divides_b n m with
317 [ true \Rightarrow n \divides m
318 | false \Rightarrow n \ndivides m].
319 intros.unfold divides_b.
320 apply eqb_elim.
321 intro.simplify.apply mod_O_to_divides.assumption.assumption.
322 intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
323 qed.
324
325 theorem divides_b_true_to_divides1:
326 \forall n,m:nat. O < n \to
327 (divides_b n m = true ) \to n \divides m.
328 intros.
329 change with 
330 match true with
331 [ true \Rightarrow n \divides m
332 | false \Rightarrow n \ndivides m].
333 rewrite < H1.apply divides_b_to_Prop.
334 assumption.
335 qed.
336
337 theorem divides_b_true_to_divides:
338 \forall n,m:nat. divides_b n m = true \to n \divides m.
339 intros 2.apply (nat_case n)
340   [apply (nat_case m)
341     [intro.apply divides_n_n
342     |simplify.intros.apply False_ind.
343      apply not_eq_true_false.apply sym_eq.
344      assumption
345     ]
346   |intros.
347    apply divides_b_true_to_divides1
348     [apply lt_O_S|assumption]
349   ]
350 qed.
351
352 theorem divides_b_false_to_not_divides1:
353 \forall n,m:nat. O < n \to
354 (divides_b n m = false ) \to n \ndivides m.
355 intros.
356 change with 
357 match false with
358 [ true \Rightarrow n \divides m
359 | false \Rightarrow n \ndivides m].
360 rewrite < H1.apply divides_b_to_Prop.
361 assumption.
362 qed.
363
364 theorem divides_b_false_to_not_divides:
365 \forall n,m:nat. divides_b n m = false \to n \ndivides m.
366 intros 2.apply (nat_case n)
367   [apply (nat_case m)
368     [simplify.unfold Not.intros.
369      apply not_eq_true_false.assumption
370     |unfold Not.intros.elim H1.
371      apply (not_eq_O_S m1).apply sym_eq.
372      assumption
373     ]
374   |intros.
375    apply divides_b_false_to_not_divides1
376     [apply lt_O_S|assumption]
377   ]
378 qed.
379
380 theorem decidable_divides: \forall n,m:nat.O < n \to
381 decidable (n \divides m).
382 intros.unfold decidable.
383 cut 
384 (match divides_b n m with
385 [ true \Rightarrow n \divides m
386 | false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m).
387 apply Hcut.apply divides_b_to_Prop.assumption.
388 elim (divides_b n m).left.apply H1.right.apply H1.
389 qed.
390
391 theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
392 n \divides m \to divides_b n m = true.
393 intros.
394 cut (match (divides_b n m) with
395 [ true \Rightarrow n \divides m
396 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = true)).
397 apply Hcut.apply divides_b_to_Prop.assumption.
398 elim (divides_b n m).reflexivity.
399 absurd (n \divides m).assumption.assumption.
400 qed.
401
402 theorem divides_to_divides_b_true1 : \forall n,m:nat.
403 O < m \to n \divides m \to divides_b n m = true.
404 intro.
405 elim (le_to_or_lt_eq O n (le_O_n n))
406   [apply divides_to_divides_b_true
407     [assumption|assumption]
408   |apply False_ind.
409    rewrite < H in H2.
410    elim H2.
411    simplify in H3.
412    apply (not_le_Sn_O O).
413    rewrite > H3 in H1.
414    assumption
415   ]
416 qed.
417
418 theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
419 \lnot(n \divides m) \to (divides_b n m) = false.
420 intros.
421 cut (match (divides_b n m) with
422 [ true \Rightarrow n \divides m
423 | false \Rightarrow n \ndivides m] \to ((divides_b n m) = false)).
424 apply Hcut.apply divides_b_to_Prop.assumption.
425 elim (divides_b n m).
426 absurd (n \divides m).assumption.assumption.
427 reflexivity.
428 qed.
429
430 theorem divides_b_div_true: 
431 \forall d,n. O < n \to 
432   divides_b d n = true \to divides_b (n/d) n = true.
433 intros.
434 apply divides_to_divides_b_true1
435   [assumption
436   |apply divides_div.
437    apply divides_b_true_to_divides.
438    assumption
439   ]
440 qed.
441
442 theorem divides_b_true_to_lt_O: \forall n,m. O < n \to divides_b m n = true \to O < m.
443 intros.
444 elim (le_to_or_lt_eq ? ? (le_O_n m))
445   [assumption
446   |apply False_ind.
447    elim H1.
448    rewrite < H2 in H1.
449    simplify in H1.
450    apply (lt_to_not_eq O n H).
451    apply sym_eq.
452    apply eqb_true_to_eq.
453    assumption
454   ]
455 qed.
456
457 (* divides and pi *)
458 theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. 
459 m \le i \to i \le n+m \to f i \divides pi n f m.
460 intros 5.elim n.simplify.
461 cut (i = m).rewrite < Hcut.apply divides_n_n.
462 apply antisymmetric_le.assumption.assumption.
463 simplify.
464 cut (i < S n1+m \lor i = S n1 + m).
465 elim Hcut.
466 apply (transitive_divides ? (pi n1 f m)).
467 apply H1.apply le_S_S_to_le. assumption.
468 apply (witness ? ? (f (S n1+m))).apply sym_times.
469 rewrite > H3.
470 apply (witness ? ? (pi n1 f m)).reflexivity.
471 apply le_to_or_lt_eq.assumption.
472 qed.
473
474 (*
475 theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. 
476 i < n \to (S O) < (f i) \to (S (pi n f)) \mod (f i) = (S O).
477 intros.cut (pi n f) \mod (f i) = O.
478 rewrite < Hcut.
479 apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
480 rewrite > Hcut.assumption.
481 apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
482 apply divides_f_pi_f.assumption.
483 qed.
484 *)
485
486 (* divides and fact *)
487 theorem divides_fact : \forall n,i:nat. 
488 O < i \to i \le n \to i \divides n!.
489 intros 3.elim n.absurd (O<i).assumption.apply (le_n_O_elim i H1).
490 apply (not_le_Sn_O O).
491 change with (i \divides (S n1)*n1!).
492 apply (le_n_Sm_elim i n1 H2).
493 intro.
494 apply (transitive_divides ? n1!).
495 apply H1.apply le_S_S_to_le. assumption.
496 apply (witness ? ? (S n1)).apply sym_times.
497 intro.
498 rewrite > H3.
499 apply (witness ? ? n1!).reflexivity.
500 qed.
501
502 theorem mod_S_fact: \forall n,i:nat. 
503 (S O) < i \to i \le n \to (S n!) \mod i = (S O).
504 intros.cut (n! \mod i = O).
505 rewrite < Hcut.
506 apply mod_S.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
507 rewrite > Hcut.assumption.
508 apply divides_to_mod_O.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
509 apply divides_fact.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
510 assumption.
511 qed.
512
513 theorem not_divides_S_fact: \forall n,i:nat. 
514 (S O) < i \to i \le n \to i \ndivides S n!.
515 intros.
516 apply divides_b_false_to_not_divides.
517 unfold divides_b.
518 rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption].
519 qed.
520
521 (* prime *)
522 definition prime : nat \to  Prop \def
523 \lambda n:nat. (S O) < n \land 
524 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
525
526 theorem not_prime_O: \lnot (prime O).
527 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
528 qed.
529
530 theorem not_prime_SO: \lnot (prime (S O)).
531 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
532 qed.
533
534 theorem prime_to_lt_O: \forall p. prime p \to O < p.
535 intros.elim H.apply lt_to_le.assumption.
536 qed.
537
538 theorem prime_to_lt_SO: \forall p. prime p \to S O < p.
539 intros.elim H.
540 assumption.
541 qed.
542
543 (* smallest factor *)
544 definition smallest_factor : nat \to nat \def
545 \lambda n:nat. 
546 match n with
547 [ O \Rightarrow O
548 | (S p) \Rightarrow 
549   match p with
550   [ O \Rightarrow (S O)
551   | (S q) \Rightarrow min_aux q (S (S O)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
552
553 (* it works !
554 theorem example1 : smallest_factor (S(S(S O))) = (S(S(S O))).
555 normalize.reflexivity.
556 qed.
557
558 theorem example2: smallest_factor (S(S(S(S O)))) = (S(S O)).
559 normalize.reflexivity.
560 qed.
561
562 theorem example3 : smallest_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
563 simplify.reflexivity.
564 qed. *)
565
566 theorem lt_SO_smallest_factor: 
567 \forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
568 intro.
569 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
570 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
571 intros.
572 change with 
573 (S O < min_aux m1 (S (S O)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
574 apply (lt_to_le_to_lt ? (S (S O))).
575 apply (le_n (S(S O))).
576 cut ((S(S O)) = (S(S m1)) - m1).
577 rewrite > Hcut.
578 apply le_min_aux.
579 apply sym_eq.apply plus_to_minus.
580 rewrite < sym_plus.simplify.reflexivity.
581 qed.
582
583 theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
584 intro.
585 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
586 intro.apply (nat_case m).intro.
587 simplify.unfold lt.apply le_n.
588 intros.apply (trans_lt ? (S O)).
589 unfold lt.apply le_n.
590 apply lt_SO_smallest_factor.unfold lt. apply le_S_S.
591 apply le_S_S.apply le_O_n.
592 qed.
593
594 theorem divides_smallest_factor_n : 
595 \forall n:nat. O < n \to smallest_factor n \divides n.
596 intro.
597 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O O H).
598 intro.apply (nat_case m).intro. simplify.
599 apply (witness ? ? (S O)). simplify.reflexivity.
600 intros.
601 apply divides_b_true_to_divides.
602 change with 
603 (eqb ((S(S m1)) \mod (min_aux m1 (S (S O)) 
604   (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
605 apply f_min_aux_true.
606 apply (ex_intro nat ? (S(S m1))).
607 split.split.
608 apply (le_S_S_to_le (S (S O)) (S (S m1)) ?).
609 apply (minus_le_O_to_le (S (S (S O))) (S (S (S m1))) ?).
610 apply (le_n O).
611 rewrite < sym_plus. simplify. apply le_n.
612 apply (eq_to_eqb_true (mod (S (S m1)) (S (S m1))) O ?).
613 apply (mod_n_n (S (S m1)) ?).
614 apply (H).
615 qed.
616   
617 theorem le_smallest_factor_n : 
618 \forall n:nat. smallest_factor n \le n.
619 intro.apply (nat_case n).simplify.apply le_n.
620 intro.apply (nat_case m).simplify.apply le_n.
621 intro.apply divides_to_le.
622 unfold lt.apply le_S_S.apply le_O_n.
623 apply divides_smallest_factor_n.
624 unfold lt.apply le_S_S.apply le_O_n.
625 qed.
626
627 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. 
628 (S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
629 intros 2.
630 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
631 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
632 intros.
633 apply divides_b_false_to_not_divides.
634 apply (lt_min_aux_to_false 
635 (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S (S O)) m1 i).
636 assumption.
637 assumption.
638 qed.
639
640 theorem prime_smallest_factor_n : 
641 \forall n:nat. (S O) < n \to prime (smallest_factor n).
642 intro.change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land 
643 (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to  m = (smallest_factor n))).
644 intro.split.
645 apply lt_SO_smallest_factor.assumption.
646 intros.
647 cut (le m (smallest_factor n)).
648 elim (le_to_or_lt_eq m (smallest_factor n) Hcut).
649 absurd (m \divides n).
650 apply (transitive_divides m (smallest_factor n)).
651 assumption.
652 apply divides_smallest_factor_n.
653 apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H.
654 apply lt_smallest_factor_to_not_divides.
655 exact H.assumption.assumption.assumption.
656 apply divides_to_le.
657 apply (trans_lt O (S O)).
658 apply (le_n (S O)).
659 apply lt_SO_smallest_factor.
660 exact H.
661 assumption.
662 qed.
663
664 theorem prime_to_smallest_factor: \forall n. prime n \to
665 smallest_factor n = n.
666 intro.apply (nat_case n).intro.apply False_ind.apply (not_prime_O H).
667 intro.apply (nat_case m).intro.apply False_ind.apply (not_prime_SO H).
668 intro.
669 change with 
670 ((S O) < (S(S m1)) \land 
671 (\forall m:nat. m \divides S(S m1) \to (S O) < m \to  m = (S(S m1))) \to 
672 smallest_factor (S(S m1)) = (S(S m1))).
673 intro.elim H.apply H2.
674 apply divides_smallest_factor_n.
675 apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption.
676 apply lt_SO_smallest_factor.
677 assumption.
678 qed.
679
680 (* a number n > O is prime iff its smallest factor is n *)
681 definition primeb \def \lambda n:nat.
682 match n with
683 [ O \Rightarrow false
684 | (S p) \Rightarrow
685   match p with
686   [ O \Rightarrow false
687   | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]].
688
689 (* it works! 
690 theorem example4 : primeb (S(S(S O))) = true.
691 normalize.reflexivity.
692 qed.
693
694 theorem example5 : primeb (S(S(S(S(S(S O)))))) = false.
695 normalize.reflexivity.
696 qed.
697
698 theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true.
699 normalize.reflexivity.
700 qed.
701
702 theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true.
703 normalize.reflexivity.
704 qed. *)
705
706 theorem primeb_to_Prop: \forall n.
707 match primeb n with
708 [ true \Rightarrow prime n
709 | false \Rightarrow \lnot (prime n)].
710 intro.
711 apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
712 intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
713 intro.
714 change with 
715 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
716 [ true \Rightarrow prime (S(S m1))
717 | false \Rightarrow \lnot (prime (S(S m1)))].
718 apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
719 intro.simplify.
720 rewrite < H.
721 apply prime_smallest_factor_n.
722 unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.
723 intro.simplify.
724 change with (prime (S(S m1)) \to False).
725 intro.apply H.
726 apply prime_to_smallest_factor.
727 assumption.
728 qed.
729
730 theorem primeb_true_to_prime : \forall n:nat.
731 primeb n = true \to prime n.
732 intros.change with
733 match true with 
734 [ true \Rightarrow prime n
735 | false \Rightarrow \lnot (prime n)].
736 rewrite < H.
737 apply primeb_to_Prop.
738 qed.
739
740 theorem primeb_false_to_not_prime : \forall n:nat.
741 primeb n = false \to \lnot (prime n).
742 intros.change with
743 match false with 
744 [ true \Rightarrow prime n
745 | false \Rightarrow \lnot (prime n)].
746 rewrite < H.
747 apply primeb_to_Prop.
748 qed.
749
750 theorem decidable_prime : \forall n:nat.decidable (prime n).
751 intro.unfold decidable.
752 cut 
753 (match primeb n with
754 [ true \Rightarrow prime n
755 | false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n)).
756 apply Hcut.apply primeb_to_Prop.
757 elim (primeb n).left.apply H.right.apply H.
758 qed.
759
760 theorem prime_to_primeb_true: \forall n:nat. 
761 prime n \to primeb n = true.
762 intros.
763 cut (match (primeb n) with
764 [ true \Rightarrow prime n
765 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = true)).
766 apply Hcut.apply primeb_to_Prop.
767 elim (primeb n).reflexivity.
768 absurd (prime n).assumption.assumption.
769 qed.
770
771 theorem not_prime_to_primeb_false: \forall n:nat. 
772 \lnot(prime n) \to primeb n = false.
773 intros.
774 cut (match (primeb n) with
775 [ true \Rightarrow prime n
776 | false \Rightarrow \lnot (prime n)] \to ((primeb n) = false)).
777 apply Hcut.apply primeb_to_Prop.
778 elim (primeb n).
779 absurd (prime n).assumption.assumption.
780 reflexivity.
781 qed.
782