SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax

 To retrieve the old behavior of spec_sub0 and spec_sub with
 precondition on order, just chain spec_sub with Zmax_r or Zmax_l.
 Idem with spec_pred0 and spec_pred.

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

1 files changed, 15 insertions, 15 deletions

diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index dc2225634..615b8d139 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -191,7 +191,7 @@ Module Make (N:NType) <: ZType.
  simpl; generalize (N.spec_compare N.zero x); case N.compare;
    rewrite N.spec_0; simpl.
   intros HH; rewrite <- HH; rewrite N.spec_1; ring.
-  intros HH; rewrite N.spec_pred; auto with zarith.
+  intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith.
  generalize (N.spec_pos x); auto with zarith.
  Qed.
 
@@ -218,13 +218,13 @@ Module Make (N:NType) <: ZType.
    exact (N.spec_add x y).
  unfold zero; generalize (N.spec_compare x y); case N.compare.
    rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
  unfold zero; generalize (N.spec_compare x y); case N.compare.
    rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
- intros; rewrite N.spec_add; try ring; auto with zarith.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
+ intros; rewrite N.spec_add; auto with zarith.
  Qed.
 
  Definition pred x :=
@@ -241,7 +241,7 @@ Module Make (N:NType) <: ZType.
  unfold pred, to_Z, minus_one; intros [x | x].
    generalize (N.spec_compare N.zero x); case N.compare;
      rewrite N.spec_0; try rewrite N.spec_1; auto with zarith.
-   intros H; exact (N.spec_pred _ H).
+   intros H; rewrite N.spec_pred, Zmax_r; auto with zarith.
  generalize (N.spec_pos x); auto with zarith.
  rewrite N.spec_succ; ring.
  Qed.
@@ -268,14 +268,14 @@ Module Make (N:NType) <: ZType.
  unfold sub, to_Z; intros [x | x] [y | y].
  unfold zero; generalize (N.spec_compare x y); case N.compare.
    rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
- rewrite N.spec_add; ring.
- rewrite N.spec_add; ring.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
+ rewrite N.spec_add; auto with zarith.
+ rewrite N.spec_add; auto with zarith.
  unfold zero; generalize (N.spec_compare x y); case N.compare.
    rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
- intros; rewrite N.spec_sub; try ring; auto with zarith.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
+ intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
  Qed.
 
  Definition mul x y :=
@@ -398,7 +398,7 @@ Module Make (N:NType) <: ZType.
  rewrite N.spec_0; intros H2.
  change (- Zpos p) with (Zneg p); lazy iota beta.
  intros H3; rewrite <- H3; auto.
- rewrite N.spec_succ; rewrite N.spec_sub.
+ rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r.
  generalize H2; case (N.to_Z r).
  intros; apply False_ind; auto with zarith.
  intros p2 _; rewrite He; auto with zarith.
@@ -430,7 +430,7 @@ Module Make (N:NType) <: ZType.
  rewrite N.spec_0; intros H2.
  change (- Zpos p1) with (Zneg p1); lazy iota beta.
  intros H3; rewrite <- H3; auto.
- rewrite N.spec_succ; rewrite N.spec_sub.
+ rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r.
  generalize H2; case (N.to_Z r).
  intros; apply False_ind; auto with zarith.
  intros p2 _; rewrite He; auto with zarith.