numbers.v 23.4 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, 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. *)
6
From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
7 8
From Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option.
9
Set Default Proof Using "Type*".
10
Open Scope nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12
Coercion Z.of_nat : nat >-> Z.
13
Instance comparison_eq_dec : EqDecision comparison.
14
Proof. solve_decision. Defined.
15

16
(** * Notations and properties of [nat] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Arguments minus !_ !_ /.
18 19 20 21
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).
22 23
Reserved Notation "x ≤ y ≤ z ≤ z'"
  (at level 70, y at next level, z at next level).
24

25
Infix "≤" := le : nat_scope.
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.
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
Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
40 41
Instance nat_le_dec:  x y : nat, Decision (x  y) := le_dec.
Instance nat_lt_dec:  x y : nat, Decision (x < y) := lt_dec.
42
Instance nat_inhabited: Inhabited nat := populate 0%nat.
43
Instance S_inj: Inj (=) (=) S.
44
Proof. by injection 1. Qed.
45
Instance nat_le_po: PartialOrder ().
46
Proof. repeat split; repeat intro; auto with lia. Qed.
47

48 49 50 51 52
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). }
57
  intros x y p q.
58
  by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
59 60 61 62
Qed.
Instance nat_lt_pi:  x y : nat, ProofIrrel (x < y).
Proof. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65 66 67 68 69 70
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).

71 72 73
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 :
74 75
  x2 < n  y2 < n  x1 * n + x2 = y1 * n + y2  x1 = y1  x2 = y2.
Proof.
76
  intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
77 78
  revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
Qed.
79 80 81
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.
82

83 84 85
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).
87 88 89
Proof.
  refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
Defined.
90 91 92 93 94 95 96 97
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.

103 104 105
(** * Notations and properties of [positive] *)
Open Scope positive_scope.

106
Infix "≤" := Pos.le : positive_scope.
107 108 109 110 111
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.
112 113
Notation "(≤)" := Pos.le (only parsing) : positive_scope.
Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116
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.
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
Proof. by injection 1. Qed.

130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
(** 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.
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.
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)).
170
Qed.
171
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
172 173 174 175 176 177 178
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 :=
179
  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.
182 183 184 185

Close Scope positive_scope.

(** * Notations and properties of [N] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
186
Infix "≤" := N.le : N_scope.
187 188 189 190
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.
191
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z')%N : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
Notation "(≤)" := N.le (only parsing) : N_scope.
193
Notation "(<)" := N.lt (only parsing) : N_scope.
194 195 196
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.

197 198
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.
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.
209
Instance N_inhabited: Inhabited N := populate 1%N.
210
Instance N_le_po: PartialOrder ()%N.
211 212 213 214
Proof.
  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
Qed.
Hint Extern 0 (_  _)%N => reflexivity.
Robbert Krebbers's avatar
Robbert Krebbers committed
215

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

Robbert Krebbers's avatar
Robbert Krebbers committed
219
Infix "≤" := Z.le : Z_scope.
220 221 222 223
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.
224
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Notation "(≤)" := Z.le (only parsing) : Z_scope.
226
Notation "(<)" := Z.lt (only parsing) : Z_scope.
227

Robbert Krebbers's avatar
Robbert Krebbers committed
228 229
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
230 231
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
232 233
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
234

235
Instance Zpos_inj : Inj (=) (=) Zpos.
236
Proof. by injection 1. Qed.
237
Instance Zneg_inj : Inj (=) (=) Zneg.
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.
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 ().
248 249 250
Proof.
  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
251 252 253 254 255 256 257 258 259 260

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.
262
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
263

264
(* Note that we cannot disable simpl for [Z.of_nat] as that would break
265
tactics as [lia]. *)
266 267 268 269 270 271 272 273 274 275
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.

276 277 278 279 280
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.
281 282 283 284 285
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.
286 287
Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
Hint Resolve Z_mod_pos Z.div_pos : zpos.
288 289
Hint Extern 1000 => lia : zpos.

Robbert Krebbers's avatar
Robbert Krebbers committed
290 291
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.
292 293
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295 296
  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.
297
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298 299 300
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
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.
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327
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.

328
(** * Notations and properties of [Qc] *)
329
Open Scope Qc_scope.
330 331
Delimit Scope Qc_scope with Qc.
Notation "1" := (Q2Qc 1) : Qc_scope.
332
Notation "2" := (1+1) : Qc_scope.
333 334 335 336
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.
337
Infix "≤" := Qcle : Qc_scope.
338 339 340 341
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.
342
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Qc_scope.
343 344 345
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

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

349
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
350
Program Instance Qc_le_dec (x y : Qc) : Decision (x  y) :=
351
  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.
354
Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y) :=
355
  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.
358

359 360 361 362 363 364 365 366
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.
367 368 369 370
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.
373
Lemma Qcle_ngt (x y : Qc) : x  y  ¬y < x.
374
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
375
Lemma Qclt_nge (x y : Qc) : x < y  ¬y  x.
376
Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
377
Lemma Qcplus_le_mono_l (x y z : Qc) : x  y  z + x  z + y.
378 379
Proof.
  split; intros.
380 381
  - by apply Qcplus_le_compat.
  - replace x with ((0 - z) + (z + x)) by ring.
382
    replace y with ((0 - z) + (z + y)) by ring.
383 384
    by apply Qcplus_le_compat.
Qed.
385
Lemma Qcplus_le_mono_r (x y z : Qc) : x  y  x + z  y + z.
386
Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
387
Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y  z + x < z + y.
388
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
389
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y  x + z < y + z.
390
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
391
Instance: Inj (=) (=) Qcopp.
392 393 394
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
395
Instance:  z, Inj (=) (=) (Qcplus z).
396
Proof.
397
  intros z x y H. by apply (anti_symm ());
398 399
    rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
400
Instance:  z, Inj (=) (=) (λ x, x + z).
401
Proof.
402
  intros z x y H. by apply (anti_symm ());
403 404
    rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
405 406 407 408 409 410 411 412 413 414 415
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|].
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].
431 432
  by apply Qcplus_le_mono_l.
Qed.
433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455
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|].
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.
469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487
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.
488
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.