numbers.v 29 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
Arguments Nat.max : simpl nomatch.

20 21 22 23
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).
24 25
Reserved Notation "x ≤ y ≤ z ≤ z'"
  (at level 70, y at next level, z at next level).
26

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

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

40
Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
41 42
Instance nat_le_dec: RelDecision le := le_dec.
Instance nat_lt_dec: RelDecision lt := lt_dec.
43
Instance nat_inhabited: Inhabited nat := populate 0%nat.
44
Instance S_inj: Inj (=) (=) S.
45
Proof. by injection 1. Qed.
46
Instance nat_le_po: PartialOrder ().
47
Proof. repeat split; repeat intro; auto with lia. Qed.
48

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

Robbert Krebbers's avatar
Robbert Krebbers committed
64 65
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
66

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

79 80 81
Notation lcm := Nat.lcm.
Notation divide := Nat.divide.
Notation "( x | y )" := (divide x y) : nat_scope.
82
Instance Nat_divide_dec : RelDecision Nat.divide.
83
Proof.
84
  refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
85
Defined.
86 87 88 89
Instance: PartialOrder divide.
Proof.
  repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
Qed.
Tej Chajed's avatar
Tej Chajed committed
90
Hint Extern 0 (_ | _) => reflexivity : core.
91 92 93
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.

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

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

122 123 124
(** * Notations and properties of [positive] *)
Open Scope positive_scope.

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

135 136 137
Arguments Pos.of_nat : simpl never.
Arguments Pmult : simpl never.

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

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

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

Lemma Preverse_go_app p1 p2 p3 :
  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
Proof.
186 187 188 189
  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.
190 191
  - apply (IH _ (_~1)).
  - apply (IH _ (_~0)).
192
Qed.
193
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
194 195 196 197 198 199
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).

200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
Lemma Preverse_involutive p :
  Preverse (Preverse p) = p.
Proof.
  induction p as [p IH|p IH|]; simpl.
  - by rewrite Preverse_xI, Preverse_app, IH.
  - by rewrite Preverse_xO, Preverse_app, IH.
  - reflexivity.
Qed.
    
Instance Preverse_inj : Inj (=) (=) Preverse.
Proof.
  intros p q eq.
  rewrite <- (Preverse_involutive p).
  rewrite <- (Preverse_involutive q).
  by rewrite eq.
Qed.

217
Fixpoint Plength (p : positive) : nat :=
218
  match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
219
Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
220
Proof. by induction p2; f_equal/=. Qed.
221

Robbert Krebbers's avatar
Robbert Krebbers committed
222 223 224 225 226 227 228
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.

229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
(** Duplicate the bits of a positive, i.e. 1~0~1 -> 1~0~0~1~1 and
    1~1~0~0 -> 1~1~1~0~0~0~0 *)
Fixpoint Pdup (p : positive) : positive :=
  match p with
  | 1 => 1
  | p'~0 => (Pdup p')~0~0
  | p'~1 => (Pdup p')~1~1
  end.

Lemma Pdup_app p q :
  Pdup (p ++ q) = Pdup p ++ Pdup q.
Proof.
  revert p.
  induction q as [p IH|p IH|]; intros q; simpl.
  - by rewrite IH.
  - by rewrite IH.
  - reflexivity.
Qed.

Lemma Pdup_suffix_eq p q s1 s2 :
  s1~1~0 ++ Pdup p = s2~1~0 ++ Pdup q  p = q.
Proof.
  revert q.
  induction p as [p IH|p IH|]; intros [q|q|] eq; simplify_eq/=.
  - by rewrite (IH q).
  - by rewrite (IH q).
  - reflexivity.
Qed.

Instance Pdup_inj : Inj (=) (=) Pdup.
Proof.
  intros p q eq.
  apply (Pdup_suffix_eq _ _ 1 1).
  by rewrite eq.
Qed.

Lemma Preverse_Pdup p :
  Preverse (Pdup p) = Pdup (Preverse p).
Proof.
  induction p as [p IH|p IH|]; simpl.
  - rewrite 3!Preverse_xI.
    rewrite (assoc_L (++)).
    rewrite IH.
    rewrite Pdup_app.
    reflexivity.
  - rewrite 3!Preverse_xO.
    rewrite (assoc_L (++)).
    rewrite IH.
    rewrite Pdup_app.
    reflexivity.
  - reflexivity.
Qed.

282 283 284
Close Scope positive_scope.

(** * Notations and properties of [N] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
285
Infix "≤" := N.le : N_scope.
286 287 288
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.
289
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z')%N : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
Notation "(≤)" := N.le (only parsing) : N_scope.
291
Notation "(<)" := N.lt (only parsing) : N_scope.
292 293 294
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.

295
Arguments N.add : simpl never.
296

Robbert Krebbers's avatar
Robbert Krebbers committed
297
Instance Npos_inj : Inj (=) (=) Npos.
Robbert Krebbers's avatar
Robbert Krebbers committed
298 299
Proof. by injection 1. Qed.

300
Instance N_eq_dec: EqDecision N := N.eq_dec.
301
Program Instance N_le_dec : RelDecision N.le := λ x y,
302
  match N.compare x y with Gt => right _ | _ => left _ end.
303
Solve Obligations with naive_solver.
304
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
305
  match N.compare x y with Lt => left _ | _ => right _ end.
306
Solve Obligations with naive_solver.
307
Instance N_inhabited: Inhabited N := populate 1%N.
308
Instance N_le_po: PartialOrder ()%N.
309 310 311
Proof.
  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
Qed.
Tej Chajed's avatar
Tej Chajed committed
312
Hint Extern 0 (_  _)%N => reflexivity : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
313

314
(** * Notations and properties of [Z] *)
315 316
Open Scope Z_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
317
Infix "≤" := Z.le : Z_scope.
318 319 320 321
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.
322
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
Notation "(≤)" := Z.le (only parsing) : Z_scope.
324
Notation "(<)" := Z.lt (only parsing) : Z_scope.
325

Robbert Krebbers's avatar
Robbert Krebbers committed
326 327
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
328 329
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
330 331
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
332

333
Instance Zpos_inj : Inj (=) (=) Zpos.
334
Proof. by injection 1. Qed.
335
Instance Zneg_inj : Inj (=) (=) Zneg.
336 337
Proof. by injection 1. Qed.

338 339 340
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.

341
Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
342 343
Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
344
Instance Z_inhabited: Inhabited Z := populate 1.
345
Instance Z_le_po : PartialOrder ().
346 347 348
Proof.
  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
349 350 351 352 353 354 355 356 357 358

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

362 363 364
Arguments Z.pred : simpl never.
Arguments Z.succ : simpl never.
Arguments Z.of_nat : simpl never.
365 366 367
Arguments Z.to_nat : simpl never.
Arguments Z.mul : simpl never.
Arguments Z.add : simpl never.
368
Arguments Z.sub : simpl never.
369 370 371 372 373 374
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.
375 376 377 378 379 380 381 382 383 384 385 386
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.
387

388 389 390 391 392
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.
393 394 395 396 397
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.
398 399
Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
Hint Resolve Z_mod_pos Z.div_pos : zpos.
400 401
Hint Extern 1000 => lia : zpos.

Robbert Krebbers's avatar
Robbert Krebbers committed
402 403
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.
404 405
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
406 407 408
  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.
409
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
410 411 412
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m)  (n | m)%nat.
Proof.
  split.
413
  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
Robbert Krebbers's avatar
Robbert Krebbers committed
414 415 416
    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.
417
  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Robbert Krebbers's avatar
Robbert Krebbers committed
418 419 420 421
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.
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439
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.

440 441 442 443 444 445 446 447
(** * 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. *)

448
(** * Notations and properties of [Qc] *)
449
Open Scope Qc_scope.
450 451
Delimit Scope Qc_scope with Qc.
Notation "1" := (Q2Qc 1) : Qc_scope.
452
Notation "2" := (1+1) : Qc_scope.
453 454
Notation "- 1" := (Qcopp 1) : Qc_scope.
Notation "- 2" := (Qcopp 2) : Qc_scope.
455
Infix "≤" := Qcle : Qc_scope.
456 457 458 459
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.
460
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Qc_scope.
461 462 463
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

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

467
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
468
Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
469
  if Qclt_le_dec y x then right _ else left _.
470 471
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
472
Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
473
  if Qclt_le_dec x y then left _ else right _.
Ralf Jung's avatar
Ralf Jung committed
474
Next Obligation. done. Qed.
475
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
476

477 478 479 480 481 482 483 484
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.
485 486 487 488
Lemma Qcmult_0_l x : 0 * x = 0.
Proof. ring. Qed.
Lemma Qcmult_0_r x : x * 0 = 0.
Proof. ring. Qed.
489 490
Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc.
Proof. ring. Qed.
491
Lemma Qcle_ngt (x y : Qc) : x  y  ¬y < x.
492
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
493
Lemma Qclt_nge (x y : Qc) : x < y  ¬y  x.
494
Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
495
Lemma Qcplus_le_mono_l (x y z : Qc) : x  y  z + x  z + y.
496 497
Proof.
  split; intros.
498 499
  - by apply Qcplus_le_compat.
  - replace x with ((0 - z) + (z + x)) by ring.
500
    replace y with ((0 - z) + (z + y)) by ring.
501 502
    by apply Qcplus_le_compat.
Qed.
503
Lemma Qcplus_le_mono_r (x y z : Qc) : x  y  x + z  y + z.
504
Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
505
Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y  z + x < z + y.
506
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
507
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y  x + z < y + z.
508
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
509
Instance Qcopp_inj : Inj (=) (=) Qcopp.
510 511 512
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
513
Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
514
Proof.
515
  intros x y H. by apply (anti_symm ());rewrite (Qcplus_le_mono_l _ _ z), H.
516
Qed.
517
Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
518
Proof.
519
  intros x y H. by apply (anti_symm ()); rewrite (Qcplus_le_mono_r _ _ z), H.
520
Qed.
521 522 523 524 525 526 527 528 529 530 531
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.
532
  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
533 534 535 536 537 538 539 540 541 542 543 544 545
  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.
546
  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
547 548
  by apply Qcplus_le_mono_l.
Qed.
549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571
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.
572
  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
573 574 575 576 577 578 579 580
  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.
581 582 583 584
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.
585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603
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.
604
Close Scope Qc_scope.
605 606 607 608 609

(** * 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
610
Hint Resolve Qp_prf : core.
611 612
Delimit Scope Qp_scope with Qp.
Bind Scope Qp_scope with Qp.
613
Arguments Qp_car _%Qp : assert.
614 615 616 617 618 619 620

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.
621 622
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.
623 624

Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
625
Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
626
  intros x y. unfold Qcdiv. assert (0 < Zpos y)%Qc.
627 628
  { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
  by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
629 630 631 632 633
    <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed.

Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
634
Infix "*" := Qp_mult : Qp_scope.
635
Infix "/" := Qp_div : Qp_scope.
636 637 638 639
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.
640 641 642 643 644 645

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
646 647 648 649 650 651 652

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.

653 654 655 656
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.
657 658 659 660
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.
661 662

Lemma Qp_minus_diag x : (x - x)%Qp = None.
Ralf Jung's avatar
Ralf Jung committed
663
Proof. unfold Qp_minus, Qcminus. by rewrite Qcplus_opp_r. Qed.
664 665
Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y.
Proof.
Ralf Jung's avatar
Ralf Jung committed
666
  unfold Qp_minus, Qcminus; simpl.
667 668 669 670
  rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r.
  destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq.
Qed.

671 672 673 674 675 676 677 678 679 680 681 682 683
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.

684 685 686 687 688 689 690
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
691
  apply Qp_eq; simpl. unfold Qcdiv.
692 693 694 695 696 697 698
  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.
699 700 701 702 703 704
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.
705

Robbert Krebbers's avatar
Robbert Krebbers committed
706 707 708 709
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
710
    unfold Qcminus. by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
711 712 713 714
  - intros [z ->]; simpl.
    rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf.
Qed.

715 716 717 718 719 720 721 722
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
723
  assert (0 < q2 +- q1 */ 2)%Qc as Hq2'.
724
  { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq].
Ralf Jung's avatar
Ralf Jung committed
725 726 727 728
    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.
729
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
730

731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750
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
751 752 753
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
754
  - assert (0 < p +- r)%Qc as Hpos.
Robbert Krebbers's avatar
Robbert Krebbers committed
755 756 757 758 759 760 761 762 763 764 765
    { 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
766
Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
Zhen Zhang's avatar
Zhen Zhang committed
767 768 769
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
Zhen Zhang's avatar
Zhen Zhang committed
770
  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
Zhen Zhang's avatar
Zhen Zhang committed
771
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
772 773 774

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