Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements

 Mostly results about Zgcd (commutativity, associativity, ...).
 Slight improvement of ZMicromega.

 Beware: some lemmas of Zdiv/ Znumtheory were asking for
 too strict or useless hypothesis. Some minor glitches may occur.

 By the way, some iff lemmas about negb in Bool.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 100 insertions, 92 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 2995f0515..dcb10f3cf 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -202,6 +202,16 @@ Proof.
   destruct b; trivial.
 Qed.
 
+Lemma negb_true_iff : forall b, negb b = true <-> b = false.
+Proof.
+ destruct b; intuition.
+Qed.
+
+Lemma negb_false_iff : forall b, negb b = false <-> b = true.
+Proof.
+ destruct b; intuition.
+Qed.
+
 
 (********************************)
 (** * Properties of [orb]     *)
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index ae2f0a298..7ec360a66 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -734,7 +734,7 @@ generalize (equal_mem_2 _ _ H x).
 rewrite filter_b; auto.
 rewrite empty_mem.
 rewrite H0; simpl;intros.
-replace true with (negb false);auto;apply negb_sym;auto.
+rewrite <- negb_false_iff; auto.
 Qed.
 
 Lemma for_all_mem_3: 
@@ -762,7 +762,7 @@ exists x.
 rewrite filter_b in H1; auto.
 elim (andb_prop _ _ H1).
 split;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
+rewrite <- negb_true_iff; auto.
 Qed.
 
 (** Properties of [exists] *)
@@ -794,8 +794,8 @@ Proof.
 intros.
 rewrite for_all_exists; auto.
 rewrite for_all_mem_1;auto with bool.
-intros;generalize (H x H0);intros. 
-symmetry;apply negb_sym;simpl;auto.
+intros;generalize (H x H0);intros.
+rewrite negb_true_iff; auto.
 Qed.
 
 Lemma exists_mem_2: 
@@ -803,9 +803,9 @@ Lemma exists_mem_2:
 Proof.
 intros.
 rewrite for_all_exists in H; auto.
-replace false with (negb true);auto;apply negb_sym;symmetry.
-rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
+rewrite negb_false_iff in H.
+rewrite <- negb_true_iff.
+apply for_all_mem_2 with (2:=H); auto.
 Qed.
 
 Lemma exists_mem_3: 
@@ -813,9 +813,9 @@ Lemma exists_mem_3:
 Proof.
 intros.
 rewrite for_all_exists; auto.
-symmetry;apply negb_sym;simpl.
+rewrite negb_true_iff.
 apply for_all_mem_3 with x;auto.
-rewrite H0;auto.
+rewrite negb_false_iff; auto.
 Qed.
 
 Lemma exists_mem_4: 
@@ -823,11 +823,11 @@ Lemma exists_mem_4:
 Proof.
 intros.
 rewrite for_all_exists in H; auto.
-elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
+rewrite negb_true_iff in H.
+elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto.
 elim p;intros.
 exists x;split;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
+rewrite <-negb_false_iff; auto.
 Qed.
 
 End Bool'.
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index d890d9287..a08c6e62f 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -356,20 +356,6 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  compute in H1; discriminate.
  compute; auto.
  Qed.
- 
- Lemma Zgcd_Zabs : forall z z', Zgcd (Zabs z) z' = Zgcd z z'.
- Proof.
- destruct z; simpl; auto.
- Qed.
-
- Lemma Zgcd_sym : forall p q, Zgcd p q = Zgcd q p.
- Proof.
- intros.
- apply Zis_gcd_gcd.
- apply Zgcd_is_pos.
- apply Zis_gcd_sym.
- apply Zgcd_is_gcd.
- Qed.
 
  Lemma Zdiv_gcd_zero : forall a b, b / Zgcd a b = 0 -> b <> 0 -> 
   Zgcd a b = 0.
@@ -383,12 +369,6 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  intros; subst k; simpl in *; subst b; elim H0; auto.
  Qed.
 
- Lemma Zgcd_1 : forall z, Zgcd z 1 = 1.
- Proof.
- intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
- Qed.
- Hint Resolve Zgcd_1.
-
  Lemma Zgcd_mult_rel_prime : forall a b c, 
   Zgcd a c = 1 -> Zgcd b c = 1 -> Zgcd (a*b) c = 1.
  Proof.
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index b439462db..7373acc9a 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -546,7 +546,6 @@ Section ZModulo.
   apply Z_div_pos; auto with zarith.
   subst a; auto with zarith.
   apply Zdiv_lt_upper_bound; auto with zarith.
-  subst a; auto with zarith.
   subst a.
   replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring.
   apply Zlt_le_trans with ([|a1|]*wB+wB); auto with zarith.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 82d65dafb..67411eac8 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -140,7 +140,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
   Zcompare_spec_alt Ncompare_spec_alt
   Z.spec_add N.spec_add Z.spec_mul N.spec_mul 
-  Z.spec_gcd N.spec_gcd Zgcd_Zabs
+  Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1
   spec_Z_of_N spec_Zabs_N
  : nz.
  Ltac nzsimpl := autorewrite with nz in *.
@@ -279,7 +279,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  replace (N.to_Z q) with 0%Z in * by romega.
  rewrite Zdiv_0_l in H0; discriminate.
  (* Gt *)
- simpl; auto.
+ simpl; auto with zarith.
  Qed.
 
  (** Reduction function : producing irreducible fractions *) 
@@ -304,7 +304,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros [ z | n d ].
  unfold red.
- symmetry; apply Qred_identity; simpl; auto.
+ symmetry; apply Qred_identity; simpl; auto with zarith.
  unfold red; apply strong_spec_norm.
  Qed.
    
@@ -700,7 +700,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  unfold Reduced; intros.
  rewrite strong_spec_red, Qred_iff.
  destruct x as [zx|nx dx]; destruct y as [zy|ny dy].
- simpl in *; auto.
+ simpl in *; auto with zarith.
  simpl.
  rewrite <- Qred_iff, <- strong_spec_red, strong_spec_mul_norm_Qz_Qq; auto.
  simpl.
@@ -714,10 +714,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (Hgc' := strong_spec_irred ny dx).
  destruct irred as (n1,d1); destruct irred as (n2,d2). 
  simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
- destr_neq_bool; simpl; nzsimpl; intros.
- apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
- destr_neq_bool; simpl; nzsimpl; intros.
- auto.
+ destr_neq_bool; simpl; nzsimpl; intros; auto.
+ destr_neq_bool; simpl; nzsimpl; intros; auto.
 
  revert H H0.
  rewrite 2 strong_spec_red, 2 Qred_iff; simpl.
@@ -729,8 +727,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite N_to_Z2P in *; auto.
  rewrite Z2P_correct.
 
- apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; 
-  apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; auto.
+ apply Zgcd_mult_rel_prime; rewrite Zgcd_comm;
+  apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto.
  
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
@@ -912,7 +910,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite Zabs_eq; auto with zarith.
  rewrite N_to_Z2P in *; auto.
  rewrite Z2P_correct; auto with zarith.
- rewrite Zgcd_sym; auto.
+ rewrite Zgcd_comm; auto.
  (* 0 > n *)
  destr_neq_bool; nzsimpl; simpl; auto; intros.
  destr_zcompare; simpl; nzsimpl; auto.
@@ -928,7 +926,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite N_to_Z2P in *; auto.
  rewrite Z2P_correct; auto with zarith.
  intros.
- rewrite Zgcd_sym, Zgcd_Zabs, Zgcd_sym.
+ rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm.
  apply Zis_gcd_gcd; auto with zarith.
  apply Zis_gcd_minus.
  rewrite Zopp_involutive, <- H1; apply Zgcd_is_gcd.
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
index 03e061f29..758b22817 100644
--- a/theories/ZArith/ZOdiv.v
+++ b/theories/ZArith/ZOdiv.v
@@ -547,16 +547,14 @@ Qed.
 (** Some additionnal inequalities about Zdiv. *)
 
 Theorem ZOdiv_le_upper_bound: 
-  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
+  forall a b q, 0 < b -> a <= q*b -> a/b <= q.
 Proof.
-  intros a b q H1 H2 H3.
-  apply Zmult_le_reg_r with b; auto with zarith.
-  apply Zle_trans with (2 := H3).
-  pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith.
-  rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
+  intros.
+  rewrite <- (ZO_div_mult q b); auto with zarith.
+  apply ZO_div_monotone; auto with zarith.
 Qed.
 
-Theorem ZOdiv_lt_upper_bound: 
+Theorem ZOdiv_lt_upper_bound:
   forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
 Proof.
   intros a b q H1 H2 H3.
@@ -566,16 +564,12 @@ Proof.
   rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
 Qed.
 
-Theorem ZOdiv_le_lower_bound: 
-  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Theorem ZOdiv_le_lower_bound:
+  forall a b q, 0 < b -> q*b <= a -> q <= a/b.
 Proof.
-  intros a b q H1 H2 H3.
-  assert (q < a / b + 1); auto with zarith.
-  apply Zmult_lt_reg_r with b; auto with zarith.
-  apply Zle_lt_trans with (1 := H3).
-  pattern a at 1; rewrite (ZO_div_mod_eq a b); auto with zarith.
-  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b);
-   auto with zarith.
+  intros.
+  rewrite <- (ZO_div_mult q b); auto with zarith.
+  apply ZO_div_monotone; auto with zarith.
 Qed.
 
 Theorem ZOdiv_sgn: forall a b, 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 4de7e8218..f341b193e 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -588,39 +588,32 @@ Qed.
 
 (** Some additionnal inequalities about Zdiv. *)
 
-Theorem Zdiv_le_upper_bound: 
-  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
+Theorem Zdiv_lt_upper_bound:
+  forall a b q, 0 < b -> a < q*b -> a/b < q.
 Proof.
-  intros a b q H1 H2 H3.
-  apply Zmult_le_reg_r with b; auto with zarith.
-  apply Zle_trans with (2 := H3).
+  intros a b q H1 H2.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (2 := H2).
   pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
   rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
 Qed.
 
-Theorem Zdiv_lt_upper_bound: 
-  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
+Theorem Zdiv_le_upper_bound:
+  forall a b q, 0 < b -> a <= q*b -> a/b <= q.
 Proof.
-  intros a b q H1 H2 H3.
-  apply Zmult_lt_reg_r with b; auto with zarith.
-  apply Zle_lt_trans with (2 := H3).
-  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
-  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+  intros.
+  rewrite <- (Z_div_mult_full q b); auto with zarith.
+  apply Z_div_le; auto with zarith.
 Qed.
 
-Theorem Zdiv_le_lower_bound: 
-  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Theorem Zdiv_le_lower_bound:
+  forall a b q, 0 < b -> q*b <= a -> q <= a/b.
 Proof.
-  intros a b q H1 H2 H3.
-  assert (q < a / b + 1); auto with zarith.
-  apply Zmult_lt_reg_r with b; auto with zarith.
-  apply Zle_lt_trans with (1 := H3).
-  pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith.
-  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (Z_mod_lt a b);
-   auto with zarith.
+  intros.
+  rewrite <- (Z_div_mult_full q b); auto with zarith.
+  apply Z_div_le; auto with zarith.
 Qed.
 
-
 (** A division of respect opposite monotonicity for the divisor *)
 
 Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 93ec1081b..f6d73d7eb 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -201,19 +201,17 @@ Qed.
 
 (** [Zdivide] can be expressed using [Zmod]. *)
 
-Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a).
+Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a).
 Proof.
-  intros a b H H0.
-  apply Zdivide_intro with (a / b).
-  pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H).
-  rewrite H0; ring.
+ intros a b NZ EQ.
+ apply Zdivide_intro with (a/b).
+ rewrite (Z_div_mod_eq_full a b NZ) at 1.
+ rewrite EQ; ring.
 Qed.
 
-Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0.
+Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0.
 Proof.
-  intros a b; simple destruct 2; intros; subst.
-  change (q * b) with (0 + q * b) in |- *.
-  rewrite Z_mod_plus; auto.
+  intros a b (c,->); apply Z_mod_mult.
 Qed.
 
 (** [Zdivide] is hence decidable *)
@@ -1131,6 +1129,42 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
+Lemma Zgcd_comm : forall a b, Zgcd a b = Zgcd b a.
+Proof.
+  intros.
+  apply Zis_gcd_gcd.
+  apply Zgcd_is_pos.
+  apply Zis_gcd_sym.
+  apply Zgcd_is_gcd.
+Qed.
+
+Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c).
+Proof.
+  intros.
+  apply Zis_gcd_gcd.
+  apply Zgcd_is_pos.
+  destruct (Zgcd_is_gcd a b).
+  destruct (Zgcd_is_gcd b c).
+  destruct (Zgcd_is_gcd a (Zgcd b c)).
+  constructor; eauto using Zdivide_trans.
+Qed.
+
+Lemma Zgcd_Zabs : forall a b, Zgcd (Zabs a) b = Zgcd a b.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zgcd_0 : forall a, Zgcd a 0 = Zabs a.
+Proof.
+  destruct a; simpl; auto.
+Qed.
+
+Lemma Zgcd_1 : forall a, Zgcd a 1 = 1.
+Proof.
+  intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
+Qed.
+Hint Resolve Zgcd_0 Zgcd_1 : zarith.
+
 Theorem Zgcd_1_rel_prime : forall a b, 
  Zgcd a b = 1 <-> rel_prime a b.
 Proof.