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

4 files changed, 74 insertions, 98 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.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index c22680be3..769d804d7 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -1129,7 +1129,7 @@ let _ =
   pr "  end.";
   pr "";
 
-  pr " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.";
+  pr " Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1.";
   pa " Admitted.";
   pp " Proof.";
   pp " intros x; case x; unfold pred.";
@@ -1172,8 +1172,17 @@ let _ =
   pp " case (spec_to_Z (wn_spec n) y1); intros HH3 HH4; auto with zarith.";
   pp " intros; exact (spec_0 w0_spec).";
   pp " Qed.";
-  pr " ";
+  pr "";
 
+  pr " Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1).";
+  pa " Admitted.";
+  pp " Proof.";
+  pp " intros. destruct (Zle_lt_or_eq _ _ (spec_pos x)).";
+  pp " rewrite Zmax_r; auto with zarith.";
+  pp " apply spec_pred_pos; auto.";
+  pp " rewrite <- H; apply spec_pred0; auto.";
+  pp " Qed.";
+  pr "";
 
   pr " (***************************************************************)";
   pr " (*                                                             *)";
@@ -1238,7 +1247,7 @@ let _ =
   pr "subn).";
   pr "";
 
-  pr " Theorem spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].";
+  pr " Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y].";
   pa " Admitted.";
   pp " Proof.";
   pp " unfold sub.";
@@ -1286,6 +1295,16 @@ let _ =
   pp " Qed.";
   pr "";
 
+  pr " Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]).";
+  pa " Admitted.";
+  pp " Proof.";
+  pp " intros. destruct (Zle_or_lt [y] [x]).";
+  pp " rewrite Zmax_r; auto with zarith. apply spec_sub_pos; auto.";
+  pp " rewrite Zmax_l; auto with zarith. apply spec_sub0; auto.";
+  pp " Qed.";
+  pr "";
+
+
 
   pr " (***************************************************************)";
   pr " (*                                                             *)";
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 5295aaec2..2dfa783aa 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -69,13 +69,11 @@ Module Type NType.
 
  Parameter pred : t -> t.
 
- Parameter spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.
- Parameter spec_pred0: forall x, [x] = 0 -> [pred x] = 0.
+ Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
 
  Parameter sub : t -> t -> t.
 
- Parameter spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].
- Parameter spec_sub0: forall x y, [x] < [y]-> [sub x y] = 0.
+ Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]).
 
  Parameter mul : t -> t -> t.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 919701879..2b199858f 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -17,59 +17,36 @@ Require Import NSig.
 
 Module NSig_NAxioms (N:NType) <: NAxiomsSig.
 
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with N.t.
-Local Open Scope IntScope.
-Notation "[ x ]" := (N.to_Z x) : IntScope.
-Infix "=="  := N.eq (at level 70) : IntScope.
-Notation "0" := N.zero : IntScope.
-Infix "+" := N.add : IntScope.
-Infix "-" := N.sub : IntScope.
-Infix "*" := N.mul : IntScope.
-
-Hint Rewrite N.spec_0 N.spec_succ N.spec_add N.spec_mul : int.
-Ltac isimpl := autorewrite with int.
+Delimit Scope NumScope with Num.
+Bind Scope NumScope with N.t.
+Local Open Scope NumScope.
+Notation "[ x ]" := (N.to_Z x) : NumScope.
+Infix "=="  := N.eq (at level 70) : NumScope.
+Notation "0" := N.zero : NumScope.
+Infix "+" := N.add : NumScope.
+Infix "-" := N.sub : NumScope.
+Infix "*" := N.mul : NumScope.
+
+Hint Rewrite
+ N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub : num.
+Ltac nsimpl := autorewrite with num.
+Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence.
+
+Obligation Tactic := ncongruence.
 
 Instance eq_equiv : Equivalence N.eq.
 
-Instance succ_wd : Proper (N.eq==>N.eq) N.succ.
-Proof.
-unfold N.eq; repeat red; intros; isimpl; f_equal; auto.
-Qed.
-
-Instance pred_wd : Proper (N.eq==>N.eq) N.pred.
-Proof.
-unfold N.eq; repeat red; intros.
-generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0).
-destruct N.eq_bool; rewrite N.spec_0; intros.
-rewrite 2 N.spec_pred0; congruence.
-rewrite 2 N.spec_pred; f_equal; auto; try omega.
-Qed.
-
-Instance add_wd : Proper (N.eq==>N.eq==>N.eq) N.add.
-Proof.
-unfold N.eq; repeat red; intros; isimpl; f_equal; auto.
-Qed.
-
-Instance sub_wd : Proper (N.eq==>N.eq==>N.eq) N.sub.
-Proof.
-unfold N.eq; intros x x' Hx y y' Hy.
-destruct (Z_lt_le_dec [x] [y]).
-rewrite 2 N.spec_sub0; f_equal; congruence.
-rewrite 2 N.spec_sub; f_equal; congruence.
-Qed.
-
-Instance mul_wd : Proper (N.eq==>N.eq==>N.eq) N.mul.
-Proof.
-unfold N.eq; repeat red; intros; isimpl; f_equal; auto.
-Qed.
+Program Instance succ_wd : Proper (N.eq==>N.eq) N.succ.
+Program Instance pred_wd : Proper (N.eq==>N.eq) N.pred.
+Program Instance add_wd : Proper (N.eq==>N.eq==>N.eq) N.add.
+Program Instance sub_wd : Proper (N.eq==>N.eq==>N.eq) N.sub.
+Program Instance mul_wd : Proper (N.eq==>N.eq==>N.eq) N.mul.
 
 Theorem pred_succ : forall n, N.pred (N.succ n) == n.
 Proof.
 unfold N.eq; repeat red; intros.
 rewrite N.spec_pred; rewrite N.spec_succ.
-omega.
-generalize (N.spec_pos n); omega.
+generalize (N.spec_pos n); omega with *.
 Qed.
 
 Definition N_of_Z z := N.of_N (Zabs_N z).
@@ -118,52 +95,38 @@ End Induction.
 
 Theorem add_0_l : forall n, 0 + n == n.
 Proof.
-intros; red; isimpl; auto with zarith.
+intros; red; nsimpl; auto with zarith.
 Qed.
 
 Theorem add_succ_l : forall n m, (N.succ n) + m == N.succ (n + m).
 Proof.
-intros; red; isimpl; auto with zarith.
+intros; red; nsimpl; auto with zarith.
 Qed.
 
 Theorem sub_0_r : forall n, n - 0 == n.
 Proof.
-intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith.
-apply N.spec_pos.
+intros; red; nsimpl. generalize (N.spec_pos n); omega with *.
 Qed.
 
 Theorem sub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m).
 Proof.
-intros; red.
-destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H].
-rewrite N.spec_sub0; auto.
-rewrite N.spec_succ in H.
-rewrite N.spec_pred0; auto.
-destruct (Z_eq_dec [n] [m]).
-rewrite N.spec_sub; auto with zarith.
-rewrite N.spec_sub0; auto with zarith.
-
-rewrite N.spec_sub, N.spec_succ in *; auto.
-rewrite N.spec_pred, N.spec_sub; auto with zarith.
-rewrite N.spec_sub; auto with zarith.
+intros; red; nsimpl. omega with *.
 Qed.
 
 Theorem mul_0_l : forall n, 0 * n == 0.
 Proof.
-intros; red.
-rewrite N.spec_mul, N.spec_0; auto with zarith.
+intros; red; nsimpl; auto with zarith.
 Qed.
 
 Theorem mul_succ_l : forall n m, (N.succ n) * m == n * m + m.
 Proof.
-intros; red.
-rewrite N.spec_add, 2 N.spec_mul, N.spec_succ; ring.
+intros; red; nsimpl. ring.
 Qed.
 
 (** Order *)
 
-Infix "<=" := N.le : IntScope.
-Infix "<" := N.lt : IntScope.
+Infix "<=" := N.le : NumScope.
+Infix "<" := N.lt : NumScope.
 
 Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z.
 Proof.
@@ -223,33 +186,29 @@ Qed.
 
 Theorem min_l : forall n m, n <= m -> N.min n m == n.
 Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
+intros n m; red; rewrite spec_le, spec_min; omega with *.
 Qed.
 
 Theorem min_r : forall n m, m <= n -> N.min n m == m.
 Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
+intros n m; red; rewrite spec_le, spec_min; omega with *.
 Qed.
 
 Theorem max_l : forall n m, m <= n -> N.max n m == n.
 Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
+intros n m; red; rewrite spec_le, spec_max; omega with *.
 Qed.
 
 Theorem max_r : forall n m, n <= m -> N.max n m == m.
 Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
+intros n m; red; rewrite spec_le, spec_max; omega with *.
 Qed.
 
 (** Properties specific to natural numbers, not integers. *)
 
 Theorem pred_0 : N.pred 0 == 0.
 Proof.
-red; rewrite N.spec_pred0; rewrite N.spec_0; auto.
+red; nsimpl; auto.
 Qed.
 
 Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=