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
(* n_divides n m = <q,r> 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.
+
(* n_divides n m = <q,r> 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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
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.
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).
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.
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.
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.
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<m \to n \leq m.
simplify.intros.unfold lt in H.elim H.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+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.
+
+
+
+
+
+
+
+
+
+
+
projects / helm.git / commitdiff