numbers.v 30.3 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
Typeclasses Opaque lt.

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
68 69
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
70

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
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).

126 127 128
(** * Notations and properties of [positive] *)
Open Scope positive_scope.

129 130 131
Typeclasses Opaque Pos.le.
Typeclasses Opaque Pos.lt.

132
Infix "≤" := Pos.le : positive_scope.
133 134 135 136
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.
137 138
Notation "(≤)" := Pos.le (only parsing) : positive_scope.
Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
139 140 141
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

142 143 144
Arguments Pos.of_nat : simpl never.
Arguments Pmult : simpl never.

145
Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
146 147 148 149
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.
150 151 152
Instance positive_le_total: Total Pos.le.
Proof. repeat intro; lia. Qed.

153 154
Instance positive_inhabited: Inhabited positive := populate 1.

155
Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157
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
158
Proof. by injection 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Instance xI_inj : Inj (=) (=) (~1).
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
Proof. by injection 1. Qed.

162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
(** 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
184
Global Instance Papp_1_l : LeftId (=) 1 (++).
185
Proof. intros p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
Global Instance Papp_1_r : RightId (=) 1 (++).
187
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Global Instance Papp_assoc : Assoc (=) (++).
189
Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191
Global Instance Papp_inj p : Inj (=) (=) (++ p).
Proof. intros ???. induction p; simplify_eq; auto. Qed.
192 193 194 195

Lemma Preverse_go_app p1 p2 p3 :
  Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
Proof.
196 197 198 199
  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.
200 201
  - apply (IH _ (_~1)).
  - apply (IH _ (_~0)).
202
Qed.
203
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
204 205 206 207 208 209
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).

210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
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.

227
Fixpoint Plength (p : positive) : nat :=
228
  match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
229
Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
230
Proof. by induction p2; f_equal/=. Qed.
231

Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235 236 237 238
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.

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 282 283 284 285 286 287 288 289 290 291
(** 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.

292 293 294
Close Scope positive_scope.

(** * Notations and properties of [N] *)
295 296 297
Typeclasses Opaque N.le.
Typeclasses Opaque N.lt.

Robbert Krebbers's avatar
Robbert Krebbers committed
298
Infix "≤" := N.le : N_scope.
299 300 301
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.
302
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z')%N : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Notation "(≤)" := N.le (only parsing) : N_scope.
304
Notation "(<)" := N.lt (only parsing) : N_scope.
305

306 307
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.
308 309
Infix "`max`" := N.max (at level 35) : N_scope.
Infix "`min`" := N.min (at level 35) : N_scope.
310

311
Arguments N.add : simpl never.
312

Robbert Krebbers's avatar
Robbert Krebbers committed
313
Instance Npos_inj : Inj (=) (=) Npos.
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315
Proof. by injection 1. Qed.

316
Instance N_eq_dec: EqDecision N := N.eq_dec.
317
Program Instance N_le_dec : RelDecision N.le := λ x y,
318
  match N.compare x y with Gt => right _ | _ => left _ end.
319
Solve Obligations with naive_solver.
320
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
321
  match N.compare x y with Lt => left _ | _ => right _ end.
322
Solve Obligations with naive_solver.
323
Instance N_inhabited: Inhabited N := populate 1%N.
324 325 326
Instance N_lt_pi x y : ProofIrrel (x < y)%N.
Proof. unfold N.lt. apply _. Qed.

327
Instance N_le_po: PartialOrder ()%N.
328 329 330
Proof.
  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
Qed.
331 332 333
Instance N_le_total: Total ()%N.
Proof. repeat intro; lia. Qed.

334
Hint Extern 0 (_  _)%N => reflexivity : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
335

336
(** * Notations and properties of [Z] *)
337 338
Open Scope Z_scope.

339 340 341
Typeclasses Opaque Z.le.
Typeclasses Opaque Z.lt.

Robbert Krebbers's avatar
Robbert Krebbers committed
342
Infix "≤" := Z.le : Z_scope.
343 344 345 346
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.
347
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Notation "(≤)" := Z.le (only parsing) : Z_scope.
349
Notation "(<)" := Z.lt (only parsing) : Z_scope.
350

351 352
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
353 354
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
355 356
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
357 358
Infix "`max`" := Z.max (at level 35) : Z_scope.
Infix "`min`" := Z.min (at level 35) : Z_scope.
359

360
Instance Zpos_inj : Inj (=) (=) Zpos.
361
Proof. by injection 1. Qed.
362
Instance Zneg_inj : Inj (=) (=) Zneg.
363 364
Proof. by injection 1. Qed.

365 366 367
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.

368
Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
369 370
Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
371
Instance Z_inhabited: Inhabited Z := populate 1.
372 373 374
Instance Z_lt_pi x y : ProofIrrel (x < y).
Proof. unfold Z.lt. apply _. Qed.

375
Instance Z_le_po : PartialOrder ().
376 377 378
Proof.
  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
379 380
Instance Z_le_total: Total Z.le.
Proof. repeat intro; lia. Qed.
381 382 383 384 385 386 387 388 389 390

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

394 395 396
Arguments Z.pred : simpl never.
Arguments Z.succ : simpl never.
Arguments Z.of_nat : simpl never.
397 398 399
Arguments Z.to_nat : simpl never.
Arguments Z.mul : simpl never.
Arguments Z.add : simpl never.
400
Arguments Z.sub : simpl never.
401 402 403 404 405 406
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.
407 408 409 410 411 412 413 414 415 416 417 418
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.
419

420 421 422 423 424
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.
425 426 427 428 429
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.
430 431
Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
Hint Resolve Z_mod_pos Z.div_pos : zpos.
432 433
Hint Extern 1000 => lia : zpos.

Robbert Krebbers's avatar
Robbert Krebbers committed
434 435
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.
436 437
Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
438 439 440
  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.
441
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
442 443 444
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m)  (n | m)%nat.
Proof.
  split.
445
  - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
Robbert Krebbers's avatar
Robbert Krebbers committed
446 447 448
    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.
449
  - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Robbert Krebbers's avatar
Robbert Krebbers committed
450 451 452 453
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.
454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469
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.
470 471 472 473 474 475 476
Lemma Z_from_zero_ind (P : Z  Prop) :
  P 0 
  ( x, 0  x  P x  P (Z.succ x)) 
  ( x, x  0  P x  P (Z.pred x)) 
  ( x, P x).
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ 0). Qed.

477 478
Close Scope Z_scope.

479 480 481 482 483 484 485 486
(** * 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. *)

487
(** * Notations and properties of [Qc] *)
488 489 490
Typeclasses Opaque Qcle.
Typeclasses Opaque Qclt.

491
Open Scope Qc_scope.
492 493
Delimit Scope Qc_scope with Qc.
Notation "1" := (Q2Qc 1) : Qc_scope.
494
Notation "2" := (1+1) : Qc_scope.
495 496
Notation "- 1" := (Qcopp 1) : Qc_scope.
Notation "- 2" := (Qcopp 2) : Qc_scope.
497
Infix "≤" := Qcle : Qc_scope.
498 499 500 501
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.
502
Notation "x ≤ y ≤ z ≤ z'" := (x  y  y  z  z  z') : Qc_scope.
503 504 505
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.

506
Hint Extern 1 (_  _) => reflexivity || discriminate : core.
507
Arguments Qred : simpl never.
508

509
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
510
Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
511
  if Qclt_le_dec y x then right _ else left _.
512 513
Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next Obligation. done. Qed.
514
Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
515
  if Qclt_le_dec x y then left _ else right _.
Ralf Jung's avatar
Ralf Jung committed
516
Next Obligation. done. Qed.
517
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
518 519
Instance Qc_lt_pi x y : ProofIrrel (x < y).
Proof. unfold Qclt. apply _. Qed.
520

521
Instance Qc_le_po: PartialOrder ().
522 523 524
Proof.
  repeat split; red. apply Qcle_refl. apply Qcle_trans. apply Qcle_antisym.
Qed.
525
Instance Qc_lt_strict: StrictOrder (<).
526 527 528
Proof.
  split; red. intros x Hx. by destruct (Qclt_not_eq x x). apply Qclt_trans.
Qed.
529 530 531
Instance Qc_le_total: Total Qcle.
Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed.

532 533 534 535
Lemma Qcmult_0_l x : 0 * x = 0.
Proof. ring. Qed.
Lemma Qcmult_0_r x : x * 0 = 0.
Proof. ring. Qed.
536 537
Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc.
Proof. ring. Qed.
538
Lemma Qcle_ngt (x y : Qc) : x  y  ¬y < x.
539
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
540
Lemma Qclt_nge (x y : Qc) : x < y  ¬y  x.
541
Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
542
Lemma Qcplus_le_mono_l (x y z : Qc) : x  y  z + x  z + y.
543 544
Proof.
  split; intros.
545 546
  - by apply Qcplus_le_compat.
  - replace x with ((0 - z) + (z + x)) by ring.
547
    replace y with ((0 - z) + (z + y)) by ring.
548 549
    by apply Qcplus_le_compat.
Qed.
550
Lemma Qcplus_le_mono_r (x y z : Qc) : x  y  x + z  y + z.
551
Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
552
Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y  z + x < z + y.
553
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
554
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y  x + z < y + z.
555
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
556
Instance Qcopp_inj : Inj (=) (=) Qcopp.
557 558 559
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
560
Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
561
Proof.
562
  intros x y H. by apply (anti_symm ());rewrite (Qcplus_le_mono_l _ _ z), H.
563
Qed.
564
Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
565
Proof.
566
  intros x y H. by apply (anti_symm ()); rewrite (Qcplus_le_mono_r _ _ z), H.
567
Qed.
568 569 570 571 572 573 574 575 576 577 578
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.
579
  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
580 581 582 583 584 585 586 587 588 589 590 591 592
  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.
593
  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
594 595
  by apply Qcplus_le_mono_l.
Qed.
596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
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.
619
  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
620 621 622 623 624 625 626 627
  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.
628 629 630 631
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.
632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650
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.
651
Close Scope Qc_scope.
652 653 654 655 656

(** * 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 }.
657
Hint Resolve Qp_prf : core.
658 659
Delimit Scope Qp_scope with Qp.
Bind Scope Qp_scope with Qp.
660
Arguments Qp_car _%Qp : assert.
661 662 663 664 665 666 667

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.
668 669
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.
670 671

Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _.
672
Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
673
  intros x y. unfold Qcdiv. assert (0 < Zpos y)%Qc.
674 675
  { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. }
  by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l,
676 677 678 679 680
    <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r.
Qed.

Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
681
Infix "*" := Qp_mult : Qp_scope.
682
Infix "/" := Qp_div : Qp_scope.
683 684 685 686
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.
687 688 689 690 691 692

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
693 694 695 696 697 698 699

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.

700 701 702 703
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.
704 705 706 707
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.
708 709

Lemma Qp_minus_diag x : (x - x)%Qp = None.
Ralf Jung's avatar
Ralf Jung committed
710
Proof. unfold Qp_minus, Qcminus. by rewrite Qcplus_opp_r. Qed.
711 712
Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y.
Proof.
Ralf Jung's avatar
Ralf Jung committed
713
  unfold Qp_minus, Qcminus; simpl.
714 715 716 717
  rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r.
  destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq.
Qed.

718 719 720 721 722 723 724 725 726 727 728 729 730
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.

731 732 733 734 735 736 737
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
738
  apply Qp_eq; simpl. unfold Qcdiv.
739 740 741 742 743 744 745
  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.
746 747 748 749 750 751
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.
752

Robbert Krebbers's avatar
Robbert Krebbers committed
753 754 755 756
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
757
    unfold Qcminus. by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
758 759 760 761
  - intros [z ->]; simpl.
    rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf.
Qed.

762 763 764 765 766 767 768 769
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
770
  assert (0 < q2 +- q1 */ 2)%Qc as Hq2'.
771
  { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq].
Ralf Jung's avatar
Ralf Jung committed
772 773 774 775
    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.
776
Qed.
777

778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797
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
798 799 800
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
801
  - assert (0 < p +- r)%Qc as Hpos.
Robbert Krebbers's avatar
Robbert Krebbers committed
802 803 804 805 806 807 808 809 810 811 812
    { 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
813
Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp  1%Qp)%Qc.
814 815 816
Proof.
  intros Hle.
  apply (Qcplus_le_mono_l q 0 1) in Hle.
Zhen Zhang's avatar
Zhen Zhang committed
817
  apply Qcle_ngt in Hle. apply Hle, Qp_prf.
818
Qed.
Zhen Zhang's avatar
Zhen Zhang committed
819 820 821

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