Require Import BinInt.
Require Import Zeven.
Require Import Zorder.
Require Import Zcompare.
Require Import ZArith_dec.
Require Import Sumbool.
The decidability of equality and order relations over
type Z give 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)%Z with
| Gt => false
| _ => true
end.
Definition Zge_bool (x y:Z) :=
match (x ?= y)%Z with
| Lt => false
| _ => true
end.
Definition Zlt_bool (x y:Z) :=
match (x ?= y)%Z with
| Lt => true
| _ => false
end.
Definition Zgt_bool (x y:Z) :=
match (x ?= y)%Z with
| Gt => true
| _ => false
end.
Definition Zeq_bool (x y:Z) :=
match (x ?= y)%Z with
| Eq => true
| _ => false
end.
Definition Zneq_bool (x y:Z) :=
match (x ?= y)%Z with
| Eq => false
| _ => true
end.
Lemma Zle_cases :
forall n m:Z, if Zle_bool n m then (n <= m)%Z else (n > m)%Z.
Proof.
intros x y; unfold Zle_bool, Zle, Zgt in |- *.
case (x ?= y)%Z; auto; discriminate.
Qed.
Lemma Zlt_cases :
forall n m:Z, if Zlt_bool n m then (n < m)%Z else (n >= m)%Z.
Proof.
intros x y; unfold Zlt_bool, Zlt, Zge in |- *.
case (x ?= y)%Z; auto; discriminate.
Qed.
Lemma Zge_cases :
forall n m:Z, if Zge_bool n m then (n >= m)%Z else (n < m)%Z.
Proof.
intros x y; unfold Zge_bool, Zge, Zlt in |- *.
case (x ?= y)%Z; auto; discriminate.
Qed.
Lemma Zgt_cases :
forall n m:Z, if Zgt_bool n m then (n > m)%Z else (n <= m)%Z.
Proof.
intros x y; unfold Zgt_bool, Zgt, Zle in |- *.
case (x ?= y)%Z; auto; discriminate.
Qed.
Lemmas on Zle_bool used in contrib/graphs
|
Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m)%Z.
Proof.
unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *.
case (x ?= y)%Z; intros; discriminate.
Qed.
Lemma Zle_imp_le_bool : forall n m:Z, (n <= m)%Z -> Zle_bool n m = true.
Proof.
unfold Zle, Zle_bool in |- *. intros x y. case (x ?= y)%Z; trivial. intro. elim (H (refl_equal _)).
Qed.
Lemma Zle_bool_refl : forall n:Z, Zle_bool n n = true.
Proof.
intro. apply Zle_imp_le_bool. apply Zeq_le. reflexivity.
Qed.
Lemma Zle_bool_antisym :
forall n m:Z, Zle_bool n m = true -> Zle_bool m n = true -> n = m.
Proof.
intros. apply Zle_antisym. apply Zle_bool_imp_le. assumption.
apply Zle_bool_imp_le. assumption.
Qed.
Lemma Zle_bool_trans :
forall n m p:Z,
Zle_bool n m = true -> Zle_bool m p = true -> Zle_bool n p = true.
Proof.
intros x y z; intros. apply Zle_imp_le_bool. apply Zle_trans with (m:= y). apply Zle_bool_imp_le. assumption.
apply Zle_bool_imp_le. assumption.
Qed.
Definition Zle_bool_total :
forall x y:Z, {Zle_bool x y = true} + {Zle_bool y x = true}.
Proof.
intros x y; intros. unfold Zle_bool in |- *. cut ((x ?= y)%Z = Gt <-> (y ?= x)%Z = Lt).
case (x ?= y)%Z. left. reflexivity.
left. reflexivity.
right. rewrite (proj1 H (refl_equal _)). reflexivity.
apply Zcompare_Gt_Lt_antisym.
Defined.
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.
Proof.
intros. apply Zle_imp_le_bool. apply Zplus_le_compat. apply Zle_bool_imp_le. assumption.
apply Zle_bool_imp_le. assumption.
Qed.
Lemma Zone_pos : Zle_bool 1 0 = false.
Proof.
reflexivity.
Qed.
Lemma Zone_min_pos : forall n:Z, Zle_bool n 0 = false -> Zle_bool 1 n = true.
Proof.
intros x; intros. apply Zle_imp_le_bool. change (Zsucc 0 <= x)%Z in |- *. apply Zgt_le_succ. generalize H.
unfold Zle_bool, Zgt in |- *. case (x ?= 0)%Z. intro H0. discriminate H0.
intro H0. discriminate H0.
reflexivity.
Qed.
Lemma Zle_is_le_bool : forall n m:Z, (n <= m)%Z <-> Zle_bool n m = true.
Proof.
intros. split. intro. apply Zle_imp_le_bool. assumption.
intro. apply Zle_bool_imp_le. assumption.
Qed.
Lemma Zge_is_le_bool : forall n m:Z, (n >= m)%Z <-> Zle_bool m n = true.
Proof.
intros. split. intro. apply Zle_imp_le_bool. apply Zge_le. assumption.
intro. apply Zle_ge. apply Zle_bool_imp_le. assumption.
Qed.
Lemma Zlt_is_le_bool :
forall n m:Z, (n < m)%Z <-> Zle_bool n (m - 1) = true.
Proof.
intros x y. split. intro. apply Zle_imp_le_bool. apply Zlt_succ_le. rewrite (Zsucc_pred y) in H.
assumption.
intro. rewrite (Zsucc_pred y). apply Zle_lt_succ. apply Zle_bool_imp_le. assumption.
Qed.
Lemma Zgt_is_le_bool :
forall n m:Z, (n > m)%Z <-> Zle_bool m (n - 1) = true.
Proof.
intros x y. apply iff_trans with (y < x)%Z. split. exact (Zgt_lt x y).
exact (Zlt_gt y x).
exact (Zlt_is_le_bool y x).
Qed.