Simplification of Numbers, mainly thanks to Include

 - No more nesting of Module and Module Type, we rather use Include.
 - Instead of in-name-qualification like NZeq, we use uniform
   short names + modular qualification like N.eq when necessary.
 - Many simplification of proofs, by some autorewrite for instance
 - In NZOrder, we instantiate an "order" tactic.
 - Some requirements in NZAxioms were superfluous: compatibility
   of le, min and max could be derived from the rest.
 - NMul removed, since it was containing only an ad-hoc result for
   ZNatPairs, that we've inlined in the proof of mul_wd there.
 - Zdomain removed (was already not compiled), idea of a module
   with eq and eqb reused in DecidableType.BooleanEqualityType.
 - ZBinDefs don't contain any definition now, migrate it to ZBinary.

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

14 files changed, 90 insertions, 95 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 32d150331..9ad1d019e 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -22,7 +22,7 @@ Require Import Znumtheory.
 Require Import BigNumPrelude.
 Require Import DoubleType.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (** First, a description via an operator record and a spec record. *)
 
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 2076a9ab2..b99df747a 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -25,71 +25,72 @@ Require Import CyclicAxioms.
 
 Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
-Definition NZ := w.
+Definition t := w.
 
-Definition NZ_to_Z : NZ -> Z := znz_to_Z w_op.
-Definition Z_to_NZ : Z -> NZ := znz_of_Z w_op.
-Notation Local wB := (base w_op.(znz_digits)).
+Definition NZ_to_Z : t -> Z := znz_to_Z w_op.
+Definition Z_to_NZ : Z -> t := znz_of_Z w_op.
+Local Notation wB := (base w_op.(znz_digits)).
 
-Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
+Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
 
-Definition NZeq (n m : NZ) := [| n |] = [| m |].
-Definition NZ0 := w_op.(znz_0).
-Definition NZsucc := w_op.(znz_succ).
-Definition NZpred := w_op.(znz_pred).
-Definition NZadd := w_op.(znz_add).
-Definition NZsub := w_op.(znz_sub).
-Definition NZmul := w_op.(znz_mul).
+Definition eq (n m : t) := [| n |] = [| m |].
+Definition zero := w_op.(znz_0).
+Definition succ := w_op.(znz_succ).
+Definition pred := w_op.(znz_pred).
+Definition add := w_op.(znz_add).
+Definition sub := w_op.(znz_sub).
+Definition mul := w_op.(znz_mul).
 
-Instance NZeq_equiv : Equivalence NZeq.
+Delimit Scope NumScope with Num.
+Bind Scope NumScope with t.
+Local Open Scope NumScope.
+Notation "x == y"  := (eq x y) (at level 70) : NumScope.
+Notation "0" := zero : NumScope.
+Notation S := succ.
+Notation P := pred.
+Notation "x + y" := (add x y) : NumScope.
+Notation "x - y" := (sub x y) : NumScope.
+Notation "x * y" := (mul x y) : NumScope.
 
-Instance NZsucc_wd : Proper (NZeq ==> NZeq) NZsucc.
+
+Hint Rewrite w_spec.(spec_0) w_spec.(spec_succ) w_spec.(spec_pred)
+ w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_sub) : w.
+Ltac wsimpl :=
+ unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w.
+Ltac wcongruence := repeat red; intros; wsimpl; congruence.
+
+Instance eq_equiv : Equivalence eq.
+
+Instance succ_wd : Proper (eq ==> eq) succ.
 Proof.
-unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H.
+wcongruence.
 Qed.
 
-Instance NZpred_wd : Proper (NZeq ==> NZeq) NZpred.
+Instance pred_wd : Proper (eq ==> eq) pred.
 Proof.
-unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H.
+wcongruence.
 Qed.
 
-Instance NZadd_wd : Proper (NZeq ==> NZeq ==> NZeq) NZadd.
+Instance add_wd : Proper (eq ==> eq ==> eq) add.
 Proof.
-unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add).
-now rewrite H1, H2.
+wcongruence.
 Qed.
 
-Instance NZsub_wd : Proper (NZeq ==> NZeq ==> NZeq) NZsub.
+Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
 Proof.
-unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub).
-now rewrite H1, H2.
+wcongruence.
 Qed.
 
-Instance NZmul_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmul.
+Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
 Proof.
-unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul).
-now rewrite H1, H2.
+wcongruence.
 Qed.
 
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with NZ.
-Open Local Scope IntScope.
-Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
-Notation "0" := NZ0 : IntScope.
-Notation S x := (NZsucc x).
-Notation P x := (NZpred x).
-(*Notation "1" := (S 0) : IntScope.*)
-Notation "x + y" := (NZadd x y) : IntScope.
-Notation "x - y" := (NZsub x y) : IntScope.
-Notation "x * y" := (NZmul x y) : IntScope.
-
 Theorem gt_wB_1 : 1 < wB.
 Proof.
-unfold base.
-apply Zpower_gt_1; unfold Zlt; auto with zarith.
+unfold base. apply Zpower_gt_1; unfold Zlt; auto with zarith.
 Qed.
 
 Theorem gt_wB_0 : 0 < wB.
@@ -97,7 +98,7 @@ Proof.
 pose proof gt_wB_1; auto with zarith.
 Qed.
 
-Lemma NZsucc_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
+Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
 Proof.
 intro n.
 pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zplus_mod.
@@ -105,7 +106,7 @@ reflexivity.
 now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
 Qed.
 
-Lemma NZpred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
+Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
 Proof.
 intro n.
 pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zminus_mod.
@@ -113,31 +114,32 @@ reflexivity.
 now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
 Qed.
 
-Lemma NZ_to_Z_mod : forall n : NZ, [| n |] mod wB = [| n |].
+Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].
 Proof.
 intro n; rewrite Zmod_small. reflexivity. apply w_spec.(spec_to_Z).
 Qed.
 
-Theorem NZpred_succ : forall n : NZ, P (S n) == n.
+Theorem pred_succ : forall n, P (S n) == n.
 Proof.
-intro n; unfold NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred), w_spec.(spec_succ).
-rewrite <- NZpred_mod_wB.
+intro n. wsimpl.
+rewrite <- pred_mod_wB.
 replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod.
 Qed.
 
-Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int.
+Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Num.
 Proof.
-unfold NZeq, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct.
-symmetry; apply w_spec.(spec_0).
+unfold NZ_to_Z, Z_to_NZ. wsimpl.
+rewrite znz_of_Z_correct; auto.
 exact w_spec. split; [auto with zarith |apply gt_wB_0].
 Qed.
 
 Section Induction.
 
-Variable A : NZ -> Prop.
-Hypothesis A_wd : Proper (NZeq ==> iff) A.
+Variable A : t -> Prop.
+Hypothesis A_wd : Proper (eq ==> iff) A.
 Hypothesis A0 : A 0.
-Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *)
+Hypothesis AS : forall n, A n <-> A (S n).
+ (* Below, we use only -> direction *)
 
 Let B (n : Z) := A (Z_to_NZ n).
 
@@ -150,8 +152,8 @@ Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
 Proof.
 intros n H1 H2 H3.
 unfold B in *. apply -> AS in H3.
-setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZeq. assumption.
-unfold NZeq. rewrite w_spec.(spec_succ).
+setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)). assumption.
+wsimpl.
 unfold NZ_to_Z, Z_to_NZ.
 do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]).
 symmetry; apply Zmod_small; auto with zarith.
@@ -164,11 +166,11 @@ apply Zbounded_induction with wB.
 apply B0. apply BS. assumption. assumption.
 Qed.
 
-Theorem NZinduction : forall n : NZ, A n.
+Theorem bi_induction : forall n, A n.
 Proof.
-intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZeq.
+intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)).
 apply B_holds. apply w_spec.(spec_to_Z).
-unfold NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
+unfold eq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct.
 reflexivity.
 exact w_spec.
 apply w_spec.(spec_to_Z).
@@ -176,47 +178,40 @@ Qed.
 
 End Induction.
 
-Theorem NZadd_0_l : forall n : NZ, 0 + n == n.
+Theorem add_0_l : forall n, 0 + n == n.
 Proof.
-intro n; unfold NZadd, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0).
+intro n. wsimpl.
 rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)].
 Qed.
 
-Theorem NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m).
+Theorem add_succ_l : forall n m, (S n) + m == S (n + m).
 Proof.
-intros n m; unfold NZadd, NZsucc, NZeq. rewrite w_spec.(spec_add).
-do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add).
-rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
+intros n m. wsimpl.
+rewrite succ_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.
 rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l.
 rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc.
 Qed.
 
-Theorem NZsub_0_r : forall n : NZ, n - 0 == n.
+Theorem sub_0_r : forall n, n - 0 == n.
 Proof.
-intro n; unfold NZsub, NZ0, NZeq. rewrite w_spec.(spec_sub).
-rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod.
+intro n. wsimpl. rewrite Zminus_0_r. apply NZ_to_Z_mod.
 Qed.
 
-Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m).
+Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).
 Proof.
-intros n m; unfold NZsub, NZsucc, NZpred, NZeq.
-rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub).
-rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r.
-rewrite Zminus_mod_idemp_l.
-now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith.
+intros n m. wsimpl. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l.
+now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z
+     by auto with zarith.
 Qed.
 
-Theorem NZmul_0_l : forall n : NZ, 0 * n == 0.
+Theorem mul_0_l : forall n, 0 * n == 0.
 Proof.
-intro n; unfold NZmul, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul).
-rewrite w_spec.(spec_0). now rewrite Zmult_0_l.
+intro n. wsimpl. now rewrite Zmult_0_l.
 Qed.
 
-Theorem NZmul_succ_l : forall n m : NZ, (S n) * m == n * m + m.
+Theorem mul_succ_l : forall n m, (S n) * m == n * m + m.
 Proof.
-intros n m; unfold NZmul, NZsucc, NZadd, NZeq. rewrite w_spec.(spec_mul).
-rewrite w_spec.(spec_add), w_spec.(spec_mul), w_spec.(spec_succ).
-rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
+intros n m. wsimpl. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.
 now rewrite Zmult_plus_distr_l, Zmult_1_l.
 Qed.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index b4f6a8160..aa798e1c7 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -17,7 +17,7 @@ Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section DoubleAdd.
  Variable w : Type.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index 82480fa2e..88c34915d 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -16,7 +16,7 @@ Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import DoubleType.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section DoubleBase.
  Variable w : Type.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index db3b622b0..eea29e7ca 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -25,7 +25,7 @@ Require Import DoubleDivn1.
 Require Import DoubleDiv.
 Require Import CyclicAxioms.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 
 Section Z_2nZ.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 89c37c0f9..9204b4e05 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -20,7 +20,7 @@ Require Import DoubleDivn1.
 Require Import DoubleAdd.
 Require Import DoubleSub.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Ltac zarith := auto with zarith.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index fd6718e4e..386bbb9e5 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -17,7 +17,7 @@ Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section GENDIVN1.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
index 28dff1a29..21e694e57 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
@@ -17,7 +17,7 @@ Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section DoubleLift.
  Variable w : Type.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index b215f6a86..7090c76a8 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
@@ -17,7 +17,7 @@ Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section DoubleMul.
  Variable w : Type.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index ac2232cc0..83a2e7177 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -17,7 +17,7 @@ Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section DoubleSqrt.
  Variable w              : Type.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
index d3a08c6e0..a7e556713 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
@@ -17,7 +17,7 @@ Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import DoubleBase.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section DoubleSub.
  Variable w : Type.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 3bd4b8127..88cbb484f 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -13,7 +13,7 @@
 Set Implicit Arguments.
 
 Require Import ZArith.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Definition base digits := Zpower 2 (Zpos digits).
 
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 6e71bad82..67d15b499 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1182,11 +1182,11 @@ End Int31_Op.
 
 Section Int31_Spec.
 
- Open Local Scope Z_scope.
+ Local Open Scope Z_scope.
 
  Notation "[| x |]" := (phi x)  (at level 0, x at level 99).
 
- Notation Local wB := (2 ^ (Z_of_nat size)).
+ Local Notation wB := (2 ^ (Z_of_nat size)).
 
  Lemma wB_pos : wB > 0.
  Proof.
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 1b1283400..4f0f6c7c4 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -24,7 +24,7 @@ Require Import BigNumPrelude.
 Require Import DoubleType.
 Require Import CyclicAxioms.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Section ZModulo.