numbers.v 26.9 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.

33 34
Infix "`div`" := Nat.div (at level 35) : nat_scope.
Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
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: RelDecision le := le_dec.
Instance nat_lt_dec: RelDecision lt := 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
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.
51
  { fix FIX 3. intros x ? [|y p] ? [|y' q].
52
    - done.
53 54 55
    - clear FIX. intros; exfalso; auto with lia.
    - clear FIX. intros; exfalso; auto with lia.
    - injection 1. intros Hy. by case (FIX x y p y' q Hy). }
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.
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 : RelDecision Nat.divide.
81
Proof.
82
  refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
83
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 135 136
Instance positive_le_dec: RelDecision Pos.le.
Proof. refine (λ x y, decide ((x ?= y)  Gt)). Defined.
Instance positive_lt_dec: RelDecision Pos.lt.
Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
137 138
Instance positive_inhabited: Inhabited positive := populate 1.

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

146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
(** 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
168
Global Instance Papp_1_l : LeftId (=) 1 (++).
169
Proof. intros p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Global Instance Papp_1_r : RightId (=) 1 (++).
171
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Global Instance Papp_assoc : Assoc (=) (++).
173
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
174 175
Global Instance Papp_inj p : Inj (=) (=) (++ p).
Proof. intros ???. induction p; simplify_eq; auto. Qed.
176 177 178 179

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

Robbert Krebbers's avatar
Robbert Krebbers committed
199 200 201 202 203 204 205
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.

206 207 208
Close Scope positive_scope.

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

219
Arguments N.add : simpl never.
220

Robbert Krebbers's avatar
Robbert Krebbers committed
221
Instance Npos_inj : Inj (=) (=) Npos.
222 223
Proof. by injection 1. Qed.

224
Instance N_eq_dec: EqDecision N := N.eq_dec.
225
Program Instance N_le_dec : RelDecision N.le := λ x y,
226
  match N.compare x y with Gt => right _ | _ => left _ end.
227
Solve Obligations with naive_solver.
228
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
229
  match N.compare x y with Lt => left _ | _ => right _ end.
230
Solve Obligations with naive_solver.
231
Instance N_inhabited: Inhabited N := populate 1%N.
232
Instance N_le_po: PartialOrder ()%N.
233 234 235 236
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
237

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

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

250 251
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
252 253
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
254 255
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
256

257
Instance Zpos_inj : Inj (=) (=) Zpos.
258
Proof. by injection 1. Qed.
259
Instance Zneg_inj : Inj (=) (=) Zneg.
260 261
Proof. by injection 1. Qed.

262 263 264
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.

265
Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
266 267
Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
268
Instance Z_inhabited: Inhabited Z := populate 1.
269
Instance Z_le_po : PartialOrder ().
270 271 272
Proof.
  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
273 274 275 276 277 278 279 280 281 282

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

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

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

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

350 351 352 353 354 355 356 357
(** * Injectivity of casts *)
Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
(* Add others here. *)

358
(** * Notations and properties of [Qc] *)
359
Open Scope Qc_scope.
360 361
Delimit Scope Qc_scope with Qc.
Notation "1" := (Q2Qc 1) : Qc_scope.
362
Notation "2" := (1+1) : Qc_scope.
363 364 365 366
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.
367
Infix "≤" := Qcle : Qc_scope.
368 369 370 371
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.
372
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Qc_scope.
373 374 375
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

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

379
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
380
Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
381
  if Qclt_le_dec y x then right _ else left _.
382 383
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
384
Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
385
  if Qclt_le_dec x y then left _ else right _.
386 387
Solve Obligations with done.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
388

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

(** * 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.
525
Arguments Qp_car _%Qp : assert.
526 527 528 529 530 531 532

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.
533 534
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.
535 536

Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
537
Next Obligation.
538 539 540
  intros x y. assert (0 < Zpos y)%Qc.
  { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
  by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
541 542 543 544 545
    <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed.

Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
546
Infix "*" := Qp_mult : Qp_scope.
547
Infix "/" := Qp_div : Qp_scope.
548 549 550 551
Notation "1" := Qp_one : Qp_scope.
Notation "2" := (1 + 1)%Qp : Qp_scope.
Notation "3" := (1 + 2)%Qp : Qp_scope.
Notation "4" := (1 + 3)%Qp : Qp_scope.
552 553 554 555 556 557

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.
558 559 560 561 562 563 564

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.

565 566 567 568
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.
569 570 571 572
Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj _). Qed.
Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp.
Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed.
573 574 575 576 577 578 579 580 581 582

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.

583 584 585 586 587 588 589 590 591 592 593 594 595
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.

596 597 598 599 600 601 602 603 604 605 606 607 608 609 610
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.
611 612 613 614 615 616
Lemma Qp_half_half : (1 / 2 + 1 / 2 = 1)%Qp.
Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_quarter_three_quarter : (1 / 4 + 3 / 4 = 1)%Qp.
Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_three_quarter_quarter : (3 / 4 + 1 / 4 = 1)%Qp.
Proof. apply (bool_decide_unpack _); by compute. Qed.
617

Robbert Krebbers's avatar
Robbert Krebbers committed
618 619 620 621 622 623 624 625 626
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.

627 628 629 630 631 632 633 634 635 636 637 638 639 640
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.
641
Qed.
642

643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662
Lemma Qp_cross_split p a b c d :
  (a + b = p  c + d = p 
   ac ad bc bd, ac + ad = a  bc + bd = b  ac + bc = c  ad + bd = d)%Qp.
Proof.
  intros H <-. revert a b c d H. cut ( a b c d : Qp,
    (a < c)%Qc  a + b = c + d 
     ac ad bc bd, ac + ad = a  bc + bd = b  ac + bc = c  ad + bd = d)%Qp.
  { intros help a b c d ?.
    destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq].
    - auto.
    - destruct (help c d a b); [done..|]. naive_solver.
    - apply (inj _) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
      eauto 10 using (comm_L Qp_plus). }
  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj _).
  destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
  eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus).
  - by rewrite (assoc_L _), (comm_L Qp_plus e).
  - by rewrite (assoc_L _), (comm_L Qp_plus a').
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
663 664 665 666 667 668 669 670 671 672 673 674 675 676 677
Lemma Qp_bounded_split (p r : Qp) :  q1 q2 : Qp, (q1  r)%Qc  p = (q1 + q2)%Qp.
Proof.
  destruct (Qclt_le_dec r p) as [?|?].
  - assert (0 < p - r)%Qc as Hpos.
    { apply (Qcplus_lt_mono_r _ _ r). rewrite <-Qcplus_assoc, (Qcplus_comm (-r)).
      by rewrite Qcplus_opp_r, Qcplus_0_l, Qcplus_0_r. }
    exists r, (mk_Qp _ Hpos); simpl; split; [done|].
    apply Qp_eq; simpl. rewrite Qcplus_comm, <-Qcplus_assoc, (Qcplus_comm (-r)).
    by rewrite Qcplus_opp_r, Qcplus_0_r.
  - exists (p / 2)%Qp, (p / 2)%Qp; split.
    + trans p; [|done]. apply Qclt_le_weak, Qp_lt_sum.
      exists (p / 2)%Qp. by rewrite Qp_div_2.
    + by rewrite Qp_div_2.
Qed.

Zhen Zhang's avatar
Zhen Zhang committed
678
Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
679 680 681
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
Zhen Zhang's avatar
Zhen Zhang committed
682
  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
683
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
684 685 686

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