diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:06 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:06 +0000 |
commit | 81c4c8bc418cdf42cc88249952dbba465068202c (patch) | |
tree | 0151cc0964c9874722f237721b800076d08cef37 /theories/Numbers/Integer | |
parent | 51c26ecf70212e6ec4130c41af9144058cd27d12 (diff) |
Numbers: change definition of divide (compat with Znumtheory)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14237 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZGcd.v | 28 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZLcm.v | 22 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 |
4 files changed, 29 insertions, 31 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index f72c1b343..e1802dbee 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -604,11 +604,9 @@ Lemma mod_divides : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)). Proof. intros a b Hb. split. -intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2. - rewrite Hab; now nzsimpl. -intros (c,Hc). -rewrite <- Hc, mul_comm. -now apply mod_mul. +intros Hab. exists (a/b). rewrite mul_comm. + rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl. +intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. End ZEuclidProp. diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index 87a95e9d7..404fc0c43 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -21,7 +21,7 @@ Module Type ZGcdProp Lemma divide_opp_l : forall n m, (-n | m) <-> (n | m). Proof. - intros n m. split; intros (p,Hp); exists (-p); rewrite <- Hp. + intros n m. split; intros (p,Hp); exists (-p); rewrite Hp. now rewrite mul_opp_l, mul_opp_r. now rewrite mul_opp_opp. Qed. @@ -29,8 +29,8 @@ Qed. Lemma divide_opp_r : forall n m, (n | -m) <-> (n | m). Proof. intros n m. split; intros (p,Hp); exists (-p). - now rewrite mul_opp_r, Hp, opp_involutive. - now rewrite <- Hp, mul_opp_r. + now rewrite mul_opp_l, <- Hp, opp_involutive. + now rewrite Hp, mul_opp_l. Qed. Lemma divide_abs_l : forall n m, (abs n | m) <-> (n | m). @@ -53,7 +53,7 @@ Qed. Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-1. Proof. - intros n (m,Hm). now apply eq_mul_1 with m. + intros n (m,H). rewrite mul_comm in H. now apply eq_mul_1 with m. Qed. Lemma divide_antisym_abs : forall n m, @@ -210,11 +210,11 @@ Proof. apply gcd_unique. apply mul_nonneg_nonneg; trivial using gcd_nonneg, abs_nonneg. destruct (gcd_divide_l n m) as (q,Hq). - rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2. - rewrite mul_shuffle1. apply divide_factor_l. + rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r. + rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l. destruct (gcd_divide_r n m) as (q,Hq). - rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2. - rewrite mul_shuffle1. apply divide_factor_l. + rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r. + rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l. intros q H H'. destruct (gcd_bezout n m (gcd n m) (eq_refl _)) as (a & b & EQ). rewrite <- EQ, <- sgn_abs, mul_add_distr_l. apply divide_add_r. @@ -257,15 +257,15 @@ Proof. apply le_lteq in G; destruct G as [G|G]. destruct (gcd_divide_l n m) as (q,Hq). exists (gcd n m). exists q. - split. easy. + split. now rewrite mul_comm. split. apply gcd_divide_r. destruct (gcd_divide_r n m) as (r,Hr). - rewrite <- Hr in H. rewrite <- Hq in H at 1. - rewrite <- mul_assoc in H. apply mul_divide_cancel_l in H; [|order]. + rewrite Hr in H. rewrite Hq in H at 1. + rewrite mul_shuffle0 in H. apply mul_divide_cancel_r in H; [|order]. apply gauss with r; trivial. - apply mul_cancel_l with (gcd n m); [order|]. - rewrite mul_1_r. - rewrite <- gcd_mul_mono_l_nonneg, Hq, Hr; order. + apply mul_cancel_r with (gcd n m); [order|]. + rewrite mul_1_l. + rewrite <- gcd_mul_mono_r_nonneg, <- Hq, <- Hr; order. symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index 052d68ab6..06af04d16 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -86,17 +86,17 @@ Qed. Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)). Proof. intros a b Hb. split. - intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2. - rewrite Hab; now nzsimpl. - intros (c,Hc). rewrite <- Hc, mul_comm. now apply mod_mul. + intros Hab. exists (a/b). rewrite mul_comm. + rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl. + intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. Lemma rem_divide : forall a b, b~=0 -> (a rem b == 0 <-> (b|a)). Proof. intros a b Hb. split. - intros Hab. exists (a÷b). rewrite (quot_rem a b Hb) at 2. - rewrite Hab; now nzsimpl. - intros (c,Hc). rewrite <- Hc, mul_comm. now apply rem_mul. + intros Hab. exists (a÷b). rewrite mul_comm. + rewrite (quot_rem a b Hb) at 1. rewrite Hab; now nzsimpl. + intros (c,Hc). rewrite Hc. now apply rem_mul. Qed. Lemma rem_mod_eq_0 : forall a b, b~=0 -> (a rem b == 0 <-> a mod b == 0). @@ -248,7 +248,7 @@ Qed. Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a). Proof. intros a b c Ha Hb (c',Hc). exists c'. - now rewrite mul_comm, <- divide_div_mul_exact, mul_comm, Hc. + now rewrite <- divide_div_mul_exact, <- Hc. Qed. Lemma lcm_least : forall a b c, @@ -262,14 +262,14 @@ Proof. set (g:=gcd a b) in *. assert (Ha' := divide_div g a c NEQ Ga Ha). assert (Hb' := divide_div g b c NEQ Gb Hb). - destruct Ha' as (a',Ha'). rewrite <- Ha' in Hb'. + destruct Ha' as (a',Ha'). rewrite Ha', mul_comm in Hb'. apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm]. destruct Hb' as (b',Hb'). exists b'. - rewrite <- mul_assoc, Hb'. + rewrite mul_shuffle3, <- Hb'. rewrite (proj2 (div_exact c g NEQ)). - rewrite <- Ha', mul_assoc. f_equiv. - apply div_exact; trivial. + rewrite Ha', mul_shuffle3, (mul_comm a a'). f_equiv. + symmetry. apply div_exact; trivial. apply mod_divide; trivial. apply mod_divide; trivial. transitivity a; trivial. Qed. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index e3fc512e7..44dd2c593 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -409,7 +409,7 @@ Qed. (** Gcd *) -Definition divide n m := exists p, n*p == m. +Definition divide n m := exists p, m == p*n. Local Notation "( x | y )" := (divide x y) (at level 0). Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. |