assumption.
qed.
+theorem mod_O_n: \forall n:nat.mod O n = O.
+intro.elim n.simplify.reflexivity.
+simplify.reflexivity.
+qed.
+
+
(* injectivity *)
theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
change with \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q.
variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def
injective_times_r.
+theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
+change with \forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q.
+intros 4.
+apply lt_O_n_elim n H.intros.
+apply inj_times_r m.assumption.
+qed.
+
+variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
+\def lt_O_to_injective_times_r.
+
theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
change with \forall n,p,q:nat.p*(S n) = q*(S n) \to p=q.
intros.
variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def
injective_times_l.
+
+theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n).
+change with \forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q.
+intros 4.
+apply lt_O_n_elim n H.intros.
+apply inj_times_l m.assumption.
+qed.
+
+variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
+\def lt_O_to_injective_times_l.
\ No newline at end of file
set "baseuri" "cic:/matita/nat/exp".
include "nat/times.ma".
+include "nat/orders.ma".
+include "higher_order_defs/functions.ma".
let rec exp n m on m\def
match m with
elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
simplify.rewrite > H.rewrite < exp_plus_times.
rewrite < times_n_Sm.reflexivity.
-qed.
\ No newline at end of file
+qed.
+
+theorem lt_O_exp: \forall n,m:nat. O < n \to O < exp n m.
+intros.elim m.simplify.apply le_n.
+simplify.rewrite > times_n_SO.
+apply le_times.assumption.assumption.
+qed.
+
+theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < exp n m.
+intros.elim m.simplify.reflexivity.
+simplify.
+apply trans_le ? ((S(S O))*(S n1)).
+simplify.
+rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
+rewrite < sym_plus.
+apply le_plus_n.
+apply le_times.assumption.assumption.
+qed.
+
+theorem exp_to_eq_O: \forall n,m:nat. (S O) < n
+\to exp n m = (S O) \to m = O.
+intros.apply antisym_le.apply le_S_S_to_le.
+rewrite < H1.change with m < exp n m.
+apply lt_m_exp_nm.assumption.
+apply le_O_n.
+qed.
+
+theorem injective_exp_r: \forall n:nat. (S O) < n \to
+injective nat nat (\lambda m:nat. exp n m).
+simplify.intros 4.
+apply nat_elim2 (\lambda x,y.exp n x = exp n y \to x = y).
+intros.apply sym_eq.apply exp_to_eq_O n.assumption.
+rewrite < H1.reflexivity.
+intros.apply exp_to_eq_O n.assumption.assumption.
+intros.apply eq_f.
+apply H1.
+(* esprimere inj_times senza S *)
+cut \forall a,b:nat.O < n \to n*a=n*b \to a=b.
+apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
+assumption.
+intros 2.
+apply nat_case n.
+intros.apply False_ind.apply not_le_Sn_O O H3.
+intros.apply inj_times_r m1.assumption.
+qed.
+
+variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
+(exp p n) = (exp p m) \to n = m \def
+injective_exp_r.
+
+
--- /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/gcd".
+
+include "nat/primes.ma".
+include "higher_order_defs/functions.ma".
+
+let rec gcd_aux p m n: nat \def
+match divides_b n m with
+[ true \Rightarrow n
+| false \Rightarrow
+ match p with
+ [O \Rightarrow n
+ |(S q) \Rightarrow gcd_aux q n (mod m n)]].
+
+definition gcd : nat \to nat \to nat \def
+\lambda n,m:nat.
+ match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
+
+theorem divides_mod: \forall p,m,n:nat. O < n \to divides p m \to divides p n \to
+divides p (mod m n).
+intros.elim H1.elim H2.
+apply witness ? ? (n2 - n1*(div m n)).
+rewrite > distr_times_minus.
+rewrite < H3.
+rewrite < assoc_times.
+rewrite < H4.
+apply sym_eq.
+apply plus_to_minus.
+rewrite > div_mod m n in \vdash (? ? %).
+rewrite > sym_times.
+apply eq_plus_to_le ? ? (mod m n).
+reflexivity.
+rewrite > sym_times.
+apply div_mod.assumption. assumption.
+qed.
+
+theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
+divides p (mod m n) \to divides p n \to divides p m.
+intros.elim H1.elim H2.
+apply witness p m ((n1*(div m n))+n2).
+rewrite > distr_times_plus.
+rewrite < H3.
+rewrite < assoc_times.
+rewrite < H4.rewrite < sym_times.
+apply div_mod.assumption.
+qed.
+
+theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
+divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n.
+intro.elim p.
+absurd O < n.assumption.apply le_to_not_lt.assumption.
+cut (divides n1 m) \lor \not (divides n1 m).
+change with
+(divides
+(match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land
+(divides
+(match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)]) n1).
+elim Hcut.rewrite > divides_to_divides_b_true.
+simplify.
+split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
+rewrite > not_divides_to_divides_b_false.
+change with
+(divides (gcd_aux n n1 (mod m n1)) m) \land
+(divides (gcd_aux n n1 (mod m n1)) n1).
+cut (divides (gcd_aux n n1 (mod m n1)) n1) \land
+(divides (gcd_aux n n1 (mod m n1)) (mod m n1)).
+elim Hcut1.
+split.apply divides_mod_to_divides ? ? n1.
+assumption.assumption.assumption.assumption.
+apply H.
+cut O \lt mod m n1 \lor O = mod m n1.
+elim Hcut1.assumption.
+apply False_ind.apply H4.apply mod_O_to_divides.
+assumption.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+apply lt_to_le.
+apply lt_mod_m_m.assumption.
+apply le_S_S_to_le.
+apply trans_le ? n1.
+change with mod m n1 < n1.
+apply lt_mod_m_m.assumption.assumption.
+apply decidable_divides n1 m.assumption.
+apply lt_to_le_to_lt ? n1.assumption.reflexivity.
+assumption.
+assumption.assumption.
+qed.
+
+theorem divides_gcd_nm: \forall n,m.
+divides (gcd n m) m \land divides (gcd n m) n.
+intros.
+change with
+divides
+(match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m
+\land
+ divides
+(match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n.
+apply leb_elim n m.
+apply nat_case1 n.
+simplify.intros.split.
+apply witness m m (S O).apply times_n_SO.
+apply witness m O O.apply times_n_O.
+intros.change with
+divides (gcd_aux (S m1) m (S m1)) m
+\land
+divides (gcd_aux (S m1) m (S m1)) (S m1).
+apply divides_gcd_aux_mn.
+simplify.apply le_S_S.apply le_O_n.
+assumption.apply le_n.
+simplify.intro.
+apply nat_case1 m.
+simplify.intros.split.
+apply witness n O O.apply times_n_O.
+apply witness n n (S O).apply times_n_SO.
+intros.change with
+divides (gcd_aux (S m1) n (S m1)) (S m1)
+\land
+divides (gcd_aux (S m1) n (S m1)) n.
+cut divides (gcd_aux (S m1) n (S m1)) n
+\land
+divides (gcd_aux (S m1) n (S m1)) (S m1).
+elim Hcut.split.assumption.assumption.
+apply divides_gcd_aux_mn.
+simplify.apply le_S_S.apply le_O_n.
+apply not_lt_to_le.simplify.intro.apply H.
+rewrite > H1.apply trans_le ? (S n).
+apply le_n_Sn.assumption.apply le_n.
+qed.
+
+theorem divides_gcd_n: \forall n,m.
+divides (gcd n m) n.
+intros.
+exact proj2 ? ? (divides_gcd_nm n m).
+qed.
+
+theorem divides_gcd_m: \forall n,m.
+divides (gcd n m) m.
+intros.
+exact proj1 ? ? (divides_gcd_nm n m).
+qed.
+
+theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
+divides d m \to divides d n \to divides d (gcd_aux p m n).
+intro.elim p.
+absurd O < n.assumption.apply le_to_not_lt.assumption.
+change with
+divides d
+(match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)]).
+cut divides n1 m \lor \not (divides n1 m).
+elim Hcut.
+rewrite > divides_to_divides_b_true.
+simplify.assumption.
+rewrite > not_divides_to_divides_b_false.
+change with divides d (gcd_aux n n1 (mod m n1)).
+apply H.
+cut O \lt mod m n1 \lor O = mod m n1.
+elim Hcut1.assumption.
+absurd divides n1 m.apply mod_O_to_divides.
+assumption.apply sym_eq.assumption.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+apply lt_to_le.
+apply lt_mod_m_m.assumption.
+apply le_S_S_to_le.
+apply trans_le ? n1.
+change with mod m n1 < n1.
+apply lt_mod_m_m.assumption.assumption.
+assumption.
+apply divides_mod.assumption.assumption.assumption.
+apply decidable_divides n1 m.assumption.
+apply lt_to_le_to_lt ? n1.assumption.reflexivity.
+assumption.assumption.assumption.
+qed.
+
+theorem divides_d_gcd: \forall m,n,d.
+divides d m \to divides d n \to divides d (gcd n m).
+intros.
+change with
+divides d (
+match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
+apply leb_elim n m.
+apply nat_case1 n.simplify.intros.assumption.
+intros.
+change with divides d (gcd_aux (S m1) m (S m1)).
+apply divides_gcd_aux.
+simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
+rewrite < H2.assumption.
+apply nat_case1 m.simplify.intros.assumption.
+intros.
+change with divides d (gcd_aux (S m1) n (S m1)).
+apply divides_gcd_aux.
+simplify.apply le_S_S.apply le_O_n.
+apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
+rewrite < H2.assumption.
+qed.
+
+theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
+ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*m = (gcd_aux p m n) \lor b*m - a*n = (gcd_aux p m n))).
+intro.
+elim p.
+absurd O < n.assumption.apply le_to_not_lt.assumption.
+cut O < m.
+cut (divides n1 m) \lor \not (divides n1 m).
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n1 - b*m = match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)]
+\lor
+b*m - a*n1 = match divides_b n1 m with
+[ true \Rightarrow n1
+| false \Rightarrow gcd_aux n n1 (mod m n1)])).
+elim Hcut1.
+rewrite > divides_to_divides_b_true.
+simplify.
+apply ex_intro ? ? (S O).
+apply ex_intro ? ? O.
+left.simplify.rewrite < plus_n_O.
+apply sym_eq.apply minus_n_O.
+rewrite > not_divides_to_divides_b_false.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n1 - b*m = gcd_aux n n1 (mod m n1)
+\lor
+b*m - a*n1 = gcd_aux n n1 (mod m n1))).
+cut
+ex nat (\lambda a. ex nat (\lambda b.
+a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
+\lor
+b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))).
+elim Hcut2.elim H5.elim H6.
+(* first case *)
+rewrite < H7.
+apply ex_intro ? ? (a1+a*(div m n1)).
+apply ex_intro ? ? a.
+right.
+rewrite < sym_plus.
+rewrite < sym_times n1.
+rewrite > distr_times_plus.
+rewrite > sym_times n1.
+rewrite > sym_times n1.
+rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?).
+rewrite > assoc_times.
+rewrite < sym_plus.
+rewrite > distr_times_plus.
+rewrite < eq_minus_minus_minus_plus.
+rewrite < sym_plus.
+rewrite < plus_minus.
+rewrite < minus_n_n.reflexivity.
+(* second case *)
+rewrite < H7.
+apply ex_intro ? ? (a1+a*(div m n1)).
+apply ex_intro ? ? a.
+left.
+rewrite > sym_times.
+rewrite > distr_times_plus.
+rewrite > sym_times.
+rewrite > sym_times n1.
+rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
+rewrite > distr_times_plus.
+rewrite > assoc_times.
+rewrite < eq_minus_minus_minus_plus.
+rewrite < sym_plus.
+rewrite < plus_minus.
+rewrite < minus_n_n.reflexivity.
+(* end second case *)
+apply H n1 (mod m n1).
+(* a lot of trivialities left *)
+cut O \lt mod m n1 \lor O = mod m n1.
+elim Hcut2.assumption.
+absurd divides n1 m.apply mod_O_to_divides.
+assumption.apply sym_eq.assumption.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+apply lt_to_le.
+apply lt_mod_m_m.assumption.
+apply le_S_S_to_le.
+apply trans_le ? n1.
+change with mod m n1 < n1.
+apply lt_mod_m_m.assumption.assumption.
+apply decidable_divides n1 m.assumption.
+apply lt_to_le_to_lt ? n1.assumption.assumption.
+assumption.assumption.assumption.assumption.assumption.
+apply le_n.assumption.
+apply le_n.
+qed.
+
+theorem eq_minus_gcd: \forall m,n.
+ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))).
+intros.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*m =
+match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
+\lor b*m - a*n =
+match leb n m with
+ [ true \Rightarrow
+ match n with
+ [ O \Rightarrow m
+ | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
+ | false \Rightarrow
+ match m with
+ [ O \Rightarrow n
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
+)).
+apply leb_elim n m.
+apply nat_case1 n.
+simplify.intros.
+apply ex_intro ? ? O.
+apply ex_intro ? ? (S O).
+right.simplify.
+rewrite < plus_n_O.
+apply sym_eq.apply minus_n_O.
+intros.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
+\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))).
+apply eq_minus_gcd_aux.
+simplify. apply le_S_S.apply le_O_n.
+assumption.apply le_n.
+apply nat_case1 m.
+simplify.intros.
+apply ex_intro ? ? (S O).
+apply ex_intro ? ? O.
+left.simplify.
+rewrite < plus_n_O.
+apply sym_eq.apply minus_n_O.
+intros.
+change with
+ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
+\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))).
+cut
+ex nat (\lambda a. ex nat (\lambda b.
+a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
+\lor
+b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))).
+elim Hcut.elim H2.elim H3.
+apply ex_intro ? ? a1.
+apply ex_intro ? ? a.
+right.assumption.
+apply ex_intro ? ? a1.
+apply ex_intro ? ? a.
+left.assumption.
+apply eq_minus_gcd_aux.
+simplify. apply le_S_S.apply le_O_n.
+apply lt_to_le.apply not_le_to_lt.assumption.
+apply le_n.
+qed.
+
+(* some properties of gcd *)
+
+theorem gcd_O_n: \forall n:nat. gcd O n = n.
+intro.simplify.reflexivity.
+qed.
+
+theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
+m = O \land n = O.
+intros.cut divides O n \land divides O m.
+elim Hcut.elim H2.split.
+assumption.elim H1.assumption.
+rewrite < H.
+apply divides_gcd_nm.
+qed.
+
+theorem symmetric_gcd: symmetric nat gcd.
+change with
+\forall n,m:nat. gcd n m = gcd m n.
+intros.
+cut O < (gcd n m) \lor O = (gcd n m).
+elim Hcut.
+cut O < (gcd m n) \lor O = (gcd m n).
+elim Hcut1.
+apply antisym_le.
+apply divides_to_le.assumption.
+apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
+apply divides_to_le.assumption.
+apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
+rewrite < H1.
+cut m=O \land n=O.
+elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+rewrite < H.
+cut n=O \land m=O.
+elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+qed.
+
+variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
+symmetric_gcd.
+
+theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
+intro.
+apply antisym_le.apply divides_to_le.simplify.apply le_n.
+apply divides_gcd_n.
+cut O < gcd (S O) n \lor O = gcd (S O) n.
+elim Hcut.assumption.
+apply False_ind.
+apply not_eq_O_S O.
+cut (S O)=O \land n=O.
+elim Hcut1.apply sym_eq.assumption.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+qed.
+
+theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to
+gcd n m = (S O).
+intros.simplify in H.change with gcd n m = (S O).
+elim H.
+apply antisym_le.
+apply not_lt_to_le.
+change with (S (S O)) \le gcd n m \to False.intro.
+apply H1.rewrite < H3 (gcd n m).
+apply divides_gcd_m.
+cut O < gcd n m \lor O = gcd n m.
+elim Hcut.assumption.
+apply False_ind.
+apply not_le_Sn_O (S O).
+cut n=O \land m=O.
+elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
+apply gcd_O_to_eq_O.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+apply divides_gcd_n.assumption.
+qed.
+
+(* esempio di sfarfallalmento !!! *)
+(*
+theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
+divides n p \lor divides n q.
+intros.
+cut divides n p \lor \not (divides n p).
+elim Hcut.left.assumption.
+right.
+cut ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+elim Hcut1.elim H3.*)
+
+theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
+divides n p \lor divides n q.
+intros.
+cut divides n p \lor \not (divides n p).
+elim Hcut.
+left.assumption.
+right.
+cut ex nat (\lambda a. ex nat (\lambda b.
+a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+elim Hcut1.elim H3.elim H4.
+(* first case *)
+rewrite > times_n_SO q.rewrite < H5.
+rewrite > distr_times_minus.
+rewrite > sym_times q (a1*p).
+rewrite > assoc_times a1.
+elim H1.rewrite > H6.
+rewrite < sym_times n.rewrite < assoc_times.
+rewrite > sym_times q.rewrite > assoc_times.
+rewrite < assoc_times a1.rewrite < sym_times n.
+rewrite > assoc_times n.
+rewrite < distr_times_minus.
+apply witness ? ? (q*a-a1*n2).reflexivity.
+(* second case *)
+rewrite > times_n_SO q.rewrite < H5.
+rewrite > distr_times_minus.
+rewrite > sym_times q (a1*p).
+rewrite > assoc_times a1.
+elim H1.rewrite > H6.
+rewrite < sym_times.rewrite > assoc_times.
+rewrite < assoc_times q.
+rewrite < sym_times n.
+rewrite < distr_times_minus.
+apply witness ? ? (n2*a1-q*a).reflexivity.
+(* end second case *)
+rewrite < prime_to_gcd_SO n p.
+apply eq_minus_gcd.
+apply decidable_divides n p.
+apply trans_lt ? (S O).simplify.apply le_n.
+simplify in H.elim H. assumption.
+assumption.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/log".
+
+include "datatypes/constructors.ma".
+include "nat/primes.ma".
+include "nat/exp.ma".
+
+(* this definition of log is based on pairs, with a remainder *)
+
+let rec plog_aux p n m \def
+ match (mod n m) with
+ [ O \Rightarrow
+ match p with
+ [ O \Rightarrow pair nat nat O n
+ | (S p) \Rightarrow
+ match (plog_aux p (div n m) m) with
+ [ (pair q r) \Rightarrow pair nat nat (S q) r]]
+ | (S a) \Rightarrow pair nat nat O n].
+
+(* plog n m = <q,r> if m divides n q times, with remainder r *)
+definition plog \def \lambda n,m:nat.plog_aux n n m.
+
+theorem plog_aux_to_Prop: \forall p,n,m. O < m \to
+ match plog_aux p n m with
+ [ (pair q r) \Rightarrow n = (exp m q)*r ].
+intro.
+elim p.
+change with
+match (
+match (mod n m) with
+ [ O \Rightarrow pair nat nat O n
+ | (S a) \Rightarrow pair nat nat O n] )
+with
+ [ (pair q r) \Rightarrow n = (exp m q)*r ].
+apply nat_case (mod n m).
+simplify.apply plus_n_O.
+intros.
+simplify.apply plus_n_O.
+change with
+match (
+match (mod n1 m) with
+ [ O \Rightarrow
+ match (plog_aux n (div n1 m) m) with
+ [ (pair q r) \Rightarrow pair nat nat (S q) r]
+ | (S a) \Rightarrow pair nat nat O n1] )
+with
+ [ (pair q r) \Rightarrow n1 = (exp m q)*r].
+apply nat_case1 (mod n1 m).intro.
+change with
+match (
+ match (plog_aux n (div n1 m) m) with
+ [ (pair q r) \Rightarrow pair nat nat (S q) r])
+with
+ [ (pair q r) \Rightarrow n1 = (exp m q)*r].
+generalize in match (H (div n1 m) m).
+elim plog_aux n (div n1 m) m.
+simplify.
+rewrite > assoc_times.
+rewrite < H3.rewrite > plus_n_O (m*(div n1 m)).
+rewrite < H2.
+rewrite > sym_times.
+rewrite < div_mod.reflexivity.
+intros.simplify.apply plus_n_O.
+assumption.assumption.
+qed.
+
+theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
+ (pair nat nat q r) = plog_aux p n m \to n = (exp m q)*r.
+intros.
+change with
+match (pair nat nat q r) with
+ [ (pair q r) \Rightarrow n = (exp m q)*r ].
+rewrite > H1.
+apply plog_aux_to_Prop.
+assumption.
+qed.
+(* questo va spostato in primes1.ma *)
+theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to
+\forall p. i \le p \to plog_aux p ((exp m i)*n) m = pair nat nat i n.
+intros 5.
+elim i.
+simplify.
+rewrite < plus_n_O.
+apply nat_case p.
+change with
+ match (mod n m) with
+ [ O \Rightarrow pair nat nat O n
+ | (S a) \Rightarrow pair nat nat O n]
+ = pair nat nat O n.
+elim (mod n m).simplify.reflexivity.simplify.reflexivity.
+intro.
+change with
+ match (mod n m) with
+ [ O \Rightarrow
+ match (plog_aux m1 (div n m) m) with
+ [ (pair q r) \Rightarrow pair nat nat (S q) r]
+ | (S a) \Rightarrow pair nat nat O n]
+ = pair nat nat O n.
+cut O < mod n m \lor O = mod n m.
+elim Hcut.apply lt_O_n_elim (mod n m) H3.
+intros. simplify.reflexivity.
+apply False_ind.
+apply H1.apply sym_eq.assumption.
+apply le_to_or_lt_eq.apply le_O_n.
+generalize in match H3.
+apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
+intros.
+change with
+ match (mod ((exp m (S n1))*n) m) with
+ [ O \Rightarrow
+ match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
+ [ (pair q r) \Rightarrow pair nat nat (S q) r]
+ | (S a) \Rightarrow pair nat nat O ((exp m (S n1))*n)]
+ = pair nat nat (S n1) n.
+cut (mod ((exp m (S n1))*n) m) = O.
+rewrite > Hcut.
+change with
+match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
+ [ (pair q r) \Rightarrow pair nat nat (S q) r]
+ = pair nat nat (S n1) n.
+cut div ((exp m (S n1))*n) m = (exp m n1)*n.
+rewrite > Hcut1.
+rewrite > H2 m1. simplify.reflexivity.
+(* div_exp *)
+change with div (m*(exp m n1)*n) m = (exp m n1)*n.
+rewrite > assoc_times.
+apply lt_O_n_elim m H.
+intro.apply div_times.
+(* mod_exp = O *)
+apply divides_to_mod_O.
+assumption.
+simplify.rewrite > assoc_times.
+apply witness ? ? ((exp m n1)*n).reflexivity.
+apply le_S_S_to_le.assumption.
+qed.
+
+theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
+ match plog_aux p n m with
+ [ (pair q r) \Rightarrow \lnot (mod r m = O)].
+intro.elim p.absurd O < n.assumption.
+apply le_to_not_lt.assumption.
+change with
+match
+ (match (mod n1 m) with
+ [ O \Rightarrow
+ match (plog_aux n(div n1 m) m) with
+ [ (pair q r) \Rightarrow pair nat nat (S q) r]
+ | (S a) \Rightarrow pair nat nat O n1])
+with
+ [ (pair q r) \Rightarrow \lnot(mod r m = O)].
+apply nat_case1 (mod n1 m).intro.
+generalize in match (H (div n1 m) m).
+elim (plog_aux n (div n1 m) m).
+apply H5.assumption.
+apply eq_mod_O_to_lt_O_div.
+apply trans_lt ? (S O).simplify.apply le_n.
+assumption.assumption.assumption.
+apply le_S_S_to_le.
+apply trans_le ? n1.change with div n1 m < n1.
+apply lt_div_n_m_n.assumption.assumption.assumption.
+intros.
+change with (\lnot (mod n1 m = O)).
+rewrite > H4.
+(* META NOT FOUND !!!
+rewrite > sym_eq. *)
+simplify.intro.
+apply not_eq_O_S m1 ?.
+rewrite > H5.reflexivity.
+qed.
+
+theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
+ pair nat nat q r = plog_aux p n m \to \lnot (mod r m = O).
+intros.
+change with
+ match (pair nat nat q r) with
+ [ (pair q r) \Rightarrow \lnot (mod r m = O)].
+rewrite > H3.
+apply plog_aux_to_Prop1.
+assumption.assumption.assumption.
+qed.
+
set "baseuri" "cic:/matita/nat/lt_arith".
+include "nat/exp.ma".
include "nat/div_and_mod.ma".
(* plus *)
intro.reflexivity.
qed.
+(* div *)
+
+theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to mod n m = O \to O < div n m.
+intros 4.apply lt_O_n_elim m H.intros.
+apply lt_times_to_lt_r m1.
+rewrite < times_n_O.
+rewrite > plus_n_O ((S m1)*(div n (S m1))).
+rewrite < H2.
+rewrite < sym_times.
+rewrite < div_mod.
+rewrite > H2.
+assumption.
+simplify.apply le_S_S.apply le_O_n.
+qed.
+
+theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to div n m \lt n.
+intros.
+apply nat_case1 (div n m).intro.
+assumption.intros.rewrite < H2.
+rewrite > (div_mod n m) in \vdash (? ? %).
+apply lt_to_le_to_lt ? ((div n m)*m).
+apply lt_to_le_to_lt ? ((div n m)*(S (S O))).
+rewrite < sym_times.
+rewrite > H2.
+simplify.
+rewrite < plus_n_O.
+rewrite < plus_n_Sm.
+apply le_S_S.
+apply le_S_S.
+apply le_plus_n.
+apply le_times_r.
+assumption.
+rewrite < sym_plus.
+apply le_plus_n.
+apply trans_lt ? (S O).
+simplify. apply le_n.assumption.
+qed.
+
+(* general properties of functions *)
+theorem monotonic_to_injective: \forall f:nat\to nat.
+monotonic nat lt f \to injective nat nat f.
+simplify.intros.
+apply nat_compare_elim x y.
+intro.apply False_ind.apply not_le_Sn_n (f x).
+rewrite > H1 in \vdash (? ? %).apply H.apply H2.
+intros.assumption.
+intro.apply False_ind.apply not_le_Sn_n (f y).
+rewrite < H1 in \vdash (? ? %).apply H.apply H2.
+qed.
+
+theorem increasing_to_injective: \forall f:nat\to nat.
+increasing f \to injective nat nat f.
+intros.apply monotonic_to_injective.
+apply increasing_to_monotonic.assumption.
+qed.
\ No newline at end of file
simplify.right.split.reflexivity.reflexivity.
qed.
+theorem le_max_n : \forall f: nat \to bool. \forall n:nat.
+max n f \le n.
+intros.elim n.rewrite > max_O_f.apply le_n.
+simplify.elim (f (S n1)).simplify.apply le_n.
+simplify.apply le_S.assumption.
+qed.
+
+theorem le_to_le_max : \forall f: nat \to bool. \forall n,m:nat.
+n\le m \to max n f \le max m f.
+intros.elim H.
+apply le_n.
+apply trans_le ? (max n1 f).apply H2.
+cut (f (S n1) = true \land max (S n1) f = (S n1)) \lor
+(f (S n1) = false \land max (S n1) f = max n1 f).
+elim Hcut.elim H3.
+rewrite > H5.
+apply le_S.apply le_max_n.
+elim H3.rewrite > H5.apply le_n.
+apply max_S_max.
+qed.
+
+theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat.
+m\le n \to f m = true \to m \le max n f.
+intros 3.elim n.apply le_n_O_elim m H.
+apply le_O_n.
+apply le_n_Sm_elim m n1 H1.
+intro.apply trans_le ? (max n1 f).
+apply H.apply le_S_S_to_le.assumption.assumption.
+apply le_to_le_max.apply le_n_Sn.
+intro.simplify.rewrite < H3.
+rewrite > H2.simplify.apply le_n.
+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)).
intros.simplify.apply le_S.assumption.
qed.
+theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
+intros.apply lt_O_n_elim n H.intro.
+apply lt_O_n_elim m H1.intro.
+simplify.apply le_S_S.apply le_minus_m.
+qed.
+
theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
intros 2.
apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m).
theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
\def distributive_times_minus.
+theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
+intros.
+cut m+p \le n \or \not m+p \le n.
+elim Hcut.
+apply sym_eq.
+apply plus_to_minus.assumption.
+rewrite > assoc_plus.
+rewrite > sym_plus p.
+rewrite < plus_minus_m_m.
+rewrite > sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+rewrite > eq_minus_n_m_O n (m+p).
+rewrite > eq_minus_n_m_O (n-m) p.reflexivity.
+apply decidable_le (m+p) n.
+apply le_plus_to_minus_r.
+rewrite > sym_plus.assumption.
+apply trans_le ? (m+p).
+rewrite < sym_plus.
+apply le_plus_n.assumption.
+apply lt_to_le.apply not_le_to_lt.assumption.
+apply le_plus_to_minus.
+apply lt_to_le.apply not_le_to_lt.
+rewrite < sym_plus.assumption.
+qed.
+
+theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
+p+(n-m) = n-(m-p).
+intros.
+apply sym_eq.
+apply plus_to_minus.
+apply le_plus_to_minus.
+apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n.
+rewrite < assoc_plus.
+rewrite < plus_minus_m_m.
+rewrite < sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+assumption.assumption.
+qed.
intros.elim n.assumption.apply H1.
qed.
+theorem nat_case1:
+\forall n:nat.\forall P:nat \to Prop.
+(n=O \to P O) \to (\forall m:nat. (n=(S m) \to P (S m))) \to P n.
+intros 2.elim n.
+apply H.reflexivity.
+apply H2.reflexivity.
+qed.
+
theorem nat_elim2 :
\forall R:nat \to nat \to Prop.
(\forall n:nat. R O n) \to
--- /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/nth_prime".
+
+include "nat/primes.ma".
+
+(* 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_O_n.
+apply lt_SO_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.
+
+(* properties of nth_prime *)
+theorem increasing_nth_prime: increasing nth_prime.
+change with \forall n:nat. (nth_prime n) < (nth_prime (S n)).
+intros.
+change with
+let previous_prime \def (nth_prime n) in
+let upper_bound \def S (fact previous_prime) in
+(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb.
+intros.
+cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
+rewrite < Hcut in \vdash (? % ?).
+apply le_min_aux.
+apply plus_to_minus.
+apply le_minus_m.
+apply plus_minus_m_m.
+apply le_S_S.
+apply le_n_fact_n.
+qed.
+
+variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
+(nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
+
+theorem injective_nth_prime: injective nat nat nth_prime.
+apply increasing_to_injective.
+apply increasing_nth_prime.
+qed.
+
+theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
+intros. elim n.simplify.apply le_n.
+apply trans_lt ? (nth_prime n1).
+assumption.apply lt_nth_prime_n_nth_prime_Sn.
+qed.
+
+theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
+intros.apply trans_lt O (S O).
+simplify. apply le_n.apply lt_SO_nth_prime_n.
+qed.
+
+theorem ex_m_le_n_nth_prime_m:
+\forall n: nat. nth_prime O \le n \to
+ex nat (\lambda m. nth_prime m \le n \land n < nth_prime (S m)).
+intros.
+apply increasing_to_le2.
+exact lt_nth_prime_n_nth_prime_Sn.assumption.
+qed.
+
+theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n)
+\to \not (prime m).
+intros.
+apply primeb_false_to_not_prime.
+letin previous_prime \def nth_prime n.
+letin upper_bound \def S (fact previous_prime).
+apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m.
+cut S (fact (nth_prime n))-(S (fact (nth_prime n)) - (S (nth_prime n))) = (S (nth_prime n)).
+rewrite > Hcut.assumption.
+apply plus_to_minus.
+apply le_minus_m.
+apply plus_minus_m_m.
+apply le_S_S.
+apply le_n_fact_n.
+assumption.
+qed.
+
+(* nth_prime enumerates all primes *)
+theorem prime_to_nth_prime : \forall p:nat. prime p \to
+ex nat (\lambda i:nat. nth_prime i = p).
+intros.
+cut ex nat (\lambda m. nth_prime m \le p \land p < nth_prime (S m)).
+elim Hcut.elim H1.
+cut nth_prime a < p \lor nth_prime a = p.
+elim Hcut1.
+absurd (prime p).
+assumption.
+apply lt_nth_prime_to_not_prime a.assumption.assumption.
+apply ex_intro nat ? a.assumption.
+apply le_to_or_lt_eq.assumption.
+apply ex_m_le_n_nth_prime_m.
+simplify.simplify in H.elim H.assumption.
+qed.
+
apply lt_to_le_to_lt p q (S n1) H3 H2.
qed.
+(* some properties of functions *)
+
+definition increasing \def \lambda f:nat \to nat.
+\forall n:nat. f n < f (S n).
+
+theorem increasing_to_monotonic: \forall f:nat \to nat.
+increasing f \to monotonic nat lt f.
+simplify.intros.elim H1.apply H.
+apply trans_le ? (f n1).
+assumption.apply trans_le ? (S (f n1)).
+apply le_n_Sn.
+apply H.
+qed.
+
+theorem le_n_fn: \forall f:nat \to nat. (increasing f)
+\to \forall n:nat. n \le (f n).
+intros.elim n.
+apply le_O_n.
+apply trans_le ? (S (f n1)).
+apply le_S_S.apply H1.
+simplify in H. apply H.
+qed.
+
+theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
+\to \forall m:nat. ex nat (\lambda i. m \le (f i)).
+intros.elim m.
+apply ex_intro ? ? O.apply le_O_n.
+elim H1.
+apply ex_intro ? ? (S a).
+apply trans_le ? (S (f a)).
+apply le_S_S.assumption.
+simplify in H.
+apply H.
+qed.
+
+theorem increasing_to_le2: \forall f:nat \to nat. (increasing f)
+\to \forall m:nat. (f O) \le m \to
+ex nat (\lambda i. (f i) \le m \land m <(f (S i))).
+intros.elim H1.
+apply ex_intro ? ? O.
+split.apply le_n.apply H.
+elim H3.elim H4.
+cut (S n1) < (f (S a)) \lor (S n1) = (f (S a)).
+elim Hcut.
+apply ex_intro ? ? a.
+split.apply le_S. assumption.assumption.
+apply ex_intro ? ? (S a).
+split.rewrite < H7.apply le_n.
+rewrite > H7.
+apply H.
+apply le_to_or_lt_eq.apply H6.
+qed.
\lambda n,m :nat. (eqb (mod m n) O).
theorem divides_b_to_Prop :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \to
match divides_b n m with
[ true \Rightarrow divides n m
| false \Rightarrow \lnot (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.
+intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
qed.
theorem divides_b_true_to_divides :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \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.
+rewrite < H1.apply divides_b_to_Prop.
+assumption.
qed.
theorem divides_b_false_to_not_divides :
-\forall n,m:nat. O < n \to O < m \to
+\forall n,m:nat. O < n \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.
+rewrite < H1.apply divides_b_to_Prop.
+assumption.
+qed.
+
+theorem decidable_divides: \forall n,m:nat.O < n \to
+decidable (divides n m).
+intros.change with (divides n m) \lor \not (divides n m).
+cut
+match divides_b n m with
+[ true \Rightarrow divides n m
+| false \Rightarrow \not (divides n m)] \to (divides n m) \lor \not (divides n m).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim (divides_b n m).left.apply H1.right.apply H1.
+qed.
+
+theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
+divides n m \to divides_b n m = true.
+intros.
+cut match (divides_b n m) with
+[ true \Rightarrow (divides n m)
+| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = true).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim divides_b n m.reflexivity.
+absurd (divides n m).assumption.assumption.
+qed.
+
+theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
+\not(divides n m) \to (divides_b n m) = false.
+intros.
+cut match (divides_b n m) with
+[ true \Rightarrow (divides n m)
+| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = false).
+apply Hcut.apply divides_b_to_Prop.assumption.
+elim divides_b n m.
+absurd (divides n m).assumption.assumption.
+reflexivity.
qed.
(* divides and pi *)
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.
simplify.reflexivity.
qed. *)
-(* not sure this is what we need *)
-theorem lt_S_O_smallest_factor:
+theorem lt_SO_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.
rewrite < sym_plus.simplify.reflexivity.
qed.
+theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
+intro.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_n O H.
+intro.apply nat_case m.intro.
+simplify.apply le_n.
+intros.apply trans_lt ? (S O).
+simplify. apply le_n.
+apply lt_SO_smallest_factor.simplify. apply le_S_S.
+apply le_S_S.apply le_O_n.
+qed.
+
theorem divides_smallest_factor_n :
-\forall n:nat. (S O) < n \to divides (smallest_factor n) n.
+\forall n:nat. 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.
+apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H.
+intro.apply nat_case m.intro. simplify.
+apply witness ? ? (S O). simplify.reflexivity.
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.
+apply lt_O_smallest_factor ? H.
change with
eqb (mod (S(S m1)) (min_aux m1 (S(S m1))
(\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true.
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.
+apply trans_lt ? (S O).apply le_n (S O).simplify.
+apply le_S_S.apply le_S_S.apply le_O_n.
qed.
theorem le_smallest_factor_n :
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.
+simplify.apply le_S_S.apply le_O_n.
qed.
theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
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.
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.
+apply lt_SO_smallest_factor.assumption.
intros.
cut le m (smallest_factor n).
elim le_to_or_lt_eq m (smallest_factor n) Hcut.
apply transitive_divides m (smallest_factor n).
assumption.
apply divides_smallest_factor_n.
-exact H.
+apply trans_lt ? (S O). simplify. apply le_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.
+apply lt_SO_smallest_factor.
exact H.
assumption.
qed.
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.
+apply trans_lt ? (S O).simplify. apply le_n.assumption.
+apply lt_SO_smallest_factor.
assumption.
qed.
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.
-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