Better comparison functions in OrderedTypeEx

The compare functions are still functions-by-tactics, but now their
computational parts are completely pure (no use of lt_eq_lt_dec in
nat_compare anymore), while their proofs parts are simply calls
to (opaque) lemmas. This seem to improve the efficiency of sets/maps,
as mentionned by T. Braibant, D. Pous and S. Lescuyer.

The earlier version of nat_compare is now called nat_compare_alt,
there is a proof of equivalence named nat_compare_equiv.

By the way, various improvements of proofs, in particular in Pnat.

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

1 files changed, 10 insertions, 20 deletions

diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 98b482bc9..36a1f1d8f 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -179,22 +179,12 @@ Lemma nat_of_Ncompare :
  forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a').
 Proof.
   destruct a; destruct a'; simpl.
-  compute; auto.
-  generalize (lt_O_nat_of_P p).
-  unfold nat_compare.
-  destruct (lt_eq_lt_dec 0 (nat_of_P p)) as [[H|H]|H]; auto.
-  rewrite <- H; inversion 1.
-  intros; generalize (lt_trans _ _ _ H0 H); inversion 1.
-  generalize (lt_O_nat_of_P p).
-  unfold nat_compare.
-  destruct (lt_eq_lt_dec (nat_of_P p) 0) as [[H|H]|H]; auto.
-  intros; generalize (lt_trans _ _ _ H0 H); inversion 1.
-  rewrite H; inversion 1.
-  unfold nat_compare.
-  destruct (lt_eq_lt_dec (nat_of_P p) (nat_of_P p0)) as [[H|H]|H]; auto.
-  apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
-  rewrite (nat_of_P_inj _ _ H); apply Pcompare_refl.
-  apply nat_of_P_gt_Gt_compare_complement_morphism; auto.
+  reflexivity.
+  assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P.
+  destruct nat_of_P; [inversion NZ|auto].
+  assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P.
+  destruct nat_of_P; [inversion NZ|auto].
+  apply nat_of_P_compare_morphism.
 Qed.
 
 Lemma N_of_nat_compare : 
@@ -210,8 +200,8 @@ Lemma nat_of_Nmin :
   forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').
 Proof.
   intros; unfold Nmin; rewrite nat_of_Ncompare.
-  unfold nat_compare.
-  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; 
+  rewrite nat_compare_equiv; unfold nat_compare_alt.
+  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|];
     simpl; intros; symmetry; auto with arith.
   apply min_l; rewrite e; auto with arith.
 Qed.
@@ -230,8 +220,8 @@ Lemma nat_of_Nmax :
   forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a').
 Proof.
   intros; unfold Nmax; rewrite nat_of_Ncompare.
-  unfold nat_compare.
-  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; 
+  rewrite nat_compare_equiv; unfold nat_compare_alt.
+  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|];
     simpl; intros; symmetry; auto with arith.
   apply max_r; rewrite e; auto with arith.
 Qed.