From: Andrea Asperti Date: Thu, 3 Nov 2005 12:52:00 +0000 (+0000) Subject: Euler totient function is multiplicative! X-Git-Tag: V_0_7_2_3~150 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cca04138889cd0dbafb669a5c3fd8abe424d699e;p=helm.git Euler totient function is multiplicative! --- diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma index 5ebc08b6c..60bdbadc4 100644 --- a/helm/matita/library/nat/count.ma +++ b/helm/matita/library/nat/count.ma @@ -123,7 +123,8 @@ theorem count_times:\forall n,m:nat. (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 > (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 ? ? @@ -131,8 +132,10 @@ apply (trans_eq ? ? 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 > (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. diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 792629aaa..d42a57e8e 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -390,6 +390,16 @@ rewrite < H. apply divides_gcd_nm. qed. +theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n. +intros. +apply (nat_case1 (gcd m n)). +intros. +generalize in match (gcd_O_to_eq_O m n H1). +intros.elim H2. +rewrite < H4 in \vdash (? ? %).assumption. +intros.simplify.apply le_S_S.apply le_O_n. +qed. + theorem symmetric_gcd: symmetric nat gcd. change with (\forall n,m:nat. gcd n m = gcd m n). @@ -418,6 +428,33 @@ qed. variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def symmetric_gcd. +theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p). +intros. +apply (nat_case n).reflexivity. +intro. +apply divides_to_le. +apply lt_O_gcd. +rewrite > (times_n_O O). +apply lt_times.simplify.apply le_S_S.apply le_O_n.assumption. +apply divides_d_gcd. +apply (transitive_divides ? (S m1)). +apply divides_gcd_m. +apply (witness ? ? p).reflexivity. +apply divides_gcd_n. +qed. + +theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to +gcd m (n*p) = (S O) \to gcd m n = (S O). +intros. +apply antisymmetric_le. +rewrite < H2. +apply le_gcd_times.assumption. +change with (O < gcd m n). +apply lt_O_gcd.assumption. +qed. + +(* for the "converse" of the previous result see the end of this development *) + 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. @@ -432,7 +469,7 @@ 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 +theorem divides_gcd_mod: \forall m,n:nat. O < n \to divides (gcd m n) (gcd n (m \mod n)). intros. apply divides_d_gcd. @@ -442,7 +479,7 @@ apply divides_gcd_m. apply divides_gcd_m. qed. -theorem divides_mod_gcd: \forall m,n:nat. O < n \to O < m \to +theorem divides_mod_gcd: \forall m,n:nat. O < n \to divides (gcd n (m \mod n)) (gcd m n) . intros. apply divides_d_gcd. @@ -453,6 +490,14 @@ apply divides_gcd_m. apply divides_gcd_n. qed. +theorem gcd_mod: \forall m,n:nat. O < n \to +(gcd n (m \mod n)) = (gcd m n) . +intros. +apply antisymmetric_divides. +apply divides_mod_gcd.assumption. +apply divides_gcd_mod.assumption. +qed. + (* gcd and primes *) theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to @@ -515,3 +560,49 @@ apply (decidable_divides n p). apply (trans_lt ? (S O)).simplify.apply le_n. simplify in H.elim H. assumption. qed. + +theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to +gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O). +intros. +apply antisymmetric_le. +apply not_lt_to_le. +unfold Not.intro. +cut (divides (smallest_factor (gcd m (n*p))) n \lor + divides (smallest_factor (gcd m (n*p))) p). +elim Hcut. +apply (not_le_Sn_n (S O)). +change with ((S O) < (S O)). +rewrite < H2 in \vdash (? ? %). +apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))). +apply lt_SO_smallest_factor.assumption. +apply divides_to_le. +rewrite > H2.simplify.apply le_n. +apply divides_d_gcd.assumption. +apply (transitive_divides ? (gcd m (n*p))). +apply divides_smallest_factor_n. +apply (trans_lt ? (S O)). simplify. apply le_n. assumption. +apply divides_gcd_n. +apply (not_le_Sn_n (S O)). +change with ((S O) < (S O)). +rewrite < H3 in \vdash (? ? %). +apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))). +apply lt_SO_smallest_factor.assumption. +apply divides_to_le. +rewrite > H3.simplify.apply le_n. +apply divides_d_gcd.assumption. +apply (transitive_divides ? (gcd m (n*p))). +apply divides_smallest_factor_n. +apply (trans_lt ? (S O)). simplify. apply le_n. assumption. +apply divides_gcd_n. +apply divides_times_to_divides. +apply prime_smallest_factor_n. +assumption. +apply (transitive_divides ? (gcd m (n*p))). +apply divides_smallest_factor_n. +apply (trans_lt ? (S O)). simplify. apply le_n. assumption. +apply divides_gcd_m. +change with (O < gcd m (n*p)). +apply lt_O_gcd. +rewrite > (times_n_O O). +apply lt_times.assumption.assumption. +qed. diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 74fd74e74..452adc89c 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -150,6 +150,23 @@ assumption. apply (decidable_le n m). qed. +theorem antisymmetric_divides: antisymmetric nat divides. +simplify.intros.elim H. elim H1. +apply (nat_case1 n2).intro. +rewrite > H3.rewrite > H2.rewrite > H4. +rewrite < times_n_O.reflexivity. +intros. +apply (nat_case1 n).intro. +rewrite > H2.rewrite > H3.rewrite > H5. +rewrite < times_n_O.reflexivity. +intros. +apply antisymmetric_le. +rewrite > H2.rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r.rewrite > H4.apply le_S_S.apply le_O_n. +rewrite > H3.rewrite > times_n_SO in \vdash (? % ?). +apply le_times_r.rewrite > H5.apply le_S_S.apply le_O_n. +qed. + (* divides le *) theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m. intros. elim H1.rewrite > H2.cut (O < n2). diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma index 6715fe854..ff425772c 100644 --- a/helm/matita/library/nat/totient.ma +++ b/helm/matita/library/nat/totient.ma @@ -28,7 +28,6 @@ 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. @@ -66,4 +65,38 @@ rewrite > eq_to_eqb_true. rewrite > eq_to_eqb_true. reflexivity. rewrite < H4. -*) +rewrite > sym_gcd. +rewrite > gcd_mod. +apply (gcd_times_SO_to_gcd_SO ? ? (S m2)). +simplify.apply le_S_S.apply le_O_n. +simplify.apply le_S_S.apply le_O_n. +assumption. +simplify.apply le_S_S.apply le_O_n. +rewrite < H5. +rewrite > sym_gcd. +rewrite > gcd_mod. +apply (gcd_times_SO_to_gcd_SO ? ? (S m)). +simplify.apply le_S_S.apply le_O_n. +simplify.apply le_S_S.apply le_O_n. +rewrite > sym_times. +assumption. +simplify.apply le_S_S.apply le_O_n. +intro. +apply eqb_elim. +intro.apply eqb_elim. +intro.apply False_ind. +apply H6. +apply eq_gcd_times_SO. +simplify.apply le_S_S.apply le_O_n. +simplify.apply le_S_S.apply le_O_n. +rewrite < gcd_mod. +rewrite > H4. +rewrite > sym_gcd.assumption. +simplify.apply le_S_S.apply le_O_n. +rewrite < gcd_mod. +rewrite > H5. +rewrite > sym_gcd.assumption. +simplify.apply le_S_S.apply le_O_n. +intro.reflexivity. +intro.reflexivity. +qed. \ No newline at end of file