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

3 files changed, 108 insertions, 113 deletions

diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index bbab81f4e..e9bc4b266 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -354,6 +354,35 @@ Proof.
   trivial.
 Qed.
 
+(* Nleb and Ncompare *)
+
+(* NB: No need to prove that Nleb a b = true <-> Ncompare a b <> Gt,
+   this statement is in fact Nleb_Nle! *)
+
+Lemma Nltb_Ncompare : forall a b,
+ Nleb a b = false <-> Ncompare a b = Gt.
+Proof.
+ intros.
+ assert (IFF : forall x:bool, x = false <-> ~ x = true)
+   by (destruct x; intuition).
+ rewrite IFF, Nleb_Nle; unfold Nle.
+ destruct (Ncompare a b); split; intro H; auto;
+  elim H; discriminate.
+Qed.
+
+Lemma Ncompare_Gt_Nltb : forall a b,
+ Ncompare a b = Gt -> Nleb a b = false.
+Proof.
+ intros; apply <- Nltb_Ncompare; auto.
+Qed.
+
+Lemma Ncompare_Lt_Nltb : forall a b,
+ Ncompare a b = Lt -> Nleb b a = false.
+Proof.
+ intros a b H.
+ rewrite Nltb_Ncompare, <- Ncompare_antisym, H; auto.
+Qed.
+
 (* An alternate [min] function over [N] *)
 
 Definition Nmin' (a b:N) := if Nleb a b then a else b.
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.
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v
index 9bec3e994..bf42c5e99 100644
--- a/theories/NArith/Pnat.v
+++ b/theories/NArith/Pnat.v
@@ -22,6 +22,10 @@ Require Import Gt.
 Require Import Plus.
 Require Import Mult.
 Require Import Minus.
+Require Import Compare_dec.
+
+Local Open Scope positive_scope.
+Local Open Scope nat_scope.
 
 (** [nat_of_P] is a morphism for addition *)
 
@@ -161,7 +165,7 @@ Qed.
 *)
 
 Lemma nat_of_P_lt_Lt_compare_morphism :
- forall p q:positive, (p ?= q)%positive Eq = Lt -> nat_of_P p < nat_of_P q.
+ forall p q:positive, (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q.
 Proof.
 intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ];
  intro H2;
@@ -193,29 +197,35 @@ Qed.
 *)
 
 Lemma nat_of_P_gt_Gt_compare_morphism :
- forall p q:positive, (p ?= q)%positive Eq = Gt -> nat_of_P p > nat_of_P q.
+ forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q.
 Proof.
-unfold gt in |- *; intro x; induction x as [p H| p H| ]; intro y;
- destruct y as [q| q| ]; intro H2;
- [ simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    apply lt_n_S; apply ZL7; apply H; assumption
- | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    elim (Pcompare_Gt_Gt p q H2);
-    [ intros H3; apply lt_S; apply ZL7; apply H; assumption
-    | intros E; rewrite E; apply lt_n_Sn ]
- | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p);
-    intros h H3; rewrite H3; simpl in |- *; apply lt_n_S; 
-    apply lt_O_Sn
- | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    apply ZL8; apply H; apply Pcompare_Lt_Gt; assumption
- | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    apply ZL7; apply H; assumption
- | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p);
-    intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;
-    apply lt_n_S; apply lt_O_Sn
- | simpl in |- *; discriminate H2
- | simpl in |- *; discriminate H2
- | simpl in |- *; discriminate H2 ].
+intros p q GT. unfold gt.
+apply nat_of_P_lt_Lt_compare_morphism.
+change ((q ?= p) (CompOpp Eq) = CompOpp Gt).
+rewrite <- Pcompare_antisym, GT; auto.
+Qed.
+
+(** [nat_of_P] is a morphism for [Pcompare] and [nat_compare] *)
+
+Lemma nat_of_P_compare_morphism : forall p q,
+ (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q).
+Proof.
+ intros p q; symmetry.
+ destruct ((p ?= q) Eq) as [ | | ]_eqn.
+ rewrite (Pcompare_Eq_eq p q); auto.
+ apply <- nat_compare_eq_iff; auto.
+ apply -> nat_compare_lt. apply nat_of_P_lt_Lt_compare_morphism; auto.
+ apply -> nat_compare_gt. apply nat_of_P_gt_Gt_compare_morphism; auto.
+Qed.
+
+(** [nat_of_P] is hence injective. *)
+
+Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q.
+Proof.
+intros.
+apply Pcompare_Eq_eq.
+rewrite nat_of_P_compare_morphism.
+apply <- nat_compare_eq_iff; auto.
 Qed.
 
 (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
@@ -225,17 +235,10 @@ Qed.
 *)
 
 Lemma nat_of_P_lt_Lt_compare_complement_morphism :
- forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q)%positive Eq = Lt.
+ forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt.
 Proof.
-intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq));
- [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H;
-    absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ]
- | intros H; elim H;
-    [ auto
-    | intros H1 H2; absurd (nat_of_P x < nat_of_P y);
-       [ apply lt_asym; change (nat_of_P x > nat_of_P y) in |- *;
-          apply nat_of_P_gt_Gt_compare_morphism; assumption
-       | assumption ] ] ].
+ intros. rewrite nat_of_P_compare_morphism.
+ apply -> nat_compare_lt; auto.
 Qed.
 
 (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
@@ -245,18 +248,13 @@ Qed.
 *)
 
 Lemma nat_of_P_gt_Gt_compare_complement_morphism :
- forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q)%positive Eq = Gt.
+ forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt.
 Proof.
-intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq));
- [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H;
-    absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ]
- | intros H; elim H;
-    [ intros H1 H2; absurd (nat_of_P y < nat_of_P x);
-       [ apply lt_asym; apply nat_of_P_lt_Lt_compare_morphism; assumption
-       | assumption ]
-    | auto ] ].
+ intros. rewrite nat_of_P_compare_morphism.
+ apply -> nat_compare_gt; auto.
 Qed.
 
+
 (** [nat_of_P] is strictly positive *)
 
 Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n.
@@ -301,21 +299,18 @@ Qed.
 
 Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p.
 Proof.
-  simple induction p. unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute.
-  rewrite Pmult_nat_4_mult_2_permute. rewrite H. simpl in |- *. rewrite <- plus_Snm_nSm. reflexivity.
-  unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute.
-  rewrite H. reflexivity.
-  reflexivity.
+  intros.
+  change 2 with (nat_of_P 2).
+  rewrite <- nat_of_P_mult_morphism.
+  f_equal.
 Qed.
 
 Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p).
 Proof.
-  simple induction p. unfold nat_of_P in |- *. simpl in |- *. intro p0. intro. rewrite Pmult_nat_2_mult_2_permute.
-  rewrite Pmult_nat_4_mult_2_permute; injection H; intro H1; rewrite H1;
-   rewrite <- plus_Snm_nSm; reflexivity.
-  unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute.
-  injection H; intro H1; rewrite H1; reflexivity.
-  reflexivity.
+  intros.
+  change 2 with (nat_of_P 2).
+  rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism.
+  f_equal.
 Qed.
 
 (**********************************************************************)
@@ -327,9 +322,9 @@ Qed.
 Theorem nat_of_P_o_P_of_succ_nat_eq_succ :
  forall n:nat, nat_of_P (P_of_succ_nat n) = S n.
 Proof.
-intro m; induction m as [| n H];
- [ reflexivity
- | simpl in |- *; rewrite nat_of_P_succ_morphism; rewrite H; auto ].
+induction n as [|n H].
+reflexivity.
+simpl; rewrite nat_of_P_succ_morphism, H; auto.
 Qed.
 
 (** Miscellaneous lemmas on [P_of_succ_nat] *)
@@ -337,17 +332,17 @@ Qed.
 Lemma ZL3 :
  forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n).
 Proof.
-intro x; induction x as [| n H];
- [ simpl in |- *; auto with arith
- | simpl in |- *; rewrite plus_comm; simpl in |- *; rewrite H;
+induction n as [| n H]; simpl;
+ [ auto with arith
+ | rewrite plus_comm; simpl; rewrite H;
     rewrite xO_succ_permute; auto with arith ].
 Qed.
 
 Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n).
 Proof.
-intro x; induction x as [| n H]; simpl in |- *;
+induction n as [| n H]; simpl;
  [ auto with arith
- | rewrite <- plus_n_Sm; simpl in |- *; simpl in H; rewrite H;
+ | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H;
     auto with arith ].
 Qed.
 
@@ -356,19 +351,9 @@ Qed.
 Theorem P_of_succ_nat_o_nat_of_P_eq_succ :
  forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p.
 Proof.
-intro x; induction x as [p H| p H| ];
- [ simpl in |- *; rewrite <- H; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism; elim (ZL4 p); 
-    unfold nat_of_P in |- *; intros n H1; rewrite H1; 
-    rewrite ZL3; auto with arith
- | unfold nat_of_P in |- *; simpl in |- *; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism;
-    rewrite <- (Ppred_succ (P_of_succ_nat (Pmult_nat p 1 + Pmult_nat p 1)));
-    rewrite <- (Ppred_succ (xI p)); simpl in |- *; 
-    rewrite <- H; elim (ZL4 p); unfold nat_of_P in |- *; 
-    intros n H1; rewrite H1; rewrite ZL5; simpl in |- *; 
-    trivial with arith
- | unfold nat_of_P in |- *; simpl in |- *; auto with arith ].
+intros.
+apply nat_of_P_inj.
+rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto.
 Qed.
 
 (** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity
@@ -377,8 +362,7 @@ Qed.
 Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id :
  forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p.
 Proof.
-intros x; rewrite P_of_succ_nat_o_nat_of_P_eq_succ; rewrite Ppred_succ;
- trivial with arith.
+intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto.
 Qed.
 
 (**********************************************************************)
@@ -389,21 +373,13 @@ Qed.
 
 Theorem nat_of_P_minus_morphism :
  forall p q:positive,
-   (p ?= q)%positive Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.
+   (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.
 Proof.
 intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r;
  [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith
  | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ].
 Qed.
 
-(** [nat_of_P] is injective *)
-
-Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q.
-Proof.
-intros x y H; rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id x);
- rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id y); 
- rewrite H; trivial with arith.
-Qed.
 
 Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p.
 Proof.
@@ -423,9 +399,9 @@ Qed.
 
 Lemma Pcompare_minus_r :
  forall p q r:positive,
-   (q ?= p)%positive Eq = Lt ->
-   (r ?= p)%positive Eq = Gt ->
-   (r ?= q)%positive Eq = Gt -> (r - p ?= r - q)%positive Eq = Lt.
+   (q ?= p) Eq = Lt ->
+   (r ?= p) Eq = Gt ->
+   (r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt.
 Proof.
 intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
  rewrite nat_of_P_minus_morphism;
@@ -446,9 +422,9 @@ Qed.
 
 Lemma Pcompare_minus_l :
  forall p q r:positive,
-   (q ?= p)%positive Eq = Lt ->
-   (p ?= r)%positive Eq = Gt ->
-   (q ?= r)%positive Eq = Gt -> (q - r ?= p - r)%positive Eq = Lt.
+   (q ?= p) Eq = Lt ->
+   (p ?= r) Eq = Gt ->
+   (q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt.
 Proof.
 intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
  rewrite nat_of_P_minus_morphism;
@@ -469,8 +445,8 @@ Qed.
 
 Theorem Pmult_minus_distr_l :
  forall p q r:positive,
-   (q ?= r)%positive Eq = Gt ->
-   (p * (q - r))%positive = (p * q - p * r)%positive.
+   (q ?= r) Eq = Gt ->
+   (p * (q - r) = p * q - p * r)%positive.
 Proof.
 intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism;
  rewrite nat_of_P_minus_morphism;