1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: Zbool.v 10063 2007-08-08 14:21:03Z emakarov $ *)
Require Import BinInt.
Require Import Zeven.
Require Import Zorder.
Require Import Zcompare.
Require Import ZArith_dec.
Require Import Sumbool.
Unset Boxed Definitions.
(** * Boolean operations from decidabilty of order *)
(** 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_lt_bool : forall n m:Z, (n < m)%Z <-> Zlt_bool n m = true.
Proof.
intros n m; unfold Zlt_bool, Zlt.
destruct (n ?= m)%Z; simpl; split; now intro.
Qed.
Lemma Zgt_is_gt_bool : forall n m:Z, (n > m)%Z <-> Zgt_bool n m = true.
Proof.
intros n m; unfold Zgt_bool, Zgt.
destruct (n ?= m)%Z; simpl; split; now intro.
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.
|
