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/Natural | |
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/Natural')
-rw-r--r-- | theories/Numbers/Natural/Abstract/NGcd.v | 14 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NLcm.v | 16 | ||||
-rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 16 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 6 |
4 files changed, 27 insertions, 25 deletions
diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v index 1192e5cdc..ece369d80 100644 --- a/theories/Numbers/Natural/Abstract/NGcd.v +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -27,7 +27,7 @@ Definition divide_antisym n m : (n | m) -> (m | n) -> n == m Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p). Proof. intros n m p (q,Hq) (r,Hr). - exists (r-q). rewrite mul_sub_distr_l, Hq, Hr. + exists (r-q). rewrite mul_sub_distr_r, <- Hq, <- Hr. now rewrite add_comm, add_sub. Qed. @@ -194,15 +194,15 @@ Proof. assert (G := gcd_nonneg n m). le_elim 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, Hq, Hr; order. + apply mul_cancel_r with (gcd n m); [order|]. + rewrite mul_1_l. + rewrite <- gcd_mul_mono_r, <- Hq, <- Hr; order. symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order. Qed. diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 321508f58..1e8e678c6 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -30,9 +30,9 @@ Module Type NLcmProp 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 divide_div_mul_exact : forall a b c, b~=0 -> (b|a) -> @@ -132,7 +132,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, @@ -146,14 +146,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/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 8a26ec6e3..b6b26363e 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -343,7 +343,7 @@ Fixpoint gcd a b := | S a' => gcd (b mod (S a')) (S a') end. -Definition divide x y := exists z, x*z=y. +Definition divide x y := exists z, y=z*x. Notation "( x | y )" := (divide x y) (at level 0) : nat_scope. Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b). @@ -351,17 +351,18 @@ Proof. fix 1. intros [|a] b; simpl. split. - exists 0; now rewrite <- mult_n_O. - exists 1; now rewrite <- mult_n_Sm, <- mult_n_O. + now exists 0. + exists 1. simpl. now rewrite <- plus_n_O. fold (b mod (S a)). destruct (gcd_divide (b mod (S a)) (S a)) as (H,H'). set (a':=S a) in *. split; auto. rewrite (div_mod b a') at 2 by discriminate. destruct H as (u,Hu), H' as (v,Hv). + rewrite mult_comm. exists ((b/a')*v + u). - rewrite mult_plus_distr_l. - now rewrite (mult_comm _ v), mult_assoc, Hv, Hu. + rewrite mult_plus_distr_r. + now rewrite <- mult_assoc, <- Hv, <- Hu. Qed. Lemma gcd_divide_l : forall a b, (gcd a b | a). @@ -383,8 +384,9 @@ Proof. set (a':=S a) in *. rewrite (div_mod b a') in H' by discriminate. destruct H as (u,Hu), H' as (v,Hv). - exists (v - u * (b/a')). - now rewrite mult_minus_distr_l, mult_assoc, Hu, Hv, minus_plus. + exists (v - (b/a')*u). + rewrite mult_comm in Hv. + now rewrite mult_minus_distr_r, <- Hv, <-mult_assoc, <-Hu, minus_plus. Qed. (** * Bitwise operations *) diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 878e46fea..33181e32a 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -331,7 +331,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]. @@ -341,8 +341,8 @@ Proof. intros (z,H). exists (of_N (Zabs_N z)). zify. rewrite Z_of_N_abs. rewrite <- (Zabs_eq [n]) by apply spec_pos. - rewrite <- Zabs_Zmult, H. - apply Zabs_eq, spec_pos. + rewrite <- Zabs_Zmult, <- H. + symmetry. apply Zabs_eq, spec_pos. Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). |