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