--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / Matita is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/minimization".
+
+include "nat/minus.ma".
+include "datatypes/bool.ma".
+
+let rec max i f \def
+ match (f i) with
+ [ true \Rightarrow i
+ | false \Rightarrow
+ match i with
+ [ O \Rightarrow O
+ | (S j) \Rightarrow max j f ]].
+
+theorem max_O_f : \forall f: nat \to bool. max O f = O.
+intro. simplify.
+elim f O.
+simplify.reflexivity.
+simplify.reflexivity.
+qed.
+
+theorem max_S_max : \forall f: nat \to bool. \forall n:nat.
+(f (S n) = true \land max (S n) f = (S n)) \lor
+(f (S n) = false \land max (S n) f = max n f).
+intros.simplify.elim (f (S n)).
+simplify.left.split.reflexivity.reflexivity.
+simplify.right.split.reflexivity.reflexivity.
+qed.
+
+definition max_spec \def \lambda f:nat \to bool.\lambda n: nat.
+ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to
+(f n) = true \land (\forall i. i < n \to (f i = false)).
+
+(* perche' si blocca per mezzo minuto qui ??? *)
+theorem f_max_true : \forall f:nat \to bool. \forall n:nat.
+ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to f (max n f) = true.
+intros 2.
+elim n.elim H.elim H1.generalize in match H3.
+apply le_n_O_elim a H2.intro.simplify.rewrite > H4.
+simplify.assumption.
+simplify.
+apply bool_ind (\lambda b:bool.
+(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+[ true \Rightarrow (S n1)
+| false \Rightarrow (max n1 f)])) = true) ? ? ?.
+reflexivity.
+simplify.intro.assumption.
+simplify.intro.apply H.
+elim H1.elim H3.generalize in match H5.
+apply le_n_Sm_elim a n1 H4.
+intros.
+apply ex_intro nat ? a.
+split.apply le_S_S_to_le.assumption.assumption.
+intros.apply False_ind.apply not_eq_true_false ?.
+rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
+qed.
+
+theorem lt_max_to_false : \forall f:nat \to bool.
+\forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
+intros 2.
+elim n.absurd le m O.assumption.
+cut O < m.apply lt_O_n_elim m Hcut.exact not_le_Sn_O.
+rewrite < max_O_f f.assumption.
+generalize in match H1.
+(* ?? non posso generalizzare su un goal implicativo ?? *)
+elim max_S_max f n1.
+elim H3.
+absurd m \le S n1.assumption.
+apply lt_to_not_le.rewrite < H6.assumption.
+elim H3.
+apply le_n_Sm_elim m n1 H2.
+intro.
+apply H.rewrite < H6.assumption.
+apply le_S_S_to_le.assumption.
+intro.rewrite > H7.assumption.
+qed.
+
+let rec min_aux off n f \def
+ match f (n-off) with
+ [ true \Rightarrow (n-off)
+ | false \Rightarrow
+ match off with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow min_aux p n f]].
+
+definition min : nat \to (nat \to bool) \to nat \def
+\lambda n.\lambda f. min_aux n n f.
+
+theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
+min_aux O i f = i.
+intros.simplify.rewrite < minus_n_O.
+elim f i.
+simplify.reflexivity.
+simplify.reflexivity.
+qed.
+
+theorem min_O_f : \forall f:nat \to bool.
+min O f = O.
+intro.apply min_aux_O_f f O.
+qed.
+
+theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
+(f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor
+(f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).
+intros.simplify.elim (f (n - (S i))).
+simplify.left.split.reflexivity.reflexivity.
+simplify.right.split.reflexivity.reflexivity.
+qed.
+
+theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat.
+ex nat (\lambda i:nat. (le (m-off) i) \land (le i m) \land (f i = true)) \to
+f (min_aux off m f) = true.
+intros 2.
+elim off.elim H.elim H1.elim H2.
+cut a = m.
+rewrite > min_aux_O_f f.rewrite < Hcut.assumption.
+apply antisym_le a m .assumption.rewrite > minus_n_O m.assumption.
+simplify.
+apply bool_ind (\lambda b:bool.
+(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+[ true \Rightarrow m-(S n)
+| false \Rightarrow (min_aux n m f)])) = true) ? ? ?.
+reflexivity.
+simplify.intro.assumption.
+simplify.intro.apply H.
+elim H1.elim H3.elim H4.
+elim (le_to_or_lt_eq (m-(S n)) a H6).
+apply ex_intro nat ? a.
+split.split.
+apply lt_minus_S_n_to_le_minus_n.assumption.
+assumption.assumption.
+absurd f a = false.rewrite < H8.assumption.
+rewrite > H5.
+apply not_eq_true_false.
+qed.
+
+theorem lt_min_aux_to_false : \forall f:nat \to bool.
+\forall n,off,m:nat. (n-off) \leq m \to m < (min_aux off n f) \to f m = false.
+intros 3.
+elim off.absurd le n m.rewrite > minus_n_O.assumption.
+apply lt_to_not_le.rewrite < min_aux_O_f f n.assumption.
+generalize in match H1.
+elim min_aux_S f n1 n.
+elim H3.
+absurd n - S n1 \le m.assumption.
+apply lt_to_not_le.rewrite < H6.assumption.
+elim H3.
+elim le_to_or_lt_eq (n -(S n1)) m.
+apply H.apply lt_minus_S_n_to_le_minus_n.assumption.
+rewrite < H6.assumption.assumption.
+rewrite < H7.assumption.
+qed.
+
+theorem le_min_aux : \forall f:nat \to bool.
+\forall n,off:nat. (n-off) \leq (min_aux off n f).
+intros 3.
+elim off.rewrite < minus_n_O.
+rewrite > min_aux_O_f f n.apply le_n.
+elim min_aux_S f n1 n.
+elim H1.rewrite > H3.apply le_n.
+elim H1.rewrite > H3.
+apply trans_le (n-(S n1)) (n-n1) ?.
+apply monotonic_le_minus_r.
+apply le_n_Sn.
+assumption.
+qed.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / Matita is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/primes".
+
+include "nat/div_and_mod.ma".
+include "nat/minimization.ma".
+include "nat/sigma_and_pi.ma".
+include "nat/factorial.ma".
+
+inductive divides (n,m:nat) : Prop \def
+witness : \forall p:nat.m = times n p \to divides n m.
+
+theorem reflexive_divides : reflexive nat divides.
+simplify.
+intros.
+exact witness x x (S O) (times_n_SO x).
+qed.
+
+theorem divides_to_div_mod_spec :
+\forall n,m. O < n \to divides n m \to div_mod_spec m n (div m n) O.
+intros.elim H1.rewrite > H2.
+constructor 1.assumption.
+apply lt_O_n_elim n H.intros.
+rewrite < plus_n_O.
+rewrite > div_times.apply sym_times.
+qed.
+
+theorem div_mod_spec_to_div :
+\forall n,m,p. div_mod_spec m n p O \to divides n m.
+intros.elim H.
+apply witness n m p.
+rewrite < sym_times.
+rewrite > plus_n_O (p*n).assumption.
+qed.
+
+theorem divides_to_mod_O:
+\forall n,m. O < n \to divides n m \to (mod m n) = O.
+intros.apply div_mod_spec_to_eq2 m n (div m n) (mod m n) (div m n) O.
+apply div_mod_spec_div_mod.assumption.
+apply divides_to_div_mod_spec.assumption.assumption.
+qed.
+
+theorem mod_O_to_divides:
+\forall n,m. O< n \to (mod m n) = O \to divides n m.
+intros.
+apply witness n m (div m n).
+rewrite > plus_n_O (n*div m n).
+rewrite < H1.
+rewrite < sym_times.
+(* perche' hint non lo trova ?*)
+apply div_mod.
+assumption.
+qed.
+
+theorem divides_n_O: \forall n:nat. divides n O.
+intro. apply witness n O O.apply times_n_O.
+qed.
+
+theorem divides_SO_n: \forall n:nat. divides (S O) n.
+intro. apply witness (S O) n n. simplify.apply plus_n_O.
+qed.
+
+theorem divides_plus: \forall n,p,q:nat.
+divides n p \to divides n q \to divides n (p+q).
+intros.
+elim H.elim H1. apply witness n (p+q) (n2+n1).
+rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
+qed.
+
+theorem divides_minus: \forall n,p,q:nat.
+divides n p \to divides n q \to divides n (p-q).
+intros.
+elim H.elim H1. apply witness n (p-q) (n2-n1).
+rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
+qed.
+
+theorem divides_times: \forall n,m,p,q:nat.
+divides n p \to divides m q \to divides (n*m) (p*q).
+intros.
+elim H.elim H1. apply witness (n*m) (p*q) (n2*n1).
+rewrite > H2.rewrite > H3.
+apply trans_eq nat ? (n*(m*(n2*n1))).
+apply trans_eq nat ? (n*(n2*(m*n1))).
+apply assoc_times.
+apply eq_f.
+apply trans_eq nat ? ((n2*m)*n1).
+apply sym_eq. apply assoc_times.
+rewrite > sym_times n2 m.apply assoc_times.
+apply sym_eq. apply assoc_times.
+qed.
+
+theorem transitive_divides: \forall n,m,p.
+divides n m \to divides m p \to divides n p.
+intros.
+elim H.elim H1. apply witness n p (n2*n1).
+rewrite > H3.rewrite > H2.
+apply assoc_times.
+qed.
+
+(* divides le *)
+theorem divides_to_le : \forall n,m. O < m \to divides n m \to n \le m.
+intros. elim H1.rewrite > H2.cut O < n2.
+apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times.
+simplify.rewrite < sym_plus.
+apply le_plus_n.
+elim le_to_or_lt_eq O n2.
+assumption.apply le_O_n.
+absurd O<m.assumption.
+rewrite > H2.rewrite < H3.rewrite < times_n_O.
+apply not_le_Sn_n O.
+qed.
+
+theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n.
+intros.elim H1.
+elim le_to_or_lt_eq O n (le_O_n n).
+assumption.
+rewrite < H3.absurd O < m.assumption.
+rewrite > H2.rewrite < H3.
+simplify.exact not_le_Sn_n O.
+qed.
+
+(* boolean divides *)
+definition divides_b : nat \to nat \to bool \def
+\lambda n,m :nat. (eqb (mod m n) O).
+
+theorem divides_b_to_Prop :
+\forall n,m:nat. O < n \to O < m \to
+match divides_b n m with
+[ true \Rightarrow divides n m
+| false \Rightarrow \lnot (divides n m)].
+intros.
+change with
+match eqb (mod m n) O with
+[ true \Rightarrow divides n m
+| false \Rightarrow \lnot (divides n m)].
+apply eqb_elim.
+intro.simplify.apply mod_O_to_divides.assumption.assumption.
+intro.simplify.intro.apply H2.apply divides_to_mod_O.assumption.assumption.
+qed.
+
+theorem divides_b_true_to_divides :
+\forall n,m:nat. O < n \to O < m \to
+(divides_b n m = true ) \to divides n m.
+intros.
+change with
+match true with
+[ true \Rightarrow divides n m
+| false \Rightarrow \lnot (divides n m)].
+rewrite < H2.apply divides_b_to_Prop.
+assumption.assumption.
+qed.
+
+theorem divides_b_false_to_not_divides :
+\forall n,m:nat. O < n \to O < m \to
+(divides_b n m = false ) \to \lnot (divides n m).
+intros.
+change with
+match false with
+[ true \Rightarrow divides n m
+| false \Rightarrow \lnot (divides n m)].
+rewrite < H2.apply divides_b_to_Prop.
+assumption.assumption.
+qed.
+
+(* divides and pi *)
+theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat.
+i < n \to divides (f i) (pi n f).
+intros 3.elim n.apply False_ind.apply not_le_Sn_O i H.
+simplify.
+apply le_n_Sm_elim (S i) n1 H1.
+intro.
+apply transitive_divides ? (pi n1 f).
+apply H.simplify.apply le_S_S_to_le. assumption.
+apply witness ? ? (f n1).apply sym_times.
+intro.cut i = n1.
+rewrite > Hcut.
+apply witness ? ? (pi n1 f).reflexivity.
+apply inj_S.assumption.
+qed.
+
+theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat.
+i < n \to (S O) < (f i) \to mod (S (pi n f)) (f i) = (S O).
+intros.cut mod (pi n f) (f i) = O.
+rewrite < Hcut.
+apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
+rewrite > Hcut.assumption.
+apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
+apply divides_f_pi_f.assumption.
+qed.
+
+(* divides and fact *)
+theorem divides_fact : \forall n,i:nat.
+O < i \to i \le n \to divides i (fact n).
+intros 3.elim n.absurd O<i.assumption.apply le_n_O_elim i H1.
+apply not_le_Sn_O O.
+change with divides i ((S n1)*(fact n1)).
+apply le_n_Sm_elim i n1 H2.
+intro.
+apply transitive_divides ? (fact n1).
+apply H1.apply le_S_S_to_le. assumption.
+apply witness ? ? (S n1).apply sym_times.
+intro.
+rewrite > H3.
+apply witness ? ? (fact n1).reflexivity.
+qed.
+
+theorem mod_S_fact: \forall n,i:nat.
+(S O) < i \to i \le n \to mod (S (fact n)) i = (S O).
+intros.cut mod (fact n) i = O.
+rewrite < Hcut.
+apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
+rewrite > Hcut.assumption.
+apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
+apply divides_fact.apply trans_lt O (S O).apply le_n (S O).assumption.
+assumption.
+qed.
+
+theorem not_divides_S_fact: \forall n,i:nat.
+(S O) < i \to i \le n \to \not (divides i (S (fact n))).
+intros.
+apply divides_b_false_to_not_divides.
+apply trans_lt O (S O).apply le_n (S O).assumption.
+simplify.apply le_S_S.apply le_O_n.
+change with (eqb (mod (S (fact n)) i) O) = false.
+rewrite > mod_S_fact.simplify.reflexivity.
+assumption.assumption.
+qed.
+
+(* prime *)
+definition prime : nat \to Prop \def
+\lambda n:nat. (S O) < n \land
+(\forall m:nat. divides m n \to (S O) < m \to m = n).
+
+theorem not_prime_O: \lnot (prime O).
+simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
+qed.
+
+theorem not_prime_SO: \lnot (prime (S O)).
+simplify.intro.elim H.apply not_le_Sn_n (S O) H1.
+qed.
+
+(* smallest factor *)
+definition smallest_factor : nat \to nat \def
+\lambda n:nat.
+match n with
+[ O \Rightarrow O
+| (S p) \Rightarrow
+ match p with
+ [ O \Rightarrow (S O)
+ | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb (mod (S(S q)) m) O))]].
+
+(* it works !
+theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
+normalize.reflexivity.
+qed.
+
+theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)).
+normalize.reflexivity.
+qed.
+
+theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
+simplify.reflexivity.
+qed. *)
+
+(* not sure this is what we need *)
+theorem lt_S_O_smallest_factor:
+\forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
+intro.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
+intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
+intros.
+change with
+S O < min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)).
+apply lt_to_le_to_lt ? (S (S O)).
+apply le_n (S(S O)).
+cut (S(S O)) = (S(S m1)) - m1.
+rewrite > Hcut.
+apply le_min_aux.
+apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn.
+rewrite < sym_plus.simplify.reflexivity.
+qed.
+
+theorem divides_smallest_factor_n :
+\forall n:nat. (S O) < n \to divides (smallest_factor n) n.
+intro.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
+intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
+intros.
+apply divides_b_true_to_divides.
+apply trans_lt ? (S O).apply le_n (S O).apply lt_S_O_smallest_factor ? H.
+apply trans_lt ? (S O).apply le_n (S O).assumption.
+change with
+eqb (mod (S(S m1)) (min_aux m1 (S(S m1))
+ (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true.
+apply f_min_aux_true.
+apply ex_intro nat ? (S(S m1)).
+split.split.
+apply le_minus_m.apply le_n.
+rewrite > mod_n_n.reflexivity.
+apply trans_lt ? (S O).apply le_n (S O).assumption.
+qed.
+
+theorem le_smallest_factor_n :
+\forall n:nat. smallest_factor n \le n.
+intro.apply nat_case n.simplify.reflexivity.
+intro.apply nat_case m.simplify.reflexivity.
+intro.apply divides_to_le.
+simplify.apply le_S_S.apply le_O_n.
+apply divides_smallest_factor_n.
+simplify.apply le_S_S.apply le_S_S. apply le_O_n.
+qed.
+
+theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
+(S O) < n \to (S O) < i \to i < (smallest_factor n) \to \lnot (divides i n).
+intros 2.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
+intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
+intros.
+apply divides_b_false_to_not_divides.
+apply trans_lt O (S O).apply le_n (S O).assumption.
+apply trans_lt O (S O).apply le_n (S O).assumption.
+change with (eqb (mod (S(S m1)) i) O) = false.
+apply lt_min_aux_to_false
+(\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i.
+cut (S(S O)) = (S(S m1)-m1).
+rewrite < Hcut.exact H1.
+apply sym_eq. apply plus_to_minus.
+apply le_S.apply le_n_Sn.
+rewrite < sym_plus.simplify.reflexivity.
+exact H2.
+qed.
+
+theorem prime_smallest_factor_n :
+\forall n:nat. (S O) < n \to prime (smallest_factor n).
+intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land
+(\forall m:nat. divides m (smallest_factor n) \to (S O) < m \to m = (smallest_factor n)).
+intro.split.
+apply lt_S_O_smallest_factor.assumption.
+intros.
+cut le m (smallest_factor n).
+elim le_to_or_lt_eq m (smallest_factor n) Hcut.
+absurd divides m n.
+apply transitive_divides m (smallest_factor n).
+assumption.
+apply divides_smallest_factor_n.
+exact H.
+apply lt_smallest_factor_to_not_divides.
+exact H.assumption.assumption.assumption.
+apply divides_to_le.
+apply trans_lt O (S O).
+apply le_n (S O).
+apply lt_S_O_smallest_factor.
+exact H.
+assumption.
+qed.
+
+theorem prime_to_smallest_factor: \forall n. prime n \to
+smallest_factor n = n.
+intro.apply nat_case n.intro.apply False_ind.apply not_prime_O H.
+intro.apply nat_case m.intro.apply False_ind.apply not_prime_SO H.
+intro.
+change with
+(S O) < (S(S m1)) \land
+(\forall m:nat. divides m (S(S m1)) \to (S O) < m \to m = (S(S m1))) \to
+smallest_factor (S(S m1)) = (S(S m1)).
+intro.elim H.apply H2.
+apply divides_smallest_factor_n.
+assumption.
+apply lt_S_O_smallest_factor.
+assumption.
+qed.
+
+(* a number n > O is prime iff its smallest factor is n *)
+definition primeb \def \lambda n:nat.
+match n with
+[ O \Rightarrow false
+| (S p) \Rightarrow
+ match p with
+ [ O \Rightarrow false
+ | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]].
+
+(* it works!
+theorem example4 : primeb (S(S(S O))) = true.
+normalize.reflexivity.
+qed.
+
+theorem example5 : primeb (S(S(S(S(S(S O)))))) = false.
+normalize.reflexivity.
+qed.
+
+theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true.
+normalize.reflexivity.
+qed.
+
+theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true.
+normalize.reflexivity.
+qed. *)
+
+theorem primeb_to_Prop: \forall n.
+match primeb n with
+[ true \Rightarrow prime n
+| false \Rightarrow \not (prime n)].
+intro.
+apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
+intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1.
+intro.
+change with
+match eqb (smallest_factor (S(S m1))) (S(S m1)) with
+[ true \Rightarrow prime (S(S m1))
+| false \Rightarrow \not (prime (S(S m1)))].
+apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)).
+intro.change with prime (S(S m1)).
+rewrite < H.
+apply prime_smallest_factor_n.
+simplify.apply le_S_S.apply le_S_S.apply le_O_n.
+intro.change with \not (prime (S(S m1))).
+change with prime (S(S m1)) \to False.
+intro.apply H.
+apply prime_to_smallest_factor.
+assumption.
+qed.
+
+theorem primeb_true_to_prime : \forall n:nat.
+primeb n = true \to prime n.
+intros.change with
+match true with
+[ true \Rightarrow prime n
+| false \Rightarrow \not (prime n)].
+rewrite < H.
+apply primeb_to_Prop.
+qed.
+
+theorem primeb_false_to_not_prime : \forall n:nat.
+primeb n = false \to \not (prime n).
+intros.change with
+match false with
+[ true \Rightarrow prime n
+| false \Rightarrow \not (prime n)].
+rewrite < H.
+apply primeb_to_Prop.
+qed.
+
+theorem decidable_prime : \forall n:nat.decidable (prime n).
+intro.change with (prime n) \lor \not (prime n).
+cut
+match primeb n with
+[ true \Rightarrow prime n
+| false \Rightarrow \not (prime n)] \to (prime n) \lor \not (prime n).
+apply Hcut.apply primeb_to_Prop.
+elim (primeb n).left.apply H.right.apply H.
+qed.
+
+theorem prime_to_primeb_true: \forall n:nat.
+prime n \to primeb n = true.
+intros.
+cut match (primeb n) with
+[ true \Rightarrow prime n
+| false \Rightarrow \not (prime n)] \to ((primeb n) = true).
+apply Hcut.apply primeb_to_Prop.
+elim primeb n.reflexivity.
+absurd (prime n).assumption.assumption.
+qed.
+
+theorem not_prime_to_primeb_false: \forall n:nat.
+\not(prime n) \to primeb n = false.
+intros.
+cut match (primeb n) with
+[ true \Rightarrow prime n
+| false \Rightarrow \not (prime n)] \to ((primeb n) = false).
+apply Hcut.apply primeb_to_Prop.
+elim primeb n.
+absurd (prime n).assumption.assumption.
+reflexivity.
+qed.
+
+(* upper bound by Bertrand's conjecture. *)
+(* Too difficult to prove.
+let rec nth_prime n \def
+match n with
+ [ O \Rightarrow (S(S O))
+ | (S p) \Rightarrow
+ let previous_prime \def S (nth_prime p) in
+ min_aux previous_prime ((S(S O))*previous_prime) primeb].
+
+theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
+normalize.reflexivity.
+qed.
+
+theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
+normalize.reflexivity.
+qed.
+
+theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
+qed. *)
+
+theorem smallest_factor_fact: \forall n:nat.
+n < smallest_factor (S (fact n)).
+intros.
+apply not_le_to_lt.
+change with smallest_factor (S (fact n)) \le n \to False.intro.
+apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
+apply divides_smallest_factor_n.
+simplify.apply le_S_S.apply le_SO_fact.
+apply lt_S_O_smallest_factor.
+simplify.apply le_S_S.apply le_SO_fact.
+assumption.
+qed.
+
+(* mi sembra che il problem sia ex *)
+theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m.
+n < m \land m \le (S (fact n)) \land (prime m)).
+intros.
+elim H.
+apply ex_intro nat ? (S(S O)).
+split.split.apply le_n (S(S O)).
+apply le_n (S(S O)).apply primeb_to_Prop (S(S O)).
+apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
+split.split.
+apply smallest_factor_fact.
+apply le_smallest_factor_n.
+(* ancora hint non lo trova *)
+apply prime_smallest_factor_n.
+change with (S(S O)) \le S (fact (S n1)).
+apply le_S.apply le_SSO_fact.
+simplify.apply le_S_S.assumption.
+qed.
+
+let rec nth_prime n \def
+match n with
+ [ O \Rightarrow (S(S O))
+ | (S p) \Rightarrow
+ let previous_prime \def (nth_prime p) in
+ let upper_bound \def S (fact previous_prime) in
+ min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
+
+(* it works, but nth_prime 4 takes already a few minutes -
+it must compute factorial of 7 ...
+
+theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
+normalize.reflexivity.
+qed.
+
+theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
+normalize.reflexivity.
+qed.
+
+theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
+*)
+
+theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
+intro.
+apply nat_case n.
+change with prime (S(S O)).
+apply primeb_to_Prop (S(S O)).
+intro.
+(* ammirare la resa del letin !! *)
+change with
+let previous_prime \def (nth_prime m) in
+let upper_bound \def S (fact previous_prime) in
+prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
+apply primeb_true_to_prime.
+apply f_min_aux_true.
+apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))).
+split.split.
+cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)).
+rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
+(* maybe we could factorize this proof *)
+apply plus_to_minus.
+apply le_minus_m.
+apply plus_minus_m_m.
+apply le_S_S.
+apply le_n_fact_n.
+apply le_smallest_factor_n.
+apply prime_to_primeb_true.
+apply prime_smallest_factor_n.
+change with (S(S O)) \le S (fact (nth_prime m)).
+apply le_S_S.apply le_SO_fact.
+qed.
\ No newline at end of file
projects / helm.git / commitdiff