diff options
Diffstat (limited to 'theories/ZArith/ZArith_dec.v')
| -rw-r--r-- | theories/ZArith/ZArith_dec.v | 226 |
1 files changed, 226 insertions, 0 deletions
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v new file mode 100644 index 00000000..dbd0df6c --- /dev/null +++ b/theories/ZArith/ZArith_dec.v @@ -0,0 +1,226 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: ZArith_dec.v,v 1.11.2.1 2004/07/16 19:31:20 herbelin Exp $ i*) + +Require Import Sumbool. + +Require Import BinInt. +Require Import Zorder. +Require Import Zcompare. +Open Local Scope Z_scope. + +Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}. +Proof. +simple induction r; auto with arith. +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. +Defined. + +Section decidability. + +Variables x y : Z. + +(** Decidability of equality on binary integers *) + +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. +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. +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. +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. +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. +Defined. + +Definition Z_lt_ge_dec : {x < y} + {x >= y}. +Proof. +exact Z_lt_dec. +Defined. + +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. +Qed. + +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. +Defined. + +Definition Z_gt_le_dec : {x > y} + {x <= y}. +Proof. +exact Z_gt_dec. +Defined. + +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. +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 H1. absurd (x > y); auto with arith. +Defined. + +End decidability. + +(** Cotransitivity of order on binary integers *) + +Lemma Zlt_cotrans : forall n m:Z, n < m -> forall p:Z, {n < p} + {p < m}. +Proof. + intros x y H z. + case (Z_lt_ge_dec x z). + intro. + left. + assumption. + intro. + right. + apply Zle_lt_trans with (m := x). + apply Zge_le. + assumption. + assumption. +Defined. + +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. +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 ]; + assumption. +Defined. + +Lemma not_Zeq_inf : forall n m:Z, n <> m -> {n < m} + {m < n}. +Proof. + intros x y H. + case Z_lt_ge_dec with x y. + intro. + left. + assumption. + intro H0. + generalize (Zge_le _ _ H0). + intro. + case (Z_le_lt_eq_dec _ _ H1). + intro. + right. + assumption. + intro. + apply False_rec. + apply H. + symmetry in |- *. + assumption. +Defined. + +Lemma Z_dec : forall n m:Z, {n < m} + {n > m} + {n = m}. +Proof. + intros x y. + case (Z_lt_ge_dec x y). + intro H. + left. + left. + assumption. + intro H. + generalize (Zge_le _ _ H). + intro H0. + case (Z_le_lt_eq_dec y x H0). + intro H1. + left. + right. + apply Zlt_gt. + assumption. + intro. + right. + symmetry in |- *. + assumption. +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; + [ right; assumption | left; apply (not_Zeq_inf _ _ H) ]. +Defined. + + + +Definition 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). + +Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).
\ No newline at end of file |