- Added two new introduction patterns with the following temptative syntaxes:

  - "*" implements Arthur Charguéraud's "introv"
  - "**" works as "; intros" (see also "*" in ssreflect).
- Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui.
- Shy attempt to seize the opportunity to clean Zarith_dec but Coq's
  library is really going anarchically (see a summary of the various
  formulations of total order, dichotomy of order and decidability of
  equality and in stdlib-project.tex in branch V8revised-theories).



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

2 files changed, 32 insertions, 18 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 076bceba48..af281b73f1 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -266,12 +266,19 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
  end.
 
 (**********************************************************************)
-(** Miscellaneous properties of binary positive numbers *)
+(** Decidability of equality on binary positive numbers *)
 
-Lemma ZL11 : forall p:positive, p = 1 \/ p <> 1.
+Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}.
 Proof.
-  intros x; case x; intros; (left; reflexivity) || (right; discriminate).
+  decide equality.
+Defined.
+
+(* begin hide *)
+Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1.
+Proof.
+  intro; edestruct positive_eq_dec; eauto.
 Qed.
+(* end hide *)
 
 (**********************************************************************)
 (** Properties of successor on binary positive numbers *)
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index d1f93d498f..f024339d84 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -15,18 +15,27 @@ Require Import Zorder.
 Require Import Zcompare.
 Open Local Scope Z_scope.
 
+(* begin hide *)
+(* Trivial, to deprecate? *)
 Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}.
 Proof.
-  simple induction r; auto with arith. 
+  induction r; auto.
+Defined.
+(* end hide *)
+
+Lemma Zcompare_rect :
+  forall (P:Type) (n m:Z),
+    ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
+Proof.
+  intros * H1 H2 H3.
+  destruct (n ?= m); auto. 
 Defined.
 
 Lemma Zcompare_rec :
   forall (P:Set) (n m:Z),
     ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
 Proof.
-  intros P x y H1 H2 H3.
-  elim (Dcompare_inf (x ?= y)).
-  intro H. elim H; auto with arith. auto with arith.
+  intro; apply Zcompare_rect.
 Defined.
 
 Section decidability.
@@ -37,12 +46,7 @@ Section decidability.
 
   Definition Z_eq_dec : {x = y} + {x <> y}.
   Proof.
-    apply Zcompare_rec with (n := x) (m := y).
-    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
-    intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
-    rewrite (H2 H4) in H3. discriminate H3.
-    intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
-    rewrite (H2 H4) in H3. discriminate H3.
+    decide equality; apply positive_eq_dec.
   Defined. 
 
   (** * Decidability of order on binary integers *)
@@ -214,13 +218,16 @@ Proof.
     [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
 Defined.
 
-
-
-Definition Z_zerop : forall x:Z, {x = 0} + {x <> 0}.
+(* begin hide *)
+(* To deprecate ? *)
+Corollary Z_zerop : forall x:Z, {x = 0} + {x <> 0}.
 Proof.
   exact (fun x:Z => Z_eq_dec x 0).
 Defined.
 
-Definition Z_notzerop (x:Z) := sumbool_not _ _ (Z_zerop x).
+Corollary Z_notzerop : forall (x:Z), {x <> 0} + {x = 0}.
+Proof (fun x => sumbool_not _ _ (Z_zerop x)).
 
-Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).
+Corollary Z_noteq_dec : forall (x y:Z), {x <> y} + {x = y}.
+Proof (fun x y => sumbool_not _ _ (Z_eq_dec x y)).
+(* end hide *)