diff options
Diffstat (limited to 'theories/ZArith/ZArith_dec.v')
| -rw-r--r-- | theories/ZArith/ZArith_dec.v | 102 |
1 files changed, 35 insertions, 67 deletions
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index b6766640..ff4f5e7b 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -1,19 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ZArith_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Sumbool. Require Import BinInt. Require Import Zorder. Require Import Zcompare. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (* begin hide *) (* Trivial, to deprecate? *) @@ -23,68 +21,43 @@ Proof. 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. +Lemma Zcompare_rect (P:Type) (n m:Z) : + ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. Proof. - intros * H1 H2 H3. + 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. - intro; apply Zcompare_rect. -Defined. +Lemma Zcompare_rec (P:Set) (n m:Z) : + ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. +Proof. apply Zcompare_rect. Defined. + +Notation Z_eq_dec := Z.eq_dec (compat "8.3"). Section decidability. Variables x y : Z. - (** * Decidability of equality on binary integers *) - - Definition Z_eq_dec : {x = y} + {x <> y}. - Proof. - decide equality; apply positive_eq_dec. - Defined. - (** * Decidability of order on binary integers *) Definition Z_lt_dec : {x < y} + {~ x < y}. Proof. - unfold Zlt in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - right. rewrite H. discriminate. - left; assumption. - right. rewrite H. discriminate. + unfold Z.lt; case Z.compare; (now left) || (now right). Defined. Definition Z_le_dec : {x <= y} + {~ x <= y}. Proof. - unfold Zle in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - left. rewrite H. discriminate. - left. rewrite H. discriminate. - right. tauto. + unfold Z.le; case Z.compare; (now left) || (right; tauto). Defined. Definition Z_gt_dec : {x > y} + {~ x > y}. Proof. - unfold Zgt in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - right. rewrite H. discriminate. - right. rewrite H. discriminate. - left; assumption. + unfold Z.gt; case Z.compare; (now left) || (now right). Defined. Definition Z_ge_dec : {x >= y} + {~ x >= y}. Proof. - unfold Zge in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - left. rewrite H. discriminate. - right. tauto. - left. rewrite H. discriminate. + unfold Z.ge; case Z.compare; (now left) || (right; tauto). Defined. Definition Z_lt_ge_dec : {x < y} + {x >= y}. @@ -94,16 +67,15 @@ Section decidability. Lemma Z_lt_le_dec : {x < y} + {y <= x}. Proof. - intros. elim Z_lt_ge_dec. - intros; left; assumption. - intros; right; apply Zge_le; assumption. + * now left. + * right; now apply Z.ge_le. Defined. Definition Z_le_gt_dec : {x <= y} + {x > y}. Proof. elim Z_le_dec; auto with arith. - intro. right. apply Znot_le_gt; auto with arith. + intro. right. Z.swap_greater. now apply Z.nle_gt. Defined. Definition Z_gt_le_dec : {x > y} + {x <= y}. @@ -114,15 +86,15 @@ Section decidability. Definition Z_ge_lt_dec : {x >= y} + {x < y}. Proof. elim Z_ge_dec; auto with arith. - intro. right. apply Znot_ge_lt; auto with arith. + intro. right. Z.swap_greater. now apply Z.lt_nge. Defined. Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}. Proof. intro H. apply Zcompare_rec with (n := x) (m := y). - intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith. - intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith. + intro. right. elim (Z.compare_eq_iff x y); auto with arith. + intro. left. elim (Z.compare_eq_iff x y); auto with arith. intro H1. absurd (x > y); auto with arith. Defined. @@ -139,8 +111,8 @@ Proof. assumption. intro. right. - apply Zle_lt_trans with (m := x). - apply Zge_le. + apply Z.le_lt_trans with (m := x). + apply Z.ge_le. assumption. assumption. Defined. @@ -149,20 +121,16 @@ Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}. Proof. intros x y H. case (Zlt_cotrans 0 (x + y) H x). - intro. - left. - assumption. - intro. - right. - apply Zplus_lt_reg_l with (p := x). - rewrite Zplus_0_r. - assumption. + - now left. + - right. + apply Z.add_lt_mono_l with (p := x). + now rewrite Z.add_0_r. Defined. Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}. Proof. intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy; - [ right; apply Zplus_lt_reg_l with (p := x); rewrite Zplus_0_r | left ]; + [ right; apply Z.add_lt_mono_l with (p := x); rewrite Z.add_0_r | left ]; assumption. Defined. @@ -174,7 +142,7 @@ Proof. left. assumption. intro H0. - generalize (Zge_le _ _ H0). + generalize (Z.ge_le _ _ H0). intro. case (Z_le_lt_eq_dec _ _ H1). intro. @@ -183,7 +151,7 @@ Proof. intro. apply False_rec. apply H. - symmetry in |- *. + symmetry . assumption. Defined. @@ -196,17 +164,17 @@ Proof. left. assumption. intro H. - generalize (Zge_le _ _ H). + generalize (Z.ge_le _ _ H). intro H0. case (Z_le_lt_eq_dec y x H0). intro H1. left. right. - apply Zlt_gt. + apply Z.lt_gt. assumption. intro. right. - symmetry in |- *. + symmetry . assumption. Defined. @@ -214,7 +182,7 @@ Defined. Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}. Proof. intros x y. - case (Z_eq_dec x y); intro H; + case (Z.eq_dec x y); intro H; [ right; assumption | left; apply (not_Zeq_inf _ _ H) ]. Defined. @@ -222,12 +190,12 @@ Defined. (* To deprecate ? *) Corollary Z_zerop : forall x:Z, {x = 0} + {x <> 0}. Proof. - exact (fun x:Z => Z_eq_dec x 0). + exact (fun x:Z => Z.eq_dec x 0). Defined. Corollary Z_notzerop : forall (x:Z), {x <> 0} + {x = 0}. Proof (fun x => sumbool_not _ _ (Z_zerop x)). Corollary Z_noteq_dec : forall (x y:Z), {x <> y} + {x = y}. -Proof (fun x y => sumbool_not _ _ (Z_eq_dec x y)). +Proof (fun x y => sumbool_not _ _ (Z.eq_dec x y)). (* end hide *) |