numbers.v 51.6 KB
Newer Older
1
2
3
(** 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. *)
4
From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
5
6
From Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option.
Ralf Jung's avatar
Ralf Jung committed
7
From stdpp Require Import options.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
8
Local Open Scope nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

10
Global Instance comparison_eq_dec : EqDecision comparison.
11
Proof. solve_decision. Defined.
12

13
(** * Notations and properties of [nat] *)
14
15
Global Arguments minus !_ !_ / : assert.
Global Arguments Nat.max : simpl nomatch.
16

17
18
Typeclasses Opaque lt.

19
20
21
22
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).
23
24
Reserved Notation "x ≤ y ≤ z ≤ z'"
  (at level 70, y at next level, z at next level).
25

26
Infix "≤" := le : nat_scope.
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.
30
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z')%nat : nat_scope.
31
32
33
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
Infix "`div`" := Nat.div (at level 35) : nat_scope.
Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
Infix "`max`" := Nat.max (at level 35) : nat_scope.
Infix "`min`" := Nat.min (at level 35) : nat_scope.
38

39
40
41
42
43
Global Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
Global Instance nat_le_dec: RelDecision le := le_dec.
Global Instance nat_lt_dec: RelDecision lt := lt_dec.
Global Instance nat_inhabited: Inhabited nat := populate 0%nat.
Global Instance S_inj: Inj (=) (=) S.
44
Proof. by injection 1. Qed.
45
Global Instance nat_le_po: PartialOrder ().
46
Proof. repeat split; repeat intro; auto with lia. Qed.
47
Global Instance nat_le_total: Total ().
48
Proof. repeat intro; lia. Qed.
49

50
Global Instance nat_le_pi:  x y : nat, ProofIrrel (x  y).
51
52
53
Proof.
  assert ( x y (p : x  y) y' (q : x  y'),
    y = y'  eq_dep nat (le x) y p y' q) as aux.
54
  { fix FIX 3. intros x ? [|y p] ? [|y' q].
55
    - done.
56
57
58
    - clear FIX. intros; exfalso; auto with lia.
    - clear FIX. intros; exfalso; auto with lia.
    - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
59
  intros x y p q.
60
  by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
61
Qed.
62
Global Instance nat_lt_pi:  x y : nat, ProofIrrel (x < y).
63
Proof. unfold lt. apply _. Qed.
64

Robbert Krebbers's avatar
Robbert Krebbers committed
65
Lemma nat_le_sum (x y : nat) : x  y   z, y = x + z.
66
Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67

68
69
70
Lemma Nat_lt_succ_succ n : n < S (S n).
Proof. auto with arith. Qed.
Lemma Nat_mul_split_l n x1 x2 y1 y2 :
71
72
  x2 < n  y2 < n  x1 * n + x2 = y1 * n + y2  x1 = y1  x2 = y2.
Proof.
73
  intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
74
75
  revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
Qed.
76
77
78
Lemma Nat_mul_split_r n x1 x2 y1 y2 :
  x1 < n  y1 < n  x1 + x2 * n = y1 + y2 * n  x1 = y1  x2 = y2.
Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
79

80
81
82
Notation lcm := Nat.lcm.
Notation divide := Nat.divide.
Notation "( x | y )" := (divide x y) : nat_scope.
83
Global Instance Nat_divide_dec : RelDecision Nat.divide.
84
Proof.
85
  refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
86
Defined.
87
Global Instance: PartialOrder divide.
88
89
90
Proof.
  repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
Qed.
91
Global Hint Extern 0 (_ | _) => reflexivity : core.
92
93
94
Lemma Nat_divide_ne_0 x y : (x | y)  y  0  x  0.
Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.

95
96
97
Lemma Nat_iter_S {A} n (f: A  A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
Proof. done. Qed.
Lemma Nat_iter_S_r {A} n (f: A  A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
100
101
Proof. induction n; by f_equal/=. Qed.
Lemma Nat_iter_add {A} n1 n2 (f : A  A) x :
  Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
Proof. induction n1; by f_equal/=. Qed.
Ralf Jung's avatar
Ralf Jung committed
102
103
104
105
106
107
Lemma Nat_iter_mul {A} n1 n2 (f : A  A) x :
  Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x.
Proof.
  intros. induction n1 as [|n1 IHn1]; [done|].
  simpl. by rewrite Nat_iter_add, IHn1.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
108

Robbert Krebbers's avatar
Robbert Krebbers committed
109
Lemma Nat_iter_ind {A} (P : A  Prop) f x k :
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
  P x  ( y, P y  P (f y))  P (Nat.iter k f x).
Proof. induction k; simpl; auto. Qed.
112

Michael Sammler's avatar
Michael Sammler committed
113

114
(** * Notations and properties of [positive] *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
115
Local Open Scope positive_scope.
116

117
118
119
Typeclasses Opaque Pos.le.
Typeclasses Opaque Pos.lt.

120
Infix "≤" := Pos.le : positive_scope.
121
122
123
124
Notation "x ≤ y ≤ z" := (x  y  y  z) : positive_scope.
Notation "x ≤ y < z" := (x  y  y < z) : positive_scope.
Notation "x < y ≤ z" := (x < y  y  z) : positive_scope.
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : positive_scope.
125
126
Notation "(≤)" := Pos.le (only parsing) : positive_scope.
Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

130
131
Global Arguments Pos.of_nat : simpl never.
Global Arguments Pmult : simpl never.
132

133
134
Global Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
Global Instance positive_le_dec: RelDecision Pos.le.
135
Proof. refine (λ x y, decide ((x ?= y)  Gt)). Defined.
136
Global Instance positive_lt_dec: RelDecision Pos.lt.
137
Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
138
Global Instance positive_le_total: Total Pos.le.
139
140
Proof. repeat intro; lia. Qed.

141
Global Instance positive_inhabited: Inhabited positive := populate 1.
142

143
144
145
Global Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
Global Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
Global Instance xO_inj : Inj (=) (=) (~0).
Robbert Krebbers's avatar
Robbert Krebbers committed
146
Proof. by injection 1. Qed.
147
Global Instance xI_inj : Inj (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
Proof. by injection 1. Qed.

150
151
152
153
154
155
156
157
158
159
160
(** 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.
161
162
Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope.
Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
163
164
165
166
167
168
169
170
171

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.

Robbert Krebbers's avatar
Robbert Krebbers committed
172
Global Instance Papp_1_l : LeftId (=) 1 (++).
173
Proof. intros p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Global Instance Papp_1_r : RightId (=) 1 (++).
175
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Global Instance Papp_assoc : Assoc (=) (++).
177
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
178
Global Instance Papp_inj p : Inj (=) (=) (.++ p).
Robbert Krebbers's avatar
Robbert Krebbers committed
179
Proof. intros ???. induction p; simplify_eq; auto. Qed.
180
181
182
183

Lemma Preverse_go_app p1 p2 p3 :
  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
Proof.
184
185
186
187
  revert p3 p1 p2.
  cut ( p1 p2 p3, Preverse_go (p2 ++ p3) p1 = p2 ++ Preverse_go p3 p1).
  { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
  intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
188
189
  - apply (IH _ (_~1)).
  - apply (IH _ (_~0)).
190
Qed.
191
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
192
193
194
195
196
197
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).

198
199
200
201
202
203
204
205
Lemma Preverse_involutive p :
  Preverse (Preverse p) = p.
Proof.
  induction p as [p IH|p IH|]; simpl.
  - by rewrite Preverse_xI, Preverse_app, IH.
  - by rewrite Preverse_xO, Preverse_app, IH.
  - reflexivity.
Qed.
Michael Sammler's avatar
Michael Sammler committed
206

207
Global Instance Preverse_inj : Inj (=) (=) Preverse.
208
209
210
211
212
213
214
Proof.
  intros p q eq.
  rewrite <- (Preverse_involutive p).
  rewrite <- (Preverse_involutive q).
  by rewrite eq.
Qed.

215
Fixpoint Plength (p : positive) : nat :=
216
  match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
217
Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
218
Proof. by induction p2; f_equal/=. Qed.
219

Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
222
223
224
225
226
Lemma Plt_sum (x y : positive) : x < y   z, y = x + z.
Proof.
  split.
  - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
  - intros [z ->]. lia.
Qed.

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
(** Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
    1~1~0~0 -> 1~1~1~0~0~0~0 *)
Fixpoint Pdup (p : positive) : positive :=
  match p with
  | 1 => 1
  | p'~0 => (Pdup p')~0~0
  | p'~1 => (Pdup p')~1~1
  end.

Lemma Pdup_app p q :
  Pdup (p ++ q) = Pdup p ++ Pdup q.
Proof.
  revert p.
  induction q as [p IH|p IH|]; intros q; simpl.
  - by rewrite IH.
  - by rewrite IH.
  - reflexivity.
Qed.

Lemma Pdup_suffix_eq p q s1 s2 :
  s1~1~0 ++ Pdup p = s2~1~0 ++ Pdup q  p = q.
Proof.
  revert q.
  induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=.
  - by rewrite (IH q).
  - by rewrite (IH q).
  - reflexivity.
Qed.

256
Global Instance Pdup_inj : Inj (=) (=) Pdup.
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
Proof.
  intros p q eq.
  apply (Pdup_suffix_eq _ _ 1 1).
  by rewrite eq.
Qed.

Lemma Preverse_Pdup p :
  Preverse (Pdup p) = Pdup (Preverse p).
Proof.
  induction p as [p IH|p IH|]; simpl.
  - rewrite 3!Preverse_xI.
    rewrite (assoc_L (++)).
    rewrite IH.
    rewrite Pdup_app.
    reflexivity.
  - rewrite 3!Preverse_xO.
    rewrite (assoc_L (++)).
    rewrite IH.
    rewrite Pdup_app.
    reflexivity.
  - reflexivity.
Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
280
Local Close Scope positive_scope.
281
282

(** * Notations and properties of [N] *)
283
284
285
Typeclasses Opaque N.le.
Typeclasses Opaque N.lt.

Robbert Krebbers's avatar
Robbert Krebbers committed
286
Infix "≤" := N.le : N_scope.
287
288
289
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.
290
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z')%N : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
Notation "(≤)" := N.le (only parsing) : N_scope.
292
Notation "(<)" := N.lt (only parsing) : N_scope.
293

294
295
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.
296
297
Infix "`max`" := N.max (at level 35) : N_scope.
Infix "`min`" := N.min (at level 35) : N_scope.
298

299
Global Arguments N.add : simpl never.
300

301
Global Instance Npos_inj : Inj (=) (=) Npos.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
Proof. by injection 1. Qed.

304
Global Instance N_eq_dec: EqDecision N := N.eq_dec.
305
Global Program Instance N_le_dec : RelDecision N.le := λ x y,
306
  match N.compare x y with Gt => right _ | _ => left _ end.
307
Solve Obligations with naive_solver.
308
Global Program Instance N_lt_dec : RelDecision N.lt := λ x y,
309
  match N.compare x y with Lt => left _ | _ => right _ end.
310
Solve Obligations with naive_solver.
311
312
Global Instance N_inhabited: Inhabited N := populate 1%N.
Global Instance N_lt_pi x y : ProofIrrel (x < y)%N.
313
314
Proof. unfold N.lt. apply _. Qed.

315
Global Instance N_le_po: PartialOrder ()%N.
316
Proof.
317
  repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
318
Qed.
319
Global Instance N_le_total: Total ()%N.
320
321
Proof. repeat intro; lia. Qed.

322
Global Hint Extern 0 (_  _)%N => reflexivity : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
323

324
(** * Notations and properties of [Z] *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
325
Local Open Scope Z_scope.
326

327
328
329
Typeclasses Opaque Z.le.
Typeclasses Opaque Z.lt.

Robbert Krebbers's avatar
Robbert Krebbers committed
330
Infix "≤" := Z.le : Z_scope.
331
332
333
334
Notation "x ≤ y ≤ z" := (x  y  y  z) : Z_scope.
Notation "x ≤ y < z" := (x  y  y < z) : Z_scope.
Notation "x < y < z" := (x < y  y < z) : Z_scope.
Notation "x < y ≤ z" := (x < y  y  z) : Z_scope.
335
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
Notation "(≤)" := Z.le (only parsing) : Z_scope.
337
Notation "(<)" := Z.lt (only parsing) : Z_scope.
338

Robbert Krebbers's avatar
Robbert Krebbers committed
339
340
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
341
342
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
343
344
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
345
346
Infix "`max`" := Z.max (at level 35) : Z_scope.
Infix "`min`" := Z.min (at level 35) : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
347

348
Global Instance Zpos_inj : Inj (=) (=) Zpos.
349
Proof. by injection 1. Qed.
350
Global Instance Zneg_inj : Inj (=) (=) Zneg.
351
352
Proof. by injection 1. Qed.

353
Global Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
354
355
Proof. intros n1 n2. apply Nat2Z.inj. Qed.

356
357
358
359
360
361
362
Global Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
Global Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
Global Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
Global Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec.
Global Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec.
Global Instance Z_inhabited: Inhabited Z := populate 1.
Global Instance Z_lt_pi x y : ProofIrrel (x < y).
363
364
Proof. unfold Z.lt. apply _. Qed.

365
Global Instance Z_le_po : PartialOrder ().
366
Proof.
367
  repeat split; red; [apply Z.le_refl | apply Z.le_trans | apply Z.le_antisymm].
368
Qed.
369
Global Instance Z_le_total: Total Z.le.
370
Proof. repeat intro; lia. Qed.
371
372
373

Lemma Z_pow_pred_r n m : 0 < m  n * n ^ (Z.pred m) = n ^ m.
Proof.
374
  intros. rewrite <-Z.pow_succ_r, Z.succ_pred; [done|]. by apply Z.lt_le_pred.
375
376
377
378
379
380
Qed.
Lemma Z_quot_range_nonneg k x y : 0  x < k  0 < y  0  x `quot` y < k.
Proof.
  intros [??] ?.
  destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
  destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
381
382
  split; [apply Z.quot_pos; lia|].
  trans x; auto. apply Z.quot_lt; lia.
383
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
384

385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
Global Arguments Z.pred : simpl never.
Global Arguments Z.succ : simpl never.
Global Arguments Z.of_nat : simpl never.
Global Arguments Z.to_nat : simpl never.
Global Arguments Z.mul : simpl never.
Global Arguments Z.add : simpl never.
Global Arguments Z.sub : simpl never.
Global Arguments Z.opp : simpl never.
Global Arguments Z.pow : simpl never.
Global Arguments Z.div : simpl never.
Global Arguments Z.modulo : simpl never.
Global Arguments Z.quot : simpl never.
Global Arguments Z.rem : simpl never.
Global Arguments Z.shiftl : simpl never.
Global Arguments Z.shiftr : simpl never.
Global Arguments Z.gcd : simpl never.
Global Arguments Z.lcm : simpl never.
Global Arguments Z.min : simpl never.
Global Arguments Z.max : simpl never.
Global Arguments Z.lor : simpl never.
Global Arguments Z.land : simpl never.
Global Arguments Z.lxor : simpl never.
Global Arguments Z.lnot : simpl never.
Global Arguments Z.square : simpl never.
Global Arguments Z.abs : simpl never.
410

411
412
413
414
415
Lemma Z_to_nat_neq_0_pos x : Z.to_nat x  0%nat  0 < x.
Proof. by destruct x. Qed.
Lemma Z_to_nat_neq_0_nonneg x : Z.to_nat x  0%nat  0  x.
Proof. by destruct x. Qed.
Lemma Z_mod_pos x y : 0 < y  0  x `mod` y.
416
417
Proof. apply Z.mod_pos_bound. Qed.

418
419
420
421
422
423
Global Hint Resolve Z.lt_le_incl : zpos.
Global Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
Global Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
Global Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
Global Hint Resolve Z_mod_pos Z.div_pos : zpos.
Global Hint Extern 1000 => lia : zpos.
424

Robbert Krebbers's avatar
Robbert Krebbers committed
425
426
Lemma Z_to_nat_nonpos x : x  0  Z.to_nat x = 0%nat.
Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
427
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y).
428
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
429
430
431
  induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|].
  by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,
    Nat2Z.inj_mul, IH by auto with zpos.
432
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
434
435
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m)  (n | m)%nat.
Proof.
  split.
436
  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
Robbert Krebbers's avatar
Robbert Krebbers committed
437
438
439
    destruct (decide (0  i)%Z).
    { by rewrite Z2Nat.inj_mul, Nat2Z.id by lia. }
    by rewrite !Z_to_nat_nonpos by auto using Z.mul_nonpos_nonneg with lia.
440
  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
442
443
444
Qed.
Lemma Z2Nat_divide n m :
  0  n  0  m  (Z.to_nat n | Z.to_nat m)%nat  (n | m).
Proof. intros. by rewrite <-Nat2Z_divide, !Z2Nat.id by done. Qed.
445
Lemma Nat2Z_inj_div x y : Z.of_nat (x `div` y) = (Z.of_nat x) `div` (Z.of_nat y).
446
447
Proof.
  destruct (decide (y = 0%nat)); [by subst; destruct x |].
448
  apply Z.div_unique with (Z.of_nat $ x `mod` y)%nat.
449
450
451
452
  { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
    apply Nat.mod_bound_pos; lia. }
  by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
Qed.
453
Lemma Nat2Z_inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y).
454
455
Proof.
  destruct (decide (y = 0%nat)); [by subst; destruct x |].
456
  apply Z.mod_unique with (Z.of_nat $ x `div` y)%nat.
457
458
459
460
  { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
    apply Nat.mod_bound_pos; lia. }
  by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
Qed.
461
Lemma Z2Nat_inj_div x y :
462
463
464
  0  x  0  y 
  Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat.
Proof.
465
  intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
466
  pose proof (Z.div_pos x y).
467
  apply (inj Z.of_nat). by rewrite Nat2Z_inj_div, !Z2Nat.id by lia.
468
Qed.
469
Lemma Z2Nat_inj_mod x y :
470
471
472
  0  x  0  y 
  Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat.
Proof.
473
  intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
474
  pose proof (Z_mod_pos x y).
475
  apply (inj Z.of_nat). by rewrite Nat2Z_inj_mod, !Z2Nat.id by lia.
476
Qed.
Simon Spies's avatar
Simon Spies committed
477
478
479
480
481
482
Lemma Z_succ_pred_induction y (P : Z  Prop) :
  P y 
  ( x, y  x  P x  P (Z.succ x)) 
  ( x, x  y  P x  P (Z.pred x)) 
  ( x, P x).
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
Michael Sammler's avatar
Michael Sammler committed
483
484
485
486
Lemma Zmod_in_range q a c :
  q * c  a < (q + 1) * c 
  a `mod` c = a - q * c.
Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed.
Simon Spies's avatar
Simon Spies committed
487

488
489
490
491
492
493
494
495
496
Lemma Z_ones_spec n m:
  0  m  0  n 
  Z.testbit (Z.ones n) m = bool_decide (m < n).
Proof.
  intros. case_bool_decide.
  - by rewrite Z.ones_spec_low by lia.
  - by rewrite Z.ones_spec_high by lia.
Qed.

497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
Lemma Z_bounded_iff_bits_nonneg k n :
  0  k  0  n 
  n < 2^k   l, k  l  Z.testbit n l = false.
Proof.
  intros. destruct (decide (n = 0)) as [->|].
  { naive_solver eauto using Z.bits_0, Z.pow_pos_nonneg with lia. }
  split.
  { intros Hb%Z.log2_lt_pow2 l Hl; [|lia]. apply Z.bits_above_log2; lia. }
  intros Hl. apply Z.nle_gt; intros ?.
  assert (Z.testbit n (Z.log2 n) = false) as Hbit.
  { apply Hl, Z.log2_le_pow2; lia. }
  by rewrite Z.bit_log2 in Hbit by lia.
Qed.

(* Goals of the form [0 ≤ n ≤ 2^k] appear often. So we also define the
derived version [Z_bounded_iff_bits_nonneg'] that does not require
proving [0 ≤ n] twice in that case. *)
Lemma Z_bounded_iff_bits_nonneg' k n :
  0  k  0  n 
  0  n < 2^k   l, k  l  Z.testbit n l = false.
Proof. intros ??. rewrite <-Z_bounded_iff_bits_nonneg; lia. Qed.

Lemma Z_bounded_iff_bits k n :
  0  k 
  -2^k  n < 2^k   l, k  l  Z.testbit n l = bool_decide (n < 0).
Proof.
  intros Hk.
  case_bool_decide; [ | rewrite <-Z_bounded_iff_bits_nonneg; lia].
  assert(n = - Z.abs n)%Z as -> by lia.
  split.
  { intros [? _] l Hl.
    rewrite Z.bits_opp, negb_true_iff by lia.
    apply Z_bounded_iff_bits_nonneg with k; lia. }
  intros Hbit. split.
  - rewrite <-Z.opp_le_mono, <-Z.lt_pred_le.
    apply Z_bounded_iff_bits_nonneg; [lia..|]. intros l Hl.
    rewrite <-negb_true_iff, <-Z.bits_opp by lia.
    by apply Hbit.
  - etrans; [|apply Z.pow_pos_nonneg]; lia.
Qed.


Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
539
Local Close Scope Z_scope.
540

541
(** * Injectivity of casts *)
542
543
544
545
546
Global Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
Global Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
Global Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
Global Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
Global Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
547
548
(* Add others here. *)

549
(** * Notations and properties of [Qc] *)
550
551
552
Typeclasses Opaque Qcle.
Typeclasses Opaque Qclt.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
553
Local Open Scope Qc_scope.
554
555
Delimit Scope Qc_scope with Qc.
Notation "1" := (Q2Qc 1) : Qc_scope.
556
Notation "2" := (1+1) : Qc_scope.
557
558
Notation "- 1" := (Qcopp 1) : Qc_scope.
Notation "- 2" := (Qcopp 2) : Qc_scope.
559
Infix "≤" := Qcle : Qc_scope.
560
561
562
563
Notation "x ≤ y ≤ z" := (x  y  y  z) : Qc_scope.
Notation "x ≤ y < z" := (x  y  y < z) : Qc_scope.
Notation "x < y < z" := (x < y  y < z) : Qc_scope.
Notation "x < y ≤ z" := (x < y  y  z) : Qc_scope.
564
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Qc_scope.
565
566
567
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

568
Global Hint Extern 1 (_  _) => reflexivity || discriminate : core.
569
Global Arguments Qred : simpl never.
570

571
572
573
574
Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n.
Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed.
Definition Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n).

575
Global Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
576
Global Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
577
  if Qclt_le_dec y x then right _ else left _.
578
579
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
580
Global Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
581
  if Qclt_le_dec x y then left _ else right _.
Ralf Jung's avatar
Ralf Jung committed
582
Next Obligation. done. Qed.
583
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
584
Global Instance Qc_lt_pi x y : ProofIrrel (x < y).
585
Proof. unfold Qclt. apply _. Qed.
586

587
Global Instance Qc_le_po: PartialOrder ().
588
Proof.
589
  repeat split; red; [apply Qcle_refl | apply Qcle_trans | apply Qcle_antisym].
590
Qed.
591
Global Instance Qc_lt_strict: StrictOrder (<).
592
Proof.
593
594
  split; red; [|apply Qclt_trans].
  intros x Hx. by destruct (Qclt_not_eq x x).
595
Qed.
596
Global Instance Qc_le_total: Total Qcle.
597
598
Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed.

599
600
601
602
Lemma Qcmult_0_l x : 0 * x = 0.
Proof. ring. Qed.
Lemma Qcmult_0_r x : x * 0 = 0.
Proof. ring. Qed.
603
604
Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc.
Proof. ring. Qed.
605
Lemma Qcle_ngt (x y : Qc) : x  y  ¬y < x.
606
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
607
Lemma Qclt_nge (x y : Qc) : x < y  ¬y  x.
608
Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
609
Lemma Qcplus_le_mono_l (x y z : Qc) : x  y  z + x  z + y.
610
611
Proof.
  split; intros.
612
613
  - by apply Qcplus_le_compat.
  - replace x with ((0 - z) + (z + x)) by ring.
614
    replace y with ((0 - z) + (z + y)) by ring.
615
616
    by apply Qcplus_le_compat.
Qed.
617
Lemma Qcplus_le_mono_r (x y z : Qc) : x  y  x + z  y + z.
618
Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
619
Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y  z + x < z + y.
620
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
621
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y  x + z < y + z.
622
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
623
Global Instance Qcopp_inj : Inj (=) (=) Qcopp.
624
625
626
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
627
Global Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
628
Proof.
629
  intros x y H. by apply (anti_symm ());rewrite (Qcplus_le_mono_l _ _ z), H.
630
Qed.
631
Global Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
632
Proof.
633
  intros x y H. by apply (anti_symm ()); rewrite (Qcplus_le_mono_r _ _ z), H.
634
Qed.
635
636
637
638
639
640
Lemma Qcplus_pos_nonneg (x y : Qc) : 0 < x  0  y  0 < x + y.
Proof.
  intros. apply Qclt_le_trans with (x + 0); [by rewrite Qcplus_0_r|].
  by apply Qcplus_le_mono_l.
Qed.
Lemma Qcplus_nonneg_pos (x y : Qc) : 0  x  0 < y  0 < x + y.
Michael Sammler's avatar
Michael Sammler committed
641
Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed.
642
643
644
645
Lemma Qcplus_pos_pos (x y : Qc) : 0 < x  0 < y  0 < x + y.
Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0  x  0  y  0  x + y.
Proof.
646
  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
647
648
649
650
651
652
653
654
655
656
657
658
659
  by apply Qcplus_le_mono_l.
Qed.
Lemma Qcplus_neg_nonpos (x y : Qc) : x < 0  y  0  x + y < 0.
Proof.
  intros. apply Qcle_lt_trans with (x + 0); [|by rewrite Qcplus_0_r].
  by apply Qcplus_le_mono_l.
Qed.
Lemma Qcplus_nonpos_neg (x y : Qc) : x  0  y < 0  x + y < 0.
Proof. rewrite (Qcplus_comm x). auto using Qcplus_neg_nonpos. Qed.
Lemma Qcplus_neg_neg (x y : Qc) : x < 0  y < 0  x + y < 0.
Proof. auto using Qcplus_nonpos_neg, Qclt_le_weak. Qed.
Lemma Qcplus_nonpos_nonpos (x y : Qc) : x  0  y  0  x + y  0.
Proof.
660
  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
661
662
  by apply Qcplus_le_mono_l.
Qed.
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
Lemma Qcmult_le_mono_nonneg_l x y z : 0  z  x  y  z * x  z * y.
Proof. intros. rewrite !(Qcmult_comm z). by apply Qcmult_le_compat_r. Qed.
Lemma Qcmult_le_mono_nonneg_r x y z : 0  z  x  y  x * z  y * z.
Proof. intros. by apply Qcmult_le_compat_r. Qed.
Lemma Qcmult_le_mono_pos_l x y z : 0 < z  x  y  z * x  z * y.
Proof.
  split; auto using Qcmult_le_mono_nonneg_l, Qclt_le_weak.
  rewrite !Qcle_ngt, !(Qcmult_comm z).
  intuition auto using Qcmult_lt_compat_r.
Qed.
Lemma Qcmult_le_mono_pos_r x y z : 0 < z  x  y  x * z  y * z.
Proof. rewrite !(Qcmult_comm _ z). by apply Qcmult_le_mono_pos_l. Qed.
Lemma Qcmult_lt_mono_pos_l x y z : 0 < z  x < y  z * x < z * y.
Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_l. Qed.
Lemma Qcmult_lt_mono_pos_r x y z : 0 < z  x < y  x * z < y * z.
Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_r. Qed.
Lemma Qcmult_pos_pos x y : 0 < x  0 < y  0 < x * y.
Proof.
  intros. apply Qcle_lt_trans with (0 * y); [by rewrite Qcmult_0_l|].
  by apply Qcmult_lt_mono_pos_r.
Qed.
Lemma Qcmult_nonneg_nonneg x y : 0  x  0  y  0  x * y.
Proof.
686
  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
687
688
689
  by apply Qcmult_le_mono_nonneg_r.
Qed.

690
691
692
693
694
695
Lemma Qcinv_pos x : 0 < x  0 < /x.
Proof.
  intros. assert (0  x) by (by apply Qclt_not_eq).
  by rewrite (Qcmult_lt_mono_pos_r _ _ x), Qcmult_0_l, Qcmult_inv_l by done.
Qed.

696
697
Lemma Z2Qc_inj_0 : Qc_of_Z 0 = 0.
Proof. by apply Qc_is_canon. Qed.
698
699
700
701
Lemma Z2Qc_inj_1 : Qc_of_Z 1 = 1.
Proof. by apply Qc_is_canon. Qed.
Lemma Z2Qc_inj_2 : Qc_of_Z 2 = 2.
Proof. by apply Qc_is_canon. Qed.
702
703
704
Lemma Z2Qc_inj n m : Qc_of_Z n = Qc_of_Z m  n = m.
Proof. by injection 1. Qed.
Lemma Z2Qc_inj_iff n m : Qc_of_Z n = Qc_of_Z m  n = m.
705
Proof. split; [ auto using Z2Qc_inj | by intros -> ]. Qed.
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
Lemma Z2Qc_inj_le n m : (n  m)%Z  Qc_of_Z n  Qc_of_Z m.
Proof. by rewrite Zle_Qle. Qed.
Lemma Z2Qc_inj_lt n m : (n < m)%Z  Qc_of_Z n < Qc_of_Z m.
Proof. by rewrite Zlt_Qlt. Qed.
Lemma Z2Qc_inj_add n m : Qc_of_Z (n + m) = Qc_of_Z n + Qc_of_Z m.
Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_plus. Qed.
Lemma Z2Qc_inj_mul n m : Qc_of_Z (n * m) = Qc_of_Z n * Qc_of_Z m.
Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_mult. Qed.
Lemma Z2Qc_inj_opp n : Qc_of_Z (-n) = -Qc_of_Z n.
Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_opp. Qed.
Lemma Z2Qc_inj_sub n m : Qc_of_Z (n - m) = Qc_of_Z n - Qc_of_Z m.
Proof.
  apply Qc_is_canon; simpl.
  by rewrite !Qred_correct, <-inject_Z_opp, <-inject_Z_plus.
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
721
Local Close Scope Qc_scope.
722
723

(** * Positive rationals *)
Ralf Jung's avatar
Ralf Jung committed
724
725
726
Declare Scope Qp_scope.
Delimit Scope Qp_scope with Qp.

727
728
Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }.
Add Printing Constructor Qp.
Ralf Jung's avatar
Ralf Jung committed
729
Bind Scope Qp_scope with Qp.
730
Global Arguments Qp_to_Qc _%Qp : assert.
731

Simon Friis Vindum's avatar
Simon Friis Vindum committed
732
733
Local Open Scope Qp_scope.

734
735
736
737
738
Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q  p = q.
Proof.
  split; [|by intros ->].
  destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
Qed.
739
Global Instance Qp_eq_dec : EqDecision Qp.
740
741
742
743
744
Proof.
  refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
    by rewrite <-Qp_to_Qc_inj_iff.
Defined.

745
Definition Qp_add (p q : Qp) : Qp :=
746
747
  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
  mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq).
748
Global Arguments Qp_add : simpl never.
749

750
Definition Qp_sub (p q : Qp) : option Qp :=
751
752
753
  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
  let pq := (p - q)%Qc in
  guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq).
754
Global Arguments Qp_sub : simpl never.
755

756
Definition Qp_mul (p q : Qp) : Qp :=
757
758
  let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
  mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq).
759
Global Arguments Qp_mul : simpl never.
760

761
762
763
Definition Qp_inv (q : Qp) : Qp :=
  let 'mk_Qp q Hq := q return _ in
  mk_Qp (/ q)%Qc (Qcinv_pos _ Hq).
764
Global Arguments Qp_inv : simpl never.
765

766
Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q).
767
Typeclasses Opaque Qp_div.
768
Global Arguments Qp_div : simpl never.
Simon Friis Vindum's avatar
Simon Friis Vindum committed
769

770
771
772
Infix "+" := Qp_add : Qp_scope.
Infix "-" := Qp_sub : Qp_scope.
Infix "*" := Qp_mul : Qp_scope.
773
Notation "/ q" := (Qp_inv q) : Qp_scope.
774
Infix "/"