Library Coq.ZArith.ZArith_dec



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}.

Lemma Zcompare_rec :
  forall (P:Set) (n m:Z),
    ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.


Section decidability.

  Variables x y : Z.

Decidability of equality on binary integers


  Definition Z_eq_dec : {x = y} + {x <> y}.






Decidability of order on binary integers


  Definition Z_lt_dec : {x < y} + {~ x < y}.



  Definition Z_le_dec : {x <= y} + {~ x <= y}.




  Definition Z_gt_dec : {x > y} + {~ x > y}.



  Definition Z_ge_dec : {x >= y} + {~ x >= y}.




  Definition Z_lt_ge_dec : {x < y} + {x >= y}.

  Lemma Z_lt_le_dec : {x < y} + {y <= x}.

  Definition Z_le_gt_dec : {x <= y} + {x > y}.


  Definition Z_gt_le_dec : {x > y} + {x <= y}.

  Definition Z_ge_lt_dec : {x >= y} + {x < y}.


  Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.




End decidability.

Cotransitivity of order on binary integers


Lemma Zlt_cotrans : forall n m:Z, n < m -> forall p:Z, {n < p} + {p < m}.

Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}.

Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}.

Lemma not_Zeq_inf : forall n m:Z, n <> m -> {n < m} + {m < n}.

Lemma Z_dec : forall n m:Z, {n < m} + {n > m} + {n = m}.

Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}.

Definition Z_zerop : forall x:Z, {x = 0} + {x <> 0}.

Definition Z_notzerop (x:Z) := sumbool_not _ _ (Z_zerop x).

Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).