Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natural numbers are isomorphic. Added NatScope and IntScope for abstract developments.

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

10 files changed, 51 insertions, 88 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index bde3d9a920..0e47356ada 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -1,20 +1,39 @@
-Require Export NumPrelude.
 Require Export NZAxioms.
 
 Set Implicit Arguments.
 
 Module Type ZAxiomsSig.
 Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
-Open Local Scope NatIntScope.
 
-Notation Z := NZ (only parsing).
-Notation E := NZE (only parsing).
+Delimit Scope IntScope with Int.
+Notation Z := NZ.
+Notation Zeq := NZeq.
+Notation Z0 := NZ0.
+Notation Z1 := (NZsucc NZ0).
+Notation S := NZsucc.
+Notation P := NZpred.
+Notation Zplus := NZplus.
+Notation Ztimes := NZtimes.
+Notation Zminus := NZminus.
+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 "1" := (NZsucc NZ0) : IntScope.
+Notation "x + y" := (NZplus x y) : IntScope.
+Notation "x - y" := (NZminus x y) : IntScope.
+Notation "x * y" := (NZtimes x y) : IntScope.
+Notation "x < y" := (NZlt x y) : IntScope.
+Notation "x <= y" := (NZle x y) : IntScope.
+Notation "x > y" := (NZlt y x) (only parsing) : IntScope.
+Notation "x >= y" := (NZle y x) (only parsing) : IntScope.
 
 Parameter Zopp : Z -> Z.
 
-Add Morphism Zopp with signature E ==> E as Zopp_wd.
+Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
 
-Notation "- x" := (Zopp x) (at level 35, right associativity) : NatIntScope.
+Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
+
+Open Local Scope IntScope.
 
 (* Integers are obtained by postulating that every number has a predecessor *)
 Axiom Zsucc_pred : forall n : Z, S (P n) == n.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 9f5ff8bd37..dbe2aa4396 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -1,8 +1,9 @@
 Require Export ZAxioms.
 Require Import NZTimesOrder.
 
-Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Open Local Scope NatIntScope.
+Module ZBasePropFunct (Export ZAxiomsMod : ZAxiomsSig).
+
+Open Local Scope IntScope.
 
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
@@ -22,7 +23,7 @@ Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
 Theorem Zcentral_induction :
-forall A : Z -> Prop, predicate_wd E A ->
+forall A : Z -> Prop, predicate_wd Zeq A ->
   forall z : Z, A z ->
     (forall n : Z, A n <-> A (S n)) ->
       forall n : Z, A n.
diff --git a/theories/Numbers/Integer/Abstract/ZDec.v b/theories/Numbers/Integer/Abstract/ZDec.v
deleted file mode 100644
index 843b48b936..0000000000
--- a/theories/Numbers/Integer/Abstract/ZDec.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
-
-
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 7ace860f38..3146b9c2c3 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -3,13 +3,13 @@ Require Export NumPrelude.
 Module Type ZDomainSignature.
 
 Parameter Inline Z : Set.
-Parameter Inline E : Z -> Z -> Prop.
+Parameter Inline Zeq : Z -> Z -> Prop.
 Parameter Inline e : Z -> Z -> bool.
 
-Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
-Axiom E_equiv : equiv Z E.
+Axiom E_equiv_e : forall x y : Z, Zeq x y <-> e x y.
+Axiom E_equiv : equiv Z Zeq.
 
-Add Relation Z E
+Add Relation Z Zeq
  reflexivity proved by (proj1 E_equiv)
  symmetry proved by (proj2 (proj2 E_equiv))
  transitivity proved by (proj1 (proj2 E_equiv))
@@ -17,15 +17,15 @@ as E_rel.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
-Notation "x == y" := (E x y) (at level 70) : IntScope.
-Notation "x # y" := (~ E x y) (at level 70) : IntScope.
+Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
+Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope.
 
 End ZDomainSignature.
 
 Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
 Open Local Scope IntScope.
 
-Add Morphism e with signature E ==> E ==> eq_bool as e_wd.
+Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
 Proof.
 intros x x' Exx' y y' Eyy'.
 case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
@@ -49,7 +49,7 @@ Qed.
 
 Declare Left Step ZE_stepl.
 
-(* The right step lemma is just transitivity of E *)
+(* The right step lemma is just transitivity of Zeq *)
 Declare Right Step (proj1 (proj2 E_equiv)).
 
 End ZDomainProperties.
diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v
index e0ef2f15d9..7eed9a8eeb 100644
--- a/theories/Numbers/Integer/Abstract/ZOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZOrder.v
@@ -2,7 +2,7 @@ Require Export ZTimes.
 
 Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZTimesPropMod := ZTimesPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 (* Axioms *)
 
@@ -140,21 +140,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem Zright_induction :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
         forall n : Z, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem Zleft_induction :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, n < z -> A (S n) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem Zorder_induction :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
       (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -162,7 +162,7 @@ Theorem Zorder_induction :
 Proof NZorder_induction.
 
 Theorem Zorder_induction' :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
       (forall n : Z, n <= z -> A n -> A (P n)) ->
@@ -175,7 +175,7 @@ unfold predicate_wd, fun_wd in A_wd; apply -> (A_wd (P (S m)) m);
 Qed.
 
 Theorem Zright_induction' :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
@@ -183,7 +183,7 @@ Theorem Zright_induction' :
 Proof NZright_induction'.
 
 Theorem Zstrong_right_induction' :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
@@ -193,7 +193,7 @@ Proof NZstrong_right_induction'.
 (** Elimintation principle for < *)
 
 Theorem Zlt_ind :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall n : Z,
       A (S n) ->
       (forall m : Z, n < m -> A m -> A (S m)) ->
@@ -203,7 +203,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem Zle_ind :
-  forall A : Z -> Prop, predicate_wd E A ->
+  forall A : Z -> Prop, predicate_wd Zeq A ->
     forall n : Z,
       A n ->
       (forall m : Z, n <= m -> A m -> A (S m)) ->
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index c22b346b43..bae74feca2 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -2,7 +2,7 @@ Require Export ZBase.
 
 Module ZPlusPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 Theorem Zplus_0_l : forall n : Z, 0 + n == n.
 Proof NZplus_0_l.
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index 6a13aa3db6..49fd6f5588 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -2,7 +2,7 @@ Require Export ZOrder.
 
 Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 (** Theorems that are true on both natural numbers and integers *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZPred.v b/theories/Numbers/Integer/Abstract/ZPred.v
deleted file mode 100644
index 4814ab086b..0000000000
--- a/theories/Numbers/Integer/Abstract/ZPred.v
+++ /dev/null
@@ -1,54 +0,0 @@
-Axiom succ_pred : forall x : Z, S (P x) == x.
-Add Morphism P with signature E ==> E as pred_wd.
-
-Theorem pred_inj : forall x y, P x == P y -> x == y.
-Proof.
-intros x y H.
-setoid_replace x with (S (P x)); [| symmetry; apply succ_pred].
-setoid_replace y with (S (P y)); [| symmetry; apply succ_pred].
-now rewrite H.
-Qed.
-
-Theorem pred_succ : forall x, P (S x) == x.
-Proof.
-intro x.
-apply succ_inj.
-now rewrite succ_pred.
-Qed.
-
-(* The following tactics are intended for replacing a certain
-occurrence of a term t in the goal by (S (P t)) or by (P (S t)).
-Unfortunately, this cannot be done by setoid_replace tactic for two
-reasons. First, it seems impossible to do rewriting when one side of
-the equation in question (succ_pred or pred_succ) is a variable, due to bug 1604.
-This does not work even when the predicate is an identifier (e.g.,
-when one tries to rewrite (A x) into (A (S (P x)))). Second, the
-setoid_rewrite tactic, like the ordinary rewrite tactic, does not
-allow specifying the exact occurrence of the term to be rewritten. Now
-while not in the setoid context, this occurrence can be specified
-using the pattern tactic, it does not work with setoids, since pattern
-creates a lambda abstractuion, and setoid_rewrite does not work with
-them. *)
-
-Ltac rewrite_succP t set_tac repl thm :=
-let x := fresh "x" in
-set_tac x t;
-setoid_replace x with (repl x); [| symmetry; apply thm];
-unfold x; clear x.
-
-Tactic Notation "rewrite_succ_pred" constr(t) :=
-rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) succ_pred.
-
-Tactic Notation "rewrite_succ_pred" constr(t) "at" integer(k) :=
-rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) succ_pred.
-
-Tactic Notation "rewrite_pred_succ" constr(t) :=
-rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) pred_succ.
-
-Tactic Notation "rewrite_pred_succ" constr(t) "at" integer(k) :=
-rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) pred_succ.
-
-(* One can add tactic notations for replacements in assumptions rather
-than in the goal. For the reason of many possible variants, the core
-of the tactic is factored out. *)
-
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index bc7321cbae..0290c237bb 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -3,7 +3,7 @@ Require Export ZPlus.
 
 Module ZTimesPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusPropMod := ZPlusPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
 Proof NZtimes_0_r.
@@ -48,7 +48,7 @@ Proof NZtimes_neq_0.
 
 (** Z forms a ring *)
 
-Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZE.
+Lemma Zring : ring_theory 0 1 NZplus NZtimes NZminus Zopp NZeq.
 Proof.
 constructor.
 exact Zplus_0_l.
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index 4381420950..b1a0551f89 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -2,7 +2,7 @@ Require Export ZPlusOrder.
 
 Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod.
-Open Local Scope NatIntScope.
+Open Local Scope IntScope.
 
 (** Theorems that are true on both natural numbers and integers *)