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