numbers.v 12.3 KB
Newer Older
1
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
4
5
(** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Require Export PArith NArith ZArith.
7
Require Import Qcanon.
8
Require Export base decidable.
9
Open Scope nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11
12
Coercion Z.of_nat : nat >-> Z.

13
(** * Notations and properties of [nat] *)
14
15
16
17
18
Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
Reserved Notation "x ≤ y < z" (at level 70, y at next level).
Reserved Notation "x < y < z" (at level 70, y at next level).
Reserved Notation "x < y ≤ z" (at level 70, y at next level).

19
Infix "≤" := le : nat_scope.
20
21
22
23
24
25
26
27
28
29
Notation "x ≤ y ≤ z" := (x  y  y  z)%nat : nat_scope.
Notation "x ≤ y < z" := (x  y  y < z)%nat : nat_scope.
Notation "x < y < z" := (x < y  y < z)%nat : nat_scope.
Notation "x < y ≤ z" := (x < y  y  z)%nat : nat_scope.
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.

Infix "`div`" := NPeano.div (at level 35) : nat_scope.
Infix "`mod`" := NPeano.modulo (at level 35) : nat_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
30
Instance nat_eq_dec:  x y : nat, Decision (x = y) := eq_nat_dec.
31
32
Instance nat_le_dec:  x y : nat, Decision (x  y) := le_dec.
Instance nat_lt_dec:  x y : nat, Decision (x < y) := lt_dec.
33
Instance nat_inhabited: Inhabited nat := populate 0%nat.
34
35
36
37
38
39

Lemma lt_n_SS n : n < S (S n).
Proof. auto with arith. Qed.
Lemma lt_n_SSS n : n < S (S (S n)).
Proof. auto with arith. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
43
44
45
46
47
Definition sum_list_with {A} (f : A  nat) : list A  nat :=
  fix go l :=
  match l with
  | [] => 0
  | x :: l => f x + go l
  end.
Notation sum_list := (sum_list_with id).

48
49
50
(** * Notations and properties of [positive] *)
Open Scope positive_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
51
Instance positive_eq_dec:  x y : positive, Decision (x = y) := Pos.eq_dec.
52
Instance positive_inhabited: Inhabited positive := populate 1.
53

Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
56
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

57
Instance: Injective (=) (=) (~0).
Robbert Krebbers's avatar
Robbert Krebbers committed
58
Proof. by injection 1. Qed.
59
Instance: Injective (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
Proof. by injection 1. Qed.

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
(** Since [positive] represents lists of bits, we define list operations
on it. These operations are in reverse, as positives are treated as snoc
lists instead of cons lists. *)
Fixpoint Papp (p1 p2 : positive) : positive :=
  match p2 with
  | 1 => p1
  | p2~0 => (Papp p1 p2)~0
  | p2~1 => (Papp p1 p2)~1
  end.
Infix "++" := Papp : positive_scope.
Notation "(++)" := Papp (only parsing) : positive_scope.
Notation "( p ++)" := (Papp p) (only parsing) : positive_scope.
Notation "(++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.

Fixpoint Preverse_go (p1 p2 : positive) : positive :=
  match p2 with
  | 1 => p1
  | p2~0 => Preverse_go (p1~0) p2
  | p2~1 => Preverse_go (p1~1) p2
  end.
Definition Preverse : positive  positive := Preverse_go 1.

Global Instance: LeftId (=) 1 (++).
Proof. intros p. induction p; simpl; intros; f_equal; auto. Qed.
Global Instance: RightId (=) 1 (++).
Proof. done. Qed.
Global Instance: Associative (=) (++).
Proof. intros ?? p. induction p; simpl; intros; f_equal; auto. Qed.
Global Instance:  p : positive, Injective (=) (=) (++ p).
Proof. intros p ???. induction p; simplify_equality; auto. Qed.

Lemma Preverse_go_app_cont p1 p2 p3 :
  Preverse_go (p2 ++ p1) p3 = p2 ++ Preverse_go p1 p3.
Proof.
  revert p1. induction p3; simpl; intros.
  * apply (IHp3 (_~1)).
  * apply (IHp3 (_~0)).
  * done.
Qed.
Lemma Preverse_go_app p1 p2 p3 :
  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
Proof.
  revert p1. induction p3; intros p1; simpl; auto.
  by rewrite <-Preverse_go_app_cont.
Qed.
Lemma Preverse_app p1 p2 :
  Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
Proof. unfold Preverse. by rewrite Preverse_go_app. Qed.

Lemma Preverse_xO p : Preverse (p~0) = (1~0) ++ Preverse p.
Proof Preverse_app p (1~0).
Lemma Preverse_xI p : Preverse (p~1) = (1~1) ++ Preverse p.
Proof Preverse_app p (1~1).

Fixpoint Plength (p : positive) : nat :=
  match p with
  | 1 => 0%nat
  | p~0 | p~1 => S (Plength p)
  end.
Lemma Papp_length p1 p2 :
  Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
Proof. induction p2; simpl; f_equal; auto. Qed.

Close Scope positive_scope.

(** * Notations and properties of [N] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Infix "≤" := N.le : N_scope.
129
130
131
132
Notation "x ≤ y ≤ z" := (x  y  y  z)%N : N_scope.
Notation "x ≤ y < z" := (x  y  y < z)%N : N_scope.
Notation "x < y < z" := (x < y  y < z)%N : N_scope.
Notation "x < y ≤ z" := (x < y  y  z)%N : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Notation "(≤)" := N.le (only parsing) : N_scope.
134
Notation "(<)" := N.lt (only parsing) : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
135

136
137
138
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
141
Instance: Injective (=) (=) Npos.
Proof. by injection 1. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
145
146
147
148
Instance N_eq_dec:  x y : N, Decision (x = y) := N.eq_dec.
Program Instance N_le_dec (x y : N) : Decision (x  y)%N :=
  match Ncompare x y with
  | Gt => right _
  | _ => left _
  end.
Next Obligation. congruence. Qed.
149
150
151
152
153
154
Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
  match Ncompare x y with
  | Lt => left _
  | _ => right _
  end.
Next Obligation. congruence. Qed.
155
Instance N_inhabited: Inhabited N := populate 1%N.
Robbert Krebbers's avatar
Robbert Krebbers committed
156

157
(** * Notations and properties of [Z] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Infix "≤" := Z.le : Z_scope.
159
160
161
162
Notation "x ≤ y ≤ z" := (x  y  y  z)%Z : Z_scope.
Notation "x ≤ y < z" := (x  y  y < z)%Z : Z_scope.
Notation "x < y < z" := (x < y  y < z)%Z : Z_scope.
Notation "x < y ≤ z" := (x < y  y  z)%Z : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Notation "(≤)" := Z.le (only parsing) : Z_scope.
164
Notation "(<)" := Z.lt (only parsing) : Z_scope.
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
168
169
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
170

Robbert Krebbers's avatar
Robbert Krebbers committed
171
172
Instance Z_eq_dec:  x y : Z, Decision (x = y) := Z.eq_dec.
Instance Z_le_dec:  x y : Z, Decision (x  y)%Z := Z_le_dec.
173
Instance Z_lt_dec:  x y : Z, Decision (x < y)%Z := Z_lt_dec.
174
Instance Z_inhabited: Inhabited Z := populate 1%Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
175

176
177
178
179
180
181
182
183
184
185
186
187
(* Note that we cannot disable simpl for [Z.of_nat] as that would break
[omega] and [lia]. *)
Arguments Z.to_nat _ : simpl never.
Arguments Z.mul _ _ : simpl never.
Arguments Z.add _ _ : simpl never.
Arguments Z.opp _ : simpl never.
Arguments Z.pow _ _ : simpl never.
Arguments Z.div _ _ : simpl never.
Arguments Z.modulo _ _ : simpl never.
Arguments Z.quot _ _ : simpl never.
Arguments Z.rem _ _ : simpl never.

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
(** * Notations and properties of [Qc] *)
Notation "2" := (1+1)%Qc : Qc_scope.
Infix "≤" := Qcle : Qc_scope.
Notation "x ≤ y ≤ z" := (x  y  y  z)%Qc : Qc_scope.
Notation "x ≤ y < z" := (x  y  y < z)%Qc : Qc_scope.
Notation "x < y < z" := (x < y  y < z)%Qc : Qc_scope.
Notation "x < y ≤ z" := (x < y  y  z)%Qc : Qc_scope.
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

Instance Qc_eq_dec:  x y : Qc, Decision (x = y) := Qc_eq_dec.
Program Instance Qc_le_dec (x y : Qc) : Decision (x  y)%Qc :=
  if Qclt_le_dec y x then right _ else left _.
Next Obligation. by apply Qclt_not_le. Qed.
Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y)%Qc :=
  if Qclt_le_dec x y then left _ else right _.
Next Obligation. by apply Qcle_not_lt. Qed.

Instance: Reflexive Qcle.
Proof. red. apply Qcle_refl. Qed.
Instance: Transitive Qcle.
Proof. red. apply Qcle_trans. Qed.

Lemma Qcle_ngt (x y : Qc) : (x  y  ¬y < x)%Qc.
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
Lemma Qclt_nge (x y : Qc) : (x < y  ¬y  x)%Qc.
Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.

Lemma Qcplus_le_mono_l (x y z : Qc) :
  (x  y  z + x  z + y)%Qc.
Proof.
  split; intros.
  * by apply Qcplus_le_compat.
  * replace x with ((0 - z) + (z + x))%Qc by ring.
    replace y with ((0 - z) + (z + y))%Qc by ring.
    by apply Qcplus_le_compat.
Qed.
Lemma Qcplus_le_mono_r (x y z : Qc) :
  (x  y  x + z  y + z)%Qc.
Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
Lemma Qcplus_lt_mono_l (x y z : Qc) :
  (x < y  z + x < z + y)%Qc.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
Lemma Qcplus_lt_mono_r (x y z : Qc) :
  (x < y  x + z < y + z)%Qc.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.

235
(** * Conversions *)
236
237
(** The function [Z_to_option_N] converts an integer [x] into a natural number
by giving [None] in case [x] is negative. *)
238
Definition Z_to_option_N (x : Z) : option N :=
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
241
242
243
  match x with
  | Z0 => Some N0
  | Zpos p => Some (Npos p)
  | Zneg _ => None
  end.
244
245
246
247
248
249
Definition Z_to_option_nat (x : Z) : option nat :=
  match x with
  | Z0 => Some 0
  | Zpos p => Some (Pos.to_nat p)
  | Zneg _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Lemma Z_to_option_N_Some x y :
  Z_to_option_N x = Some y  (0  x)%Z  y = Z.to_N x.
Proof.
  split.
  * intros. by destruct x; simpl in *; simplify_equality;
      auto using Zle_0_pos.
  * intros [??]. subst. destruct x; simpl; auto; lia.
Qed.
Lemma Z_to_option_N_Some_alt x y :
  Z_to_option_N x = Some y  (0  x)%Z  x = Z.of_N y.
Proof.
  rewrite Z_to_option_N_Some.
  split; intros [??]; subst; auto using N2Z.id, Z2N.id, eq_sym.
Qed.

Lemma Z_to_option_nat_Some x y :
  Z_to_option_nat x = Some y  (0  x)%Z  y = Z.to_nat x.
Proof.
  split.
  * intros. by destruct x; simpl in *; simplify_equality;
      auto using Zle_0_pos.
  * intros [??]. subst. destruct x; simpl; auto; lia.
Qed.
Lemma Z_to_option_nat_Some_alt x y :
  Z_to_option_nat x = Some y  (0  x)%Z  x = Z.of_nat y.
Proof.
  rewrite Z_to_option_nat_Some.
  split; intros [??]; subst; auto using Nat2Z.id, Z2Nat.id, eq_sym.
Qed.
Lemma Z_to_option_of_nat x :
  Z_to_option_nat (Z.of_nat x) = Some x.
Proof. apply Z_to_option_nat_Some_alt. auto using Nat2Z.is_nonneg. Qed.

(** The function [Z_of_sumbool] converts a sumbool [P] into an integer
by yielding one if [P] and zero if [Q]. *)
Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q}) : Z :=
  (if p then 1 else 0)%Z.
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345

(** Some correspondence lemmas between [nat] and [N] that are not part of the
standard library. We declare a hint database [natify] to rewrite a goal
involving [N] into a corresponding variant involving [nat]. *)
Lemma N_to_nat_lt x y : N.to_nat x < N.to_nat y  (x < y)%N.
Proof. by rewrite <-N.compare_lt_iff, nat_compare_lt, N2Nat.inj_compare. Qed.
Lemma N_to_nat_le x y : N.to_nat x  N.to_nat y  (x  y)%N.
Proof. by rewrite <-N.compare_le_iff, nat_compare_le, N2Nat.inj_compare. Qed.
Lemma N_to_nat_0 : N.to_nat 0 = 0.
Proof. done. Qed.
Lemma N_to_nat_1 : N.to_nat 1 = 1.
Proof. done. Qed.
Lemma N_to_nat_div x y : N.to_nat (x `div` y) = N.to_nat x `div` N.to_nat y.
Proof.
  destruct (decide (y = 0%N)).
  { subst. by destruct x. }
  apply NPeano.Nat.div_unique with (N.to_nat (x `mod` y)).
  { by apply N_to_nat_lt, N.mod_lt. }
  rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
  by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
Qed.
(* We have [x `mod` 0 = 0] on [nat], and [x `mod` 0 = x] on [N]. *)
Lemma N_to_nat_mod x y :
  y  0%N 
  N.to_nat (x `mod` y) = N.to_nat x `mod` N.to_nat y.
Proof.
  intros.
  apply NPeano.Nat.mod_unique with (N.to_nat (x `div` y)).
  { by apply N_to_nat_lt, N.mod_lt. }
  rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
  by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
Qed.

Hint Rewrite <-N2Nat.inj_iff : natify.
Hint Rewrite <-N_to_nat_lt : natify.
Hint Rewrite <-N_to_nat_le : natify.
Hint Rewrite Nat2N.id : natify.
Hint Rewrite N2Nat.inj_add : natify.
Hint Rewrite N2Nat.inj_mul : natify.
Hint Rewrite N2Nat.inj_sub : natify.
Hint Rewrite N2Nat.inj_succ : natify.
Hint Rewrite N2Nat.inj_pred : natify.
Hint Rewrite N_to_nat_div : natify.
Hint Rewrite N_to_nat_0 : natify.
Hint Rewrite N_to_nat_1 : natify.
Ltac natify := repeat autorewrite with natify in *.

Hint Extern 100 (Nlt _ _) => natify : natify.
Hint Extern 100 (Nle _ _) => natify : natify.
Hint Extern 100 (@eq N _ _) => natify : natify.
Hint Extern 100 (lt _ _) => natify : natify.
Hint Extern 100 (le _ _) => natify : natify.
Hint Extern 100 (@eq nat _ _) => natify : natify.

Instance:  x, PropHolds (0 < x)%N  PropHolds (0 < N.to_nat x).
Proof. unfold PropHolds. intros. by natify. Qed.
Instance:  x, PropHolds (0  x)%N  PropHolds (0  N.to_nat x).
Proof. unfold PropHolds. intros. by natify. Qed.