Library Coq.ZArith.Zbool


Require Import BinInt.
Require Import Zeven.
Require Import Zorder.
Require Import Zcompare.
Require Import ZArith_dec.
Require Import Sumbool.

Local Open 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.

Boolean comparisons of binary integers


Notation Zle_bool := Z.leb (only parsing).
Notation Zge_bool := Z.geb (only parsing).
Notation Zlt_bool := Z.ltb (only parsing).
Notation Zgt_bool := Z.gtb (only parsing).

We now provide a direct Z.eqb that doesn't refer to Z.compare. The old Zeq_bool is kept for compatibility.

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 n m : if n <=? m then n <= m else n > m.

Lemma Zlt_cases n m : if n <? m then n < m else n >= m.

Lemma Zge_cases n m : if n >=? m then n >= m else n < m.

Lemma Zgt_cases n m : if n >? m then n > m else n <= m.

Lemmas on Z.leb used in contrib/graphs

Lemma Zle_bool_imp_le n m : (n <=? m) = true -> (n <= m).

Lemma Zle_imp_le_bool n m : (n <= m) -> (n <=? m) = true.

Notation Zle_bool_refl := Z.leb_refl (only parsing).

Lemma Zle_bool_antisym n m :
 (n <=? m) = true -> (m <=? n) = true -> n = m.

Lemma Zle_bool_trans n m p :
 (n <=? m) = true -> (m <=? p) = true -> (n <=? p) = true.

Definition Zle_bool_total x y :
  { x <=? y = true } + { y <=? x = true }.

Lemma Zle_bool_plus_mono n m p q :
 (n <=? m) = true ->
 (p <=? q) = true ->
 (n + p <=? m + q) = true.

Lemma Zone_pos : 1 <=? 0 = false.

Lemma Zone_min_pos n : (n <=? 0) = false -> (1 <=? n) = true.

Properties in term of iff
Properties of the deprecated Zeq_bool

Lemma Zeq_is_eq_bool x y : x = y <-> Zeq_bool x y = true.

Lemma Zeq_bool_eq x y : Zeq_bool x y = true -> x = y.

Lemma Zeq_bool_neq x y : Zeq_bool x y = false -> x <> y.

Lemma Zeq_bool_if x y : if Zeq_bool x y then x=y else x<>y.