numbers.v 22.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
Open Scope nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
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
35 36
Infix "`max`" := Nat.max (at level 35) : nat_scope.
Infix "`min`" := Nat.min (at level 35) : nat_scope.
37

38
Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
39 40
Instance nat_le_dec:  x y : nat, Decision (x  y) := le_dec.
Instance nat_lt_dec:  x y : nat, Decision (x < y) := lt_dec.
41
Instance nat_inhabited: Inhabited nat := populate 0%nat.
42
Instance S_inj: Inj (=) (=) S.
43
Proof. by injection 1. Qed.
44
Instance nat_le_po: PartialOrder ().
45
Proof. repeat split; repeat intro; auto with lia. Qed.
46

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

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

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

82 83 84
Notation lcm := Nat.lcm.
Notation divide := Nat.divide.
Notation "( x | y )" := (divide x y) : nat_scope.
85
Instance Nat_divide_dec x y : Decision (x | y).
86 87 88
Proof.
  refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
Defined.
89 90 91 92 93 94 95 96
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.

97 98 99 100 101
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.

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

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

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

119
Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
120 121
Instance positive_inhabited: Inhabited positive := populate 1.

122 123
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.
124
Instance: Inj (=) (=) (~0).
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Proof. by injection 1. Qed.
126
Instance: Inj (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128
Proof. by injection 1. Qed.

129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
(** 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 (++).
152
Proof. intros p. by induction p; intros; f_equal/=. Qed.
153 154
Global Instance: RightId (=) 1 (++).
Proof. done. Qed.
155
Global Instance: Assoc (=) (++).
156
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
157
Global Instance:  p : positive, Inj (=) (=) (++ p).
158
Proof. intros p ???. induction p; simplify_eq; auto. Qed.
159 160 161 162

Lemma Preverse_go_app p1 p2 p3 :
  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
Proof.
163 164 165 166
  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.
167 168
  - apply (IH _ (_~1)).
  - apply (IH _ (_~0)).
169
Qed.
170
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
171 172 173 174 175 176 177
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 :=
178
  match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
179
Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
180
Proof. by induction p2; f_equal/=. Qed.
181 182 183 184

Close Scope positive_scope.

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

196 197
Arguments N.add _ _ : simpl never.

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

201
Instance N_eq_dec: EqDecision N := N.eq_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
Program Instance N_le_dec (x y : N) : Decision (x  y)%N :=
203 204
  match Ncompare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
205
Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
206 207
  match Ncompare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
208
Instance N_inhabited: Inhabited N := populate 1%N.
209
Instance N_le_po: PartialOrder ()%N.
210 211 212 213
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
214

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

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

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

234
Instance Zpos_inj : Inj (=) (=) Zpos.
235
Proof. by injection 1. Qed.
236
Instance Zneg_inj : Inj (=) (=) Zneg.
237 238
Proof. by injection 1. Qed.

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

242
Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
243 244 245
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.
246
Instance Z_le_po : PartialOrder ().
247 248 249
Proof.
  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
250 251 252 253 254 255 256 257 258 259

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 |].
260
  split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
261
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
262

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
289 290
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.
291 292
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294 295
  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.
296
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
297 298 299
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m)  (n | m)%nat.
Proof.
  split.
300
  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302 303
    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.
304
  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Robbert Krebbers's avatar
Robbert Krebbers committed
305 306 307 308
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.
309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
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.

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

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

348
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
349
Program Instance Qc_le_dec (x y : Qc) : Decision (x  y) :=
350
  if Qclt_le_dec y x then right _ else left _.
351 352
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
353
Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y) :=
354
  if Qclt_le_dec x y then left _ else right _.
355 356
Solve Obligations with done.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
357

358 359 360 361 362 363 364 365
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.
366 367 368 369
Lemma Qcmult_0_l x : 0 * x = 0.
Proof. ring. Qed.
Lemma Qcmult_0_r x : x * 0 = 0.
Proof. ring. Qed.
370 371
Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc.
Proof. ring. Qed.
372
Lemma Qcle_ngt (x y : Qc) : x  y  ¬y < x.
373
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
374
Lemma Qclt_nge (x y : Qc) : x < y  ¬y  x.
375
Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
376
Lemma Qcplus_le_mono_l (x y z : Qc) : x  y  z + x  z + y.
377 378
Proof.
  split; intros.
379 380
  - by apply Qcplus_le_compat.
  - replace x with ((0 - z) + (z + x)) by ring.
381
    replace y with ((0 - z) + (z + y)) by ring.
382 383
    by apply Qcplus_le_compat.
Qed.
384
Lemma Qcplus_le_mono_r (x y z : Qc) : x  y  x + z  y + z.
385
Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
386
Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y  z + x < z + y.
387
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
388
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y  x + z < y + z.
389
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
390
Instance: Inj (=) (=) Qcopp.
391 392 393
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
394
Instance:  z, Inj (=) (=) (Qcplus z).
395
Proof.
396
  intros z x y H. by apply (anti_symm ());
397 398
    rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
399
Instance:  z, Inj (=) (=) (λ x, x + z).
400
Proof.
401
  intros z x y H. by apply (anti_symm ());
402 403
    rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
404 405 406 407 408 409 410 411 412 413 414
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.
415
  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
416 417 418 419 420 421 422 423 424 425 426 427 428
  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.
429
  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
430 431
  by apply Qcplus_le_mono_l.
Qed.
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454
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.
455
  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
456 457 458 459 460 461 462 463
  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.
464 465 466 467
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.
468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
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.
487
Close Scope Qc_scope.
488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516

(** * 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.
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.
Infix "/" := Qp_div : Qp_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
517 518
Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.

519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552
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.
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.

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

554 555 556 557 558 559 560 561 562 563 564 565 566 567
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.
568
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
569 570 571 572 573 574 575

Lemma Qp_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
  apply Qcle_ngt in Hle. by destruct q.
Qed.