From e65e31bab82994cf8400bb4c294cf7d16fa2c83c Mon Sep 17 00:00:00 2001 From: Cristian Armentano Date: Fri, 7 Sep 2007 14:10:46 +0000 Subject: [PATCH] some simplifications. --- .../matita/library/nat/gcd_properties1.ma | 55 +----- .../nat/propr_div_mod_lt_le_totient1_aux.ma | 182 ++++++------------ helm/software/matita/library/nat/totient1.ma | 45 +---- 3 files changed, 67 insertions(+), 215 deletions(-) diff --git a/helm/software/matita/library/nat/gcd_properties1.ma b/helm/software/matita/library/nat/gcd_properties1.ma index 637c20f4a..ad5cb2c6b 100644 --- a/helm/software/matita/library/nat/gcd_properties1.ma +++ b/helm/software/matita/library/nat/gcd_properties1.ma @@ -157,20 +157,12 @@ apply (leb_elim n m) ] qed. -(* 2 basic properties of divides predicate *) -theorem aDIVb_to_bDIVa_to_aEQb: -\forall a,b:nat. -a \divides b \to b \divides a \to a = b. -intros. -apply antisymmetric_divides; - assumption. -qed. - +(* a basic property of divides predicate *) theorem O_div_c_to_c_eq_O: \forall c:nat. O \divides c \to c = O. intros. -apply aDIVb_to_bDIVa_to_aEQb +apply antisymmetric_divides [ apply divides_n_O | assumption ] @@ -182,7 +174,7 @@ c \divides a \to c \divides b \to (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c. intros. elim (H2 ((gcd a b))) -[ apply (aDIVb_to_bDIVa_to_aEQb (gcd a b) c) +[ apply (antisymmetric_divides (gcd a b) c) [ apply (witness (gcd a b) c n2). assumption | apply divides_d_gcd; @@ -224,47 +216,6 @@ apply (nat_case1 c) ] ] qed. - - (* - apply (nat_case1 a) - [ intros. - rewrite > (sym_times c O). - simplify. - reflexivity - | intros. - rewrite < H1. - apply (nat_case1 b) - [ intros. - rewrite > (sym_times ? O). - rewrite > (sym_gcd a O). - rewrite > sym_gcd. - simplify. - reflexivity - | intros. - rewrite < H2. - apply gcd1 - [ apply divides_times - [ apply divides_n_n - | apply divides_gcd_n. - ] - | apply divides_times - [ apply divides_n_n - | rewrite > sym_gcd. - apply divides_gcd_n - ] - | intros. - apply (divides_d_times_gcd) - [ rewrite > H. - apply lt_O_S - | assumption - | assumption - ] - ] - ] - ] -] -qed.*) - theorem associative_nat_gcd: associative nat gcd. change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))). diff --git a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma index fae1afc2c..975114306 100644 --- a/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma +++ b/helm/software/matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma @@ -112,77 +112,21 @@ apply (le_times_to_le c (a/c) a) qed. -theorem bTIMESc_le_a_to_c_le_aDIVb: \forall a,b,c:nat. -O \lt b \to (b*c) \le a \to c \le (a /b). -intros. -rewrite > (div_mod a b) in H1 -[ apply (le_times_to_le b ? ?) - [ assumption - | cut ( (c*b) \le ((a/b)*b) \lor ((a/b)*b) \lt (c*b)) - [ elim Hcut - [ rewrite < (sym_times c b). - rewrite < (sym_times (a/b) b). - assumption - | cut (a/b \lt c) - [ change in Hcut1 with ((S (a/b)) \le c). - cut( b*(S (a/b)) \le b*c) - [ rewrite > (sym_times b (S (a/b))) in Hcut2. - simplify in Hcut2. - cut ((b + (a/b)*b) \le ((a/b)*b + (a \mod b))) - [ cut (b \le (a \mod b)) - [ apply False_ind. - apply (lt_to_not_le (a \mod b) b) - [ apply (lt_mod_m_m). - assumption - | assumption - ] - | apply (le_plus_to_le ((a/b)*b)). - rewrite > sym_plus. - assumption. - ] - | apply (trans_le ? (b*c) ?); - assumption - ] - | apply (le_times_r b ? ?). - assumption - ] - | apply (lt_times_n_to_lt b (a/b) c) - [ assumption - | assumption - ] - ] - ] - | apply (leb_elim (c*b) ((a/b)*b)) - [ intros. - left. - assumption - | intros. - right. - apply cic:/matita/nat/orders/not_le_to_lt.con. - 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. -cut (O \lt n2) -[ rewrite > H3. - rewrite > (sym_times a n2). - rewrite > (div_times_ltO n2 a); - assumption -| apply (divides_to_lt_O n2 b) +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. @@ -208,17 +152,17 @@ cut(O \lt c) ] qed. - +(* theorem div_times_to_eqSO: \forall a,d:nat. O \lt d \to a*d = d \to a = (S O). intros. -apply (cic:/matita/nat/div_and_mod/inj_times_r1.con d) +apply (inj_times_r1 d) [ assumption | rewrite > sym_times. rewrite < (times_n_SO d). assumption ] -qed. +qed.*) theorem div_mod_minus: @@ -231,6 +175,7 @@ rewrite > (div_mod a b) in \vdash (? ? ? (? % ?)) ] qed. +(* theorem sum_div_eq_div: \forall a,b,c:nat. O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c. intros. @@ -245,7 +190,7 @@ rewrite > (div_plus_times c n2 b) | assumption ] qed. - +*) (* A corollary to the division theorem (between natural numbers). * @@ -270,83 +215,74 @@ split | rewrite < (times_n_Sm b c). rewrite < H1. rewrite > sym_times. - rewrite > div_mod_minus - [ rewrite < (eq_minus_plus_plus_minus b a (a \mod b)) - [ rewrite < (sym_plus a b). - rewrite > (eq_minus_plus_plus_minus a b (a \mod b)) - [ rewrite > (plus_n_O a) in \vdash (? % ?). - apply (le_to_lt_to_plus_lt) - [ apply (le_n a) - | apply cic:/matita/nat/minus/lt_to_lt_O_minus.con. - apply cic:/matita/nat/div_and_mod/lt_mod_m_m.con. - assumption - ] - | apply lt_to_le. - apply lt_mod_m_m. - assumption - ] - | rewrite > (div_mod a b) in \vdash (? ? %) - [ rewrite > plus_n_O in \vdash (? % ?). - rewrite > sym_plus. - apply cic:/matita/nat/le_arith/le_plus_n.con - | assumption - ] - ] + 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) -[ cut (a/b \le c \lor c \lt a/b) - [ elim Hcut - [ assumption - | change in H3 with ((S c) \le (a/b)). - cut (b*(S c) \le (b*(a/b))) - [ rewrite > (sym_times b (S c)) in Hcut1. - cut (a \lt (b * (a/b))) - [ rewrite > (div_mod a b) in Hcut2:(? % ?) - [ rewrite > (plus_n_O (b*(a/b))) in Hcut2:(? ? %). - cut ((a \mod b) \lt O) - [ apply False_ind. - apply (lt_to_not_le (a \mod b) O) - [ assumption - | apply le_O_n - ] - | apply (lt_plus_to_lt_r ((a/b)*b)). - rewrite > (sym_times b (a/b)) in Hcut2:(? ? (? % ?)). - assumption - ] - | assumption - ] - | apply (lt_to_le_to_lt ? (b*(S c)) ?) +[ 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 b (S c)). + | rewrite > (sym_times (a/b) b). + apply le_times_r. assumption ] + | assumption ] - | apply le_times_r. - assumption + | apply le_O_n ] - ] - | apply (leb_elim (a/b) c) - [ intros. - left. + | apply not_le_to_lt. assumption - | intros. - right. - apply cic:/matita/nat/orders/not_le_to_lt.con. + ] + ] +| 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 ] - ] -| apply (bTIMESc_le_a_to_c_le_aDIVb); - 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. diff --git a/helm/software/matita/library/nat/totient1.ma b/helm/software/matita/library/nat/totient1.ma index d7483b3b4..b46120341 100644 --- a/helm/software/matita/library/nat/totient1.ma +++ b/helm/software/matita/library/nat/totient1.ma @@ -136,7 +136,7 @@ apply divides_SO_n. qed. theorem sum_divisor_totient1_aux_3: \forall i,n:nat. -i < n*n \to +(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))) @@ -153,42 +153,8 @@ apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n)) | rewrite > (NdivM_times_M_to_N ) [ rewrite > (NdivM_times_M_to_N ) in \vdash (? ? %) [ apply (monotonic_lt_times_variant (pred n)) - [ apply (nat_case1 n) - [ intros. - rewrite > H2 in H:(? ? %). - change in H:(? ? %) with (O). - change in H:(%) with ((S i) \le O). - apply False_ind. - apply (not_le_Sn_O i H) - | intro. - elim m - [ rewrite > H2 in H1:(%). - rewrite > H2 in H:(%). - simplify in H. - cut (i = O) - [ rewrite > Hcut in H1:(%). - simplify in H1. - apply False_ind. - apply (not_eq_true_false H1) - | change in H:(%) with((S i) \le (S O)). - cut (i \le O ) - [ apply (nat_case1 i) - [ intros. - reflexivity - | intros. - rewrite > H3 in Hcut:(%). - apply False_ind. - apply (not_le_Sn_O m1 Hcut) - ] - | apply (le_S_S_to_le i O). - assumption - ] - ] - | change with ((S O) \le (S n1)). - apply (le_S_S O n1). - apply (le_O_n n1) - ] - ] + [ 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 @@ -220,8 +186,7 @@ apply (lt_to_le_to_lt ((i \mod n)*(pred n) / (i/n)) ] | rewrite > (sym_times). rewrite > (div_times_ltO ) - [ apply (le_n (pred n)). - + [ 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. @@ -483,7 +448,7 @@ 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_totiet) + 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. -- 2.39.2