OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith

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

5 files changed, 60 insertions, 31 deletions

diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index 55f3cbf64d..e6312a1470 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -160,24 +160,16 @@ Module N_as_OT <: UsualOrderedType.
   Definition eq_sym := @sym_eq t.
   Definition eq_trans := @trans_eq t.
 
-  Definition lt p q:= Nleb q p = false.
- 
-  Definition lt_trans := Nltb_trans.
-
-  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-  Proof.
-  intros; intro.
-  rewrite H0 in H.
-  unfold lt in H.
-  rewrite Nleb_refl in H; discriminate.
-  Qed.
+  Definition lt:=Nlt.
+  Definition lt_trans := Nlt_trans.
+  Definition lt_not_eq := Nlt_not_eq.
 
   Definition compare : forall x y : t, Compare lt eq x y.
   Proof.
   intros x y. destruct (x ?= y)%N as [ | | ]_eqn.
   apply EQ; apply Ncompare_Eq_eq; assumption.
-  apply LT; apply Ncompare_Lt_Nltb; assumption.
-  apply GT; apply Ncompare_Gt_Nltb; assumption.
+  apply LT; assumption.
+  apply GT. apply Ngt_Nlt; assumption.
   Defined.
 
   Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 84af2fe852..147d1e8d34 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -206,6 +206,21 @@ Definition CompOpp (r:comparison) :=
     | Gt => Lt
   end.
 
+Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c.
+Proof.
+  destruct c; reflexivity.
+Qed.
+
+Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'.
+Proof.
+  destruct c; destruct c'; auto; discriminate.
+Qed.
+
+Lemma CompOpp_iff : forall c c', CompOpp c = c' <-> c = CompOpp c'.
+Proof.
+  split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto.
+Qed.
+
 (** Identity *)
 
 Definition ID := forall A:Type, A -> A.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index d9d848f0db..eaf3f126ab 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -383,11 +383,30 @@ destruct n; destruct m; simpl; auto.
 exact (Pcompare_antisym p p0 Eq).
 Qed.
 
+Lemma Ngt_Nlt : forall n m, n > m -> m < n.
+Proof.
+unfold Ngt, Nlt; intros n m GT.
+rewrite <- Ncompare_antisym, GT; reflexivity.
+Qed.
+
 Theorem Nlt_irrefl : forall n : N, ~ n < n.
 Proof.
 intro n; unfold Nlt; now rewrite Ncompare_refl.
 Qed.
 
+Theorem Nlt_trans : forall n m q, n < m -> m < q -> n < q.
+Proof.
+destruct n;
+ destruct m; try discriminate;
+ destruct q; try discriminate; auto.
+eapply Plt_trans; eauto.
+Qed.
+
+Theorem Nlt_not_eq : forall n m, n < m -> ~ n = m.
+Proof.
+ intros n m LT EQ. subst m. elim (Nlt_irrefl n); auto.
+Qed.
+
 Theorem Ncompare_n_Sm :
   forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m.
 Proof.
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 8244d4ceb3..35a900afd5 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -64,29 +64,33 @@ Qed.
 
 Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.
 Proof.
-  intros x y; split; intro H;
-    [ change Lt with (CompOpp Gt) in |- *; rewrite <- Zcompare_antisym;
-      rewrite H; reflexivity
-      | change Gt with (CompOpp Lt) in |- *; rewrite <- Zcompare_antisym;
-	rewrite H; reflexivity ].
+  intros x y.
+  rewrite <- Zcompare_antisym. change Gt with (CompOpp Lt).
+  split.
+  auto using CompOpp_inj.
+  intros; f_equal; auto.
 Qed.
 
 (** * Transitivity of comparison *)
 
+Lemma Zcompare_Lt_trans :
+  forall n m p:Z, (n ?= m) = Lt -> (m ?= p) = Lt -> (n ?= p) = Lt.
+Proof.
+  intros x y z; case x; case y; case z; simpl;
+    try discriminate; auto with arith.
+  intros; eapply Plt_trans; eauto.
+  intros p q r; rewrite 3 Pcompare_antisym; simpl.
+  intros; eapply Plt_trans; eauto.
+Qed.
+
 Lemma Zcompare_Gt_trans :
   forall n m p:Z, (n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt.
 Proof.
-  intros x y z; case x; case y; case z; simpl in |- *;
-    try (intros; discriminate H || discriminate H0); auto with arith;
-      [ intros p q r H H0; apply nat_of_P_gt_Gt_compare_complement_morphism;
-	unfold gt in |- *; apply lt_trans with (m := nat_of_P q);
-	  apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; 
-	    assumption
-	| intros p q r; do 3 rewrite <- ZC4; intros H H0;
-	  apply nat_of_P_gt_Gt_compare_complement_morphism; 
-	    unfold gt in |- *; apply lt_trans with (m := nat_of_P q);
-	      apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; 
-		assumption ].
+  intros n m p Hnm Hmp.
+  apply <- Zcompare_Gt_Lt_antisym.
+  apply -> Zcompare_Gt_Lt_antisym in Hnm.
+  apply -> Zcompare_Gt_Lt_antisym in Hmp.
+  eapply Zcompare_Lt_trans; eauto.
 Qed.
 
 (** * Comparison and opposite *)
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 454560b858..9ab0aadfd9 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -276,8 +276,7 @@ Qed.
 
 Lemma Zlt_trans : forall n m p:Z, n < m -> m < p -> n < p.
 Proof.
-  intros n m p H1 H2; apply Zgt_lt; apply Zgt_trans with (m := m); apply Zlt_gt;
-    assumption.
+  exact Zcompare_Lt_trans.
 Qed.
 
 (** Mixed transitivity *)