Better visibility of the inductive CompSpec used to specify comparison functions

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

4 files changed, 38 insertions, 30 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 813956332..8d589f053 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -427,6 +427,21 @@ pose proof (Pcompare_p_Sq p q) as (_,?);
 assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
 Qed.
 
+Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y.
+Proof.
+unfold Nle, Nlt; intros.
+generalize (Ncompare_eq_correct x y).
+destruct (x ?= y); intuition; discriminate.
+Qed.
+
+Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y).
+Proof.
+intros.
+destruct (Ncompare x y) as [ ]_eqn; constructor; auto.
+apply Ncompare_Eq_eq; auto.
+apply Ngt_Nlt; auto.
+Qed.
+
 (** 0 is the least natural number *)
 
 Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 20cfb43a3..7e3523a8c 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -857,6 +857,15 @@ Proof.
   symmetry; apply Pcompare_antisym.
 Qed.
 
+Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq).
+Proof.
+  intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor.
+  apply Pcompare_Eq_eq; auto.
+  auto.
+  apply ZC1; auto.
+Qed.
+
+
 (** Comparison and the successor *)
 
 Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
@@ -932,6 +941,14 @@ Proof.
   destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto.
 Qed.
 
+Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q.
+Proof.
+  unfold Ple, Plt. intros.
+  generalize (Pcompare_eq_iff p q).
+  destruct ((p ?= q) Eq); intuition; discriminate.
+Qed.
+
+
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
index 8f69cd656..bd701cbea 100644
--- a/theories/NArith/NOrderedType.v
+++ b/theories/NArith/NOrderedType.v
@@ -39,23 +39,12 @@ Module N_as_OT <: OrderedTypeFull.
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Nlt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof.
- unfold Nle, Nlt; intros. rewrite <- Ncompare_eq_correct.
- destruct (x ?= y); intuition; discriminate.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (Ncompare x y).
- Proof.
- intros.
- destruct (Ncompare x y) as [ ]_eqn; constructor; auto.
- apply Ncompare_Eq_eq; auto.
- apply Ngt_Nlt; 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]
+(** Note that [N_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)
 
 
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
index 2f89b0e68..a4eeb9b97 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/NArith/POrderedType.v
@@ -39,25 +39,12 @@ Module Positive_as_OT <: OrderedTypeFull.
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Plt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof.
- unfold Ple, Plt. intros.
- rewrite <- Pcompare_eq_iff.
- destruct (Pcompare x y Eq); intuition; discriminate.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
- Proof.
- intros; unfold compare.
- destruct (Pcompare x y Eq) as [ ]_eqn; constructor.
- apply Pcompare_Eq_eq; auto.
- auto.
- apply ZC1; auto.
- Qed.
+ Definition le_lteq := Ple_lteq.
+ Definition compare_spec := Pcompare_spec.
 
 End Positive_as_OT.
 
-(* Note that [Positive_as_OT] can also be seen as a [UsualOrderedType]
+(** Note that [Positive_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)