Adding BigQ and proofs

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

2 files changed, 133 insertions, 2 deletions

diff --git a/theories/Ints/Z/ZAux.v b/theories/Ints/Z/ZAux.v
index 3f0c7a5c65..83c54bd478 100644
--- a/theories/Ints/Z/ZAux.v
+++ b/theories/Ints/Z/ZAux.v
@@ -729,6 +729,60 @@ apply Zgcd_is_gcd.
 inversion_clear H3; auto.
 Qed.
 
+ Theorem Zggcd_opp: 
+   forall x y, Zggcd (-x) y = 
+      let (p1,p) := Zggcd x y in
+      let (p2,p3) := p in
+       (p1,(-p2,p3))%Z.
+ intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto.
+ case Pggcd; intros p1 (p2, p3); auto.
+ case Pggcd; intros p1 (p2, p3); auto.
+ case Pggcd; intros p1 (p2, p3); auto.
+ case Pggcd; intros p1 (p2, p3); auto.
+ Qed.
+
+ Theorem Zgcd_inv_0_l: forall x y, (Zgcd x y = 0)%Z -> x = 0%Z.
+ intros x y H.
+ assert (F1: (Zdivide 0 x)%Z).
+  rewrite <- H.
+  generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
+ inversion F1 as[z H1].
+ rewrite H1; ring.
+ Qed.
+
+ Theorem Zgcd_inv_0_r: forall x y, (Zgcd x y = 0)%Z -> y = 0%Z.
+ intros x y H.
+ assert (F1: (Zdivide 0 y)%Z).
+  rewrite <- H.
+  generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto.
+ inversion F1 as[z H1].
+ rewrite H1; ring.
+ Qed.
+
+ Theorem Zgcd_div: forall a b c,
+  (0 < c -> (c | b) -> (a * b)/c = a * (b/c))%Z.
+ intros a b c H1 H2.
+ inversion H2 as [z Hz].
+ rewrite Hz; rewrite Zmult_assoc.
+ repeat rewrite Z_div_mult; auto with zarith.
+ Qed.
+
+ Theorem Zgcd_div_swap a b c:
+ (0 < Zgcd a b)%Z ->
+ (0 < b)%Z ->
+ (c * a / Zgcd a b * b)%Z = (c * a * (b/Zgcd a b))%Z.
+ intros a b c Hg Hb.
+ assert (F := (Zgcd_is_gcd a b)); inversion F as [F1 F2 F3].
+ pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+ repeat rewrite Zmult_assoc.
+ apply f_equal2 with (f := Zmult); auto.
+ rewrite Zgcd_div; auto.
+ rewrite <- Zmult_assoc.
+ rewrite (fun x y => Zmult_comm (x /y)); 
+   rewrite <- (Zdivide_Zdiv_eq); auto.
+ Qed.
+
+
 (**************************************
   Properties rel_prime
 **************************************)
@@ -1233,6 +1287,56 @@ intros z n; unfold Zpower_nat_tr.
 rewrite Zpower_tr_aux_correct with (p := 0%nat); auto.
 Qed.
 
+
+ Theorem Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
+ Proof.
+ intros x; unfold Zpower_pos; simpl; ring.
+ Qed.
+
+ Theorem Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1%Z.
+ Proof.
+ intros p; elim p; clear p.
+ intros p Hrec.
+   rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l.
+   repeat rewrite Zpower_pos_is_exp.
+   rewrite Zpower_pos_1_r.
+   rewrite Hrec; ring.
+ intros p Hrec.
+   rewrite <- Pplus_diag.
+   repeat rewrite Zpower_pos_is_exp.
+   rewrite Hrec; ring.
+ rewrite Zpower_pos_1_r; auto.
+ Qed.
+
+
+
+ Theorem Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0%Z.
+ intros p; elim p; clear p.
+ intros p H1.
+ change (xI p) with (1 + (xO p))%positive.
+ rewrite Zpower_pos_is_exp; rewrite Zpower_pos_1_r; auto.
+ intros p Hrec; rewrite <- Pplus_diag; 
+  rewrite Zpower_pos_is_exp; rewrite Hrec; auto.
+ rewrite Zpower_pos_1_r; auto.
+ Qed.
+
+
+ Theorem Zpower_pos_pos: forall x p, 
+     (0 < x -> 0 < Zpower_pos x p)%Z.
+ Proof.
+ intros x p; elim p; clear p.
+ intros p Hrec H0.
+ rewrite xI_succ_xO; rewrite <- Pplus_diag; rewrite Pplus_one_succ_l.
+   repeat rewrite Zpower_pos_is_exp.
+   rewrite Zpower_pos_1_r.
+   repeat apply Zmult_lt_0_compat; auto.
+ intros p Hrec H0.
+ rewrite <- Pplus_diag.
+   repeat rewrite Zpower_pos_is_exp.
+   repeat apply Zmult_lt_0_compat; auto.
+ rewrite Zpower_pos_1_r; auto.
+ Qed.
+
 (************************************** 
   Definition of Zsquare 
 **************************************)
diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v
index cb6a01fcd3..127d3cefab 100644
--- a/theories/Ints/Z/ZDivModAux.v
+++ b/theories/Ints/Z/ZDivModAux.v
@@ -211,9 +211,24 @@ Hint Resolve Zlt_gt Zle_ge: zarith.
   rewrite Zmult_assoc; apply Z_div_mod_eq; auto with zarith.
  Qed.
 
- Theorem Zdiv_0: forall a, 0 < a -> 0 / a = 0.
+ Theorem Zdiv_0_l: forall a, 0 / a = 0.
  Proof.
-  intros a H;apply sym_equal;apply Zdiv_unique with (r := 0); auto with zarith.
+  intros a; case a; auto.
+ Qed.
+
+ Theorem Zdiv_0_r: forall a, a / 0 = 0.
+ Proof.
+  intros a; case a; auto.
+ Qed.
+
+ Theorem Zmod_0_l: forall a, 0 mod a = 0.
+ Proof.
+  intros a; case a; auto.
+ Qed.
+
+ Theorem Zmod_0_r: forall a, a mod 0 = 0.
+ Proof.
+  intros a; case a; auto.
  Qed.
 
  Theorem Zdiv_le_upper_bound: 
@@ -449,4 +464,16 @@ Hint Resolve Zlt_gt Zle_ge: zarith.
   destruct x;change (0<y);auto with zarith.
   destruct p;trivial;discriminate z.
  Qed.
+
+
+ Theorem Zgcd_div_pos a b:
+   (0 < b)%Z -> (0 < Zgcd a b)%Z -> (0 < b / Zgcd a b)%Z.
+ intros a b Ha Hg.
+ case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto.
+ apply Zdiv_pos; auto with zarith.
+ intros H; generalize Ha.
+ pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto.
+ rewrite <- H; auto with zarith.
+ assert (F := (Zgcd_is_gcd a b)); inversion F; auto.
+ Qed.