From 77440acc493b0e04b7e009b942c6a3268a46c141 Mon Sep 17 00:00:00 2001 From: Cristian Armentano Date: Wed, 27 Jun 2007 18:05:37 +0000 Subject: [PATCH] new gcd properties, and theorems for totient, and theorems for totient1 --this line, and those below, will be ignored-- M minus.ma M le_arith.ma M lt_arith.ma M div_and_mod.ma M div_and_mod_new.ma M orders.ma A propr_div_mod_lt_le_totient1_aux.ma A gcd_properties1.ma --- matita/library/nat/div_and_mod.ma | 12 + matita/library/nat/div_and_mod_new.ma | 9 + matita/library/nat/gcd_properties1.ma | 589 ++++++++++++++++++ matita/library/nat/le_arith.ma | 13 +- matita/library/nat/lt_arith.ma | 65 ++ matita/library/nat/minus.ma | 9 + matita/library/nat/orders.ma | 13 + .../nat/propr_div_mod_lt_le_totient1_aux.ma | 488 +++++++++++++++ 8 files changed, 1197 insertions(+), 1 deletion(-) create mode 100644 matita/library/nat/gcd_properties1.ma create mode 100644 matita/library/nat/propr_div_mod_lt_le_totient1_aux.ma diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma index 537d3bcf0..d7750e39a 100644 --- a/matita/library/nat/div_and_mod.ma +++ b/matita/library/nat/div_and_mod.ma @@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/div_and_mod". include "datatypes/constructors.ma". include "nat/minus.ma". + let rec mod_aux p m n: nat \def match (leb m n) with [ true \Rightarrow m @@ -331,3 +332,14 @@ 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/div_and_mod_new.ma b/matita/library/nat/div_and_mod_new.ma index 2f881b155..f08a5f94e 100644 --- a/matita/library/nat/div_and_mod_new.ma +++ b/matita/library/nat/div_and_mod_new.ma @@ -358,3 +358,12 @@ 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 new file mode 100644 index 000000000..aa9783a96 --- /dev/null +++ b/matita/library/nat/gcd_properties1.ma @@ -0,0 +1,589 @@ +(**************************************************************************) +(* ___ *) +(* ||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/gcd_properties1". + +include "nat/propr_div_mod_lt_le_totient1_aux.ma". + +(* this file contains some important properites of gcd in N *) + +(*it's a generalization of the existing theorem divides_gcd_aux (in which + c = 1), proved in file gcd.ma + *) +theorem divides_times_gcd_aux: \forall p,m,n,d,c. +O \lt c \to O < n \to n \le m \to n \le p \to +d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n. +intro. +elim p +[ absurd (O < n) + [ assumption + | apply le_to_not_lt. + assumption + ] +| simplify. + cut (n1 \divides m \lor n1 \ndivides m) + [ elim Hcut + [ rewrite > divides_to_divides_b_true + [ simplify. + assumption + | assumption + | assumption + ] + | rewrite > not_divides_to_divides_b_false + [ simplify. + apply H + [ assumption + | cut (O \lt m \mod n1 \lor O = m \mod n1) + [ elim Hcut1 + [ assumption + | absurd (n1 \divides 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 (m \mod n1 < n1). + apply lt_mod_m_m. + assumption + | assumption + ] + | assumption + | rewrite < times_mod + [ rewrite < (sym_times c m). + rewrite < (sym_times c n1). + apply divides_mod + [ rewrite > (S_pred c) + [ rewrite > (S_pred n1) + [ apply (lt_O_times_S_S) + | assumption + ] + | assumption + ] + | assumption + | assumption + ] + | assumption + | assumption + ] + ] + | assumption + | assumption + ] + ] + | apply (decidable_divides n1 m). + assumption + ] +] +qed. + +(*it's a generalization of the existing theorem divides_gcd_d (in which + c = 1), proved in file gcd.ma + *) +theorem divides_d_times_gcd: \forall m,n,d,c. +O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m. +intros. +change with +(d \divides c * +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 (d \divides c*gcd_aux (S m1) m (S m1)). + apply divides_times_gcd_aux + [ assumption + | unfold lt. + apply le_S_S. + apply le_O_n + | assumption + | apply (le_n (S m1)) + | assumption + | rewrite < H3. + assumption + ] + ] +| apply (nat_case1 m) + [ simplify. + intros. + assumption + | intros. + change with (d \divides c * gcd_aux (S m1) n (S m1)). + apply divides_times_gcd_aux + [ unfold lt. + change with (O \lt c). + assumption + | apply lt_O_S + | apply lt_to_le. + apply not_le_to_lt. + assumption + | apply (le_n (S m1)). + | assumption + | rewrite < H3. + assumption + ] + ] +] +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. + + +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 divides_n_O +| assumption +] +qed. + +(* an alternative characterization for gcd *) +theorem gcd1: \forall a,b,c:nat. +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 (witness (gcd a b) c n2). + assumption + | apply divides_d_gcd; + assumption + ] +| apply divides_gcd_n +| rewrite > sym_gcd. + apply divides_gcd_n +] +qed. + + +theorem eq_gcd_times_times_eqv_times_gcd: \forall a,b,c:nat. +(gcd (c*a) (c*b)) = c*(gcd a b). +intros. +apply (nat_case1 c) +[ intros. + simplify. + reflexivity +| intros. + rewrite < H. + 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))). +intros. +apply gcd1 +[ apply divides_d_gcd + [ apply (trans_divides ? (gcd b c) ?) + [ apply divides_gcd_m + | apply divides_gcd_n + ] + | apply divides_gcd_n + ] +| apply (trans_divides ? (gcd b c) ?) + [ apply divides_gcd_m + | apply divides_gcd_m + ] +| intros. + cut (d \divides a \land d \divides b) + [ elim Hcut. + cut (d \divides (gcd b c)) + [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2) + | apply (divides_d_gcd c b d H1 H3) + ] + | split + [ apply (trans_divides d (gcd a b) a H). + apply divides_gcd_n + | apply (trans_divides d (gcd a b) b H). + apply divides_gcd_m + ] + ] +] +qed. + +theorem aDIVIDES_b_TIMES_c_to_GCD_a_b_eq_d_to_aDIVd_DIVIDES_c: \forall a,b,c,d:nat. +a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c. +intros. +apply (nat_case1 a) +[ intros. + apply (nat_case1 b) + [ intros. + cut (d = 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 (O_div_c_to_c_eq_O (b*c) H) + ] + ] + | rewrite < H1. + apply lt_O_gcd. + rewrite > H3. + apply lt_O_S + ] + ] +| intros. + rewrite < H2. + 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_eqv_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 + | assumption + ] + | assumption + | assumption + ] + | 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 + ] + ] +] +qed. + +theorem gcd_sum_times_eq_gcd_aux: \forall a,b,d,m:nat. +(gcd (a+m*b) b) = d \to (gcd a b) = d. +intros. +apply gcd1 +[ rewrite > (minus_plus_m_m a (m*b)). + apply divides_minus + [ rewrite < H. + apply divides_gcd_n + | rewrite > (times_n_SO d). + rewrite > (sym_times d ?). + apply divides_times + [ apply divides_SO_n + | rewrite < H. + apply divides_gcd_m + ] + ] +| rewrite < H. + apply divides_gcd_m +| intros. + rewrite < H. + apply divides_d_gcd + [ assumption + | apply divides_plus + [ assumption + | rewrite > (times_n_SO d1). + rewrite > (sym_times d1 ?). + apply divides_times + [ apply divides_SO_n + | assumption + ] + ] + ] +] +qed. + +theorem gcd_sum_times_eq_gcd: \forall a,b,m:nat. +(gcd (a+m*b) b) = (gcd a b). +intros. +apply sym_eq. +apply (gcd_sum_times_eq_gcd_aux a b (gcd (a+m*b) b) m). +reflexivity. +qed. + +theorem gcd_div_div_eq_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_eqv_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 gcdSO_divides_divides_times_divides: \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. + elim H1. + elim H2. + rewrite > H5. + rewrite > (sym_times e f). + apply (divides_times) + [ 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) + | 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). + *) +theorem gcd_aTIMESb_c_eq_gcd_a_c_TIMES_gcd_b_c: \forall a,b,c:nat. +(gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c). +intros. +apply gcd1 +[ apply divides_times; + apply divides_gcd_n +| apply (gcdSO_divides_divides_times_divides c (gcd a c) (gcd b c)) + [ apply gcd1 + [ apply divides_SO_n + | apply divides_SO_n + | intros. + cut (d \divides a) + [ cut (d \divides b) + [ rewrite < H. + apply (divides_d_gcd b a d Hcut1 Hcut) + | apply (trans_divides d (gcd b c) b) + [ assumption + | apply (divides_gcd_n) + ] + ] + | apply (trans_divides d (gcd a c) a) + [ assumption + | apply (divides_gcd_n) + ] + ] + ] + | apply (divides_gcd_m) + | apply (divides_gcd_m) + ] +| intros. + rewrite < (eq_gcd_times_times_eqv_times_gcd b c (gcd a c)). + rewrite > (sym_times (gcd a c) b). + rewrite > (sym_times (gcd a c) c). + rewrite < (eq_gcd_times_times_eqv_times_gcd a c b). + rewrite < (eq_gcd_times_times_eqv_times_gcd a c c). + apply (divides_d_gcd) + [ apply (divides_d_gcd) + [ rewrite > (times_n_SO d). + apply (divides_times) + [ assumption + | apply divides_SO_n + ] + | rewrite > (times_n_SO d). + apply (divides_times) + [ assumption + | apply divides_SO_n + ] + ] + | apply (divides_d_gcd) + [ rewrite > (times_n_SO d). + rewrite > (sym_times d (S O)). + apply (divides_times) + [ apply (divides_SO_n) + | assumption + ] + | rewrite < (sym_times a b). + assumption + ] + ] +] +qed. + + +theorem gcd_eq_gcd_minus: \forall a,b:nat. +a \lt b \to (gcd a b) = (gcd (b - a) b). +intros. +apply sym_eq. +apply gcd1 +[ apply (divides_minus (gcd a b) b a) + [ apply divides_gcd_m + | apply divides_gcd_n + ] +| apply divides_gcd_m +| intros. + elim H1. + elim H2. + cut(b = (d*n2) + a) + [ cut (b - (d*n2) = a) + [ rewrite > H4 in Hcut1. + rewrite < (distr_times_minus d n n2) in Hcut1. + apply divides_d_gcd + [ assumption + | apply (witness d a (n - n2)). + apply sym_eq. + assumption + ] + | apply (plus_to_minus ? ? ? Hcut) + ] + | rewrite > sym_plus. + apply (minus_to_plus) + [ apply lt_to_le. + assumption + | assumption + ] + ] +] +qed. + diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma index 90f3e182b..9ab53fd74 100644 --- a/matita/library/nat/le_arith.ma +++ b/matita/library/nat/le_arith.ma @@ -131,4 +131,15 @@ apply nat_elim2;intros assumption ] ] -qed. \ No newline at end of file +qed. + +(*0 and times *) +theorem O_lt_const_to_le_times_const: \forall a,c:nat. +O \lt c \to a \le a*c. +intros. +rewrite > (times_n_SO a) in \vdash (? % ?). +apply le_times +[ apply le_n +| assumption +] +qed. diff --git a/matita/library/nat/lt_arith.ma b/matita/library/nat/lt_arith.ma index f0fdbdbd6..e71514726 100644 --- a/matita/library/nat/lt_arith.ma +++ b/matita/library/nat/lt_arith.ma @@ -63,11 +63,61 @@ rewrite > sym_plus. rewrite > (sym_plus q).assumption. qed. +theorem le_to_lt_to_plus_lt: \forall a,b,c,d:nat. +a \le c \to b \lt d \to (a + b) \lt (c+d). +intros. +cut (a \lt c \lor a = c) +[ elim Hcut + [ apply (lt_plus ); + assumption + | rewrite > H2. + apply (lt_plus_r c b d). + assumption + ] +| apply le_to_or_lt_eq. + assumption +] +qed. + + (* times and zero *) theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m). intros.simplify.unfold lt.apply le_S_S.apply le_O_n. qed. +theorem lt_times_eq_O: \forall a,b:nat. +O \lt a \to (a * b) = O \to b = O. +intros. +apply (nat_case1 b) +[ intros. + reflexivity +| intros. + rewrite > H2 in H1. + rewrite > (S_pred a) in H1 + [ apply False_ind. + apply (eq_to_not_lt O ((S (pred a))*(S m))) + [ apply sym_eq. + assumption + | apply lt_O_times_S_S + ] + | assumption + ] +] +qed. + +theorem O_lt_times_to_O_lt: \forall a,c:nat. +O \lt (a * c) \to O \lt a. +intros. +apply (nat_case1 a) +[ intros. + rewrite > H1 in H. + simplify in H. + assumption +| intros. + apply lt_O_S +] +qed. + (* times *) theorem monotonic_lt_times_r: \forall n:nat.monotonic nat lt (\lambda m.(S n)*m). @@ -77,6 +127,20 @@ simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption. apply lt_plus.assumption.assumption. qed. +(* a simple variant of the previus monotionic_lt_times *) +theorem monotonic_lt_times_variant: \forall c:nat. +O \lt c \to monotonic nat lt (\lambda t.(t*c)). +intros. +apply (increasing_to_monotonic). +unfold increasing. +intros. +simplify. +rewrite > sym_plus. +rewrite > plus_n_O in \vdash (? % ?). +apply lt_plus_r. +assumption. +qed. + theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q \def monotonic_lt_times_r. @@ -236,6 +300,7 @@ apply (trans_lt ? (S O)). unfold lt. 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. diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma index f1178107a..11585f206 100644 --- a/matita/library/nat/minus.ma +++ b/matita/library/nat/minus.ma @@ -287,6 +287,15 @@ rewrite < plus_n_Sm. apply H.apply H1. qed. +theorem lt_O_minus_to_lt: \forall a,b:nat. +O \lt b-a \to a \lt b. +intros. +rewrite > (plus_n_O a). +rewrite > (sym_plus a O). +apply (lt_minus_to_plus O a b). +assumption. +qed. + theorem distributive_times_minus: distributive nat times minus. unfold distributive. intros. diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma index 3257e2e1a..8053d50de 100644 --- a/matita/library/nat/orders.ma +++ b/matita/library/nat/orders.ma @@ -139,6 +139,19 @@ apply Hcut.assumption.rewrite < H1. apply not_le_Sn_n. qed. +(*not lt*) +theorem eq_to_not_lt: \forall a,b:nat. +a = b \to a \nlt b. +intros. +unfold Not. +intros. +rewrite > H in H1. +apply (lt_to_not_eq b b) +[ assumption +| reflexivity +] +qed. + (* le vs. lt *) theorem lt_to_le : \forall n,m:nat. n 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. +elim H +[ simplify. + apply (lt_O_S O) +| rewrite < (pred_Sn n1). + apply (lt_to_le_to_lt O (S (S O)) n1) + [ apply le_S. + apply (le_n (S O)) + | assumption + ] +] +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 (O = n \mod m) +[ rewrite > Hcut. + apply div_mod. + assumption +| apply sym_eq. + 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 (? % ?) + [ rewrite < (sym_times a c). + apply (O_lt_const_to_le_times_const). + assumption + | assumption + | assumption + ] +] +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) + [ assumption + | apply (witness n2 b a). + rewrite > sym_times. + 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_times_to_eqSO: \forall a,d:nat. +O \lt d \to a*d = d \to a = (S O). +intros. +rewrite > (plus_n_O d) in H1:(? ? ? %). +cut (a*d -d = O) +[ rewrite > sym_times in Hcut. + rewrite > times_n_SO in Hcut:(? ? (? ? %) ?). + rewrite < distr_times_minus in Hcut. + cut ((a - (S O)) = O) + [ apply (minus_to_plus a (S O) O) + [ apply (nat_case1 a) + [ intros. + rewrite > H2 in H1. + simplify in H1. + rewrite < (plus_n_O d) in H1. + rewrite < H1 in H. + apply False_ind. + change in H with ((S O) \le O). + apply (not_le_Sn_O O H) + | intros. + apply (le_S_S O m). + apply (le_O_n m) + ] + | assumption + ] + | apply (lt_times_eq_O d (a - (S O))); + assumption + ] +| apply (plus_to_minus ). + assumption +] +qed. + +theorem div_mod_minus: +\forall a,b:nat. O \lt b \to +(a /b)*b = a - (a \mod b). +intros. +apply sym_eq. +apply (inj_plus_r (a \mod b)). +rewrite > (sym_plus (a \mod b) ?). +rewrite < (plus_minus_m_m a (a \mod b)) +[ rewrite > sym_plus. + apply div_mod. + 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 + ] +] +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. +elim H2. +rewrite > H3. +rewrite > (sym_times c n2). +rewrite > (div_plus_times c n2 b) +[ rewrite > (div_times_ltO n2 c) + [ reflexivity + | assumption + ] +| 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_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 + ] + ] + | 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)) ?) + [ assumption + | rewrite > (sym_times b (S c)). + assumption + ] + ] + | apply le_times_r. + assumption + ] + ] + | apply (leb_elim (a/b) c) + [ intros. + left. + assumption + | intros. + right. + apply cic:/matita/nat/orders/not_le_to_lt.con. + 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. +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. + + + + + + + + + + + -- 2.39.2