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

6 files changed, 215 insertions, 215 deletions

diff --git a/CHANGES b/CHANGES
index 92fd6e11d..032c224d9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -43,6 +43,9 @@ Library
 
 - Use "Coq standard" names for the properties of eq and identity
   (e.g. refl_equal is now eq_refl). Support for compatibility is provided.
+- The function Compare_dec.nat_compare is now defined directly,
+  instead of relying on lt_eq_lt_dec. The earlier version is still
+  available under the name nat_compare_alt.
 
 Changes from V8.1 to V8.2
 =========================
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index ac44586c1..573f54e9f 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -113,80 +113,95 @@ Qed.
 
 (** A ternary comparison function in the spirit of [Zcompare]. *)
 
-Definition nat_compare (n m:nat) :=
-  match lt_eq_lt_dec n m with 
-    | inleft (left _) => Lt
-    | inleft (right _) => Eq
-    | inright _ => Gt
+Fixpoint nat_compare n m :=
+  match n, m with
+   | O, O => Eq
+   | O, S _ => Lt
+   | S _, O => Gt
+   | S n', S m' => nat_compare n' m'
   end.
 
 Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m.
 Proof.
-  unfold nat_compare; intros.
-  simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto.
+ reflexivity.
+Qed.
+
+Lemma nat_compare_eq_iff : forall n m, nat_compare n m = Eq <-> n = m.
+Proof.
+  induction n; destruct m; simpl; split; auto; try discriminate;
+   destruct (IHn m); auto.
 Qed.
 
 Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m.
 Proof.
-  induction n; destruct m; simpl; auto.
-  unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  rewrite nat_compare_S; auto.
+  intros; apply -> nat_compare_eq_iff; auto.
 Qed.
 
 Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt.
 Proof.
-  induction n; destruct m; simpl.
-  unfold nat_compare; simpl; intuition; [inversion H | discriminate H].
-  split; auto with arith.
-  split; [inversion 1 |].
-  unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  rewrite nat_compare_S.
-  generalize (IHn m); clear IHn; intuition.
+  induction n; destruct m; simpl; split; auto with arith;
+   try solve [inversion 1].
+  destruct (IHn m); auto with arith.
+  destruct (IHn m); auto with arith.
 Qed.
 
 Lemma nat_compare_gt : forall n m, n>m <-> nat_compare n m = Gt.
 Proof.
-  induction n; destruct m; simpl.
-  unfold nat_compare; simpl; intuition; [inversion H | discriminate H].
-  split; [inversion 1 |].
-  unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H]; 
-    auto; intros; try discriminate.
-  split; auto with arith.
-  rewrite nat_compare_S.
-  generalize (IHn m); clear IHn; intuition.
+  induction n; destruct m; simpl; split; auto with arith;
+   try solve [inversion 1].
+  destruct (IHn m); auto with arith.
+  destruct (IHn m); auto with arith.
 Qed.
 
 Lemma nat_compare_le : forall n m, n<=m <-> nat_compare n m <> Gt.
 Proof.
   split.
-  intros.
-  intro.
-  destruct (nat_compare_gt n m).
-  generalize (le_lt_trans _ _ _ H (H2 H0)).
-  exact (lt_irrefl n).
-  intros.
-  apply not_gt.
-  contradict H.
-  destruct (nat_compare_gt n m); auto.
-Qed.  
+  intros LE; contradict LE.
+   apply lt_not_le. apply <- nat_compare_gt; auto.
+  intros NGT. apply not_lt. contradict NGT.
+   apply -> nat_compare_gt; auto.
+Qed.
 
 Lemma nat_compare_ge : forall n m, n>=m <-> nat_compare n m <> Lt.
 Proof.
   split.
-  intros.
-  intro.
-  destruct (nat_compare_lt n m).
-  generalize (le_lt_trans _ _ _ H (H2 H0)).
-  exact (lt_irrefl m).
-  intros.
-  apply not_lt.
-  contradict H.
-  destruct (nat_compare_lt n m); auto.
-Qed.  
+  intros GE; contradict GE.
+   apply lt_not_le. apply <- nat_compare_lt; auto.
+  intros NLT. apply not_lt. contradict NLT.
+   apply -> nat_compare_lt; auto.
+Qed.
+
+(** Some projections of the above equivalences, used in OrderedTypeEx. *)
+
+Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m.
+Proof.
+  intros; apply <- nat_compare_lt; auto.
+Qed.
+
+Lemma nat_compare_Gt_gt : forall n m, nat_compare n m = Gt -> n>m.
+Proof.
+  intros; apply <- nat_compare_gt; auto.
+Qed.
+
+(** A previous definition of [nat_compare] in terms of [lt_eq_lt_dec].
+    The new version avoids the creation of proof parts. *)
+
+Definition nat_compare_alt (n m:nat) :=
+  match lt_eq_lt_dec n m with
+    | inleft (left _) => Lt
+    | inleft (right _) => Eq
+    | inright _ => Gt
+  end.
+
+Lemma nat_compare_equiv: forall n m,
+ nat_compare n m = nat_compare_alt n m.
+Proof.
+  intros; unfold nat_compare_alt; destruct lt_eq_lt_dec as [[LT|EQ]|GT].
+  apply -> nat_compare_lt; auto.
+  apply <- nat_compare_eq_iff; auto.
+  apply -> nat_compare_gt; auto.
+Qed.
+
 
 (** A boolean version of [le] over [nat]. *)
 
@@ -200,48 +215,48 @@ Fixpoint leb (m:nat) : nat -> bool :=
                    end
   end.
 
-Lemma leb_correct : forall m n:nat, m <= n -> leb m n = true.
+Lemma leb_correct : forall m n, m <= n -> leb m n = true.
 Proof.
   induction m as [| m IHm]. trivial.
   destruct n. intro H. elim (le_Sn_O _ H).
   intros. simpl in |- *. apply IHm. apply le_S_n. assumption.
 Qed.
 
-Lemma leb_complete : forall m n:nat, leb m n = true -> m <= n.
+Lemma leb_complete : forall m n, leb m n = true -> m <= n.
 Proof.
   induction m. trivial with arith.
   destruct n. intro H. discriminate H.
   auto with arith.
 Qed.
 
-Lemma leb_correct_conv : forall m n:nat, m < n -> leb n m = false.
+Lemma leb_iff : forall m n, leb m n = true <-> m <= n.
 Proof.
-  intros. 
+  split; auto using leb_correct, leb_complete.
+Qed.
+
+Lemma leb_correct_conv : forall m n, m < n -> leb n m = false.
+Proof.
+  intros.
   generalize (leb_complete n m).
   destruct (leb n m); auto.
-  intros.
-  elim (lt_irrefl _ (lt_le_trans _ _ _ H (H0 (refl_equal true)))).
+  intros; elim (lt_not_le m n); auto.
 Qed.
 
-Lemma leb_complete_conv : forall m n:nat, leb n m = false -> m < n.
+Lemma leb_complete_conv : forall m n, leb n m = false -> m < n.
 Proof.
-  intros. elim (le_or_lt n m). intro. conditional trivial rewrite leb_correct in H. discriminate H.
-  trivial.
+  intros m n EQ. apply not_le.
+  intro LE. apply leb_correct in LE. rewrite LE in EQ; discriminate.
+Qed.
+
+Lemma leb_iff_conv : forall m n, leb n m = false <-> m < n.
+Proof.
+  split; auto using leb_complete_conv, leb_correct_conv.
 Qed.
 
 Lemma leb_compare : forall n m, leb n m = true <-> nat_compare n m <> Gt.
 Proof.
- induction n; destruct m; simpl.
- unfold nat_compare; simpl.
- intuition; discriminate.
- split; auto with arith.
- unfold nat_compare; destruct (lt_eq_lt_dec 0 (S m)) as [[H|H]|H]; 
-  intuition; try discriminate.
- inversion H.
- split; try (intros; discriminate).
- unfold nat_compare; destruct (lt_eq_lt_dec (S n) 0) as [[H|H]|H]; 
-  intuition; try discriminate.
- inversion H.
- rewrite nat_compare_S; auto.
-Qed. 
+ split; intros.
+ apply -> nat_compare_le. auto using leb_complete.
+ apply leb_correct. apply <- nat_compare_le; auto.
+Qed.
 
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index 8f82fe93d..55f3cbf64 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -55,18 +55,17 @@ Module Nat_as_OT <: UsualOrderedType.
   Definition lt := lt.
 
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
-  Proof. unfold lt in |- *; intros; apply lt_trans with y; auto. Qed.
+  Proof. unfold lt; intros; apply lt_trans with y; auto. Qed.
 
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-  Proof. unfold lt, eq in |- *; intros; omega. Qed.
+  Proof. unfold lt, eq; intros; omega. Qed.
 
   Definition compare : forall x y : t, Compare lt eq x y.
   Proof.
-    intros; case (lt_eq_lt_dec x y).
-    simple destruct 1; intro.
-    constructor 1; auto.
-    constructor 2; auto.
-    intro; constructor 3; auto.
+    intros x y; destruct (nat_compare x y) as [ | | ]_eqn.
+    apply EQ. apply nat_compare_eq; assumption.
+    apply LT. apply nat_compare_Lt_lt; assumption.
+    apply GT. apply nat_compare_Gt_gt; assumption.
   Defined.
 
   Definition eq_dec := eq_nat_dec.
@@ -96,10 +95,10 @@ Module Z_as_OT <: UsualOrderedType.
 
   Definition compare : forall x y, Compare lt eq x y.
   Proof.
-    intros x y; case_eq (x ?= y); intros.
-    apply EQ; unfold eq; apply Zcompare_Eq_eq; auto.
-    apply LT; unfold lt, Zlt; auto.
-    apply GT; unfold lt, Zlt; rewrite <- Zcompare_Gt_Lt_antisym; auto.
+    intros x y; destruct (x ?= y) as [ | | ]_eqn.
+    apply EQ; apply Zcompare_Eq_eq; assumption.
+    apply LT; assumption.
+    apply GT; apply Zgt_lt; assumption.
   Defined.
 
   Definition eq_dec := Z_eq_dec.
@@ -136,13 +135,10 @@ Module Positive_as_OT <: UsualOrderedType.
 
   Definition compare : forall x y : t, Compare lt eq x y.
   Proof.
-  intros x y.
-  case_eq ((x ?= y) Eq); intros.
-  apply EQ; apply Pcompare_Eq_eq; auto.
-  apply LT; unfold lt; auto.
-  apply GT; unfold lt.
-  replace Eq with (CompOpp Eq); auto.
-  rewrite <- Pcompare_antisym; rewrite H; auto.
+  intros x y. destruct ((x ?= y) Eq) as [ | | ]_eqn.
+  apply EQ; apply Pcompare_Eq_eq; assumption.
+  apply LT; assumption.
+  apply GT; apply ZC1; assumption.
   Defined.
 
   Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
@@ -178,19 +174,10 @@ Module N_as_OT <: UsualOrderedType.
 
   Definition compare : forall x y : t, Compare lt eq x y.
   Proof.
-  intros x y.
-  case_eq ((x ?= y)%N); intros.
-  apply EQ; apply Ncompare_Eq_eq; auto.
-  apply LT; unfold lt; auto.
-   generalize (Nleb_Nle y x).
-   unfold Nle; rewrite <- Ncompare_antisym.
-   destruct (x ?= y)%N; simpl; try discriminate.
-   clear H; intros H.
-   destruct (Nleb y x); intuition.
-  apply GT; unfold lt.
-   generalize (Nleb_Nle x y).
-   unfold Nle; destruct (x ?= y)%N; simpl; try discriminate.
-   destruct (Nleb x y); intuition.
+  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.
   Defined.
 
   Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
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;