numbers.v 27.5 KB
Newer Older
1
(* Copyright (c) 2012-2019, 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: 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.
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 : 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
Instance: PartialOrder divide.
Proof.
  repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
Qed.
Tej Chajed's avatar
Tej Chajed committed
88
Hint Extern 0 (_ | _) => reflexivity : core.
89 90 91
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
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97 98 99
Proof. induction n; by f_equal/=. Qed.
Lemma Nat_iter_add {A} n1 n2 (f : A  A) x :
  Nat.iter (n1 + n2) f x = Nat.iter n1 f (Nat.iter n2 f x).
Proof. induction n1; by f_equal/=. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
100
Lemma Nat_iter_ind {A} (P : A  Prop) f x k :
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102
  P x  ( y, P y  P (f y))  P (Nat.iter k f x).
Proof. induction k; simpl; auto. Qed.
103

Robbert Krebbers's avatar
Robbert Krebbers committed
104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
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).

120 121 122
(** * Notations and properties of [positive] *)
Open Scope positive_scope.

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

133 134 135
Arguments Pos.of_nat : simpl never.
Arguments Pmult : simpl never.

136
Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
137 138 139 140
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.
141 142
Instance positive_inhabited: Inhabited positive := populate 1.

143
Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145
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
146
Proof. by injection 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Instance xI_inj : Inj (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
148 149
Proof. by injection 1. Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205 206 207 208 209
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.

210 211 212
Close Scope positive_scope.

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

223
Arguments N.add : simpl never.
224

Robbert Krebbers's avatar
Robbert Krebbers committed
225
Instance Npos_inj : Inj (=) (=) Npos.
Robbert Krebbers's avatar
Robbert Krebbers committed
226 227
Proof. by injection 1. Qed.

228
Instance N_eq_dec: EqDecision N := N.eq_dec.
229
Program Instance N_le_dec : RelDecision N.le := λ x y,
230
  match N.compare x y with Gt => right _ | _ => left _ end.
231
Solve Obligations with naive_solver.
232
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
233
  match N.compare x y with Lt => left _ | _ => right _ end.
234
Solve Obligations with naive_solver.
235
Instance N_inhabited: Inhabited N := populate 1%N.
236
Instance N_le_po: PartialOrder ()%N.
237 238 239
Proof.
  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
Qed.
Tej Chajed's avatar
Tej Chajed committed
240
Hint Extern 0 (_  _)%N => reflexivity : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
241

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
254 255
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
256 257
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
258 259
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
260

261
Instance Zpos_inj : Inj (=) (=) Zpos.
262
Proof. by injection 1. Qed.
263
Instance Zneg_inj : Inj (=) (=) Zneg.
264 265
Proof. by injection 1. Qed.

266 267 268
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.

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

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

290 291 292
Arguments Z.pred : simpl never.
Arguments Z.succ : simpl never.
Arguments Z.of_nat : simpl never.
293 294 295
Arguments Z.to_nat : simpl never.
Arguments Z.mul : simpl never.
Arguments Z.add : simpl never.
296
Arguments Z.sub : simpl never.
297 298 299 300 301 302
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.
303 304 305 306 307 308 309 310 311 312 313 314
Arguments Z.shiftl : simpl never.
Arguments Z.shiftr : simpl never.
Arguments Z.gcd : simpl never.
Arguments Z.lcm : simpl never.
Arguments Z.min : simpl never.
Arguments Z.max : simpl never.
Arguments Z.lor : simpl never.
Arguments Z.land : simpl never.
Arguments Z.lxor : simpl never.
Arguments Z.lnot : simpl never.
Arguments Z.square : simpl never.
Arguments Z.abs : simpl never.
315

316 317 318 319 320
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.
321 322 323 324 325
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.
326 327
Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
Hint Resolve Z_mod_pos Z.div_pos : zpos.
328 329
Hint Extern 1000 => lia : zpos.

Robbert Krebbers's avatar
Robbert Krebbers committed
330 331
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.
332 333
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
334 335 336
  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.
337
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
338 339 340
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m)  (n | m)%nat.
Proof.
  split.
341
  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
Robbert Krebbers's avatar
Robbert Krebbers committed
342 343 344
    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.
345
  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Robbert Krebbers's avatar
Robbert Krebbers committed
346 347 348 349
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.
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
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.

368 369 370 371 372 373 374 375
(** * 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. *)

376
(** * Notations and properties of [Qc] *)
377
Open Scope Qc_scope.
378 379
Delimit Scope Qc_scope with Qc.
Notation "1" := (Q2Qc 1) : Qc_scope.
380
Notation "2" := (1+1) : Qc_scope.
381 382
Notation "- 1" := (Qcopp 1) : Qc_scope.
Notation "- 2" := (Qcopp 2) : Qc_scope.
383
Infix "≤" := Qcle : Qc_scope.
384 385 386 387
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.
388
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Qc_scope.
389 390 391
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

Tej Chajed's avatar
Tej Chajed committed
392
Hint Extern 1 (_  _) => reflexivity || discriminate : core.
393
Arguments Qred : simpl never.
394

395
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
396
Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
397
  if Qclt_le_dec y x then right _ else left _.
398 399
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
400
Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
401
  if Qclt_le_dec x y then left _ else right _.
402 403
Solve Obligations with done.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
404

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

(** * 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 }.
Tej Chajed's avatar
Tej Chajed committed
538
Hint Resolve Qp_prf : core.
539 540
Delimit Scope Qp_scope with Qp.
Bind Scope Qp_scope with Qp.
541
Arguments Qp_car _%Qp : assert.
542 543 544 545 546 547 548

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.
549 550
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.
551 552

Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
553
Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
554
  intros x y. unfold Qcdiv. assert (0 < Zpos y)%Qc.
555 556
  { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
  by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
557 558 559 560 561
    <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed.

Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
562
Infix "*" := Qp_mult : Qp_scope.
563
Infix "/" := Qp_div : Qp_scope.
564 565 566 567
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.
568 569 570 571 572 573

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
574 575 576 577 578 579 580

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.

581 582 583 584
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.
585 586 587 588
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.
589 590

Lemma Qp_minus_diag x : (x - x)%Qp = None.
Ralf Jung's avatar
Ralf Jung committed
591
Proof. unfold Qp_minus, Qcminus. by rewrite Qcplus_opp_r. Qed.
592 593
Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y.
Proof.
Ralf Jung's avatar
Ralf Jung committed
594
  unfold Qp_minus, Qcminus; simpl.
595 596 597 598
  rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r.
  destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq.
Qed.

599 600 601 602 603 604 605 606 607 608 609 610 611
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.

612 613 614 615 616 617 618
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.
Ralf Jung's avatar
Ralf Jung committed
619
  apply Qp_eq; simpl. unfold Qcdiv.
620 621 622 623 624 625 626
  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.
627 628 629 630 631 632
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.
633

Robbert Krebbers's avatar
Robbert Krebbers committed
634 635 636 637
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.
Ralf Jung's avatar
Ralf Jung committed
638
    unfold Qcminus. by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
639 640 641 642
  - intros [z ->]; simpl.
    rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf.
Qed.

643 644 645 646 647 648 649 650
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.
Ralf Jung's avatar
Ralf Jung committed
651
  assert (0 < q2 +- q1 */ 2)%Qc as Hq2'.
652
  { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq].
Ralf Jung's avatar
Ralf Jung committed
653 654 655 656
    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. unfold Qcdiv. ring.
657
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
658

659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678
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
679 680 681
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 [?|?].
Ralf Jung's avatar
Ralf Jung committed
682
  - assert (0 < p +- r)%Qc as Hpos.
Robbert Krebbers's avatar
Robbert Krebbers committed
683 684 685 686 687 688 689 690 691 692 693
    { 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
694
Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
Zhen Zhang's avatar
Zhen Zhang committed
695 696 697
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
Zhen Zhang's avatar
Zhen Zhang committed
698
  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
Zhen Zhang's avatar
Zhen Zhang committed
699
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
700 701 702

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