diff options
| -rw-r--r-- | theories/NArith/BinNat.v | 10 | ||||
| -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 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZGcd.v | 50 | ||||
| -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 | ||||
| -rw-r--r-- | theories/PArith/BinPos.v | 52 | ||||
| -rw-r--r-- | theories/PArith/BinPosDef.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 14 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zquot.v | 3 |
16 files changed, 136 insertions, 111 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 2ca046808..228be4d1a 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -60,7 +60,7 @@ Notation "x <= y < z" := (x <= y /\ y < z) : N_scope. Notation "x < y < z" := (x < y /\ y < z) : N_scope. Notation "x < y <= z" := (x < y /\ y <= z) : N_scope. -Definition divide p q := exists r, p*r = q. +Definition divide p q := exists r, q = r*p. Notation "( p | q )" := (divide p q) (at level 0) : N_scope. Definition Even n := exists m, n = 2*m. @@ -636,13 +636,15 @@ Qed. Lemma gcd_divide_l a b : (gcd a b | a). Proof. rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). - destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto. + destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa. + now rewrite mul_comm. Qed. Lemma gcd_divide_r a b : (gcd a b | b). Proof. rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). - destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto. + destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb. + now rewrite mul_comm. Qed. (** We now prove directly that gcd is the greatest amongst common divisors *) @@ -650,7 +652,7 @@ Qed. Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c|gcd a b). Proof. destruct a as [ |p], b as [ |q]; simpl; trivial. - destruct c as [ |r]. intros (s,H). discriminate. + destruct c as [ |r]. intros (s,H). destruct s; discriminate. intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *. destruct (Pos.gcd_greatest p q r) as (u,H). exists s. now inversion Hs. 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]. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index 6788cd4e8..f72023d92 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -18,7 +18,7 @@ End Gcd. Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A). Import A B. - Definition divide n m := exists p, n*p == m. + Definition divide n m := exists p, m == p*n. Local Notation "( n | m )" := (divide n m) (at level 0). Axiom gcd_divide_l : forall n m, (gcd n m | n). Axiom gcd_divide_r : forall n m, (gcd n m | m). @@ -83,9 +83,17 @@ Proof. rewrite <- Hn, mul_0_l in H. order'. Qed. +Lemma eq_mul_1_nonneg' : forall n m, + 0<=m -> n*m == 1 -> n==1 /\ m==1. +Proof. + intros n m Hm H. rewrite mul_comm in H. + now apply and_comm, eq_mul_1_nonneg. +Qed. + Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1. Proof. - intros n Hn (m,Hm). now apply (eq_mul_1_nonneg n m). + intros n Hn (m,Hm). symmetry in Hm. + now apply (eq_mul_1_nonneg' m n). Qed. Lemma divide_refl : forall n, (n | n). @@ -95,8 +103,8 @@ Qed. Lemma divide_trans : forall n m p, (n | m) -> (m | p) -> (n | p). Proof. - intros n m p (q,Hq) (r,Hr). exists (q*r). - now rewrite mul_assoc, Hq. + intros n m p (q,Hq) (r,Hr). exists (r*q). + now rewrite Hr, Hq, mul_assoc. Qed. Instance divide_reflexive : Reflexive divide := divide_refl. @@ -110,29 +118,29 @@ Proof. intros n m Hn Hm (q,Hq) (r,Hr). le_elim Hn. destruct (lt_ge_cases q 0) as [Hq'|Hq']. - generalize (mul_pos_neg n q Hn Hq'). order. - rewrite <- Hq, <- mul_assoc in Hr. - apply mul_id_r in Hr; [|order]. - destruct (eq_mul_1_nonneg q r) as [H _]; trivial. - now rewrite H, mul_1_r in Hq. - rewrite <- Hn, mul_0_l in Hq. now rewrite <- Hn. + generalize (mul_neg_pos q n Hq' Hn). order. + rewrite Hq, mul_assoc in Hr. symmetry in Hr. + apply mul_id_l in Hr; [|order]. + destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial. + now rewrite H, mul_1_l in Hq. + rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn. Qed. Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m). Proof. - intros n m p (q,Hq). exists q. now rewrite <- mul_assoc, Hq. + intros n m p (q,Hq). exists q. now rewrite mul_shuffle3, Hq. Qed. Lemma mul_divide_mono_r : forall n m p, (n | m) -> (n * p | m * p). Proof. - intros n m p (q,Hq). exists q. now rewrite mul_shuffle0, Hq. + intros n m p (q,Hq). exists q. now rewrite mul_assoc, Hq. Qed. Lemma mul_divide_cancel_l : forall n m p, p ~= 0 -> ((p * n | p * m) <-> (n | m)). Proof. intros n m p Hp. split. - intros (q,Hq). exists q. now rewrite <- mul_assoc, mul_cancel_l in Hq. + intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq. apply mul_divide_mono_l. Qed. @@ -145,12 +153,12 @@ Qed. Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p). Proof. intros n m p (q,Hq) (r,Hr). exists (q+r). - now rewrite mul_add_distr_l, Hq, Hr. + now rewrite mul_add_distr_r, Hq, Hr. Qed. Lemma divide_mul_l : forall n m p, (n | m) -> (n | m * p). Proof. - intros n m p (q,Hq). exists (q*p). now rewrite mul_assoc, Hq. + intros n m p (q,Hq). exists (q*p). now rewrite mul_shuffle0, Hq. Qed. Lemma divide_mul_r : forall n m p, (n | p) -> (n | m * p). @@ -172,13 +180,13 @@ Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m. Proof. intros n m Hm (q,Hq). destruct (le_gt_cases n 0) as [Hn|Hn]. order. - rewrite <- Hq. + rewrite Hq. destruct (lt_ge_cases q 0) as [Hq'|Hq']. - generalize (mul_pos_neg n q Hn Hq'). order. + generalize (mul_neg_pos q n Hq' Hn). order. le_elim Hq'. - rewrite <- (mul_1_r n) at 1. apply mul_le_mono_pos_l; trivial. + rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial. now rewrite one_succ, le_succ_l. - rewrite <- Hq', mul_0_r in Hq. order. + rewrite <- Hq', mul_0_l in Hq. order. Qed. (** Basic properties of gcd *) @@ -291,8 +299,8 @@ Qed. Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n). Proof. - intros n m Hn. split. intros (q,Hq). rewrite <- Hq. - now apply gcd_mul_diag_l. + intros n m Hn. split. intros (q,Hq). rewrite Hq. + rewrite mul_comm. now apply gcd_mul_diag_l. intros EQ. rewrite <- EQ. apply gcd_divide_r. Qed. 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). diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 852ae591d..956421785 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1292,6 +1292,11 @@ Proof. now apply mul_lt_mono_l. Qed. +Lemma mul_sub_distr_r p q r : q<p -> (p-q)*r = p*r-q*r. +Proof. + intros H. rewrite 3 (mul_comm _ r). now apply mul_sub_distr_l. +Qed. + Lemma sub_lt_mono_l p q r: q<p -> p<r -> r-p < r-q. Proof. intros Hqp Hpr. @@ -1640,11 +1645,11 @@ Lemma divide_add_cancel_l p q r : (p | r) -> (p | q + r) -> (p | q). Proof. intros (s,Hs) (t,Ht). exists (t-s). - rewrite mul_sub_distr_l. - rewrite Hs, Ht. - apply add_sub. - apply mul_lt_mono_l with p. - rewrite Hs, Ht, add_comm. + rewrite mul_sub_distr_r. + rewrite <- Hs, <- Ht. + symmetry. apply add_sub. + apply mul_lt_mono_r with p. + rewrite <- Hs, <- Ht, add_comm. apply lt_add_r. Qed. @@ -1652,20 +1657,22 @@ Lemma divide_xO_xI p q r : (p | q~0) -> (p | r~1) -> (p | q). Proof. intros (s,Hs) (t,Ht). destruct p. - destruct s; try easy. rewrite mul_xO_r in Hs. destr_eq Hs. now exists s. - discriminate. - exists q; auto. + destruct s; try easy. simpl in Hs. destr_eq Hs. now exists s. + rewrite mul_xO_r in Ht; discriminate. + exists q; now rewrite mul_1_r. Qed. Lemma divide_xO_xO p q : (p~0|q~0) <-> (p|q). Proof. - split; intros (r,H); simpl in *. destr_eq H. now exists r. - exists r; simpl; f_equal; auto. + split; intros (r,H); simpl in *. + rewrite mul_xO_r in H. destr_eq H. now exists r. + exists r; simpl. rewrite mul_xO_r. f_equal; auto. Qed. Lemma divide_mul_l p q r : (p|q) -> (p|q*r). Proof. - intros (s,H). exists (s*r). rewrite mul_assoc; now f_equal. + intros (s,H). exists (s*r). + rewrite <- mul_assoc, (mul_comm r p), mul_assoc. now f_equal. Qed. Lemma divide_mul_r p q r : (p|r) -> (p|q*r). @@ -1733,13 +1740,15 @@ Qed. Lemma gcd_divide_l : forall a b, (gcd a b | a). Proof. intros a b. rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). - destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto. + destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa. + now rewrite mul_comm. Qed. Lemma gcd_divide_r : forall a b, (gcd a b | b). Proof. intros a b. rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). - destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto. + destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb. + now rewrite mul_comm. Qed. (** We now prove directly that gcd is the greatest amongst common divisors *) @@ -1782,14 +1791,14 @@ Proof. apply divide_mul_r. apply IHn; clear IHn. apply le_S_n in LE. apply le_Sn_le. now rewrite plus_n_Sm. - apply divide_xO_xI with p; trivial. exists 1; now rewrite mul_1_r. - apply divide_xO_xI with p; trivial. exists 1; now rewrite mul_1_r. + apply divide_xO_xI with p; trivial. now exists 1. + apply divide_xO_xI with p; trivial. now exists 1. apply divide_xO_xO. apply IHn; clear IHn. apply le_S_n in LE. apply le_Sn_le. now rewrite plus_n_Sm. now apply divide_xO_xO. now apply divide_xO_xO. - exists (gcdn n a b)~0. auto. + exists (gcdn n a b)~0. now rewrite mul_1_r. Qed. Lemma gcd_greatest : forall a b p, (p|a) -> (p|b) -> (p|gcd a b). @@ -1808,11 +1817,14 @@ Proof. intros H (EQa,EQb) p Hp1 Hp2; subst. assert (H' : (g*p | g)). apply H. - destruct Hp1 as (r,Hr). exists r. now rewrite <- Hr, mul_assoc. - destruct Hp2 as (r,Hr). exists r. now rewrite <- Hr, mul_assoc. + destruct Hp1 as (r,Hr). exists r. + now rewrite mul_assoc, (mul_comm r g), <- mul_assoc, <- Hr. + destruct Hp2 as (r,Hr). exists r. + now rewrite mul_assoc, (mul_comm r g), <- mul_assoc, <- Hr. destruct H' as (q,H'). - apply mul_eq_1 with q. - apply mul_reg_l with g. now rewrite mul_assoc, mul_1_r. + rewrite (mul_comm g p), mul_assoc in H'. + apply mul_eq_1 with q; rewrite mul_comm. + now apply mul_reg_r with g. Qed. End Pos. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 9b6081176..b6b7ab7a5 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -338,7 +338,7 @@ Definition sqrt p := fst (sqrtrem p). (** ** Greatest Common Divisor *) -Definition divide p q := exists r, p*r = q. +Definition divide p q := exists r, q = r*p. Notation "( p | q )" := (divide p q) (at level 0) : positive_scope. (** Instead of the Euclid algorithm, we use here the Stein binary diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 673276d3e..379e68544 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -60,7 +60,7 @@ Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope. Notation "x < y < z" := (x < y /\ y < z) : Z_scope. Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope. -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). Definition Even a := exists b, a = 2*b. @@ -847,12 +847,12 @@ Qed. Lemma divide_Zpos_Zneg_r n p : (n|Zpos p) <-> (n|Zneg p). Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_r, H. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. Qed. Lemma divide_Zpos_Zneg_l n p : (Zpos p|n) <-> (Zneg p|n). Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_r, <- mul_opp_l. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. Qed. (** ** Correctness proofs for gcd *) @@ -876,20 +876,22 @@ Qed. Lemma gcd_divide_l a b : (gcd a b | a). Proof. rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). - destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto. + destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa. + now rewrite mul_comm. Qed. Lemma gcd_divide_r a b : (gcd a b | b). Proof. rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). - destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto. + destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb. + now rewrite mul_comm. Qed. Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b). Proof. assert (H : forall p q r, (r|Zpos p) -> (r|Zpos q) -> (r|Zpos (Pos.gcd p q))). intros p q [|r|r] H H'. - now destruct H. + destruct H; now rewrite mul_comm in *. apply divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos. apply divide_Zpos_Zneg_l, divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos, divide_Zpos_Zneg_l. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index ff221f35e..477e2e122 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -519,7 +519,7 @@ Lemma Zmod_divides : forall a b, b<>0 -> (a mod b = 0 <-> exists c, a = b*c). Proof. intros. rewrite Z.mod_divide; trivial. - split; intros (c,Hc); exists c; auto. + split; intros (c,Hc); exists c; subst; auto with zarith. Qed. (** Particular case : dividing by 2 is related with parity *) diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index b9788de8b..bbc984af1 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -39,7 +39,7 @@ Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope. Lemma Zdivide_equiv : forall a b, Z.divide a b <-> Zdivide a b. Proof. - intros a b; split; intros (c,H); exists c; rewrite Zmult_comm; auto. + intros a b; split; intros (c,H); now exists c. Qed. Lemma Zdivide_refl : forall a:Z, (a | a). diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index b8b780831..6b6ad7423 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -462,7 +462,8 @@ Lemma Zrem_divides : forall a b, Zrem a b = 0 <-> exists c, a = b*c. Proof. intros. zero_or_not b. firstorder. - rewrite Z.rem_divide; trivial. split; intros (c,Hc); exists c; auto. + rewrite Z.rem_divide; trivial. + split; intros (c,Hc); exists c; subst; auto with zarith. Qed. (** Particular case : dividing by 2 is related with parity *) |