numbers.v 23.4 KB
Newer Older
1
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
(* This file is distributed under the terms of the BSD license. *)
(** 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. *)
6
From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
7
From Coq Require Import QArith Qcanon.
8
From iris.prelude Require Export base decidable option.
9
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12
Open Scope nat_scope.

Coercion Z.of_nat : nat >-> Z.
13
Instance comparison_eq_dec : EqDecision comparison.
14
Proof. solve_decision. Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

(** * Notations and properties of [nat] *)
Arguments minus !_ !_ /.
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).
Reserved Notation "x ≤ y ≤ z ≤ z'"
  (at level 70, y at next level, z at next level).

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

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
38

39
Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
Instance nat_le_dec:  x y : nat, Decision (x  y) := le_dec.
Instance nat_lt_dec:  x y : nat, Decision (x < y) := lt_dec.
Instance nat_inhabited: Inhabited nat := populate 0%nat.
43
Instance S_inj: Inj (=) (=) S.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Proof. by injection 1. Qed.
45
Instance nat_le_po: PartialOrder ().
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
49
50
51
52
Proof. repeat split; repeat intro; auto with lia. Qed.

Instance nat_le_pi:  x y : nat, ProofIrrel (x  y).
Proof.
  assert ( x y (p : x  y) y' (q : x  y'),
    y = y'  eq_dep nat (le x) y p y' q) as aux.
  { fix 3. intros x ? [|y p] ? [|y' q].
53
54
55
56
    - done.
    - clear nat_le_pi. intros; exfalso; auto with lia.
    - clear nat_le_pi. intros; exfalso; auto with lia.
    - injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  intros x y p q.
58
  by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Qed.
Instance nat_lt_pi:  x y : nat, ProofIrrel (x < y).
Proof. apply _. Qed.

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).

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 :
  x2 < n  y2 < n  x1 * n + x2 = y1 * n + y2  x1 = y1  x2 = y2.
Proof.
  intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
  revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
Qed.
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.

Notation lcm := Nat.lcm.
Notation divide := Nat.divide.
Notation "( x | y )" := (divide x y) : nat_scope.
86
Instance Nat_divide_dec x y : Decision (x | y).
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
89
90
91
92
93
94
95
96
97
Proof.
  refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
Defined.
Instance: PartialOrder divide.
Proof.
  repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
Qed.
Hint Extern 0 (_ | _) => reflexivity.
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.

98
99
100
101
102
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).
Proof. induction n; f_equal/=; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
106
107
108
109
110
111
112
113
114
115
116
(** * Notations and properties of [positive] *)
Open Scope positive_scope.

Infix "≤" := Pos.le : 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" := (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.
Notation "(≤)" := Pos.le (only parsing) : positive_scope.
Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

117
118
119
Arguments Pos.of_nat : simpl never.
Arguments Pmult : simpl never.

120
Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
Instance positive_inhabited: Inhabited positive := populate 1.

123
124
Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
Instance maybe_x1 : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
125
Instance: Inj (=) (=) (~0).
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Proof. by injection 1. Qed.
127
Instance: Inj (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Proof. by injection 1. Qed.

(** 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 (++).
153
Proof. intros p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
Global Instance: RightId (=) 1 (++).
Proof. done. Qed.
156
Global Instance: Assoc (=) (++).
157
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
158
Global Instance:  p : positive, Inj (=) (=) (++ p).
159
Proof. intros p ???. induction p; simplify_eq; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
162
163

Lemma Preverse_go_app p1 p2 p3 :
  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
Proof.
164
165
166
167
  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.
168
169
  - apply (IH _ (_~1)).
  - apply (IH _ (_~0)).
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Qed.
171
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
175
176
177
178
179
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.
180
Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
181
Proof. by induction p2; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198

Close Scope positive_scope.

(** * Notations and properties of [N] *)
Infix "≤" := N.le : 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.
Notation "x < y ≤ z" := (x < y  y  z)%N : N_scope.
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z')%N : N_scope.
Notation "(≤)" := N.le (only parsing) : N_scope.
Notation "(<)" := N.lt (only parsing) : N_scope.
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.

Arguments N.add _ _ : simpl never.

199
Instance: Inj (=) (=) Npos.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
201
Proof. by injection 1. Qed.

202
Instance N_eq_dec: EqDecision N := N.eq_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
Program Instance N_le_dec (x y : N) : Decision (x  y)%N :=
204
205
  match Ncompare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
207
208
  match Ncompare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
Instance N_inhabited: Inhabited N := populate 1%N.
210
Instance N_le_po: PartialOrder ()%N.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
Proof.
  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
Qed.
Hint Extern 0 (_  _)%N => reflexivity.

(** * Notations and properties of [Z] *)
Open Scope Z_scope.

Infix "≤" := Z.le : 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.
Notation "x < y ≤ z" := (x < y  y  z) : Z_scope.
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
Notation "(<)" := Z.lt (only parsing) : Z_scope.

Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.

235
Instance Zpos_inj : Inj (=) (=) Zpos.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
Proof. by injection 1. Qed.
237
Instance Zneg_inj : Inj (=) (=) Zneg.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
239
Proof. by injection 1. Qed.

240
241
242
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.

243
Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
245
246
Instance Z_le_dec:  x y : Z, Decision (x  y) := Z_le_dec.
Instance Z_lt_dec:  x y : Z, Decision (x < y) := Z_lt_dec.
Instance Z_inhabited: Inhabited Z := populate 1.
247
Instance Z_le_po : PartialOrder ().
Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
250
251
252
253
254
255
256
257
258
259
260
Proof.
  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.

Lemma Z_pow_pred_r n m : 0 < m  n * n ^ (Z.pred m) = n ^ m.
Proof.
  intros. rewrite <-Z.pow_succ_r, Z.succ_pred. done. by apply Z.lt_le_pred.
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 |].
261
  split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Qed.

(* Note that we cannot disable simpl for [Z.of_nat] as that would break
tactics as [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.

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.
Proof. apply Z.mod_pos_bound. Qed.

Hint Resolve Z.lt_le_incl : zpos.
Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
Hint Resolve Z_mod_pos Z.div_pos : zpos.
Hint Extern 1000 => lia : zpos.

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.
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
Proof.
  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.
Qed.
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m)  (n | m)%nat.
Proof.
  split.
301
  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
304
    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.
305
  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
346
347
348
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.
Lemma Z2Nat_inj_div x y : Z.of_nat (x `div` y) = x `div` y.
Proof.
  destruct (decide (y = 0%nat)); [by subst; destruct x |].
  apply Z.div_unique with (x `mod` y)%nat.
  { 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.
Lemma Z2Nat_inj_mod x y : Z.of_nat (x `mod` y) = x `mod` y.
Proof.
  destruct (decide (y = 0%nat)); [by subst; destruct x |].
  apply Z.mod_unique with (x `div` y)%nat.
  { 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.
Close Scope Z_scope.

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

Hint Extern 1 (_  _) => reflexivity || discriminate.
Arguments Qred _ : simpl never.

349
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
351
Program Instance Qc_le_dec (x y : Qc) : Decision (x  y) :=
  if Qclt_le_dec y x then right _ else left _.
352
353
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y) :=
  if Qclt_le_dec x y then left _ else right _.
356
357
Solve Obligations with done.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
360
361
362
363
364
365
366
367
368
369
370

Instance: PartialOrder ().
Proof.
  repeat split; red. apply Qcle_refl. apply Qcle_trans. apply Qcle_antisym.
Qed.
Instance: StrictOrder (<).
Proof.
  split; red. intros x Hx. by destruct (Qclt_not_eq x x). apply Qclt_trans.
Qed.
Lemma Qcmult_0_l x : 0 * x = 0.
Proof. ring. Qed.
Lemma Qcmult_0_r x : x * 0 = 0.
Proof. ring. Qed.
371
372
Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc.
Proof. ring. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
374
375
376
377
378
379
Lemma Qcle_ngt (x y : Qc) : x  y  ¬y < x.
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
Lemma Qclt_nge (x y : Qc) : x < y  ¬y  x.
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.
Proof.
  split; intros.
380
381
  - by apply Qcplus_le_compat.
  - replace x with ((0 - z) + (z + x)) by ring.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
384
385
386
387
388
389
390
    replace y with ((0 - z) + (z + y)) by ring.
    by apply Qcplus_le_compat.
Qed.
Lemma Qcplus_le_mono_r (x y z : Qc) : x  y  x + z  y + z.
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.
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.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
391
Instance: Inj (=) (=) Qcopp.
Robbert Krebbers's avatar
Robbert Krebbers committed
392
393
394
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
395
Instance:  z, Inj (=) (=) (Qcplus z).
Robbert Krebbers's avatar
Robbert Krebbers committed
396
Proof.
397
  intros z x y H. by apply (anti_symm ());
Robbert Krebbers's avatar
Robbert Krebbers committed
398
399
    rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
400
Instance:  z, Inj (=) (=) (λ x, x + z).
Robbert Krebbers's avatar
Robbert Krebbers committed
401
Proof.
402
  intros z x y H. by apply (anti_symm ());
Robbert Krebbers's avatar
Robbert Krebbers committed
403
404
405
406
407
408
409
410
411
412
413
414
415
    rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
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.
Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed. 
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.
416
  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
Robbert Krebbers's avatar
Robbert Krebbers committed
417
418
419
420
421
422
423
424
425
426
427
428
429
  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.
430
  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
Robbert Krebbers's avatar
Robbert Krebbers committed
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
  by apply Qcplus_le_mono_l.
Qed.
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.
456
  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
459
460
461
462
463
464
  by apply Qcmult_le_mono_nonneg_r.
Qed.

Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n.
Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed.
Coercion Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n).
Lemma Z2Qc_inj_0 : Qc_of_Z 0 = 0.
Proof. by apply Qc_is_canon. Qed.
465
466
467
468
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
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.
Proof. split. auto using Z2Qc_inj. by intros ->. Qed.
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.
Close Scope Qc_scope.
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504

(** * Positive rationals *)
(** The theory of positive rationals is very incomplete. We merely provide
some operations and theorems that are relevant for fractional permissions. *)
Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
Hint Resolve Qp_prf.
Delimit Scope Qp_scope with Qp.
Bind Scope Qp_scope with Qp.
Arguments Qp_car _%Qp.

Definition Qp_one : Qp := mk_Qp 1 eq_refl.
Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _.
Next Obligation. by intros x y; apply Qcplus_pos_pos. Qed.
Definition Qp_minus (x y : Qp) : option Qp :=
  let z := (x - y)%Qc in
  match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end.
505
506
Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _.
Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed.
507
508
509
510
511
512
513
514
515
516
517
Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / ('y)%Z) _.  
Next Obligation.
  intros x y. assert (0 < ('y)%Z)%Qc.
  { apply (Z2Qc_inj_lt 0%Z (' y)), Pos2Z.is_pos. }
  by rewrite (Qcmult_lt_mono_pos_r _ _ ('y)%Z), Qcmult_0_l,
    <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed.

Notation "1" := Qp_one : Qp_scope.
Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
518
Infix "*" := Qp_mult : Qp_scope.
519
520
521
522
523
524
525
Infix "/" := Qp_div : Qp_scope.

Lemma Qp_eq x y : x = y  Qp_car x = Qp_car y.
Proof.
  split; [by intros ->|].
  destruct x, y; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
527
528
529
530
531
532

Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
Instance Qp_eq_dec : EqDecision Qp.
Proof.
 refine (λ x y, cast_if (decide (Qp_car x = Qp_car y))); by rewrite Qp_eq.
Defined.

533
534
535
536
537
538
539
540
541
542
543
544
545
546
Instance Qp_plus_assoc : Assoc (=) Qp_plus.
Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
Instance Qp_plus_comm : Comm (=) Qp_plus.
Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.

Lemma Qp_minus_diag x : (x - x)%Qp = None.
Proof. unfold Qp_minus. by rewrite Qcplus_opp_r. Qed.
Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y.
Proof.
  unfold Qp_minus; simpl.
  rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r.
  destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq.
Qed.

547
548
549
550
551
552
553
554
555
556
557
558
559
Instance Qp_mult_assoc : Assoc (=) Qp_mult.
Proof. intros x y z; apply Qp_eq, Qcmult_assoc. Qed.
Instance Qp_mult_comm : Comm (=) Qp_mult.
Proof. intros x y; apply Qp_eq, Qcmult_comm. Qed.
Lemma Qp_mult_plus_distr_r x y z: (x * (y + z) = x * y + x * z)%Qp.
Proof. apply Qp_eq, Qcmult_plus_distr_r. Qed.
Lemma Qp_mult_plus_distr_l x y z: ((x + y) * z = x * z + y * z)%Qp.
Proof. apply Qp_eq, Qcmult_plus_distr_l. Qed.
Lemma Qp_mult_1_l x: (1 * x)%Qp = x.
Proof. apply Qp_eq, Qcmult_1_l. Qed.
Lemma Qp_mult_1_r x: (x * 1)%Qp = x.
Proof. apply Qp_eq, Qcmult_1_r. Qed.

560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
Lemma Qp_div_1 x : (x / 1 = x)%Qp.
Proof.
  apply Qp_eq; simpl.
  rewrite <-(Qcmult_div_r x 1) at 2 by done. by rewrite Qcmult_1_l.
Qed.
Lemma Qp_div_S x y : (x / (2 * y) + x / (2 * y) = x / y)%Qp.
Proof.
  apply Qp_eq; simpl.
  rewrite <-Qcmult_plus_distr_l, Pos2Z.inj_mul, Z2Qc_inj_mul, Z2Qc_inj_2.
  rewrite Qcplus_diag. by field_simplify.
Qed.
Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp.
Proof.
  change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1.
Qed.
575

576
577
578
579
580
581
582
583
584
585
586
587
588
589
Lemma Qp_lower_bound q1 q2 :  q q1' q2', (q1 = q + q1'  q2 = q + q2')%Qp.
Proof.
  revert q1 q2. cut ( q1 q2 : Qp, (q1  q2)%Qc 
     q q1' q2', (q1 = q + q1'  q2 = q + q2')%Qp).
  { intros help q1 q2.
    destruct (Qc_le_dec q1 q2) as [LE|LE%Qclt_nge%Qclt_le_weak]; [by eauto|].
    destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto. }
  intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
  assert (0 < q2 - q1 / 2)%Qc as Hq2'.
  { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq].
    replace (q1 - q1 / 2)%Qc with (q1 * (1 - 1/2))%Qc by ring.
    replace 0%Qc with (0 * (1-1/2))%Qc by ring. by apply Qcmult_lt_compat_r. }
  exists (mk_Qp (q2 - q1 / 2%Z) Hq2'). split; [by rewrite Qp_div_2|].
  apply Qp_eq; simpl. ring.
590
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
591

Zhen Zhang's avatar
Zhen Zhang committed
592
Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
Zhen Zhang's avatar
Zhen Zhang committed
593
594
595
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
Zhen Zhang's avatar
Zhen Zhang committed
596
  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
Zhen Zhang's avatar
Zhen Zhang committed
597
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
598
599
600

Lemma Qp_ge_0 (q: Qp): (0  q)%Qc.
Proof. apply Qclt_le_weak, Qp_prf. Qed.