BinInt: Z.add become the alternative Z.add'

 It relies on Z.pos_sub instead of a Pos.compare followed by Pos.sub.
 Proofs seem to be quite easy to adapt, via some rewrite Z.pos_sub_spec.

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

4 files changed, 35 insertions, 60 deletions

diff --git a/plugins/setoid_ring/Cring_initial.v b/plugins/setoid_ring/Cring_initial.v
index 3cd9d4d3e..ca894027a 100644
--- a/plugins/setoid_ring/Cring_initial.v
+++ b/plugins/setoid_ring/Cring_initial.v
@@ -146,15 +146,11 @@ Ltac rsimpl := simpl;  set_cring_notations.
  Qed.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1
-    match (x ?= y)%positive with
-    | Eq => Z0
-    | Lt => Zneg (y - x)
-    | Gt => Zpos (x - y)
-    end
+ gen_phiZ1 (Z.pos_sub x y)
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
+  rewrite Z.pos_sub_spec.
   assert (H0 := Pminus_mask_Gt x y). unfold Pgt in H0.
   assert (H1 := Pminus_mask_Gt y x). unfold Pgt in H1.
   rewrite Pos.compare_antisym in H1.
@@ -181,10 +177,8 @@ Ltac rsimpl := simpl;  set_cring_notations.
   induction x;destruct y;simpl;norm.
   apply ARgen_phiPOS_add.
   apply gen_phiZ1_add_pos_neg.
-  rewrite Pos.compare_antisym;simpl.
-  cring_rewrite match_compOpp.
-  cring_rewrite cring_add_comm.
-  apply gen_phiZ1_add_pos_neg.
+  rewrite gen_phiZ1_add_pos_neg.
+  cring_rewrite cring_add_comm. norm.
   cring_rewrite ARgen_phiPOS_add; norm.
  Qed.
 
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 766473c6f..6f4747dcf 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -732,6 +732,14 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
  Notation pow_pos_plus :=  (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext)
                         ARth.(ARmul_comm) ARth.(ARmul_assoc)).
 
+ Lemma Z_pos_sub_gt : forall p q, (p > q)%positive ->
+  Z.pos_sub p q = Zpos (p - q).
+ Proof.
+  intros. apply Z.pos_sub_gt. now apply Pos.gt_lt.
+ Qed.
+
+ Ltac simpl_pos_sub := rewrite ?Z_pos_sub_gt in * by assumption.
+
  Lemma isIn_correct_aux : forall l e1 e2 p1 p2,
   match
       (if  PExpr_eq e1 e2 then
@@ -751,6 +759,7 @@ Fixpoint isIn (e1:PExpr C)  (p1:positive)
 Proof.
   intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2);
    case (PExpr_eq e1 e2); simpl; auto; intros H.
+  rewrite Z.pos_sub_spec.
   case_eq ((p1 ?= p2)%positive);intros;simpl.
   repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
   rewrite (Pcompare_Eq_eq _ _ H0).
@@ -763,22 +772,17 @@ Proof.
   rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial.
   repeat rewrite pow_th.(rpow_pow_N);simpl.
   rewrite H;trivial.
-   change (ZtoN
-     match (p1 ?= p1 - p2)%positive with
-     | Eq => 0
-     | Lt => Zneg (p1 - p2 - p1)
-     | Gt => Zpos (p1 - (p1 - p2))
-     end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))).
+   change (Z.pos_sub p1 (p1-p2)) with (Zpos p1 - Zpos (p1 -p2))%Z.
   replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z.
   split.
   repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth).
-  rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl.
+  rewrite Zplus_assoc, Z.add_opp_diag_r. simpl.
   ring [ (morph1 CRmorph)].
  assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _).
  apply Zplus_gt_reg_l with (Zpos p2).
  rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z.
  apply Zplus_gt_compat_r. refine (refl_equal _).
- simpl;rewrite H0;trivial.
+ simpl. now simpl_pos_sub.
 Qed.
 
 Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2).
@@ -808,7 +812,7 @@ destruct n.
   destruct n;simpl.
     rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl.
     intros (H1,H2) (H3,H4).
-    unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
+    simpl_pos_sub. simpl in H3.
     rewrite pow_pos_mul. rewrite H1;rewrite H3.
     assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
         (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) ==
@@ -818,11 +822,10 @@ destruct n.
    split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial.
    repeat rewrite pow_th.(rpow_pow_N);simpl.
    intros (H1,H2) (H3,H4).
-   unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3.
-   rewrite H2 in H1;simpl in H1.
+   simpl_pos_sub. simpl in H1, H3.
    assert (Zpos p1 > Zpos p6)%Z.
      apply Zgt_trans with (Zpos p4). exact H4. exact H2.
-  unfold Zgt in H;simpl in H;rewrite H.
+  simpl_pos_sub.
   split. 2:exact H.
   rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3.
   assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 *
@@ -835,12 +838,12 @@ destruct n.
   assert
      (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
  change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
- rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)%Z).
- simpl. rewrite Pcompare_refl. simpl. reflexivity.
+ rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)).
+ simpl. rewrite Z.pos_sub_diag. simpl. reflexivity.
  unfold Zminus, Zopp in H0. simpl in H0.
-  rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
+  simpl_pos_sub. inversion H0; trivial.
  simpl. repeat rewrite pow_th.(rpow_pow_N).
- intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3.
+ intros H1 (H2,H3). simpl_pos_sub.
  rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
  simpl in H2. rewrite pow_th.(rpow_pow_N);simpl.
  rewrite pow_pos_mul. split. ring [H2]. exact H3.
@@ -851,8 +854,7 @@ destruct n.
  rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl.
  repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul.
  intros (H1, H2);rewrite H1;split.
-   unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1.
-   simpl in H1;ring [H1]. trivial.
+   simpl_pos_sub. simpl in H1;ring [H1]. trivial.
  trivial.
  destruct n. trivial.
  generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3.
@@ -910,8 +912,7 @@ Proof.
      repeat rewrite NPEpow_correct;simpl;
      repeat rewrite pow_th.(rpow_pow_N);simpl).
   intros (H, Hgt);split;try ring [H CRmorph.(morph1)].
-  intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H.
-  simpl in H;split;try ring [H].
+  intros (H, Hgt). simpl_pos_sub. simpl in H;split;try ring [H].
   rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial.
   simpl;intros. repeat rewrite NPEmul_correct;simpl.
   rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)].
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 56935bb79..9e4ac94b4 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -170,16 +170,11 @@ Section ZMORPHISM.
   rewrite H1;rrefl.
  Qed.
 
- Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1
-    match (x ?= y)%positive with
-    | Eq => Z0
-    | Lt => Zneg (y - x)
-    | Gt => Zpos (x - y)
-    end
- == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Lemma gen_phiZ1_pos_sub : forall x y,
+ gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
+  rewrite Z.pos_sub_spec.
   case Pos.compare_spec; intros H; simpl.
   rewrite H. rewrite (Ropp_def Rth);rrefl.
   rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
@@ -190,21 +185,13 @@ Section ZMORPHISM.
   add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
  Qed.
 
- Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
-  match CompOpp x with Eq => be | Lt => bl | Gt => bg end
-  = match x with Eq => be | Lt => bg | Gt => bl end.
- Proof. destruct x;simpl;intros;trivial. Qed.
-
  Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
  Proof.
   intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
-  induction x;destruct y;simpl;norm.
+  destruct x, y; simpl; norm.
   apply (ARgen_phiPOS_add ARth).
-  apply gen_phiZ1_add_pos_neg.
-  rewrite Pos.compare_antisym.
-  rewrite match_compOpp.
-  rewrite (Radd_comm Rth).
-  apply gen_phiZ1_add_pos_neg.
+  apply gen_phiZ1_pos_sub.
+  rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
   rewrite (ARgen_phiPOS_add ARth); norm.
  Qed.
 
diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ring2_initial.v
index f94ad9b0f..7c5631d4e 100644
--- a/plugins/setoid_ring/Ring2_initial.v
+++ b/plugins/setoid_ring/Ring2_initial.v
@@ -146,15 +146,11 @@ Ltac rsimpl := simpl;  set_ring_notations.
  Qed.
 
  Lemma gen_phiZ1_add_pos_neg : forall x y,
- gen_phiZ1
-    match (x ?= y)%positive with
-    | Eq => Z0
-    | Lt => Zneg (y - x)
-    | Gt => Zpos (x - y)
-    end
+ gen_phiZ1 (Z.pos_sub x y)
  == gen_phiPOS1 x + -gen_phiPOS1 y.
  Proof.
   intros x y.
+  rewrite Z.pos_sub_spec.
   assert (H0 := Pminus_mask_Gt x y). unfold Pos.gt in H0.
   assert (H1 := Pminus_mask_Gt y x). unfold Pos.gt in H1.
   rewrite Pos.compare_antisym in H1.
@@ -181,11 +177,8 @@ Ltac rsimpl := simpl;  set_ring_notations.
   induction x;destruct y;simpl;norm.
   apply ARgen_phiPOS_add.
   apply gen_phiZ1_add_pos_neg.
-  replace Eq with (CompOpp Eq);trivial.
-  rewrite Pos.compare_antisym;simpl.
-  ring_rewrite match_compOpp.
-  ring_rewrite ring_add_comm.
-  apply gen_phiZ1_add_pos_neg.
+  rewrite gen_phiZ1_add_pos_neg.
+  ring_rewrite ring_add_comm. norm.
   ring_rewrite ARgen_phiPOS_add; norm.
  Qed.