aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/ZArith_dec.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-06-07 17:10:17 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-06-07 17:10:17 +0000
commit6a13615a1efa7e2e10ea8e7187d2bda0819fd1d5 (patch)
treebb5a5d217f7eb0d2774c9159537176fa7ec5c03a /theories/ZArith/ZArith_dec.v
parent0329bbb517f0cb0f3707b209ef849d389cf870dc (diff)
- 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
Diffstat (limited to 'theories/ZArith/ZArith_dec.v')
-rw-r--r--theories/ZArith/ZArith_dec.v37
1 files changed, 22 insertions, 15 deletions
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index d1f93d498..f024339d8 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 *)