From 0a9ed4329c069d2e06902934b6d1d58d3690959c Mon Sep 17 00:00:00 2001 From: Cristian Armentano Date: Tue, 18 Sep 2007 17:47:29 +0000 Subject: [PATCH] some theorems have been moved to more appropriate files in library. --- matita/library/datatypes/bool.ma | 5 +- matita/library/nat/div_and_mod.ma | 29 +- matita/library/nat/gcd_properties1.ma | 214 ++--- matita/library/nat/generic_iter_p.ma | 2 +- matita/library/nat/lt_arith.ma | 157 ++++ matita/library/nat/primes.ma | 39 + .../nat/propr_div_mod_lt_le_totient1_aux.ma | 358 -------- matita/library/nat/totient1.ma | 825 ++++-------------- 8 files changed, 494 insertions(+), 1135 deletions(-) delete mode 100644 matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma diff --git a/matita/library/datatypes/bool.ma b/matita/library/datatypes/bool.ma index b5abbb35d..37a2a377d 100644 --- a/matita/library/datatypes/bool.ma +++ b/matita/library/datatypes/bool.ma @@ -163,11 +163,10 @@ elim A; reflexivity. qed. -theorem andb_t_t_t: \forall A,B,C:bool. -A = true \to B = true \to C = true \to (A \land (B \land C)) = true. +theorem true_to_true_to_andb_true: \forall A,B:bool. +A = true \to B = true \to (A \land B) = true. intros. rewrite > H. rewrite > H1. -rewrite > H2. reflexivity. qed. \ No newline at end of file diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma index d7750e39a..658b07b68 100644 --- a/matita/library/nat/div_and_mod.ma +++ b/matita/library/nat/div_and_mod.ma @@ -101,6 +101,16 @@ simplify. apply div_aux_mod_aux. qed. +theorem eq_times_div_minus_mod: +\forall a,b:nat. O \lt b \to +(a /b)*b = a - (a \mod b). +intros. +rewrite > (div_mod a b) in \vdash (? ? ? (? % ?)) +[ apply (minus_plus_m_m (times (div a b) b) (mod a b)) +| assumption +] +qed. + inductive div_mod_spec (n,m,q,r:nat) : Prop \def div_mod_spec_intro: r < m \to n=q*m+r \to (div_mod_spec n m q r). @@ -224,6 +234,15 @@ apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O); ] qed. +(*a simple variant of div_times theorem *) +theorem lt_O_to_div_times: \forall a,b:nat. O \lt b \to +a*b/b = a. +intros. +rewrite > sym_times. +rewrite > (S_pred b H). +apply div_times. +qed. + theorem div_n_n: \forall n:nat. O < n \to n / n = S O. intros. apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O). @@ -333,13 +352,3 @@ let rec n_divides_aux p n m acc \def (* n_divides n m = if m divides n q times, with remainder r *) definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. - -(*a simple variant of div_times theorem *) -theorem div_times_ltO: \forall a,b:nat. O \lt b \to -a*b/b = a. -intros. -rewrite > sym_times. -rewrite > (S_pred b H). -apply div_times. -qed. - diff --git a/matita/library/nat/gcd_properties1.ma b/matita/library/nat/gcd_properties1.ma index 535e7b42a..8687e2c1f 100644 --- a/matita/library/nat/gcd_properties1.ma +++ b/matita/library/nat/gcd_properties1.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/nat/gcd_properties1". -include "nat/propr_div_mod_lt_le_totient1_aux.ma". +include "nat/gcd.ma". (* this file contains some important properites of gcd in N *) @@ -238,107 +238,96 @@ apply gcd1 ] qed. -theorem divides_times_to_gcd_to_divides_div: \forall a,b,c,d:nat. -a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c. + +theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat. +O \lt m \to m \divides a \to m \divides b \to +(gcd (a/m) (b/m)) = (gcd a b) / m. +intros. +apply (inj_times_r1 m H). +rewrite > (sym_times m ((gcd a b)/m)). +rewrite > (divides_to_times_div (gcd a b) m) +[ rewrite < eq_gcd_times_times_times_gcd. + rewrite > (sym_times m (a/m)). + rewrite > (sym_times m (b/m)). + rewrite > (divides_to_times_div a m H H1). + rewrite > (divides_to_times_div b m H H2). + reflexivity +| assumption +| apply divides_d_gcd; + assumption +] +qed. + + + +theorem divides_times_to_divides_div_gcd: \forall a,b,c:nat. +a \divides (b*c) \to (a/(gcd a b)) \divides c. intros. apply (nat_case1 a) [ intros. apply (nat_case1 b) - [ intros. - cut (d = O) (*this is an impossible case*) + [ (*It's an impossible situation*) + intros. + simplify. + apply divides_SO_n + | intros. + cut (c = O) [ rewrite > Hcut. - simplify. - apply divides_SO_n - | rewrite > H2 in H1. - rewrite > H3 in H1. - apply sym_eq. - assumption - ] - | intros. - cut (O \lt d) - [ rewrite > (S_pred d Hcut). - simplify. - rewrite > H2 in H. - cut (c = O) - [ rewrite > Hcut1. - apply (divides_n_n O) - | apply (lt_times_eq_O b c) - [ rewrite > H3. - apply lt_O_S - | apply antisymmetric_divides - [ apply divides_n_O - | assumption - ] + apply (divides_n_n O) + | apply (lt_times_eq_O b c) + [ rewrite > H2. + apply lt_O_S + | apply antisymmetric_divides + [ apply divides_n_O + | rewrite < H1. + assumption ] ] - | rewrite < H1. - apply lt_O_gcd. - rewrite > H3. - apply lt_O_S ] ] | intros. - rewrite < H2. + rewrite < H1. elim H. - cut (d \divides a \land d \divides b) - [ cut (O \lt a) - [ cut (O \lt d) - [ elim Hcut. - rewrite < (NdivM_times_M_to_N a d) in H3 - [ rewrite < (NdivM_times_M_to_N b d) in H3 - [ cut (b/d*c = a/d*n2) - [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c) - [ apply (O_lt_times_to_O_lt (a/d) d). - rewrite > (NdivM_times_M_to_N a d); - assumption - | apply (inj_times_r1 d ? ?) - [ assumption - | rewrite < (eq_gcd_times_times_times_gcd (a/d) (b/d) d). - rewrite < (times_n_SO d). - rewrite < (sym_times (a/d) d). - rewrite < (sym_times (b/d) d). - rewrite > (NdivM_times_M_to_N a d) - [ rewrite > (NdivM_times_M_to_N b d); - assumption - | assumption - | assumption - ] - ] - | apply (witness (a/d) ((b/d)*c) n2 Hcut3) - ] - | apply (inj_times_r1 d ? ?) - [ assumption - | rewrite > sym_times. - rewrite > (sym_times d ((a/d) * n2)). - rewrite > assoc_times. - rewrite > (assoc_times (a/d) n2 d). - rewrite > (sym_times c d). - rewrite > (sym_times n2 d). - rewrite < assoc_times. - rewrite < (assoc_times (a/d) d n2). - assumption - ] - ] - | assumption + cut (O \lt a) + [ cut (O \lt (gcd a b)) + [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c) + [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)). + rewrite > (divides_to_times_div a (gcd a b)) + [ assumption + | assumption + | apply divides_gcd_n + ] + | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %) + [ apply eq_gcd_div_div_div_gcd + [ assumption + | apply divides_gcd_n + | apply divides_gcd_m + ] + | assumption + ] + | apply (witness ? ? n2). + apply (inj_times_r1 (gcd a b) Hcut1). + rewrite < assoc_times. + rewrite < sym_times in \vdash (? ? (? % ?) ?). + rewrite > (divides_to_times_div b (gcd a b)) + [ rewrite < assoc_times in \vdash (? ? ? %). + rewrite < sym_times in \vdash (? ? ? (? % ?)). + rewrite > (divides_to_times_div a (gcd a b)) + [ assumption | assumption + | apply divides_gcd_n ] | assumption - | assumption + | apply divides_gcd_m ] - | rewrite < H1. - rewrite > sym_gcd. - apply lt_O_gcd. - assumption ] - | rewrite > H2. - apply lt_O_S - ] - | rewrite < H1. - split - [ apply divides_gcd_n - | apply divides_gcd_m + | rewrite > sym_gcd. + apply lt_O_gcd. + assumption ] - ] + | rewrite > H1. + apply lt_O_S + ] ] qed. @@ -374,53 +363,14 @@ apply gcd1 qed. -theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat. -O \lt m \to m \divides a \to m \divides b \to -(gcd (a/m) (b/m)) = (gcd a b) / m. -intros. -apply (inj_times_r1 m H). -rewrite > (sym_times m ((gcd a b)/m)). -rewrite > (NdivM_times_M_to_N (gcd a b) m) -[ rewrite < eq_gcd_times_times_times_gcd. - rewrite > (sym_times m (a/m)). - rewrite > (sym_times m (b/m)). - rewrite > (NdivM_times_M_to_N a m H H1). - rewrite > (NdivM_times_M_to_N b m H H2). - reflexivity -| assumption -| apply divides_d_gcd; - assumption -] -qed. - theorem gcd_SO_to_divides_to_divides_to_divides_times: \forall c,e,f:nat. (gcd e f) = (S O) \to e \divides c \to f \divides c \to (e*f) \divides c. intros. -apply (nat_case1 e) -[ intros. - apply (nat_case1 c) - [ intros. - simplify. - apply (divides_n_n O). - | intros. - rewrite > H3 in H1. - apply False_ind. - cut (O \lt O) - [ apply (le_to_not_lt O O) - [ apply (le_n O) - | assumption - ] - | apply (divides_to_lt_O O c) - [ rewrite > H4. - apply lt_O_S - | assumption - ] - ] - ] -| intros. - rewrite < H3. +apply (nat_case1 c); intros +[ apply divides_n_O +| rewrite < H3. elim H1. elim H2. rewrite > H5. @@ -429,16 +379,18 @@ apply (nat_case1 e) [ apply (divides_n_n) | rewrite > H5 in H1. apply (gcd_SO_to_divides_times_to_divides f e n) - [ rewrite > H3. - apply (lt_O_S m) + [ rewrite < H5 in H1. + rewrite > H3 in H1. + apply (divides_to_lt_O e (S m)) + [ apply lt_O_S + | assumption + ] | assumption | assumption ] ] ] qed. - - (* the following theorem shows that gcd is a multiplicative function in the following sense: if a1 and a2 are relatively prime, then gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b). diff --git a/matita/library/nat/generic_iter_p.ma b/matita/library/nat/generic_iter_p.ma index 75100b3f5..c424f82e0 100644 --- a/matita/library/nat/generic_iter_p.ma +++ b/matita/library/nat/generic_iter_p.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/generic_iter_p.ma". +set "baseuri" "cic:/matita/nat/generic_iter_p". include "nat/primes.ma". include "nat/ord.ma". diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma index e71514726..cce6626a0 100644 --- a/matita/library/nat/lt_arith.ma +++ b/matita/library/nat/lt_arith.ma @@ -301,6 +301,162 @@ unfold lt. apply le_n.assumption. qed. +(* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *) +(* The theorem is shown in two different parts: *) + +theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat. +O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)). +intros. +split +[ rewrite < H1. + rewrite > sym_times. + rewrite > eq_times_div_minus_mod + [ apply (le_minus_m a (a \mod b)) + | assumption + ] +| rewrite < (times_n_Sm b c). + rewrite < H1. + rewrite > sym_times. + rewrite > (div_mod a b) in \vdash (? % ?) + [ rewrite > (sym_plus b ((a/b)*b)). + apply lt_plus_r. + apply lt_mod_m_m. + assumption + | assumption + ] +] +qed. + +theorem lt_to_le_times_to_lt_S_to_div: \forall a,c,b:nat. +O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c. +intros. +apply (le_to_le_to_eq) +[ apply (leb_elim (a/b) c);intros + [ assumption + | cut (c \lt (a/b)) + [ apply False_ind. + apply (lt_to_not_le (a \mod b) O) + [ apply (lt_plus_to_lt_l ((a/b)*b)). + simplify. + rewrite < sym_plus. + rewrite < div_mod + [ apply (lt_to_le_to_lt ? (b*(S c)) ?) + [ assumption + | rewrite > (sym_times (a/b) b). + apply le_times_r. + assumption + ] + | assumption + ] + | apply le_O_n + ] + | apply not_le_to_lt. + assumption + ] + ] +| apply (leb_elim c (a/b));intros + [ assumption + | cut((a/b) \lt c) + [ apply False_ind. + apply (lt_to_not_le (a \mod b) b) + [ apply (lt_mod_m_m). + assumption + | apply (le_plus_to_le ((a/b)*b)). + rewrite < (div_mod a b) + [ apply (trans_le ? (b*c) ?) + [ rewrite > (sym_times (a/b) b). + rewrite > (times_n_SO b) in \vdash (? (? ? %) ?). + rewrite < distr_times_plus. + rewrite > sym_plus. + simplify in \vdash (? (? ? %) ?). + apply le_times_r. + assumption + | assumption + ] + | assumption + ] + ] + | apply not_le_to_lt. + assumption + ] + ] +] +qed. + + +theorem lt_to_lt_to_eq_div_div_times_times: \forall a,b,c:nat. +O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c). +intros. +apply sym_eq. +cut (b*(a/b) \le a \land a \lt b*(S (a/b))) +[ elim Hcut. + apply lt_to_le_times_to_lt_S_to_div + [ rewrite > (S_pred b) + [ rewrite > (S_pred c) + [ apply (lt_O_times_S_S) + | assumption + ] + | assumption + ] + | rewrite > assoc_times. + rewrite > (sym_times c (a/b)). + rewrite < assoc_times. + rewrite > (sym_times (b*(a/b)) c). + rewrite > (sym_times a c). + apply (le_times_r c (b*(a/b)) a). + assumption + | rewrite > (sym_times a c). + rewrite > (assoc_times ). + rewrite > (sym_times c (S (a/b))). + rewrite < (assoc_times). + rewrite > (sym_times (b*(S (a/b))) c). + apply (lt_times_r1 c a (b*(S (a/b)))); + assumption + ] +| apply (lt_to_div_to_and_le_times_lt_S) + [ assumption + | reflexivity + ] +] +qed. + +theorem times_mod: \forall a,b,c:nat. +O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b). +intros. +apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b))) +[ rewrite > (lt_to_lt_to_eq_div_div_times_times a b c) + [ apply div_mod_spec_div_mod. + rewrite > (S_pred b) + [ rewrite > (S_pred c) + [ apply lt_O_times_S_S + | assumption + ] + | assumption + ] + | assumption + | assumption + ] +| apply div_mod_spec_intro + [ rewrite > (sym_times b c). + apply (lt_times_r1 c) + [ assumption + | apply (lt_mod_m_m). + assumption + ] + | rewrite < (assoc_times (a/b) b c). + rewrite > (sym_times a c). + rewrite > (sym_times ((a/b)*b) c). + rewrite < (distr_times_plus c ? ?). + apply eq_f. + apply (div_mod a b). + assumption + ] +] +qed. + + + + (* general properties of functions *) theorem monotonic_to_injective: \forall f:nat\to nat. monotonic nat lt f \to injective nat nat f. @@ -322,3 +478,4 @@ increasing f \to injective nat nat f. intros.apply monotonic_to_injective. apply increasing_to_monotonic.assumption. qed. + diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma index a95b2e88f..45f520d08 100644 --- a/matita/library/nat/primes.ma +++ b/matita/library/nat/primes.ma @@ -190,6 +190,45 @@ rewrite > H2.rewrite < H3. simplify.exact (not_le_Sn_n O). qed. +(*divides and div*) + +theorem divides_to_times_div: \forall n,m:nat. +O \lt m \to m \divides n \to (n / m) * m = n. +intros. +rewrite > plus_n_O. +apply sym_eq. +cut (n \mod m = O) +[ rewrite < Hcut. + apply div_mod. + assumption +| apply divides_to_mod_O; + assumption. +] +qed. + +(*to remove hypotesis b > 0*) +theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat. +O \lt b \to c \divides b \to a * (b /c) = (a*b)/c. +(*theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat. +c \divides b \to a * (b /c) = (a*b)/c.*) +intros. +elim H1. +rewrite > H2. +rewrite > (sym_times c n2). +cut(O \lt c) +[ rewrite > (lt_O_to_div_times n2 c) + [ rewrite < assoc_times. + rewrite > (lt_O_to_div_times (a *n2) c) + [ reflexivity + | assumption + ] + | assumption + ] +| apply (divides_to_lt_O c b); + assumption. +] +qed. + (* boolean divides *) definition divides_b : nat \to nat \to bool \def \lambda n,m :nat. (eqb (m \mod n) O). diff --git a/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma b/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma deleted file mode 100644 index f26f0ea00..000000000 --- a/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma +++ /dev/null @@ -1,358 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/". - -include "nat/iteration2.ma". - -(*this part of the library contains some properties useful to prove - the main theorem in totient1.ma, and some new properties about gcd - (see gcd_properties1.ma). - These theorems are saved separately from the other part of the library - in order to avoid to create circular dependences in it. - *) - -(* some basic properties of and - or*) -(*theorem andb_sym: \forall A,B:bool. -(A \land B) = (B \land A). -intros. -elim A; - elim B; - simplify; - reflexivity. -qed. - -theorem andb_assoc: \forall A,B,C:bool. -(A \land (B \land C)) = ((A \land B) \land C). -intros. -elim A; - elim B; - elim C; - simplify; - reflexivity. -qed. - -theorem orb_sym: \forall A,B:bool. -(A \lor B) = (B \lor A). -intros. -elim A; - elim B; - simplify; - reflexivity. -qed. - -theorem andb_t_t_t: \forall A,B,C:bool. -A = true \to B = true \to C = true \to (A \land (B \land C)) = true. -intros. -rewrite > H. -rewrite > H1. -rewrite > H2. -reflexivity. -qed. -*) -(*properties about relational operators*) - -theorem Sa_le_b_to_O_lt_b: \forall a,b:nat. -(S a) \le b \to O \lt b. -intros. -elim H; - apply lt_O_S. -qed. - - -theorem n_gt_Uno_to_O_lt_pred_n: \forall n:nat. -(S O) \lt n \to O \lt (pred n). -intros. -apply (Sa_le_b_to_O_lt_b (pred (S O)) (pred n) ?). - apply (lt_pred (S O) n ? ?); - [ apply (lt_O_S O) - | apply (H) - ] -qed. - - -theorem NdivM_times_M_to_N: \forall n,m:nat. -O \lt m \to m \divides n \to (n / m) * m = n. -intros. -rewrite > plus_n_O. -apply sym_eq. -cut (n \mod m = O) -[ rewrite < Hcut. - apply div_mod. - assumption -| apply divides_to_mod_O; - assumption. -] -qed. - -theorem lt_to_divides_to_div_le: \forall a,c:nat. -O \lt c \to c \divides a \to a/c \le a. -intros. -apply (le_times_to_le c (a/c) a) -[ assumption -| rewrite > (sym_times c (a/c)). - rewrite > (NdivM_times_M_to_N a c) in \vdash (? % ?) - [ apply (le_times_n c a ?). - assumption - | assumption - | assumption - ] -] -qed. - - -theorem lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb: -\forall a,b:nat. -O \lt a \to O \lt b \to a \divides b \to O \lt (b/a). -intros. -elim H2. -rewrite > H3. -rewrite > (sym_times a n2). -rewrite > (div_times_ltO n2 a) -[ apply (divides_to_lt_O n2 b) - [ assumption - | apply (witness n2 b a). - rewrite > sym_times. - assumption - ] -| assumption -] -qed. - -(* some properties of div operator between natural numbers *) - -theorem separazioneFattoriSuDivisione: \forall a,b,c:nat. -O \lt b \to c \divides b \to a * (b /c) = (a*b)/c. -intros. -elim H1. -rewrite > H2. -rewrite > (sym_times c n2). -cut(O \lt c) -[ rewrite > (div_times_ltO n2 c) - [ rewrite < assoc_times. - rewrite > (div_times_ltO (a *n2) c) - [ reflexivity - | assumption - ] - | assumption - ] -| apply (divides_to_lt_O c b); - assumption. -] -qed. - - -theorem div_mod_minus: -\forall a,b:nat. O \lt b \to -(a /b)*b = a - (a \mod b). -intros. -rewrite > (div_mod a b) in \vdash (? ? ? (? % ?)) -[ apply (minus_plus_m_m (times (div a b) b) (mod a b)) -| assumption -] -qed. - - -(* A corollary to the division theorem (between natural numbers). - * - * Forall a,b,c: Nat, b > O, - * a/b = c iff (b*c <= a && a < b*(c+1) - * - * two parts of the theorem are proved separately - * - (=>) th_div_interi_2 - * - (<=) th_div_interi_1 - *) - -theorem th_div_interi_2: \forall a,b,c:nat. -O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)). -intros. -split -[ rewrite < H1. - rewrite > sym_times. - rewrite > div_mod_minus - [ apply (le_minus_m a (a \mod b)) - | assumption - ] -| rewrite < (times_n_Sm b c). - rewrite < H1. - rewrite > sym_times. - rewrite > (div_mod a b) in \vdash (? % ?) - [ rewrite > (sym_plus b ((a/b)*b)). - apply lt_plus_r. - apply lt_mod_m_m. - assumption - | assumption - ] -] -qed. - - -theorem th_div_interi_1: \forall a,c,b:nat. -O \lt b \to (b*c) \le a \to a \lt (b*(S c)) \to a/b = c. -intros. -apply (le_to_le_to_eq) -[ apply (leb_elim (a/b) c);intros - [ assumption - | cut (c \lt (a/b)) - [ apply False_ind. - apply (lt_to_not_le (a \mod b) O) - [ apply (lt_plus_to_lt_l ((a/b)*b)). - simplify. - rewrite < sym_plus. - rewrite < div_mod - [ apply (lt_to_le_to_lt ? (b*(S c)) ?) - [ assumption - | rewrite > (sym_times (a/b) b). - apply le_times_r. - assumption - ] - | assumption - ] - | apply le_O_n - ] - | apply not_le_to_lt. - assumption - ] - ] -| apply (leb_elim c (a/b));intros - [ assumption - | cut((a/b) \lt c) - [ apply False_ind. - apply (lt_to_not_le (a \mod b) b) - [ apply (lt_mod_m_m). - assumption - | apply (le_plus_to_le ((a/b)*b)). - rewrite < (div_mod a b) - [ apply (trans_le ? (b*c) ?) - [ rewrite > (sym_times (a/b) b). - rewrite > (times_n_SO b) in \vdash (? (? ? %) ?). - rewrite < distr_times_plus. - rewrite > sym_plus. - simplify in \vdash (? (? ? %) ?). - apply le_times_r. - assumption - | assumption - ] - | assumption - ] - ] - | apply not_le_to_lt. - assumption - ] - ] -] -qed. - - -theorem times_numerator_denominator_aux: \forall a,b,c,d:nat. -O \lt c \to O \lt b \to d = (a/b) \to d= (a*c)/(b*c). -intros. -apply sym_eq. -cut (b*d \le a \land a \lt b*(S d)) -[ elim Hcut. - apply th_div_interi_1 - [ rewrite > (S_pred b) - [ rewrite > (S_pred c) - [ apply (lt_O_times_S_S) - | assumption - ] - | assumption - ] - | rewrite > assoc_times. - rewrite > (sym_times c d). - rewrite < assoc_times. - rewrite > (sym_times (b*d) c). - rewrite > (sym_times a c). - apply (le_times_r c (b*d) a). - assumption - | rewrite > (sym_times a c). - rewrite > (assoc_times ). - rewrite > (sym_times c (S d)). - rewrite < (assoc_times). - rewrite > (sym_times (b*(S d)) c). - apply (lt_times_r1 c a (b*(S d))); - assumption - ] -| apply (th_div_interi_2) - [ assumption - | apply sym_eq. - assumption - ] -] -qed. - -theorem times_numerator_denominator: \forall a,b,c:nat. -O \lt c \to O \lt b \to (a/b) = (a*c)/(b*c). -intros. -apply (times_numerator_denominator_aux a b c (a/b)) -[ assumption -| assumption -| reflexivity -] -qed. - -theorem times_mod: \forall a,b,c:nat. -O \lt c \to O \lt b \to ((a*c) \mod (b*c)) = c*(a\mod b). -intros. -apply (div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b))) -[ apply div_mod_spec_intro - [ apply (lt_mod_m_m (a*c) (b*c)). - rewrite > (S_pred b) - [ rewrite > (S_pred c) - [ apply lt_O_times_S_S - | assumption - ] - | assumption - ] - | rewrite > (times_numerator_denominator a b c) - [ apply (div_mod (a*c) (b*c)). - rewrite > (S_pred b) - [ rewrite > (S_pred c) - [ apply (lt_O_times_S_S) - | assumption - ] - | assumption - ] - | assumption - | assumption - ] - ] -| constructor 1 - [ rewrite > (sym_times b c). - apply (lt_times_r1 c) - [ assumption - | apply (lt_mod_m_m). - assumption - ] - | rewrite < (assoc_times (a/b) b c). - rewrite > (sym_times a c). - rewrite > (sym_times ((a/b)*b) c). - rewrite < (distr_times_plus c ? ?). - apply eq_f. - apply (div_mod a b). - assumption - ] -] -qed. - - - - - - - - - - - diff --git a/matita/library/nat/totient1.ma b/matita/library/nat/totient1.ma index 5ce43d4ac..3d6b6fafc 100644 --- a/matita/library/nat/totient1.ma +++ b/matita/library/nat/totient1.ma @@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/nat/totient1". include "nat/totient.ma". include "nat/iteration2.ma". -include "nat/propr_div_mod_lt_le_totient1_aux.ma". include "nat/gcd_properties1.ma". (* This file contains the proof of the following theorem about Euler's totient @@ -25,686 +24,248 @@ include "nat/gcd_properties1.ma". The sum of the applications of Phi function over the divisor of a natural number n is equal to n *) - -(*two easy properties of gcd, directly obtainable from the more general theorem - eq_gcd_times_times_eqv_times_gcd*) -theorem gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO:\forall a,b,d:nat. -O \lt d \to O \lt b \to gcd (b*d) (a*d) = d \to (gcd a b) = (S O). +theorem eq_div_times_div_times: \forall a,b,c:nat. +O \lt b \to b \divides a \to b \divides c \to +a / b * c = a * (c/b). intros. -apply (inj_times_r1 d) -[ assumption -| rewrite < (times_n_SO d). - rewrite < (eq_gcd_times_times_eqv_times_gcd a b d). - rewrite > sym_gcd. - rewrite > (sym_times d a). - rewrite > (sym_times d b). - assumption -] -qed. - -theorem gcd_SO_to_gcd_times: \forall a,b,c:nat. -O \lt c \to (gcd a b) = (S O) \to (gcd (a*c) (b*c)) = c. -intros. -rewrite > (sym_times a c). -rewrite > (sym_times b c). -rewrite > (eq_gcd_times_times_eqv_times_gcd a b c). -rewrite > H1. -apply sym_eq. -apply times_n_SO. +elim H1. +elim H2. +rewrite > H3. +rewrite > H4. +rewrite > (sym_times) in \vdash (? ? ? (? ? (? % ?))). +rewrite > (sym_times) in \vdash (? ? (? (? % ?) ?) ?). +rewrite > (lt_O_to_div_times ? ? H). +rewrite > (lt_O_to_div_times ? ? H) in \vdash (? ? ? (? ? %)). +rewrite > (sym_times b n2). +rewrite > assoc_times. +reflexivity. qed. - - -(* The proofs of the 6 sub-goals activated after the application of the theorem - eq_sigma_p_gh in the proof of the main theorem - *) - - - -(* 2nd*) -theorem sum_divisor_totient1_aux2: \forall i,n:nat. -(S O) \lt n \to i (sym_times ((pred n)/(i/n)) (i/n)). - cut ((i \mod n)*(pred n)/(i/n) = (i \mod n) * ((pred n) / (i/n))) - [ rewrite > Hcut2. - apply (gcd_SO_to_gcd_times (i/n) (i \mod n) ((pred n)/(i/n))) - [ apply (lt_O_a_lt_O_b_a_divides_b_to_lt_O_aDIVb (i/n) (pred n)); - assumption - | rewrite > sym_gcd. - assumption - ] - | apply sym_eq. - apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n)); - assumption. - ] - | assumption - | assumption - ] - | apply (divides_to_lt_O (i/n) (pred n)); - assumption - ] -| apply n_gt_Uno_to_O_lt_pred_n. - assumption. -] -qed. - -(*3rd*) -theorem aux_S_i_mod_n_le_i_div_n: \forall i,n:nat. -i < n*n \to (divides_b (i/n) (pred n) \land - (leb (S(i\mod n)) (i/n) \land - eqb (gcd (i\mod n) (i/n)) (S O))) =true - \to - (S (i\mod n)) \le (i/n). -intros. -cut (leb (S (i \mod n)) (i/n) = true) -[ change with ( - match (true) with - [ true \Rightarrow (S (i \mod n)) \leq (i/n) - | false \Rightarrow (S (i \mod n)) \nleq (i/n)] - ). - rewrite < Hcut. - apply (leb_to_Prop (S(i \mod n)) (i/n)) -| apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ). - apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n))) - (eqb (gcd (i\mod n) (i/n)) (S O)) - ). - rewrite > andb_sym in \vdash (? ? (? % ?) ?). - rewrite < (andb_assoc) in \vdash (? ? % ?). - assumption +apply (O_lt_times_to_O_lt ? a). +rewrite > (divides_to_times_div b a) +[ assumption +| apply (divides_to_lt_O a b H H1) +| assumption ] qed. - -(*the following theorem is just a particular case of the theorem - divides_times, prooved in primes.ma - *) -theorem a_divides_b_to_a_divides_b_times_c: \forall a,b,c:nat. -a \divides b \to a \divides (b*c). -intros. -rewrite > (times_n_SO a). -apply (divides_times). -assumption. -apply divides_SO_n. -qed. - -theorem sum_divisor_totient1_aux_3: \forall i,n:nat. -(S O) \lt n \to i < n*n \to - (divides_b (i/n) (pred n) -\land (leb (S(i\mod n)) (i/n) -\land eqb (gcd (i\mod n) (i/n)) (S O))) - =true - \to i\mod n*pred n/(i/n)<(pred n). -intros. -apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n)) - ((i/n)*(pred n) / (i/n)) - (pred n)) -[ apply (lt_times_n_to_lt (i/n) ((i\mod n)*(pred n)/(i/n)) ((i/n)*(pred n)/(i/n))) - [ apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)). - apply (aux_S_i_mod_n_le_i_div_n i n); - assumption. - | rewrite > (NdivM_times_M_to_N ) - [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %) - [ apply (monotonic_lt_times_variant (pred n)) - [ apply n_gt_Uno_to_O_lt_pred_n. - assumption - | change with ((S (i\mod n)) \le (i/n)). - apply (aux_S_i_mod_n_le_i_div_n i n); - assumption - ] - | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)). - apply (aux_S_i_mod_n_le_i_div_n i n); +(*tha main theorem*) +theorem sigma_p_Sn_divides_b_totient_n': \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n. +intros. +unfold totient. +apply (trans_eq ? ? +(sigma_p (S n) (\lambda d:nat.divides_b d n) +(\lambda d:nat.sigma_p (S n) (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O)))) +[ apply eq_sigma_p1 + [ intros. + reflexivity + | intros. + apply sym_eq. + apply (trans_eq ? ? + (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O))) + [ apply false_to_eq_sigma_p + [ apply lt_to_le. + assumption + | intros. + rewrite > lt_to_leb_false + [ reflexivity + | apply le_S_S. assumption - | rewrite > (times_n_SO (i/n)) in \vdash (? % ?). - apply (divides_times). - apply divides_n_n. - apply divides_SO_n + ] ] - | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)). - apply (aux_S_i_mod_n_le_i_div_n i n); - assumption - | rewrite > (times_n_SO (i/n)). - rewrite > (sym_times (i \mod n) (pred n)). - apply (divides_times) - [ apply divides_b_true_to_divides. - apply (andb_true_true (divides_b (i/n) (pred n)) (leb (S (i\mod n)) (i/n))). - apply (andb_true_true - ((divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n))) - (eqb (gcd (i\mod n) (i/n)) (S O))). - rewrite < (andb_assoc) in \vdash (? ? % ?). - assumption - | apply divides_SO_n + | apply eq_sigma_p + [ intros. + rewrite > le_to_leb_true + [ reflexivity + | assumption + ] + | intros. + reflexivity ] ] ] -| rewrite > (sym_times). - rewrite > (div_times_ltO ) - [ apply (le_n (pred n)) - | apply (Sa_le_b_to_O_lt_b (i \mod n) (i/n)). - apply (aux_S_i_mod_n_le_i_div_n i n); - assumption. - ] -]qed. - - -(*4th*) -theorem sum_divisor_totient1_aux_4: \forall j,n:nat. -j \lt (pred n) \to (S O) \lt n \to -((divides_b ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) (pred n)) - \land ((leb (S ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n)) - ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) - \land (eqb - (gcd ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)\mod n) - ((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n)) (S O)))) -=true. -intros. -cut (O \lt (pred n)) -[ cut ( O \lt (gcd (pred n) j)) - [ cut (j/(gcd (pred n) j) \lt n) - [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j)/n) = pred n/gcd (pred n) j) - [ cut (((pred n/gcd (pred n) j*n+j/gcd (pred n) j) \mod n) = j/gcd (pred n) j) - [ rewrite > Hcut3. - rewrite > Hcut4. - apply andb_t_t_t - [ apply divides_to_divides_b_true - [ apply (lt_times_n_to_lt (gcd (pred n) j) O (pred n/gcd (pred n) j)) - [ assumption - | rewrite > (sym_times O (gcd (pred n) j)). - rewrite < (times_n_O (gcd (pred n) j)). - rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j)) +| apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O))) + [ apply sym_eq. + apply (sigma_p_knm + (\lambda x. (S O)) + (\lambda i,j.j*(n/i)) + (\lambda p. n / (gcd p n)) + (\lambda p. p / (gcd p n)) + );intros + [ cut (O \lt (gcd x n)) + [split + [ split + [ split + [ split + [ apply divides_to_divides_b_true + [ apply (O_lt_times_to_O_lt ? (gcd x n)). + rewrite > (divides_to_times_div n (gcd x n)) [ assumption | assumption - | apply (divides_gcd_n (pred n)) + | apply (divides_gcd_m) ] + | rewrite > sym_gcd. + apply (divides_times_to_divides_div_gcd). + apply (witness n (x * n) x). + apply (symmetric_times x n) ] - | apply (witness (pred n/(gcd (pred n) j)) (pred n) (gcd (pred n) j)). - rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j)) - [ reflexivity - | assumption - | apply (divides_gcd_n (pred n)) - ] - ] - | apply (le_to_leb_true). - apply lt_S_to_le. - apply cic:/matita/algebra/finite_groups/lt_S_S.con. - apply (lt_times_n_to_lt (gcd (pred n) j) ? ?) - [ assumption - | rewrite > (NdivM_times_M_to_N j (gcd (pred n) j)) - [ rewrite > (NdivM_times_M_to_N (pred n) (gcd (pred n) j)) + | apply (true_to_true_to_andb_true) + [ apply (le_to_leb_true). + change with (x/(gcd x n) \lt n/(gcd x n)). + apply (lt_times_n_to_lt (gcd x n) ? ?) [ assumption + | rewrite > (divides_to_times_div x (gcd x n)) + [ rewrite > (divides_to_times_div n (gcd x n)) + [ assumption + | assumption + | apply divides_gcd_m + ] + | assumption + | apply divides_gcd_n + ] + ] + | apply cic:/matita/nat/compare/eq_to_eqb_true.con. + rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n)) + [ apply (div_n_n (gcd x n) Hcut) | assumption | apply divides_gcd_n + | apply divides_gcd_m ] - | assumption - | rewrite > sym_gcd. - apply divides_gcd_n ] - ] - | apply cic:/matita/nat/compare/eq_to_eqb_true.con. - apply (gcd_bTIMESd_aTIMESd_eq_d_to_gcd_a_b_eq_SO ? ? (gcd (pred n) j)) - [ assumption - | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?) + ] + | apply (inj_times_l1 (n/(gcd x n))) + [ apply lt_O_to_divides_to_lt_O_div [ assumption - | simplify. - rewrite > NdivM_times_M_to_N + | apply divides_gcd_m + ] + | rewrite > associative_times. + rewrite > (divides_to_times_div n (n/(gcd x n))) + [ apply eq_div_times_div_times [ assumption - | assumption | apply divides_gcd_n + | apply divides_gcd_m ] - ] - | rewrite > NdivM_times_M_to_N - [ rewrite > (NdivM_times_M_to_N j (gcd (pred n) j)) - [ reflexivity - | assumption - | rewrite > sym_gcd. - apply divides_gcd_n - ] - | assumption - | apply divides_gcd_n - ] - ] - ] - | apply (mod_plus_times). - assumption - ] - | apply (div_plus_times). - assumption - ] - | apply (lt_times_n_to_lt (gcd (pred n) j) ? ?) - [ assumption - | rewrite > NdivM_times_M_to_N - [ apply (lt_to_le_to_lt j (pred n) ?) - [ assumption - | apply (lt_to_le). - apply (lt_to_le_to_lt ? n ?) - [ change with ((S (pred n)) \le n). - rewrite < (S_pred n) - [ apply le_n - | apply (trans_lt ? (S O) ?) - [ change with ((S O) \le (S O)). - apply (le_n (S O)) + (*rewrite > sym_times. + rewrite > (divides_to_eq_times_div_div_times n). + rewrite > (divides_to_eq_times_div_div_times x). + rewrite > (sym_times n x). + reflexivity. + assumption. + apply divides_gcd_m. + apply (divides_to_lt_O (gcd x n)). + apply lt_O_gcd. + assumption. + apply divides_gcd_n.*) + | apply lt_O_to_divides_to_lt_O_div + [ assumption + | apply divides_gcd_m + ] + | apply (witness ? ? (gcd x n)). + rewrite > divides_to_times_div + [ reflexivity | assumption + | apply divides_gcd_m + ] ] - | rewrite > (times_n_SO n) in \vdash (? % ?). - apply (le_times n) - [ apply (le_n n) - | change with (O \lt (gcd (pred n) j)). - assumption - ] - ] + ] ] - | assumption - | rewrite > sym_gcd. - apply (divides_gcd_n) - ] - ] - ] - | rewrite > sym_gcd. - apply (lt_O_gcd). - assumption - ] -| apply n_gt_Uno_to_O_lt_pred_n. - assumption -] -qed. - - - - -(*5th*) -theorem sum_divisor_totient1_aux5: \forall a,b,c:nat. -O \lt c \to O \lt b \to a \lt c \to b \divides a \to b \divides c \to -a / b * c / (c/b) = a. -intros. -elim H3. -elim H4. -cut (O \lt n) -[ rewrite > H6 in \vdash (? ? (? ? %) ?). - rewrite > sym_times in \vdash (? ? (? ? %) ?). - rewrite > (div_times_ltO n b) - [ cut (n \divides c) - [ cut (a/b * c /n = a/b * (c/n)) - [ rewrite > Hcut2. - cut (c/n = b) - [ rewrite > Hcut3. - apply (NdivM_times_M_to_N a b); + | apply (le_to_lt_to_lt ? n) + [ apply cic:/matita/Z/dirichlet_product/le_div.con. assumption - | rewrite > H6. - apply (div_times_ltO b n). - assumption - ] - | elim Hcut1. - rewrite > H7. - rewrite < assoc_times in \vdash (? ? (? % ?) ?). - rewrite > (sym_times ((a/b)*n) n1). - rewrite < (assoc_times n1 (a/b) n). - rewrite > (div_times_ltO (n1*(a/b)) n) - [ rewrite > (sym_times n n1). - rewrite > (div_times_ltO n1 n) - [ rewrite > (sym_times (a/b) n1). - reflexivity - | assumption + | change with ((S n) \le (S n)). + apply le_n ] - | assumption ] - ] - | apply (witness n c b). - rewrite > (sym_times n b). - assumption - ] - | assumption - ] -| apply (divides_to_lt_O n c) - [ assumption - | apply (witness n c b). - rewrite > sym_times. - assumption - ] -] -qed. - - -(*6th*) -theorem sum_divisor_totient1_aux_6: \forall j,n:nat. -j \lt (pred n) \to (S O) \lt n \to ((pred n)/(gcd (pred n) j))*n+j/(gcd (pred n) j) H2 in H. - apply False_ind. - apply (not_le_Sn_O j H) -| intros. - rewrite < (pred_Sn m). - rewrite < (times_n_Sm (S m) m). - rewrite > (sym_plus (S m) ((S m) * m)). - apply le_to_lt_to_plus_lt - [ rewrite > (sym_times (S m) m). - apply le_times_l. - apply (lt_to_divides_to_div_le) - [ apply (nat_case1 m) - [ intros. - rewrite > H3 in H2. - rewrite > H2 in H1. - apply False_ind. - apply (le_to_not_lt (S O) (S O)) - [ apply le_n - | assumption - ] - | intros. - rewrite > sym_gcd in \vdash (? ? %). - apply (lt_O_gcd j (S m1)). - apply (lt_O_S m1) - ] - | apply divides_gcd_n - ] - | apply (le_to_lt_to_lt (j / (gcd m j)) j (S m)) - [ - apply lt_to_divides_to_div_le - [ apply (nat_case1 m) - [ intros. - rewrite > H3 in H2. - rewrite > H2 in H1. - apply False_ind. - apply (le_to_not_lt (S O) (S O)) - [ apply le_n - | assumption + | apply (le_to_lt_to_lt ? x) + [ apply cic:/matita/Z/dirichlet_product/le_div.con. + assumption + | apply (trans_lt ? n ?) + [ assumption + | change with ((S n) \le (S n)). + apply le_n ] - | intros. - rewrite > sym_gcd in \vdash (? ? %). - apply (lt_O_gcd j (S m1)). - apply (lt_O_S m1) ] - | rewrite > sym_gcd in \vdash (? % ?). - apply divides_gcd_n - ] - | rewrite > H2 in H. - rewrite < (pred_Sn m) in H. - apply (trans_lt j m (S m)) - [ assumption. - | change with ((S m) \le (S m)). - apply (le_n (S m)) ] - ] - ] -] -qed. - - - - -(* The main theorem, adding the hypotesis n > 1 (the cases n= 0 - and n = 1 are dealed as particular cases in theorem - sum_divisor_totient) - *) -theorem sum_divisor_totient1: \forall n. (S O) \lt n \to sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n). -intros. -unfold totient. -apply (trans_eq ? ? -(sigma_p n (\lambda d:nat.divides_b d (pred n)) -(\lambda d:nat.sigma_p n (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O)))) - [ apply eq_sigma_p1 - [ intros. - reflexivity - | intros. - apply sym_eq. - apply (trans_eq ? ? - (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O))) - [ apply false_to_eq_sigma_p - [ apply lt_to_le. - assumption - | intros. - rewrite > lt_to_leb_false - [ reflexivity - | apply le_S_S. - assumption - ] - ] - | apply eq_sigma_p - [ intros. - rewrite > le_to_leb_true - [ reflexivity - | assumption - ] - | intros. - reflexivity - ] + | apply (divides_to_lt_O ? n) + [ assumption + | apply divides_gcd_m ] - ] - | rewrite < (sigma_p2' n n - (\lambda d:nat.divides_b d (pred n)) - (\lambda d,m:nat.leb (S m) d\land eqb (gcd m d) (S O)) - (\lambda x,y.(S O))). - apply (trans_eq ? ? (sigma_p (pred n) (\lambda x.true) (\lambda x.S O))) - [ apply (eq_sigma_p_gh - (\lambda x:nat. (S O)) - (\lambda i:nat. (((i \mod n)*(pred n)) / (i / n) ) ) - (\lambda j:nat. (((pred n)/(gcd (pred n) j))*n + (j / (gcd (pred n) j))) ) - (n*n) - (pred n) - (\lambda x:nat. - divides_b (x/n) (pred n) - \land (leb (S (x \mod n)) (x/n) - \land eqb (gcd (x \mod n) (x/n)) (S O))) - (\lambda x:nat.true) - ) - [ intros. - reflexivity - | intros. - cut ((i/n) \divides (pred n)) - [ cut ((i \mod n ) \lt (i/n)) - [ cut ((gcd (i \mod n) (i / n)) = (S O)) - [ cut ((gcd (pred n) ((i \mod n)*(pred n)/ (i/n)) = (pred n) / (i/n))) - [ rewrite > Hcut3. - cut ((i \mod n) * (pred n)/(i/n)/((pred n)/(i/n)) = (i \mod n)) - [ rewrite > Hcut4. - cut ((pred n)/ ((pred n)/(i/n)) = (i/n)) - [ rewrite > Hcut5. - apply sym_eq. - apply div_mod. - apply (trans_lt O (S O) n) - [ apply (lt_O_S O) - | assumption - ] - | elim Hcut. - rewrite > H3 in \vdash (? ? (? ? (? % ?)) ?). - rewrite > sym_times in \vdash (? ? (? ? (? % ?)) ?). - rewrite > (div_times_ltO n2 (i/n)) - [ rewrite > H3. - apply div_times_ltO. - apply (divides_to_lt_O n2 (pred n)) - [ apply (n_gt_Uno_to_O_lt_pred_n n). - assumption - | apply (witness n2 (pred n) (i/n)). - rewrite > sym_times. - assumption - ] - | apply (divides_to_lt_O (i/n) (pred n)) - [ apply (n_gt_Uno_to_O_lt_pred_n n). - assumption - | apply (witness (i/n) (pred n) n2). - assumption - ] - ] - ] - | elim Hcut. - cut (( i \mod n * (pred n)/(i/n)) = ( i\mod n * ((pred n)/(i/n)))) - [ rewrite > Hcut4. - rewrite > H3. - rewrite < (sym_times n2 (i/n)). - rewrite > (div_times_ltO n2 (i/n)) - [ rewrite > (div_times_ltO (i \mod n) n2) - [ reflexivity - | apply (divides_to_lt_O n2 (pred n)) - [ apply (n_gt_Uno_to_O_lt_pred_n n). - assumption - | apply (witness n2 (pred n) (i/n)). - rewrite > sym_times. - assumption - ] - ] - | apply (divides_to_lt_O (i/n) (pred n)) - [ apply (n_gt_Uno_to_O_lt_pred_n n). + ] + | cut (i \divides n) + [ cut (j \lt i) + [ cut ((gcd j i) = (S O) ) + [ cut ((gcd (j*(n/i)) n) = n/i) + [ split + [ split + [ split + [ reflexivity + | rewrite > Hcut3. + apply (cic:/matita/Z/dirichlet_product/div_div.con); + assumption + ] + | rewrite > Hcut3. + rewrite < divides_to_eq_times_div_div_times + [ rewrite > div_n_n + [ apply sym_eq. + apply times_n_SO. + | apply lt_O_to_divides_to_lt_O_div; (*n/i 1*) assumption - | assumption - ] ] - | apply (sym_eq). - apply (separazioneFattoriSuDivisione (i \mod n) (pred n) (i/n)) - [ apply (n_gt_Uno_to_O_lt_pred_n n). + | apply lt_O_to_divides_to_lt_O_div; (*n/i 2*) assumption - | assumption - ] + | apply divides_n_n ] ] - | apply (sum_divisor_totient1_aux2); - assumption + | rewrite < (divides_to_times_div n i) in \vdash (? ? %) + [ rewrite > sym_times. + apply (lt_times_r1) + [ apply lt_O_to_divides_to_lt_O_div; (*n/i 3*) + assumption + | assumption + ] + | apply (divides_to_lt_O i n); assumption + | assumption + ] ] - | apply (eqb_true_to_eq (gcd (i \mod n) (i/n)) (S O)). - apply (andb_true_true - (eqb (gcd (i\mod n) (i/n)) (S O)) - (leb (S (i\mod n)) (i/n)) - ). - apply (andb_true_true - ((eqb (gcd (i\mod n) (i/n)) (S O)) - \land - (leb (S (i\mod n)) (i/n))) - (divides_b (i/n) (pred n)) - ). - rewrite > andb_sym. - rewrite > andb_sym in \vdash (? ? (? ? %) ?). - assumption - ] - | change with (S (i \mod n) \le (i/n)). - cut (leb (S (i \mod n)) (i/n) = true) - [ change with ( - match (true) with - [ true \Rightarrow (S (i \mod n)) \leq (i/n) - | false \Rightarrow (S (i \mod n)) \nleq (i/n)] - ). - rewrite < Hcut1. - apply (leb_to_Prop (S(i \mod n)) (i/n)) - | apply (andb_true_true (leb (S(i\mod n)) (i/n)) (divides_b (i/n) (pred n)) ). - apply (andb_true_true ((leb (S(i\mod n)) (i/n)) \land (divides_b (i/n) (pred n))) - (eqb (gcd (i\mod n) (i/n)) (S O)) - ). - rewrite > andb_sym in \vdash (? ? (? % ?) ?). - rewrite < (andb_assoc) in \vdash (? ? % ?). - assumption - ] - ] - | apply (divides_b_true_to_divides ). - apply (andb_true_true (divides_b (i/n) (pred n)) - (leb (S (i\mod n)) (i/n))). - apply (andb_true_true ( (divides_b (i/n) (pred n)) \land (leb (S (i\mod n)) (i/n)) ) - (eqb (gcd (i\mod n) (i/n)) (S O)) - ). - rewrite < andb_assoc. - assumption. - ] - | intros. - apply (sum_divisor_totient1_aux_3); - assumption. - | intros. - apply (sum_divisor_totient1_aux_4); - assumption. - | intros. - cut (j/(gcd (pred n) j) \lt n) - [ rewrite > (div_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j)) - [ rewrite > (mod_plus_times n (pred n/gcd (pred n) j) (j/gcd (pred n) j)) - [ apply (sum_divisor_totient1_aux5 j (gcd (pred n) j) (pred n)) - [ apply (n_gt_Uno_to_O_lt_pred_n n). - assumption - | rewrite > sym_gcd. - apply lt_O_gcd. - apply (n_gt_Uno_to_O_lt_pred_n n). - assumption + | rewrite < (divides_to_times_div n i) in \vdash (? ? (? ? %) ?) + [ rewrite > (sym_times j). + rewrite > times_n_SO in \vdash (? ? ? %). + rewrite < Hcut2. + apply eq_gcd_times_times_times_gcd. + | apply (divides_to_lt_O i n); assumption | assumption - | apply divides_gcd_m - | rewrite > sym_gcd. - apply divides_gcd_m ] - | assumption ] - | assumption + | apply eqb_true_to_eq. + apply (andb_true_true_r (leb (S j) i)). + assumption ] - | apply (le_to_lt_to_lt (j/gcd (pred n) j) j n) - [ apply (lt_to_divides_to_div_le) - [ rewrite > sym_gcd. - apply lt_O_gcd. - apply (n_gt_Uno_to_O_lt_pred_n n). - assumption - | apply divides_gcd_m - ] - | apply (lt_to_le_to_lt j (pred n) n) - [ assumption - | apply le_pred_n - ] + | change with ((S j) \le i). + cut((leb (S j) i) = true) + [ change with( + match (true) with + [ true \Rightarrow ((S j) \leq i) + | false \Rightarrow ((S j) \nleq i)] + ). + rewrite < Hcut1. + apply (leb_to_Prop) + | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))). + assumption ] ] - | intros. - apply (sum_divisor_totient1_aux_6); - assumption. + | apply (divides_b_true_to_divides). + assumption ] - | apply (sigma_p_true). ] - ] -qed. - - -(*there's a little difference between the following definition of the - theorem, and the abstract definition given before. - in fact (sigma_p n f p) works on (pred n), and not on n, as first element. - that's why in the definition of the theorem the summary is set equal to - (pred n). - *) -theorem sum_divisor_totient: \forall n. -sigma_p n (\lambda d.divides_b d (pred n)) totient = (pred n). -intros. -apply (nat_case1 n) -[ intros. - simplify. - reflexivity -| intros. - apply (nat_case1 m) - [ intros. - simplify. - reflexivity - | intros. - rewrite < H1. - rewrite < H. - rewrite > (pred_Sn m). - rewrite < H. - apply( sum_divisor_totient1). - rewrite > H. - rewrite > H1. - apply cic:/matita/algebra/finite_groups/lt_S_S.con. - apply lt_O_S + | apply (sigma_p_true). ] ] -qed. - - - - - - - - - - - - - - - - - - +qed. + + -- 2.39.2