From 6a13615a1efa7e2e10ea8e7187d2bda0819fd1d5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 7 Jun 2009 17:10:17 +0000 Subject: - 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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/ZArith_dec.v | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) (limited to 'theories/ZArith/ZArith_dec.v') 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 *) -- cgit v1.2.3