An update on theories/Numbers.

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

2 files changed, 22 insertions, 228 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 4019b47742..d3c0410ea5 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -4,154 +4,17 @@ Require Export NZAxioms.
 Set Implicit Arguments.
 
 Module Type ZAxiomsSig.
+Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
+Open Local Scope NatIntScope.
 
-Parameter Inline Z : Set.
-Parameter Inline ZE : Z -> Z -> Prop.
-Parameter Inline Z0 : Z.
-Parameter Inline Zsucc : Z -> Z.
-Parameter Inline Zpred : Z -> Z.
-Parameter Inline Zplus : Z -> Z -> Z.
-Parameter Inline Zminus : Z -> Z -> Z.
-Parameter Inline Ztimes : Z -> Z -> Z.
-Parameter Inline Zlt : Z -> Z -> Prop.
-Parameter Inline Zle : Z -> Z -> Prop.
+Notation Z := NZ (only parsing).
+Notation E := NZE (only parsing).
 
-Delimit Scope IntScope with Int.
-Open Local Scope IntScope.
-Notation "x == y" := (ZE x y) (at level 70, no associativity) : IntScope.
-Notation "x ~= y" := (~ ZE x y) (at level 70, no associativity) : IntScope.
-Notation "0" := Z0 : IntScope.
-Notation "'S'" := Zsucc : IntScope.
-Notation "'P'" := Zpred : IntScope.
-Notation "1" := (S 0) : IntScope.
-Notation "x + y" := (Zplus x y) : IntScope.
-Notation "x - y" := (Zminus x y) : IntScope.
-Notation "x * y" := (Ztimes x y) : IntScope.
-Notation "x < y" := (Zlt x y) : IntScope.
-Notation "x <= y" := (Zle x y) : IntScope.
-Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
-Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
+(** Integers are obtained by postulating that every number has a predecessor *)
+Axiom S_P : forall n : Z, S (P n) == n.
 
-Axiom ZE_equiv : equiv Z ZE.
+End ZAxiomsSig.
 
-Add Relation Z ZE
- reflexivity proved by (proj1 ZE_equiv)
- symmetry proved by (proj2 (proj2 ZE_equiv))
- transitivity proved by (proj1 (proj2 ZE_equiv))
-as ZE_rel.
-
-Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
-Add Morphism Zpred with signature ZE ==> ZE as Zpred_wd.
-Add Morphism Zplus with signature ZE ==> ZE ==> ZE as Zplus_wd.
-Add Morphism Zminus with signature ZE ==> ZE ==> ZE as Zminus_wd.
-Add Morphism Ztimes with signature ZE ==> ZE ==> ZE as Ztimes_wd.
-Add Morphism Zlt with signature ZE ==> ZE ==> iff as Zlt_wd.
-Add Morphism Zle with signature ZE ==> ZE ==> iff as Zle_wd.
-
-Axiom S_inj : forall x y : Z, S x == S y -> x == y.
-Axiom S_P : forall x : Z, S (P x) == x.
-
-Axiom induction :
-  forall Q : Z -> Prop,
-    pred_wd E Q -> Q 0 ->
-    (forall x, Q x -> Q (S x)) ->
-    (forall x, Q x -> Q (P x)) -> forall x, Q x.
-
-End IntSignature.
-
-Module IntProperties (Import IntModule : IntSignature).
-Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule.
-Open Local Scope IntScope.
-
-Ltac induct n :=
-  try intros until n;
-  pattern n; apply induction; clear n;
-  [unfold NumPrelude.pred_wd;
-  let n := fresh "n" in
-  let m := fresh "m" in
-  let H := fresh "H" in intros n m H; qmorphism n m | | |].
-
-Theorem P_inj : forall x y, P x == P y -> x == y.
-Proof.
-intros x y H.
-setoid_replace x with (S (P x)); [| symmetry; apply S_P].
-setoid_replace y with (S (P y)); [| symmetry; apply S_P].
-now rewrite H.
-Qed.
-
-Theorem P_S : forall x, P (S x) == x.
-Proof.
-intro x.
-apply S_inj.
-now rewrite S_P.
-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 (S_P or P_S) 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 (Q x) into (Q (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_SP 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_S_P" constr(t) :=
-rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) S_P.
-
-Tactic Notation "rewrite_S_P" constr(t) "at" integer(k) :=
-rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) S_P.
-
-Tactic Notation "rewrite_P_S" constr(t) :=
-rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) P_S.
-
-Tactic Notation "rewrite_P_S" constr(t) "at" integer(k) :=
-rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) P_S.
-
-(* 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. *)
-
-Section Induction.
-
-Variable Q : Z -> Prop.
-Hypothesis Q_wd : pred_wd E Q.
-
-Add Morphism Q with signature E ==> iff as Q_morph.
-Proof Q_wd.
-
-Theorem induction_n :
-  forall n, Q n ->
-    (forall m, Q m -> Q (S m)) ->
-    (forall m, Q m -> Q (P m)) -> forall m, Q m.
-Proof.
-induct n.
-intros; now apply induction.
-intros n IH H1 H2 H3; apply IH; try assumption. apply H3 in H1; now rewrite P_S in H1.
-intros n IH H1 H2 H3; apply IH; try assumption. apply H2 in H1; now rewrite S_P in H1.
-Qed.
-
-End Induction.
-
-Ltac induct_n k n :=
-  try intros until k;
-  pattern k; apply induction_n with (n := n); clear k;
-  [unfold NumPrelude.pred_wd;
-  let n := fresh "n" in
-  let m := fresh "m" in
-  let H := fresh "H" in intros n m H; qmorphism n m | | |].
-
-End IntProperties.
 
 (*
  Local Variables:
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index e0b753d4e6..8f5c284e74 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -1,98 +1,29 @@
-Require Export NumPrelude.
-Require Import NZBase.
+Require Export ZAxioms.
+Require Import NZTimesOrder.
 
-Module Type ZBaseSig.
+Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).
+Open Local Scope NatIntScope.
 
-Parameter Z : Set.
-Parameter ZE : Z -> Z -> Prop.
-
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with Z.
-Open Local Scope IntScope.
-
-Notation "x == y"  := (ZE x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ ZE x y) (at level 70) : IntScope.
-
-Axiom ZE_equiv : equiv Z ZE.
-
-Add Relation Z ZE
- reflexivity proved by (proj1 ZE_equiv)
- symmetry proved by (proj2 (proj2 ZE_equiv))
- transitivity proved by (proj1 (proj2 ZE_equiv))
-as ZE_rel.
-
-Parameter Z0 : Z.
-Parameter Zsucc : Z -> Z.
-
-Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd.
-
-Notation "0" := Z0 : IntScope.
-Notation "'S'" := Zsucc : IntScope.
-Notation "1" := (S 0) : IntScope.
-(* Note: if we put the line declaring 1 before the line declaring 'S' and
-change (S 0) to (Zsucc 0), then 1 will be parsed but not printed ((S 0)
-will be printed instead of 1) *)
-
-Axiom Zsucc_inj : forall x y : Z, S x == S y -> x == y.
-
-Axiom Zinduction :
-  forall A : predicate Z, predicate_wd ZE A ->
-    A 0 -> (forall x, A x <-> A (S x)) -> forall x, A x.
-
-End ZBaseSig.
-
-Module ZBasePropFunct (Import ZBaseMod : ZBaseSig).
-Open Local Scope IntScope.
-
-Module NZBaseMod <: NZBaseSig.
-
-Definition NZ := Z.
-Definition NZE := ZE.
-Definition NZ0 := Z0.
-Definition NZsucc := Zsucc.
-
-(* Axioms *)
-Definition NZE_equiv := ZE_equiv.
-
-Add Relation NZ NZE
- reflexivity proved by (proj1 NZE_equiv)
- symmetry proved by (proj2 (proj2 NZE_equiv))
- transitivity proved by (proj1 (proj2 NZE_equiv))
-as NZE_rel.
-
-Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
-Proof Zsucc_wd.
-
-Definition NZsucc_inj := Zsucc_inj.
-Definition NZinduction := Zinduction.
-
-End NZBaseMod.
-
-Module Export NZBasePropMod := NZBasePropFunct NZBaseMod.
+Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
 Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n.
 Proof NZneq_symm.
 
-Theorem Zcentral_induction :
-  forall A : Z -> Prop, predicate_wd ZE A ->
-    forall z : Z, A z ->
-      (forall n : Z, A n <-> A (S n)) ->
-        forall n : Z, A n.
-Proof NZcentral_induction.
+Theorem Zsucc_inj : forall n1 n2 : Z, S n1 == S n2 -> n1 == n2.
+Proof NZsucc_inj.
 
-Theorem Zsucc_inj_wd : forall n m, S n == S m <-> n == m.
+Theorem Zsucc_inj_wd : forall n1 n2 : Z, S n1 == S n2 <-> n1 == n2.
 Proof NZsucc_inj_wd.
 
-Theorem Zsucc_inj_neg : forall n m, S n ~= S m <-> n ~= m.
+Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m.
 Proof NZsucc_inj_wd_neg.
 
-Tactic Notation "Zinduct" ident(n) :=
-  induction_maker n ltac:(apply Zinduction).
-(* FIXME: Zinduction probably has to be redeclared in the functor because
-the parameters like Zsucc are not unfolded for Zinduction in the signature *)
-
-Tactic Notation "Zinduct" ident(n) constr(z) :=
-  induction_maker n ltac:(apply Zcentral_induction with z).
+Theorem Zcentral_induction :
+forall A : Z -> Prop, predicate_wd E A ->
+  forall z : Z, A z ->
+    (forall n : Z, A n <-> A (S n)) ->
+      forall n : Z, A n.
+Proof NZcentral_induction.
 
 End ZBasePropFunct.