NBinary improved, contains more, subsumes NOrderedType

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

6 files changed, 50 insertions, 125 deletions

diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 53ba50ffe7..3a87880ac2 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -14,5 +14,21 @@ Require Export BinPos.
 Require Export BinNat.
 Require Export Nnat.
 Require Export Ndigits.
-
 Require Export NArithRing.
+Require NBinary Nminmax.
+
+Module N := NBinary.N <+ Nminmax.Nextend.
+
+(** [N] contains An [order] tactic for natural numbers *)
+
+(** Note that [N.order] is domain-agnostic: it will not prove
+    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
+
+Local Open Scope N_scope.
+
+Section TestOrder.
+ Let test : forall x y, x<=y -> y<=x -> x=y.
+ Proof.
+ N.order.
+ Qed.
+End TestOrder.
diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
deleted file mode 100644
index c5dd395bb2..0000000000
--- a/theories/NArith/NOrderedType.v
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import BinNat Equalities Orders OrdersTac.
-
-Local Open Scope N_scope.
-
-(** * DecidableType structure for [N] binary natural numbers *)
-
-Module N_as_UBE <: UsualBoolEq.
- Definition t := N.
- Definition eq := @eq N.
- Definition eqb := Neqb.
- Definition eqb_eq := Neqb_eq.
-End N_as_UBE.
-
-Module N_as_DT <: UsualDecidableTypeFull := Make_UDTF N_as_UBE.
-
-(** Note that the last module fulfills by subtyping many other
-    interfaces, such as [DecidableType] or [EqualityType]. *)
-
-
-
-(** * OrderedType structure for [N] numbers *)
-
-Module N_as_OT <: OrderedTypeFull.
- Include N_as_DT.
- Definition lt := Nlt.
- Definition le := Nle.
- Definition compare := Ncompare.
-
- Instance lt_strorder : StrictOrder Nlt.
- Proof. split; [ exact Nlt_irrefl | exact Nlt_trans ]. Qed.
-
- Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Nlt.
- Proof. repeat red; intros; subst; auto. Qed.
-
- Definition le_lteq := Nle_lteq.
- Definition compare_spec := Ncompare_spec.
-
-End N_as_OT.
-
-(** Note that [N_as_OT] can also be seen as a [UsualOrderedType]
-   and a [OrderedType] (and also as a [DecidableType]). *)
-
-
-
-(** * An [order] tactic for [N] numbers *)
-
-Module NOrder := OTF_to_OrderTac N_as_OT.
-Ltac n_order := NOrder.order.
-
-(** Note that [n_order] is domain-agnostic: it will not prove
-    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
-
diff --git a/theories/NArith/Nminmax.v b/theories/NArith/Nminmax.v
index 475b4dfb82..53c7ecae72 100644
--- a/theories/NArith/Nminmax.v
+++ b/theories/NArith/Nminmax.v
@@ -6,55 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Orders BinNat Nnat NOrderedType GenericMinMax.
+Require Import Orders BinNat Nnat NBinary.
 
 (** * Maximum and Minimum of two [N] numbers *)
 
 Local Open Scope N_scope.
 
-(** The functions [Nmax] and [Nmin] implement indeed
-    a maximum and a minimum *)
+(** Generic properties of min and max are already in [NBinary.N].
+    We add here the ones specific to N. *)
 
-Lemma Nmax_l : forall x y, y<=x -> Nmax x y = x.
-Proof.
- unfold Nle, Nmax. intros x y.
- generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Nmax_r : forall x y, x<=y -> Nmax x y = y.
-Proof.
- unfold Nle, Nmax. intros x y. destruct (x ?= y); intuition.
-Qed.
-
-Lemma Nmin_l : forall x y, x<=y -> Nmin x y = x.
-Proof.
- unfold Nle, Nmin. intros x y. destruct (x ?= y); intuition.
-Qed.
-
-Lemma Nmin_r : forall x y, y<=x -> Nmin x y = y.
-Proof.
- unfold Nle, Nmin. intros x y.
- generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Module NHasMinMax <: HasMinMax N_as_OT.
- Definition max := Nmax.
- Definition min := Nmin.
- Definition max_l := Nmax_l.
- Definition max_r := Nmax_r.
- Definition min_l := Nmin_l.
- Definition min_r := Nmin_r.
-End NHasMinMax.
-
-Module N.
-
-(** We obtain hence all the generic properties of max and min. *)
-
-Include UsualMinMaxProperties N_as_OT NHasMinMax.
-
-(** * Properties specific to the [positive] domain *)
+Module Type Nextend (N:NBinary.N).
 
 (** Simplifications *)
 
@@ -81,7 +42,7 @@ Proof. intros. rewrite N.min_comm. apply min_0_l. Qed.
 Lemma succ_max_distr :
  forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m).
 Proof.
- intros. symmetry. apply max_monotone.
+ intros. symmetry. apply N.max_monotone.
  intros x x'. unfold Nle.
  rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc.
  simpl; auto.
@@ -89,38 +50,38 @@ Qed.
 
 Lemma succ_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m).
 Proof.
- intros. symmetry. apply min_monotone.
+ intros. symmetry. apply N.min_monotone.
  intros x x'. unfold Nle.
  rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc.
  simpl; auto.
 Qed.
 
-Lemma plus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m.
+Lemma add_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m.
 Proof.
- intros. apply max_monotone.
+ intros. apply N.max_monotone.
  intros x x'. unfold Nle.
  rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus.
  rewrite <- 2 Compare_dec.nat_compare_le. auto with arith.
 Qed.
 
-Lemma plus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p.
+Lemma add_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p.
 Proof.
- intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p).
- apply plus_max_distr_l.
+ intros. rewrite (N.add_comm n p), (N.add_comm m p), (N.add_comm _ p).
+ apply add_max_distr_l.
 Qed.
 
-Lemma plus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m.
+Lemma add_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m.
 Proof.
- intros. apply min_monotone.
+ intros. apply N.min_monotone.
  intros x x'. unfold Nle.
  rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus.
  rewrite <- 2 Compare_dec.nat_compare_le. auto with arith.
 Qed.
 
-Lemma plus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p.
+Lemma add_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p.
 Proof.
- intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p).
- apply plus_min_distr_l.
+ intros. rewrite (N.add_comm n p), (N.add_comm m p), (N.add_comm _ p).
+ apply add_min_distr_l.
 Qed.
 
-End N.
\ No newline at end of file
+End Nextend.
\ No newline at end of file
diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget
index 32f94f0139..17ac948b08 100644
--- a/theories/NArith/vo.itarget
+++ b/theories/NArith/vo.itarget
@@ -8,5 +8,4 @@ Nnat.vo
 Pnat.vo
 POrderedType.vo
 Pminmax.vo
-NOrderedType.vo
 Nminmax.vo
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 7211112f26..d29bb32eb2 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -18,7 +18,8 @@ Local Open Scope N_scope.
 
 (** * Implementation of [NAxiomsSig] module type via [BinNat.N] *)
 
-Module NBinaryAxiomsMod <: NAxiomsSig.
+Module Type N
+ <: NAxiomsSig <: UsualOrderedTypeFull <: TotalOrder <: DecidableTypeFull.
 
 (** Bi-directional induction. *)
 
@@ -65,6 +66,10 @@ apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1.
 right; now apply Pcompare_Eq_eq. now left. exfalso; now apply H.
 Qed.
 
+Definition eqb_eq := Neqb_eq.
+
+Definition compare_spec := Ncompare_spec.
+
 Theorem min_l : forall n m, n <= m -> Nmin n m = n.
 Proof.
 unfold Nmin, Nle; intros n m H.
@@ -138,6 +143,9 @@ Qed.
 
 Definition t := N.
 Definition eq := @eq N.
+Definition eqb := Neqb.
+Definition compare := Ncompare.
+Definition eq_dec := N_eq_dec.
 Definition zero := N0.
 Definition succ := Nsucc.
 Definition pred := Npred.
@@ -149,9 +157,10 @@ Definition le := Nle.
 Definition min := Nmin.
 Definition max := Nmax.
 
-End NBinaryAxiomsMod.
+Include NPropFunct
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
-Module Export NBinaryPropMod := NPropFunct NBinaryAxiomsMod.
+End N.
 
 (*
 Require Import NDefOps.
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index d7c0deb949..90840ce1f6 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -13,8 +13,8 @@
 
 (* $Id$ *)
 
-Require Import Orders NatOrderedType POrderedType NOrderedType
- ZBinary RelationPairs EqualitiesFacts.
+Require Import Orders NatOrderedType POrderedType NArith
+ ZArith RelationPairs EqualitiesFacts.
 
 (** * Examples of Ordered Type structures. *)
 
@@ -23,8 +23,8 @@ Require Import Orders NatOrderedType POrderedType NOrderedType
 
 Module Nat_as_OT := NatOrderedType.Nat_as_OT.
 Module Positive_as_OT := POrderedType.Positive_as_OT.
-Module N_as_OT := NOrderedType.N_as_OT.
-Module Z_as_OT := ZBinary.Z.
+Module N_as_OT := NArith.N.
+Module Z_as_OT := ZArith.Z.
 
 (** An OrderedType can now directly be seen as a DecidableType *)