Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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.

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

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.n, m:Z
if n <=? m then n <= m else n > m
Proof.n, m:Z
if n <=? m then n <= m else n > m
 case Z.leb_spec; now Z.swap_greater.
Qed.

Lemma Zlt_cases n m : if n <? m then n < m else n >= m.n, m:Z
if n <? m then n < m else n >= m
Proof.n, m:Z
if n <? m then n < m else n >= m
 case Z.ltb_spec; now Z.swap_greater.
Qed.

Lemma Zge_cases n m : if n >=? m then n >= m else n < m.n, m:Z
if n >=? m then n >= m else n < m
Proof.n, m:Z
if n >=? m then n >= m else n < m
 rewrite Z.geb_leb.n, m:Z
if m <=? n then n >= m else n < m case Z.leb_spec; now Z.swap_greater.
Qed.

Lemma Zgt_cases n m : if n >? m then n > m else n <= m.n, m:Z
if n >? m then n > m else n <= m
Proof.n, m:Z
if n >? m then n > m else n <= m
 rewrite Z.gtb_ltb.n, m:Z
if m <? n then n > m else n <= m case Z.ltb_spec; now Z.swap_greater.
Qed.

Lemmas on Z.leb used in contrib/graphs

Lemma Zle_bool_imp_le n m : (n <=? m) = true -> (n <= m).n, m:Z
(n <=? m) = true -> n <= m
Proof.n, m:Z
(n <=? m) = true -> n <= m
 apply Z.leb_le.
Qed.

Lemma Zle_imp_le_bool n m : (n <= m) -> (n <=? m) = true.n, m:Z
n <= m -> (n <=? m) = true
Proof.n, m:Z
n <= m -> (n <=? m) = true
 apply Z.leb_le.
Qed.

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

Lemma Zle_bool_antisym n m :
 (n <=? m) = true -> (m <=? n) = true -> n = m.n, m:Z
(n <=? m) = true -> (m <=? n) = true -> n = m
Proof.n, m:Z
(n <=? m) = true -> (m <=? n) = true -> n = m
 rewrite !Z.leb_le.n, m:Z
n <= m -> m <= n -> n = m apply Z.le_antisymm.
Qed.

Lemma Zle_bool_trans n m p :
 (n <=? m) = true -> (m <=? p) = true -> (n <=? p) = true.n, m, p:Z
(n <=? m) = true ->
(m <=? p) = true -> (n <=? p) = true
Proof.n, m, p:Z
(n <=? m) = true ->
(m <=? p) = true -> (n <=? p) = true
 rewrite !Z.leb_le.n, m, p:Z
n <= m -> m <= p -> n <= p apply Z.le_trans.
Qed.

Definition Zle_bool_total x y :
  { x <=? y = true } + { y <=? x = true }.x, y:Z
{(x <=? y) = true} + {(y <=? x) = true}
Proof.x, y:Z
{(x <=? y) = true} + {(y <=? x) = true}
 case_eq (x <=? y); intros H.x, y:Z
H:(x <=? y) = true
{true = true} + {(y <=? x) = true}
x, y:Z
H:(x <=? y) = false
{false = true} + {(y <=? x) = true}
 -x, y:Z
H:(x <=? y) = true
{true = true} + {(y <=? x) = true} left; trivial.
 -x, y:Z
H:(x <=? y) = false
{false = true} + {(y <=? x) = true} right.x, y:Z
H:(x <=? y) = false
(y <=? x) = true apply Z.leb_gt in H.x, y:Z
H:y < x
(y <=? x) = true now apply Z.leb_le, Z.lt_le_incl.
Defined.

Lemma Zle_bool_plus_mono n m p q :
 (n <=? m) = true ->
 (p <=? q) = true ->
 (n + p <=? m + q) = true.n, m, p, q:Z
(n <=? m) = true ->
(p <=? q) = true -> (n + p <=? m + q) = true
Proof.n, m, p, q:Z
(n <=? m) = true ->
(p <=? q) = true -> (n + p <=? m + q) = true
 rewrite !Z.leb_le.n, m, p, q:Z
n <= m -> p <= q -> n + p <= m + q apply Z.add_le_mono.
Qed.

Lemma Zone_pos : 1 <=? 0 = false.(1 <=? 0) = false
Proof.(1 <=? 0) = false
 reflexivity.
Qed.

Lemma Zone_min_pos n : (n <=? 0) = false -> (1 <=? n) = true.n:Z
(n <=? 0) = false -> (1 <=? n) = true
Proof.n:Z
(n <=? 0) = false -> (1 <=? n) = true
 rewrite Z.leb_le, Z.leb_gt.n:Z
0 < n -> 1 <= n apply Z.le_succ_l.
Qed.

Properties in term of iff

Lemma Zle_is_le_bool n m : (n <= m) <-> (n <=? m) = true.n, m:Z
n <= m <-> (n <=? m) = true
Proof.n, m:Z
n <= m <-> (n <=? m) = true
 symmetry.n, m:Z
(n <=? m) = true <-> n <= m apply Z.leb_le.
Qed.

Lemma Zge_is_le_bool n m : (n >= m) <-> (m <=? n) = true.n, m:Z
n >= m <-> (m <=? n) = true
Proof.n, m:Z
n >= m <-> (m <=? n) = true
 Z.swap_greater.n, m:Z
m <= n <-> (m <=? n) = true symmetry.n, m:Z
(m <=? n) = true <-> m <= n apply Z.leb_le.
Qed.

Lemma Zlt_is_lt_bool n m : (n < m) <-> (n <? m) = true.n, m:Z
n < m <-> (n <? m) = true
Proof.n, m:Z
n < m <-> (n <? m) = true
 symmetry.n, m:Z
(n <? m) = true <-> n < m apply Z.ltb_lt.
Qed.

Lemma Zgt_is_gt_bool n m : (n > m) <-> (n >? m) = true.n, m:Z
n > m <-> (n >? m) = true
Proof.n, m:Z
n > m <-> (n >? m) = true
 Z.swap_greater.n, m:Z
m < n <-> (n >? m) = true rewrite Z.gtb_ltb.n, m:Z
m < n <-> (m <? n) = true symmetry.n, m:Z
(m <? n) = true <-> m < n apply Z.ltb_lt.
Qed.

Lemma Zlt_is_le_bool n m : (n < m) <-> (n <=? m - 1) = true.n, m:Z
n < m <-> (n <=? m - 1) = true
Proof.n, m:Z
n < m <-> (n <=? m - 1) = true
 rewrite Z.leb_le.n, m:Z
n < m <-> n <= m - 1 apply Z.lt_le_pred.
Qed.

Lemma Zgt_is_le_bool n m : (n > m) <-> (m <=? n - 1) = true.n, m:Z
n > m <-> (m <=? n - 1) = true
Proof.n, m:Z
n > m <-> (m <=? n - 1) = true
 Z.swap_greater.n, m:Z
m < n <-> (m <=? n - 1) = true rewrite Z.leb_le.n, m:Z
m < n <-> m <= n - 1 apply Z.lt_le_pred.
Qed.

Properties of the deprecated Zeq_bool

Lemma Zeq_is_eq_bool x y : x = y <-> Zeq_bool x y = true.x, y:Z
x = y <-> Zeq_bool x y = true
Proof.x, y:Z
x = y <-> Zeq_bool x y = true
 unfold Zeq_bool.x, y:Z
x = y <->
match x ?= y with
| Eq => true
| _ => false
end = true
 rewrite <- Z.compare_eq_iff.x, y:Z
(x ?= y) = Eq <->
match x ?= y with
| Eq => true
| _ => false
end = true destruct Z.compare; now split.
Qed.

Lemma Zeq_bool_eq x y : Zeq_bool x y = true -> x = y.x, y:Z
Zeq_bool x y = true -> x = y
Proof.x, y:Z
Zeq_bool x y = true -> x = y
 apply Zeq_is_eq_bool.
Qed.

Lemma Zeq_bool_neq x y : Zeq_bool x y = false -> x <> y.x, y:Z
Zeq_bool x y = false -> x <> y
Proof.x, y:Z
Zeq_bool x y = false -> x <> y
 rewrite Zeq_is_eq_bool; now destruct Zeq_bool.
Qed.

Lemma Zeq_bool_if x y : if Zeq_bool x y then x=y else x<>y.x, y:Z
if Zeq_bool x y then x = y else x <> y
Proof.x, y:Z
if Zeq_bool x y then x = y else x <> y
 generalize (Zeq_bool_eq x y) (Zeq_bool_neq x y).x, y:Z
(Zeq_bool x y = true -> x = y) ->
(Zeq_bool x y = false -> x <> y) ->
if Zeq_bool x y then x = y else x <> y
 destruct Zeq_bool; auto.
Qed.