numbers.v 24.7 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: 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 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 : 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).
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Proof. by injection 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Instance xI_inj : Inj (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 227
  match Ncompare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
228
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
229 230
  match Ncompare x y with Lt => left _ | _ => right _ end.
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: Inj (=) (=) Qcopp.
422 423 424
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
425
Instance:  z, Inj (=) (=) (Qcplus z).
426
Proof.
427
  intros z x y H. by apply (anti_symm ());
428 429
    rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
430
Instance:  z, Inj (=) (=) (λ x, x + z).
431
Proof.
432
  intros z x y H. by apply (anti_symm ());
433 434
    rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
435 436 437 438 439 440 441 442 443 444 445
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.
446
  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
447 448 449 450 451 452 453 454 455 456 457 458 459
  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.
460
  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
461 462
  by apply Qcplus_le_mono_l.
Qed.
463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485
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.
486
  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
487 488 489 490 491 492 493 494
  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.
495 496 497 498
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.
499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517
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.
518
Close Scope Qc_scope.
519 520 521 522 523 524 525 526

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

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.
535 536
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.
537 538

Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
539
Next Obligation.
540 541 542
  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,
543 544 545 546 547 548
    <-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.
549
Infix "*" := Qp_mult : Qp_scope.
550 551 552 553 554 555 556
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
557 558 559 560 561 562 563

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.

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

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

591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
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.
606

Robbert Krebbers's avatar
Robbert Krebbers committed
607 608 609 610 611 612 613 614 615
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.

616 617 618 619 620 621 622 623 624 625 626 627 628 629
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.
630
Qed.
631

Zhen Zhang's avatar
Zhen Zhang committed
632
Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
633 634 635
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
Zhen Zhang's avatar
Zhen Zhang committed
636
  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
637
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
638 639 640

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