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

3 files changed, 10 insertions, 33 deletions

diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index d890d9287b..a08c6e62f9 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 b439462db3..7373acc9ad 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 82d65dafb1..67411eac81 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.