summaryrefslogtreecommitdiff
path: root/theories/ZArith/ZArith_dec.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/ZArith_dec.v')
-rw-r--r--theories/ZArith/ZArith_dec.v326
1 files changed, 163 insertions, 163 deletions
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 40c5860c..84249955 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ZArith_dec.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: ZArith_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Import Sumbool.
@@ -17,210 +17,210 @@ Open Local Scope Z_scope.
Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}.
Proof.
-simple induction r; auto with arith.
+ 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.
+ 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.
+ 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.
+ 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 *)
+(** * 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.
+ 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.
+ 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.
+ 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.
+ 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.
+ 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) ].
+ 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).
+ 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
+Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 08:14:20 +0000