From 65312e560c25b49336241762107e401e7f9c5c3c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 2 Nov 2005 10:44:02 +0000 Subject: [PATCH] Totient function and related files. --- .../library/higher_order_defs/functions.ma | 1 + helm/matita/library/nat/chinese_reminder.ma | 251 ++++++++++++++++++ helm/matita/library/nat/compare.ma | 22 ++ helm/matita/library/nat/congruence.ma | 24 ++ helm/matita/library/nat/count.ma | 243 +++++++++++++++++ helm/matita/library/nat/gcd.ma | 23 ++ helm/matita/library/nat/minimization.ma | 11 + helm/matita/library/nat/minus.ma | 19 ++ helm/matita/library/nat/totient.ma | 67 +++++ 9 files changed, 661 insertions(+) create mode 100644 helm/matita/library/nat/chinese_reminder.ma create mode 100644 helm/matita/library/nat/count.ma create mode 100644 helm/matita/library/nat/totient.ma diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma index 78c2e2f89..a1b54c80c 100644 --- a/helm/matita/library/higher_order_defs/functions.ma +++ b/helm/matita/library/higher_order_defs/functions.ma @@ -64,3 +64,4 @@ definition distributive: \forall A:Type.\forall f,g:A \to A \to A.Prop definition distributive2: \forall A,B:Type.\forall f:A \to B \to B. \forall g: B\to B\to B. Prop \def \lambda A,B.\lambda f,g.\forall x:A.\forall y,z:B. f x (g y z) = g (f x y) (f x z). + diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma new file mode 100644 index 000000000..748b06632 --- /dev/null +++ b/helm/matita/library/nat/chinese_reminder.ma @@ -0,0 +1,251 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/chinese_reminder". + +include "nat/exp.ma". +include "nat/gcd.ma". +include "nat/permutation.ma". +include "nat/congruence.ma". + +theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to +gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n). +intros. +cut \exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O). +elim Hcut.elim H3.elim H4. +apply ex_intro nat ? ((a+b*m)*a1*n-b*a2*m). +split. +(* congruent to a *) +cut a1*n = a2*m + (S O). +rewrite > assoc_times. +rewrite > Hcut1. +rewrite < sym_plus ? (a2*m). +rewrite > distr_times_plus. +rewrite < times_n_SO. +rewrite > assoc_plus. +rewrite < assoc_times. +rewrite < times_plus_l. +rewrite > eq_minus_plus_plus_minus. +rewrite < times_minus_l. +rewrite > sym_plus. +apply eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2). +assumption.reflexivity. +apply le_times_l. +apply trans_le ? ((a+b*m)*a2). +apply le_times_l. +apply trans_le ? (b*m). +rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r.assumption. +apply le_plus_n. +apply le_plus_n. +apply minus_to_plus. +apply lt_to_le. +change with (O + a2*m < a1*n). +apply lt_minus_to_plus. +rewrite > H5.simplify.apply le_n. +assumption. +(* congruent to b *) +cut a2*m = a1*n - (S O). +rewrite > assoc_times b a2. +rewrite > Hcut1. +rewrite > distr_times_minus. +rewrite < assoc_times. +rewrite < eq_plus_minus_minus_minus. +rewrite < times_n_SO. +rewrite < times_minus_l. +rewrite < sym_plus. +apply eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1). +assumption.reflexivity. +rewrite > assoc_times. +apply le_times_r. +apply trans_le ? (a1*n - a2*m). +rewrite > H5.apply le_n. +apply le_minus_m ? (a2*m). +apply le_times_l. +apply le_times_l. +apply trans_le ? (b*m). +rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r.assumption. +apply le_plus_n. +apply sym_eq. apply plus_to_minus. +rewrite > sym_plus. +apply minus_to_plus. +apply lt_to_le. +change with (O + a2*m < a1*n). +apply lt_minus_to_plus. +rewrite > H5.simplify.apply le_n. +assumption. +(* and now the symmetric case; the price to pay for working + in nat instead than Z *) +apply ex_intro nat ? ((b+a*n)*a2*m-a*a1*n). +split. +(* congruent to a *) +cut a1*n = a2*m - (S O). +rewrite > assoc_times a a1. +rewrite > Hcut1. +rewrite > distr_times_minus. +rewrite < assoc_times. +rewrite < eq_plus_minus_minus_minus. +rewrite < times_n_SO. +rewrite < times_minus_l. +rewrite < sym_plus. +apply eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2). +assumption.reflexivity. +rewrite > assoc_times. +apply le_times_r. +apply trans_le ? (a2*m - a1*n). +rewrite > H5.apply le_n. +apply le_minus_m ? (a1*n). +rewrite > assoc_times.rewrite > assoc_times. +apply le_times_l. +apply trans_le ? (a*n). +rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r.assumption. +apply le_plus_n. +apply sym_eq.apply plus_to_minus. +rewrite > sym_plus. +apply minus_to_plus. +apply lt_to_le. +change with (O + a1*n < a2*m). +apply lt_minus_to_plus. +rewrite > H5.simplify.apply le_n. +assumption. +(* congruent to a *) +cut a2*m = a1*n + (S O). +rewrite > assoc_times. +rewrite > Hcut1. +rewrite > sym_plus (a1*n). +rewrite > distr_times_plus. +rewrite < times_n_SO. +rewrite < assoc_times. +rewrite > assoc_plus. +rewrite < times_plus_l. +rewrite > eq_minus_plus_plus_minus. +rewrite < times_minus_l. +rewrite > sym_plus. +apply eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1). +assumption.reflexivity. +apply le_times_l. +apply trans_le ? ((b+a*n)*a1). +apply le_times_l. +apply trans_le ? (a*n). +rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r. +assumption. +apply le_plus_n. +apply le_plus_n. +apply minus_to_plus. +apply lt_to_le. +change with (O + a1*n < a2*m). +apply lt_minus_to_plus. +rewrite > H5.simplify.apply le_n. +assumption. +(* proof of the cut *) +rewrite < H2. +apply eq_minus_gcd. +qed. + +theorem and_congruent_congruent_lt: \forall m,n,a,b:nat. O < n \to O < m \to +gcd n m = (S O) \to +ex nat (\lambda x. (congruent x a m \land congruent x b n) \land + (x < m*n)). +intros.elim and_congruent_congruent m n a b. +elim H3. +apply ex_intro ? ? (a1 \mod (m*n)). +split.split. +apply transitive_congruent m ? a1. +unfold congruent. +apply sym_eq. +change with congruent a1 (a1 \mod (m*n)) m. +rewrite < sym_times. +apply congruent_n_mod_times. +assumption.assumption.assumption. +apply transitive_congruent n ? a1. +unfold congruent. +apply sym_eq. +change with congruent a1 (a1 \mod (m*n)) n. +apply congruent_n_mod_times. +assumption.assumption.assumption. +apply lt_mod_m_m. +rewrite > times_n_O O. +apply lt_times.assumption.assumption. +assumption.assumption.assumption. +qed. + +definition cr_pair : nat \to nat \to nat \to nat \to nat \def +\lambda n,m,a,b. +min (pred (n*m)) (\lambda x. andb (eqb (x \mod n) a) (eqb (x \mod m) b)). + +theorem cr_pair1: cr_pair (S (S O)) (S (S (S O))) O O = O. +reflexivity. +qed. + +theorem cr_pair2: cr_pair (S(S O)) (S(S(S O))) (S O) O = (S(S(S O))). +simplify. +reflexivity. +qed. + +theorem cr_pair3: cr_pair (S(S O)) (S(S(S O))) (S O) (S(S O)) = (S(S(S(S(S O))))). +reflexivity. +qed. + +theorem cr_pair4: cr_pair (S(S(S(S(S O))))) (S(S(S(S(S(S(S O))))))) (S(S(S O))) (S(S O)) = +(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S O))))))))))))))))))))))). +reflexivity. +qed. + +theorem mod_cr_pair : \forall m,n,a,b. a \lt m \to b \lt n \to +gcd n m = (S O) \to +(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b. +intros. +cut andb (eqb ((cr_pair m n a b) \mod m) a) + (eqb ((cr_pair m n a b) \mod n) b) = true. +generalize in match Hcut. +apply andb_elim. +apply eqb_elim.intro. +rewrite > H3. +change with +eqb ((cr_pair m n a b) \mod n) b = true +\to a = a \land (cr_pair m n a b) \mod n = b. +intro.split.reflexivity. +apply eqb_true_to_eq.assumption. +intro. +change with false = true \to +(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b. +intro.apply False_ind. +apply not_eq_true_false.apply sym_eq.assumption. +apply f_min_aux_true +(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n)). +elim and_congruent_congruent_lt m n a b. +apply ex_intro ? ? a1.split.split. +rewrite < minus_n_n.apply le_O_n. +elim H3.apply le_S_S_to_le.apply trans_le ? (m*n). +assumption.apply nat_case (m*n).apply le_O_n. +intro. +rewrite < pred_Sn.apply le_n. +elim H3.elim H4. +apply andb_elim. +cut a1 \mod m = a. +cut a1 \mod n = b. +rewrite > eq_to_eqb_true ? ? Hcut. +rewrite > eq_to_eqb_true ? ? Hcut1. +simplify.reflexivity. +rewrite < lt_to_eq_mod b n.assumption. +assumption. +rewrite < lt_to_eq_mod a m.assumption. +assumption. +apply le_to_lt_to_lt ? b.apply le_O_n.assumption. +apply le_to_lt_to_lt ? a.apply le_O_n.assumption. +assumption. +qed. \ No newline at end of file diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index 6431f5f29..e85a80265 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -69,6 +69,28 @@ intro.elim n.simplify.reflexivity. simplify.assumption. qed. +theorem eqb_true_to_eq: \forall n,m:nat. +eqb n m = true \to n = m. +intros. +change with +match true with +[ true \Rightarrow n = m +| false \Rightarrow n \neq m]. +rewrite < H. +apply eqb_to_Prop. +qed. + +theorem eqb_false_to_not_eq: \forall n,m:nat. +eqb n m = false \to n \neq m. +intros. +change with +match false with +[ true \Rightarrow n = m +| false \Rightarrow n \neq m]. +rewrite < H. +apply eqb_to_Prop. +qed. + theorem eq_to_eqb_true: \forall n,m:nat. n = m \to eqb n m = true. intros.apply (eqb_elim n m). diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma index 7681f191f..6bc2b6f68 100644 --- a/helm/matita/library/nat/congruence.ma +++ b/helm/matita/library/nat/congruence.ma @@ -52,12 +52,36 @@ assumption. assumption. qed. +theorem mod_times_mod : \forall n,m,p:nat. O

times_plus_l. +rewrite > assoc_plus. +rewrite < div_mod. +rewrite > assoc_times. +rewrite < div_mod. +reflexivity. +rewrite > times_n_O O. +apply lt_times. +assumption.assumption.assumption. +qed. + theorem congruent_n_mod_n : \forall n,p:nat. O < p \to congruent n (n \mod p) p. intros.unfold congruent. apply mod_mod.assumption. qed. +theorem congruent_n_mod_times : +\forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p. +intros.unfold congruent. +apply mod_times_mod.assumption.assumption. +qed. + theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to n = r*p+m \to congruent n m p. intros.unfold congruent. diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma new file mode 100644 index 000000000..b1cb31cf3 --- /dev/null +++ b/helm/matita/library/nat/count.ma @@ -0,0 +1,243 @@ +(**************************************************************************) +(* __ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/count". + +include "nat/relevant_equations.ma". +include "nat/sigma_and_pi.ma". +include "nat/permutation.ma". + +theorem sigma_f_g : \forall n,m:nat.\forall f,g:nat \to nat. +sigma n (\lambda p.f p + g p) m = sigma n f m + sigma n g m. +intros.elim n. +simplify.reflexivity. +simplify.rewrite > H. +rewrite > assoc_plus. +rewrite < assoc_plus (g (S (n1+m))). +rewrite > sym_plus (g (S (n1+m))). +rewrite > assoc_plus (sigma n1 f m). +rewrite < assoc_plus. +reflexivity. +qed. + +theorem sigma_plus: \forall n,p,m:nat.\forall f:nat \to nat. +sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m. +intros. elim p. +simplify. +rewrite < sym_plus n m.reflexivity. +simplify. +rewrite > assoc_plus in \vdash (? ? ? %). +rewrite < H. +simplify. +rewrite < plus_n_Sm. +rewrite > sym_plus n. +rewrite > assoc_plus. +rewrite < sym_plus m. +rewrite < assoc_plus n1. +reflexivity. +qed. + +theorem sigma_plus1: \forall n,p,m:nat.\forall f:nat \to nat. +sigma (p+(S n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m. +intros. elim p. +simplify.reflexivity. +simplify. +rewrite > assoc_plus in \vdash (? ? ? %). +rewrite < H. +rewrite < plus_n_Sm. +rewrite < plus_n_Sm.simplify. +rewrite < sym_plus n. +rewrite > assoc_plus. +rewrite < sym_plus m. +rewrite < assoc_plus n. +reflexivity. +qed. + +theorem eq_sigma_sigma : \forall n,m:nat.\forall f:nat \to nat. +sigma (pred ((S n)*(S m))) f O = +sigma m (\lambda a.(sigma n (\lambda b.f (b*(S m) + a)) O)) O. +intro.elim n.simplify. +rewrite < plus_n_O. +apply eq_sigma.intros.reflexivity. +change with +sigma (m+(S n1)*(S m)) f O = +sigma m (\lambda a.(f ((S(n1+O))*(S m)+a)) + (sigma n1 (\lambda b.f (b*(S m)+a)) O)) O. +rewrite > sigma_f_g. +rewrite < plus_n_O. +rewrite < H. +rewrite > S_pred ((S n1)*(S m)). +apply sigma_plus1. +simplify.apply le_S_S.apply le_O_n. +qed. + +theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat. +sigma (pred ((S n)*(S m))) f O = +sigma n (\lambda a.(sigma m (\lambda b.f (b*(S n) + a)) O)) O. +intros. +rewrite > sym_times. +apply eq_sigma_sigma. +qed. + +theorem sigma_times: \forall n,m,p:nat.\forall f:nat \to nat. +(sigma n f m)*p = sigma n (\lambda i.(f i) * p) m. +intro. elim n.simplify.reflexivity. +simplify.rewrite < H. +apply times_plus_l. +qed. + +definition bool_to_nat: bool \to nat \def +\lambda b. match b with +[ true \Rightarrow (S O) +| false \Rightarrow O ]. + +theorem bool_to_nat_andb: \forall a,b:bool. +bool_to_nat (andb a b) = (bool_to_nat a)*(bool_to_nat b). +intros. elim a.elim b. +simplify.reflexivity. +reflexivity. +reflexivity. +qed. + +definition count : nat \to (nat \to bool) \to nat \def +\lambda n.\lambda f. sigma (pred n) (\lambda n.(bool_to_nat (f n))) O. + +theorem count_times:\forall n,m:nat. +\forall f,f1,f2:nat \to bool. +\forall g:nat \to nat \to nat. +\forall g1,g2: nat \to nat. +(\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to +(\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to +(\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to +(\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to +(count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2). +intros.unfold count. +rewrite < eq_map_iter_i_sigma. +rewrite > permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? (\lambda i.g (div i (S n)) (mod i (S n))). +rewrite > eq_map_iter_i_sigma. +rewrite > eq_sigma_sigma1. +apply trans_eq ? ? +(sigma n (\lambda a. + sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O). +apply eq_sigma.intros. +apply eq_sigma.intros. +rewrite > div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i. +rewrite > div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i. +rewrite > H3. +apply bool_to_nat_andb. +simplify.apply le_S_S.assumption. +simplify.apply le_S_S.assumption. +apply div_mod_spec_div_mod. +simplify.apply le_S_S.apply le_O_n. +constructor 1.simplify.apply le_S_S.assumption. +reflexivity. +apply div_mod_spec_div_mod. +simplify.apply le_S_S.apply le_O_n. +constructor 1.simplify.apply le_S_S.assumption. +reflexivity. +apply trans_eq ? ? +(sigma n (\lambda n.((bool_to_nat (f1 n)) * +(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O). +apply eq_sigma. +intros. +rewrite > sym_times. +apply trans_eq ? ? +(sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O). +reflexivity. +apply sym_eq. apply sigma_times. +change in match (pred (S n)) with n. +change in match (pred (S m)) with m. +apply sym_eq. apply sigma_times. +unfold permut. +split. +intros. +rewrite < plus_n_O. +apply le_S_S_to_le. +rewrite < S_pred in \vdash (? ? %). +change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)). +apply H. +apply lt_mod_m_m. +simplify. apply le_S_S.apply le_O_n. +apply lt_times_to_lt_l n. +apply le_to_lt_to_lt ? i. +rewrite > div_mod i (S n) in \vdash (? ? %). +rewrite > sym_plus. +apply le_plus_n. +simplify. apply le_S_S.apply le_O_n. +unfold lt. +rewrite > S_pred in \vdash (? ? %). +apply le_S_S. +rewrite > plus_n_O in \vdash (? ? %). +rewrite > sym_times. assumption. +rewrite > times_n_O O. +apply lt_times. +simplify. apply le_S_S.apply le_O_n. +simplify. apply le_S_S.apply le_O_n. +rewrite > times_n_O O. +apply lt_times. +simplify. apply le_S_S.apply le_O_n. +simplify. apply le_S_S.apply le_O_n. +rewrite < plus_n_O. +unfold injn. +intros. +cut i < (S n)*(S m). +cut j < (S n)*(S m). +cut (i \mod (S n)) < (S n). +cut (i/(S n)) < (S m). +cut (j \mod (S n)) < (S n). +cut (j/(S n)) < (S m). +rewrite > div_mod i (S n). +rewrite > div_mod j (S n). +rewrite < H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3. +rewrite < H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3 in \vdash (? ? (? % ?) ?). +rewrite < H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5. +rewrite < H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5 in \vdash (? ? ? (? % ?)). +rewrite > H6.reflexivity. +simplify. apply le_S_S.apply le_O_n. +simplify. apply le_S_S.apply le_O_n. +apply lt_times_to_lt_l n. +apply le_to_lt_to_lt ? j. +rewrite > div_mod j (S n) in \vdash (? ? %). +rewrite > sym_plus. +apply le_plus_n. +simplify. apply le_S_S.apply le_O_n. +rewrite < sym_times. assumption. +apply lt_mod_m_m. +simplify. apply le_S_S.apply le_O_n. +apply lt_times_to_lt_l n. +apply le_to_lt_to_lt ? i. +rewrite > div_mod i (S n) in \vdash (? ? %). +rewrite > sym_plus. +apply le_plus_n. +simplify. apply le_S_S.apply le_O_n. +rewrite < sym_times. assumption. +apply lt_mod_m_m. +simplify. apply le_S_S.apply le_O_n. +unfold lt. +rewrite > S_pred in \vdash (? ? %). +apply le_S_S.assumption. +rewrite > times_n_O O. +apply lt_times. +simplify. apply le_S_S.apply le_O_n. +simplify. apply le_S_S.apply le_O_n. +unfold lt. +rewrite > S_pred in \vdash (? ? %). +apply le_S_S.assumption. +rewrite > times_n_O O. +apply lt_times. +simplify. apply le_S_S.apply le_O_n. +simplify. apply le_S_S.apply le_O_n. +intros. +apply False_ind. +apply not_le_Sn_O m1 H4. +qed. diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 8cb4867ff..eb2043c98 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -432,6 +432,29 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. qed. +theorem divides_gcd_mod: \forall m,n:nat. O < n \to O < m \to +divides (gcd m n) (gcd n (m \mod n)). +intros. +apply divides_d_gcd. +apply divides_mod.assumption. +apply divides_gcd_n. +apply divides_gcd_m. +apply divides_gcd_m. +qed. + +theorem divides_mod_gcd: \forall m,n:nat. O < n \to O < m \to +divides (gcd n (m \mod n)) (gcd m n) . +intros. +apply divides_d_gcd. +apply divides_gcd_n. +apply divides_mod_to_divides ? ? n. +assumption. +apply divides_gcd_m. +apply divides_gcd_n. +qed. + +(* gcd and primes *) + theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to gcd n m = (S O). intros.simplify in H.change with (gcd n m = (S O)). diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma index bc60b50ac..94e4ee367 100644 --- a/helm/matita/library/nat/minimization.ma +++ b/helm/matita/library/nat/minimization.ma @@ -209,3 +209,14 @@ apply le_n_Sn. assumption. qed. +theorem le_min_aux_r : \forall f:nat \to bool. +\forall n,off:nat. (min_aux off n f) \le n. +intros. +elim off.simplify.rewrite < minus_n_O. +elim (f n).simplify.apply le_n. +simplify.apply le_n. +simplify.elim (f (n -(S n1))). +simplify.apply le_plus_to_minus. +rewrite < sym_plus.apply le_plus_n. +simplify.assumption. +qed. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 4910f3003..1ee70bd39 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -225,6 +225,16 @@ apply H.apply le_S_S_to_le. rewrite > plus_n_Sm.assumption. qed. +(* minus and lt - to be completed *) +theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p). +intros 3.apply nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)). +intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption. +simplify.intros.apply False_ind.apply not_le_Sn_O n H. +simplify.intros. +apply le_S_S. +rewrite < plus_n_Sm. +apply H.apply H1. +qed. theorem distributive_times_minus: distributive nat times minus. simplify. @@ -247,6 +257,15 @@ qed. theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p \def distributive_times_minus. +theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p). +intros. +apply plus_to_minus. +rewrite > sym_plus in \vdash (? ? ? %). +rewrite > assoc_plus. +rewrite < plus_minus_m_m. +reflexivity.assumption. +qed. + theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). intros. cut (m+p \le n \or m+p \nleq n). diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma new file mode 100644 index 000000000..7fc8d95ee --- /dev/null +++ b/helm/matita/library/nat/totient.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* __ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/totient". + +include "nat/count.ma". +include "nat/chinese_reminder.ma". + +definition totient : nat \to nat \def +\lambda n. count n (\lambda m. eqb (gcd m n) (S O)). + +theorem totient3: totient (S(S(S O))) = (S(S O)). +reflexivity. +qed. + +theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)). +reflexivity. +qed. + +theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to +totient (n*m) = (totient n)*(totient m). +intro. +apply nat_case n. +intro.simplify.intro.reflexivity. +intros 2.apply nat_case m1. +rewrite < sym_times. +rewrite < sym_times (totient O). +simplify.intro.reflexivity. +intros. +unfold totient. +apply count_times m m2 ? ? ? +(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)). +intros.unfold cr_pair. +apply le_to_lt_to_lt ? (pred ((S m)*(S m2))). +unfold min. +apply le_min_aux_r. +change with (S (pred ((S m)*(S m2)))) \le ((S m)*(S m2)). +apply nat_case ((S m)*(S m2)).apply le_n. +intro.apply le_n. +intros. +generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). +intro.elim H3. +apply H4. +intros. +generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). +intro.elim H3. +apply H5. +intros. +generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). +intro.elim H3. +apply eqb_elim. +intro. +rewrite > eq_to_eqb_true. +rewrite > eq_to_eqb_true. +reflexivity. +rewrite < H4. \ No newline at end of file -- 2.39.2