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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import BinPos.
Require Import BinNat.
Require Import Pnat.
Require Import Nnat.
Require Import Ndigits.
Local Open Scope N_scope.
(** Obsolete results about boolean comparisons over [N],
kept for compatibility with IntMap and SMC. *)
Notation Peqb := Pos.eqb (compat "8.3").
Notation Neqb := N.eqb (compat "8.3").
Notation Peqb_correct := Pos.eqb_refl (compat "8.3").
Notation Neqb_correct := N.eqb_refl (compat "8.3").
Notation Neqb_comm := N.eqb_sym (compat "8.3").
Lemma Peqb_complete p p' : Pos.eqb p p' = true -> p = p'.
Proof. now apply Pos.eqb_eq. Qed.
Lemma Peqb_Pcompare p p' : Pos.eqb p p' = true -> Pos.compare p p' = Eq.
Proof. now rewrite Pos.compare_eq_iff, <- Pos.eqb_eq. Qed.
Lemma Pcompare_Peqb p p' : Pos.compare p p' = Eq -> Pos.eqb p p' = true.
Proof. now rewrite Pos.eqb_eq, <- Pos.compare_eq_iff. Qed.
Lemma Neqb_Ncompare n n' : N.eqb n n' = true -> N.compare n n' = Eq.
Proof. now rewrite N.compare_eq_iff, <- N.eqb_eq. Qed.
Lemma Ncompare_Neqb n n' : N.compare n n' = Eq -> N.eqb n n' = true.
Proof. now rewrite N.eqb_eq, <- N.compare_eq_iff. Qed.
Lemma Neqb_complete n n' : N.eqb n n' = true -> n = n'.
Proof. now apply N.eqb_eq. Qed.
Lemma Nxor_eq_true n n' : N.lxor n n' = 0 -> N.eqb n n' = true.
Proof.
intro H. apply N.lxor_eq in H. subst. apply N.eqb_refl.
Qed.
Ltac eqb2eq := rewrite <- ?not_true_iff_false in *; rewrite ?N.eqb_eq in *.
Lemma Nxor_eq_false n n' p :
N.lxor n n' = N.pos p -> N.eqb n n' = false.
Proof.
intros. eqb2eq. intro. subst. now rewrite N.lxor_nilpotent in *.
Qed.
Lemma Nodd_not_double a :
Nodd a -> forall a0, N.eqb (N.double a0) a = false.
Proof.
intros. eqb2eq. intros <-.
unfold Nodd in *. now rewrite Ndouble_bit0 in *.
Qed.
Lemma Nnot_div2_not_double a a0 :
N.eqb (N.div2 a) a0 = false -> N.eqb a (N.double a0) = false.
Proof.
intros H. eqb2eq. contradict H. subst. apply N.div2_double.
Qed.
Lemma Neven_not_double_plus_one a :
Neven a -> forall a0, N.eqb (N.succ_double a0) a = false.
Proof.
intros. eqb2eq. intros <-.
unfold Neven in *. now rewrite Ndouble_plus_one_bit0 in *.
Qed.
Lemma Nnot_div2_not_double_plus_one a a0 :
N.eqb (N.div2 a) a0 = false -> N.eqb (N.succ_double a0) a = false.
Proof.
intros H. eqb2eq. contradict H. subst. apply N.div2_succ_double.
Qed.
Lemma Nbit0_neq a a' :
N.odd a = false -> N.odd a' = true -> N.eqb a a' = false.
Proof.
intros. eqb2eq. now intros <-.
Qed.
Lemma Ndiv2_eq a a' :
N.eqb a a' = true -> N.eqb (N.div2 a) (N.div2 a') = true.
Proof.
intros. eqb2eq. now subst.
Qed.
Lemma Ndiv2_neq a a' :
N.eqb (N.div2 a) (N.div2 a') = false -> N.eqb a a' = false.
Proof.
intros H. eqb2eq. contradict H. now subst.
Qed.
Lemma Ndiv2_bit_eq a a' :
N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'.
Proof.
intros H H'; now rewrite (N.div2_odd a), (N.div2_odd a'), H, H'.
Qed.
Lemma Ndiv2_bit_neq a a' :
N.eqb a a' = false ->
N.odd a = N.odd a' -> N.eqb (N.div2 a) (N.div2 a') = false.
Proof.
intros H H'. eqb2eq. contradict H. now apply Ndiv2_bit_eq.
Qed.
Lemma Nneq_elim a a' :
N.eqb a a' = false ->
N.odd a = negb (N.odd a') \/
N.eqb (N.div2 a) (N.div2 a') = false.
Proof.
intros.
enough (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')) as [].
- right. apply Ndiv2_bit_neq; assumption.
- left. assumption.
- case (N.odd a), (N.odd a'); auto.
Qed.
Lemma Ndouble_or_double_plus_un a :
{a0 : N | a = N.double a0} + {a1 : N | a = N.succ_double a1}.
Proof.
elim (sumbool_of_bool (N.odd a)); intros H; [right|left];
exists (N.div2 a); symmetry;
apply Ndiv2_double_plus_one || apply Ndiv2_double; auto.
Qed.
(** An inefficient boolean order on [N]. Please use [N.leb] instead now. *)
Definition Nleb (a b:N) := leb (N.to_nat a) (N.to_nat b).
Lemma Nleb_alt a b : Nleb a b = N.leb a b.
Proof.
unfold Nleb.
now rewrite eq_iff_eq_true, N.leb_le, leb_compare, <- N2Nat.inj_compare.
Qed.
Lemma Nleb_Nle a b : Nleb a b = true <-> a <= b.
Proof. now rewrite Nleb_alt, N.leb_le. Qed.
Lemma Nleb_refl a : Nleb a a = true.
Proof. rewrite Nleb_Nle; apply N.le_refl. Qed.
Lemma Nleb_antisym a b : Nleb a b = true -> Nleb b a = true -> a = b.
Proof. rewrite !Nleb_Nle. apply N.le_antisymm. Qed.
Lemma Nleb_trans a b c : Nleb a b = true -> Nleb b c = true -> Nleb a c = true.
Proof. rewrite !Nleb_Nle. apply N.le_trans. Qed.
Lemma Nleb_ltb_trans a b c :
Nleb a b = true -> Nleb c b = false -> Nleb c a = false.
Proof.
unfold Nleb. intros. apply leb_correct_conv.
apply le_lt_trans with (m := N.to_nat b).
apply leb_complete. assumption.
apply leb_complete_conv. assumption.
Qed.
Lemma Nltb_leb_trans a b c :
Nleb b a = false -> Nleb b c = true -> Nleb c a = false.
Proof.
unfold Nleb. intros. apply leb_correct_conv.
apply lt_le_trans with (m := N.to_nat b).
apply leb_complete_conv. assumption.
apply leb_complete. assumption.
Qed.
Lemma Nltb_trans a b c :
Nleb b a = false -> Nleb c b = false -> Nleb c a = false.
Proof.
unfold Nleb. intros. apply leb_correct_conv.
apply lt_trans with (m := N.to_nat b).
apply leb_complete_conv. assumption.
apply leb_complete_conv. assumption.
Qed.
Lemma Nltb_leb_weak a b : Nleb b a = false -> Nleb a b = true.
Proof.
unfold Nleb. intros. apply leb_correct. apply lt_le_weak.
apply leb_complete_conv. assumption.
Qed.
Lemma Nleb_double_mono a b :
Nleb a b = true -> Nleb (N.double a) (N.double b) = true.
Proof.
unfold Nleb. intros. rewrite !N2Nat.inj_double. apply leb_correct.
apply mult_le_compat_l. now apply leb_complete.
Qed.
Lemma Nleb_double_plus_one_mono a b :
Nleb a b = true ->
Nleb (N.succ_double a) (N.succ_double b) = true.
Proof.
unfold Nleb. intros. rewrite !N2Nat.inj_succ_double. apply leb_correct.
apply le_n_S, mult_le_compat_l. now apply leb_complete.
Qed.
Lemma Nleb_double_mono_conv a b :
Nleb (N.double a) (N.double b) = true -> Nleb a b = true.
Proof.
unfold Nleb. rewrite !N2Nat.inj_double. intro. apply leb_correct.
apply (mult_S_le_reg_l 1). now apply leb_complete.
Qed.
Lemma Nleb_double_plus_one_mono_conv a b :
Nleb (N.succ_double a) (N.succ_double b) = true ->
Nleb a b = true.
Proof.
unfold Nleb. rewrite !N2Nat.inj_succ_double. intro. apply leb_correct.
apply (mult_S_le_reg_l 1). apply le_S_n. now apply leb_complete.
Qed.
Lemma Nltb_double_mono a b :
Nleb a b = false -> Nleb (N.double a) (N.double b) = false.
Proof.
intros. elim (sumbool_of_bool (Nleb (N.double a) (N.double b))). intro H0.
rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H.
trivial.
Qed.
Lemma Nltb_double_plus_one_mono a b :
Nleb a b = false ->
Nleb (N.succ_double a) (N.succ_double b) = false.
Proof.
intros. elim (sumbool_of_bool (Nleb (N.succ_double a) (N.succ_double b))).
intro H0.
rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H. discriminate H.
trivial.
Qed.
Lemma Nltb_double_mono_conv a b :
Nleb (N.double a) (N.double b) = false -> Nleb a b = false.
Proof.
intros. elim (sumbool_of_bool (Nleb a b)). intro H0.
rewrite (Nleb_double_mono _ _ H0) in H. discriminate H.
trivial.
Qed.
Lemma Nltb_double_plus_one_mono_conv a b :
Nleb (N.succ_double a) (N.succ_double b) = false ->
Nleb a b = false.
Proof.
intros. elim (sumbool_of_bool (Nleb a b)). intro H0.
rewrite (Nleb_double_plus_one_mono _ _ H0) in H. discriminate H.
trivial.
Qed.
(* Nleb and N.compare *)
(* NB: No need to prove that Nleb a b = true <-> N.compare a b <> Gt,
this statement is in fact Nleb_Nle! *)
Lemma Nltb_Ncompare a b : Nleb a b = false <-> N.compare a b = Gt.
Proof.
now rewrite N.compare_nle_iff, <- Nleb_Nle, not_true_iff_false.
Qed.
Lemma Ncompare_Gt_Nltb a b : N.compare a b = Gt -> Nleb a b = false.
Proof. apply <- Nltb_Ncompare; auto. Qed.
Lemma Ncompare_Lt_Nltb a b : N.compare a b = Lt -> Nleb b a = false.
Proof.
intros H. rewrite Nltb_Ncompare, N.compare_antisym, H; auto.
Qed.
(* Old results about [N.min] *)
Notation Nmin_choice := N.min_dec (compat "8.3").
Lemma Nmin_le_1 a b : Nleb (N.min a b) a = true.
Proof. rewrite Nleb_Nle. apply N.le_min_l. Qed.
Lemma Nmin_le_2 a b : Nleb (N.min a b) b = true.
Proof. rewrite Nleb_Nle. apply N.le_min_r. Qed.
Lemma Nmin_le_3 a b c : Nleb a (N.min b c) = true -> Nleb a b = true.
Proof. rewrite !Nleb_Nle. apply N.min_glb_l. Qed.
Lemma Nmin_le_4 a b c : Nleb a (N.min b c) = true -> Nleb a c = true.
Proof. rewrite !Nleb_Nle. apply N.min_glb_r. Qed.
Lemma Nmin_le_5 a b c :
Nleb a b = true -> Nleb a c = true -> Nleb a (N.min b c) = true.
Proof. rewrite !Nleb_Nle. apply N.min_glb. Qed.
Lemma Nmin_lt_3 a b c : Nleb (N.min b c) a = false -> Nleb b a = false.
Proof.
rewrite <- !not_true_iff_false, !Nleb_Nle.
rewrite N.min_le_iff; auto.
Qed.
Lemma Nmin_lt_4 a b c : Nleb (N.min b c) a = false -> Nleb c a = false.
Proof.
rewrite <- !not_true_iff_false, !Nleb_Nle.
rewrite N.min_le_iff; auto.
Qed.
|
