# Library Coq.ZArith.Zbool

Require Import BinInt.
Require Import Zeven.
Require Import Zorder.
Require Import Zcompare.
Require Import ZArith_dec.
Require Import Sumbool.
Open Local Scope Z_scope.

# Boolean operations from decidability of order

The decidability of equality and order relations over type Z gives some boolean functions with the adequate specification.
Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y).
Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y).
Definition Z_le_gt_bool (x y:Z) := bool_of_sumbool (Z_le_gt_dec x y).
Definition Z_gt_le_bool (x y:Z) := bool_of_sumbool (Z_gt_le_dec x y).
Definition Z_eq_bool (x y:Z) := bool_of_sumbool (Z_eq_dec x y).
Definition Z_noteq_bool (x y:Z) := bool_of_sumbool (Z_noteq_dec x y).
Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x).

# Boolean comparisons of binary integers

Definition Zle_bool (x y:Z) :=
match x ?= y with
| Gt => false
| _ => true
end.
Definition Zge_bool (x y:Z) :=
match x ?= y with
| Lt => false
| _ => true
end.
Definition Zlt_bool (x y:Z) :=
match x ?= y with
| Lt => true
| _ => false
end.
Definition Zgt_bool (x y:Z) :=
match x ?= y with
| Gt => true
| _ => false
end.
Definition Zeq_bool (x y:Z) :=
match x ?= y with
| Eq => true
| _ => false
end.
Definition Zneq_bool (x y:Z) :=
match x ?= y with
| Eq => false
| _ => true
end.
Properties in term of if ... then ... else ...
Lemma Zle_cases :
forall n m:Z, if Zle_bool n m then (n <= m) else (n > m).
Lemma Zlt_cases :
forall n m:Z, if Zlt_bool n m then (n < m) else (n >= m).
Lemma Zge_cases :
forall n m:Z, if Zge_bool n m then (n >= m) else (n < m).
Lemma Zgt_cases :
forall n m:Z, if Zgt_bool n m then (n > m) else (n <= m).
Lemmas on Zle_bool used in contrib/graphs
Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m).
Lemma Zle_imp_le_bool : forall n m:Z, (n <= m) -> Zle_bool n m = true.
Lemma Zle_bool_refl : forall n:Z, Zle_bool n n = true.
Lemma Zle_bool_antisym :
forall n m:Z, Zle_bool n m = true -> Zle_bool m n = true -> n = m.
Lemma Zle_bool_trans :
forall n m p:Z,
Zle_bool n m = true -> Zle_bool m p = true -> Zle_bool n p = true.
Definition Zle_bool_total :
forall x y:Z, { Zle_bool x y = true } + { Zle_bool y x = true }.
Lemma Zle_bool_plus_mono :
forall n m p q:Z,
Zle_bool n m = true ->
Zle_bool p q = true -> Zle_bool (n + p) (m + q) = true.
Lemma Zone_pos : Zle_bool 1 0 = false.
Lemma Zone_min_pos : forall n:Z, Zle_bool n 0 = false -> Zle_bool 1 n = true.
Properties in term of iff
Lemma Zle_is_le_bool : forall n m:Z, ( n <= m ) <-> Zle_bool n m = true.
Lemma Zge_is_le_bool : forall n m:Z, ( n >= m ) <-> Zle_bool m n = true.
Lemma Zlt_is_lt_bool : forall n m:Z, ( n < m ) <-> Zlt_bool n m = true.
Lemma Zgt_is_gt_bool : forall n m:Z, ( n > m ) <-> Zgt_bool n m = true.
Lemma Zlt_is_le_bool :
forall n m:Z, ( n < m ) <-> Zle_bool n (m - 1) = true.
Lemma Zgt_is_le_bool :
forall n m:Z, ( n > m ) <-> Zle_bool m (n - 1) = true.
Lemma Zeq_is_eq_bool : forall x y, x = y <-> Zeq_bool x y = true.
Lemma Zeq_bool_eq : forall x y, Zeq_bool x y = true -> x = y.
Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y.
Lemma Zeq_bool_if : forall x y, if Zeq_bool x y then x = y else x <> y.