numbers.v 24.2 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
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] *)
17
Arguments minus !_ !_ / : assert.
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
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
Lemma nat_le_sum (x y : nat) : x  y   z, y = x + z.
Proof. split. exists (y - x); lia. intros [z ->]; lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64

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

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

92 93 94 95
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
96
Lemma Nat_iter_ind {A} (P : A  Prop) f x k :
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98
  P x  ( y, P y  P (f y))  P (Nat.iter k f x).
Proof. induction k; simpl; auto. Qed.
99

Robbert Krebbers's avatar
Robbert Krebbers committed
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
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).

Definition max_list_with {A} (f : A  nat) : list A  nat :=
  fix go l :=
  match l with
  | [] => 0
  | x :: l => f x `max` go l
  end.
Notation max_list := (max_list_with id).

116 117 118
(** * Notations and properties of [positive] *)
Open Scope positive_scope.

119
Infix "≤" := Pos.le : positive_scope.
120 121 122 123
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.
124 125
Notation "(≤)" := Pos.le (only parsing) : positive_scope.
Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
126 127 128
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

129 130 131
Arguments Pos.of_nat : simpl never.
Arguments Pmult : simpl never.

132
Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
133 134
Instance positive_inhabited: Inhabited positive := populate 1.

135
Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137
Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
Instance xO_inj : Inj (=) (=) (~0).
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Proof. by injection 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Instance xI_inj : Inj (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141
Proof. by injection 1. Qed.

142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
(** 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
164
Global Instance Papp_1_l : LeftId (=) 1 (++).
165
Proof. intros p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Global Instance Papp_1_r : RightId (=) 1 (++).
167
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Global Instance Papp_assoc : Assoc (=) (++).
169
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
170 171
Global Instance Papp_inj p : Inj (=) (=) (++ p).
Proof. intros ???. induction p; simplify_eq; auto. Qed.
172 173 174 175

Lemma Preverse_go_app p1 p2 p3 :
  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
Proof.
176 177 178 179
  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.
180 181
  - apply (IH _ (_~1)).
  - apply (IH _ (_~0)).
182
Qed.
183
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
184 185 186 187 188 189 190
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 :=
191
  match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
192
Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
193
Proof. by induction p2; f_equal/=. Qed.
194

Robbert Krebbers's avatar
Robbert Krebbers committed
195 196 197 198 199 200 201
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.

202 203 204
Close Scope positive_scope.

(** * Notations and properties of [N] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Infix "≤" := N.le : N_scope.
206 207 208
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.
209
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z')%N : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Notation "(≤)" := N.le (only parsing) : N_scope.
211
Notation "(<)" := N.lt (only parsing) : N_scope.
212 213 214
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.

215
Arguments N.add : simpl never.
216

Robbert Krebbers's avatar
Robbert Krebbers committed
217
Instance Npos_inj : Inj (=) (=) Npos.
Robbert Krebbers's avatar
Robbert Krebbers committed
218 219
Proof. by injection 1. Qed.

220
Instance N_eq_dec: EqDecision N := N.eq_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
Program Instance N_le_dec (x y : N) : Decision (x  y)%N :=
222 223
  match Ncompare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
224
Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
225 226
  match Ncompare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
227
Instance N_inhabited: Inhabited N := populate 1%N.
228
Instance N_le_po: PartialOrder ()%N.
229 230 231 232
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
233

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

Robbert Krebbers's avatar
Robbert Krebbers committed
237
Infix "≤" := Z.le : Z_scope.
238 239 240 241
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.
242
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
Notation "(≤)" := Z.le (only parsing) : Z_scope.
244
Notation "(<)" := Z.lt (only parsing) : Z_scope.
245

246 247
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
248 249
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
250 251
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
252

253
Instance Zpos_inj : Inj (=) (=) Zpos.
254
Proof. by injection 1. Qed.
255
Instance Zneg_inj : Inj (=) (=) Zneg.
256 257
Proof. by injection 1. Qed.

258 259 260
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.

261
Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
262 263 264
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.
265
Instance Z_le_po : PartialOrder ().
266 267 268
Proof.
  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
269 270 271 272 273 274 275 276 277 278

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

282
(* Note that we cannot disable simpl for [Z.of_nat] as that would break
283
tactics as [lia]. *)
284 285 286 287 288 289 290 291 292
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.
293

294 295 296 297 298
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.
299 300 301 302 303
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.
304 305
Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
Hint Resolve Z_mod_pos Z.div_pos : zpos.
306 307
Hint Extern 1000 => lia : zpos.

Robbert Krebbers's avatar
Robbert Krebbers committed
308 309
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.
310 311
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
312 313 314
  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.
315
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
316 317 318
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m)  (n | m)%nat.
Proof.
  split.
319
  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
Robbert Krebbers's avatar
Robbert Krebbers committed
320 321 322
    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.
323
  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Robbert Krebbers's avatar
Robbert Krebbers committed
324 325 326 327
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.
328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345
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.

346
(** * Notations and properties of [Qc] *)
347
Open Scope Qc_scope.
348 349
Delimit Scope Qc_scope with Qc.
Notation "1" := (Q2Qc 1) : Qc_scope.
350
Notation "2" := (1+1) : Qc_scope.
351 352 353 354
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.
355
Infix "≤" := Qcle : Qc_scope.
356 357 358 359
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.
360
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Qc_scope.
361 362 363
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

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

367
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
368
Program Instance Qc_le_dec (x y : Qc) : Decision (x  y) :=
369
  if Qclt_le_dec y x then right _ else left _.
370 371
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
372
Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y) :=
373
  if Qclt_le_dec x y then left _ else right _.
374 375
Solve Obligations with done.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
376

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

(** * 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.
515
Arguments Qp_car _%Qp : assert.
516 517 518 519 520 521 522

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.
523 524
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.
525 526 527 528 529 530 531 532 533 534 535
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.
536
Infix "*" := Qp_mult : Qp_scope.
537 538 539 540 541 542 543
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
544 545 546 547 548 549 550

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.

551 552 553 554 555 556 557 558 559 560 561 562 563 564
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.

565 566 567 568 569 570 571 572 573 574 575 576 577
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.

578 579 580 581 582 583 584 585 586 587 588 589 590 591 592
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.
593

Robbert Krebbers's avatar
Robbert Krebbers committed
594 595 596 597 598 599 600 601 602
Lemma Qp_lt_sum (x y : Qp) : (x < y)%Qc   z, y = (x + z)%Qp.
Proof.
  split.
  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
    by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
  - intros [z ->]; simpl.
    rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf.
Qed.

603 604 605 606 607 608 609 610 611 612 613 614 615 616
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.
617
Qed.
618

Zhen Zhang's avatar
Zhen Zhang committed
619
Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
620 621 622
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
Zhen Zhang's avatar
Zhen Zhang committed
623
  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
624
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
625 626 627

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