numbers.v 26.9 KB
 Robbert Krebbers committed Mar 15, 2017 1 ``````(* Copyright (c) 2012-2017, Coq-std++ developers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 ``````(* This file is distributed under the terms of the BSD license. *) `````` Robbert Krebbers committed Oct 19, 2012 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. *) `````` Robbert Krebbers committed Aug 22, 2016 6 ``````From Coq Require Export EqdepFacts PArith NArith ZArith NPeano. `````` Robbert Krebbers committed Feb 13, 2016 7 8 ``````From Coq Require Import QArith Qcanon. From stdpp Require Export base decidable option. `````` Ralf Jung committed Jan 31, 2017 9 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Feb 19, 2013 10 ``````Open Scope nat_scope. `````` Robbert Krebbers committed Jun 11, 2012 11 `````` `````` Robbert Krebbers committed Feb 01, 2013 12 ``````Coercion Z.of_nat : nat >-> Z. `````` Robbert Krebbers committed Sep 20, 2016 13 ``````Instance comparison_eq_dec : EqDecision comparison. `````` Robbert Krebbers committed Feb 26, 2016 14 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Feb 01, 2013 15 `````` `````` Robbert Krebbers committed Feb 19, 2013 16 ``````(** * Notations and properties of [nat] *) `````` Robbert Krebbers committed Sep 08, 2017 17 ``````Arguments minus !_ !_ / : assert. `````` Robbert Krebbers committed Nov 12, 2012 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). `````` Robbert Krebbers committed May 02, 2014 22 23 ``````Reserved Notation "x ≤ y ≤ z ≤ z'" (at level 70, y at next level, z at next level). `````` Robbert Krebbers committed Nov 12, 2012 24 `````` `````` Robbert Krebbers committed Aug 21, 2012 25 ``````Infix "≤" := le : nat_scope. `````` Robbert Krebbers committed Nov 12, 2012 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. `````` Robbert Krebbers committed May 02, 2014 29 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_scope. `````` Robbert Krebbers committed Nov 12, 2012 30 31 32 ``````Notation "(≤)" := le (only parsing) : nat_scope. Notation "(<)" := lt (only parsing) : nat_scope. `````` Robbert Krebbers committed Feb 01, 2017 33 34 ``````Infix "`div`" := Nat.div (at level 35) : nat_scope. Infix "`mod`" := Nat.modulo (at level 35) : nat_scope. `````` Robbert Krebbers committed Jul 03, 2016 35 36 ``````Infix "`max`" := Nat.max (at level 35) : nat_scope. Infix "`min`" := Nat.min (at level 35) : nat_scope. `````` Robbert Krebbers committed Nov 12, 2012 37 `````` `````` Robbert Krebbers committed Sep 20, 2016 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. `````` Robbert Krebbers committed Jan 05, 2013 41 ``````Instance nat_inhabited: Inhabited nat := populate 0%nat. `````` Robbert Krebbers committed Sep 20, 2016 42 ``````Instance S_inj: Inj (=) (=) S. `````` Robbert Krebbers committed Jun 17, 2013 43 ``````Proof. by injection 1. Qed. `````` Robbert Krebbers committed Sep 20, 2016 44 ``````Instance nat_le_po: PartialOrder (≤). `````` Robbert Krebbers committed Jun 17, 2013 45 ``````Proof. repeat split; repeat intro; auto with lia. Qed. `````` Robbert Krebbers committed Oct 19, 2012 46 `````` `````` Robbert Krebbers committed May 07, 2013 47 48 49 50 ``````Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y). Proof. assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'), y = y' → eq_dep nat (le x) y p y' q) as aux. `````` Robbert Krebbers committed Apr 27, 2018 51 `````` { fix FIX 3. intros x ? [|y p] ? [|y' q]. `````` Robbert Krebbers committed Feb 17, 2016 52 `````` - done. `````` Robbert Krebbers committed Apr 27, 2018 53 54 55 `````` - clear FIX. intros; exfalso; auto with lia. - clear FIX. intros; exfalso; auto with lia. - injection 1. intros Hy. by case (FIX x y p y' q Hy). } `````` Robbert Krebbers committed May 07, 2013 56 `````` intros x y p q. `````` Robbert Krebbers committed Feb 13, 2016 57 `````` by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux. `````` Robbert Krebbers committed May 07, 2013 58 59 60 61 ``````Qed. Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y). Proof. apply _. Qed. `````` Robbert Krebbers committed Mar 11, 2017 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 committed Jan 05, 2013 64 `````` `````` Robbert Krebbers committed Jun 17, 2013 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 : `````` Robbert Krebbers committed May 07, 2013 68 69 `````` x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2. Proof. `````` Robbert Krebbers committed Jun 17, 2013 70 `````` intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |]. `````` Robbert Krebbers committed May 07, 2013 71 72 `````` revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia. Qed. `````` Robbert Krebbers committed Jun 17, 2013 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. `````` Robbert Krebbers committed May 07, 2013 76 `````` `````` Robbert Krebbers committed May 02, 2014 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. `````` Robbert Krebbers committed Nov 15, 2014 81 ``````Proof. `````` 82 `````` refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff. `````` Robbert Krebbers committed Nov 15, 2014 83 ``````Defined. `````` Robbert Krebbers committed May 02, 2014 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. `````` Robbert Krebbers committed Aug 04, 2016 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 committed Mar 11, 2017 96 ``````Lemma Nat_iter_ind {A} (P : A → Prop) f x k : `````` Robbert Krebbers committed Mar 09, 2017 97 98 `````` P x → (∀ y, P y → P (f y)) → P (Nat.iter k f x). Proof. induction k; simpl; auto. Qed. `````` Robbert Krebbers committed Aug 04, 2016 99 `````` `````` Robbert Krebbers committed Mar 11, 2017 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). `````` Robbert Krebbers committed Feb 19, 2013 116 117 118 ``````(** * Notations and properties of [positive] *) Open Scope positive_scope. `````` Robbert Krebbers committed Jun 17, 2013 119 ``````Infix "≤" := Pos.le : positive_scope. `````` Robbert Krebbers committed May 02, 2014 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. `````` Robbert Krebbers committed Jun 17, 2013 124 125 ``````Notation "(≤)" := Pos.le (only parsing) : positive_scope. Notation "(<)" := Pos.lt (only parsing) : positive_scope. `````` Robbert Krebbers committed Jun 11, 2012 126 127 128 ``````Notation "(~0)" := xO (only parsing) : positive_scope. Notation "(~1)" := xI (only parsing) : positive_scope. `````` Robbert Krebbers committed Feb 26, 2016 129 130 131 ``````Arguments Pos.of_nat : simpl never. Arguments Pmult : simpl never. `````` Robbert Krebbers committed Sep 20, 2016 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. `````` Robbert Krebbers committed Jun 17, 2013 137 138 ``````Instance positive_inhabited: Inhabited positive := populate 1. `````` Robbert Krebbers committed Dec 11, 2015 139 ``````Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end. `````` Robbert Krebbers committed Mar 11, 2017 140 141 ``````Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end. Instance xO_inj : Inj (=) (=) (~0). `````` Robbert Krebbers committed Jan 05, 2013 142 ``````Proof. by injection 1. Qed. `````` Robbert Krebbers committed Mar 11, 2017 143 ``````Instance xI_inj : Inj (=) (=) (~1). `````` Robbert Krebbers committed Jan 05, 2013 144 145 ``````Proof. by injection 1. Qed. `````` Robbert Krebbers committed Feb 19, 2013 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 committed Mar 11, 2017 168 ``````Global Instance Papp_1_l : LeftId (=) 1 (++). `````` Robbert Krebbers committed Feb 17, 2016 169 ``````Proof. intros p. by induction p; intros; f_equal/=. Qed. `````` Robbert Krebbers committed Mar 11, 2017 170 ``````Global Instance Papp_1_r : RightId (=) 1 (++). `````` Robbert Krebbers committed Feb 19, 2013 171 ``````Proof. done. Qed. `````` Robbert Krebbers committed Mar 11, 2017 172 ``````Global Instance Papp_assoc : Assoc (=) (++). `````` Robbert Krebbers committed Feb 17, 2016 173 ``````Proof. intros ?? p. by induction p; intros; f_equal/=. Qed. `````` Robbert Krebbers committed Mar 11, 2017 174 175 ``````Global Instance Papp_inj p : Inj (=) (=) (++ p). Proof. intros ???. induction p; simplify_eq; auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 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. `````` Robbert Krebbers committed Dec 08, 2015 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. `````` Robbert Krebbers committed Feb 17, 2016 184 185 `````` - apply (IH _ (_~1)). - apply (IH _ (_~0)). `````` Robbert Krebbers committed Feb 19, 2013 186 ``````Qed. `````` Robbert Krebbers committed Dec 08, 2015 187 ``````Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1. `````` Robbert Krebbers committed Feb 19, 2013 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 := `````` Robbert Krebbers committed May 02, 2014 195 `````` match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end. `````` Robbert Krebbers committed Dec 08, 2015 196 ``````Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat. `````` Robbert Krebbers committed Feb 17, 2016 197 ``````Proof. by induction p2; f_equal/=. Qed. `````` Robbert Krebbers committed Feb 19, 2013 198 `````` `````` Robbert Krebbers committed Mar 11, 2017 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. `````` Robbert Krebbers committed Feb 19, 2013 206 207 208 ``````Close Scope positive_scope. (** * Notations and properties of [N] *) `````` Robbert Krebbers committed Jun 11, 2012 209 ``````Infix "≤" := N.le : N_scope. `````` Robbert Krebbers committed Nov 12, 2012 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. `````` Robbert Krebbers committed May 02, 2014 213 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope. `````` Robbert Krebbers committed Jun 11, 2012 214 ``````Notation "(≤)" := N.le (only parsing) : N_scope. `````` Robbert Krebbers committed Oct 19, 2012 215 ``````Notation "(<)" := N.lt (only parsing) : N_scope. `````` Robbert Krebbers committed Nov 12, 2012 216 217 218 ``````Infix "`div`" := N.div (at level 35) : N_scope. Infix "`mod`" := N.modulo (at level 35) : N_scope. `````` Robbert Krebbers committed Sep 08, 2017 219 ``````Arguments N.add : simpl never. `````` Robbert Krebbers committed Jun 16, 2014 220 `````` `````` Robbert Krebbers committed Mar 11, 2017 221 ``````Instance Npos_inj : Inj (=) (=) Npos. `````` Robbert Krebbers committed Jan 05, 2013 222 223 ``````Proof. by injection 1. Qed. `````` Robbert Krebbers committed Sep 20, 2016 224 ``````Instance N_eq_dec: EqDecision N := N.eq_dec. `````` 225 ``````Program Instance N_le_dec : RelDecision N.le := λ x y, `````` Robbert Krebbers committed Mar 08, 2018 226 `````` match N.compare x y with Gt => right _ | _ => left _ end. `````` Robbert Krebbers committed Jan 12, 2016 227 ``````Solve Obligations with naive_solver. `````` 228 ``````Program Instance N_lt_dec : RelDecision N.lt := λ x y, `````` Robbert Krebbers committed Mar 08, 2018 229 `````` match N.compare x y with Lt => left _ | _ => right _ end. `````` Robbert Krebbers committed Jan 12, 2016 230 ``````Solve Obligations with naive_solver. `````` Robbert Krebbers committed Jan 05, 2013 231 ``````Instance N_inhabited: Inhabited N := populate 1%N. `````` Robbert Krebbers committed Sep 20, 2016 232 ``````Instance N_le_po: PartialOrder (≤)%N. `````` Robbert Krebbers committed Aug 12, 2013 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 committed Jun 11, 2012 237 `````` `````` Robbert Krebbers committed Feb 19, 2013 238 ``````(** * Notations and properties of [Z] *) `````` Robbert Krebbers committed Jun 17, 2013 239 240 ``````Open Scope Z_scope. `````` Robbert Krebbers committed Jun 11, 2012 241 ``````Infix "≤" := Z.le : Z_scope. `````` Robbert Krebbers committed Jun 17, 2013 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. `````` Robbert Krebbers committed May 02, 2014 246 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope. `````` Robbert Krebbers committed Jun 11, 2012 247 ``````Notation "(≤)" := Z.le (only parsing) : Z_scope. `````` Robbert Krebbers committed Oct 19, 2012 248 ``````Notation "(<)" := Z.lt (only parsing) : Z_scope. `````` Robbert Krebbers committed Nov 12, 2012 249 `````` `````` Robbert Krebbers committed Jan 05, 2013 250 251 ``````Infix "`div`" := Z.div (at level 35) : Z_scope. Infix "`mod`" := Z.modulo (at level 35) : Z_scope. `````` Robbert Krebbers committed Mar 14, 2013 252 253 ``````Infix "`quot`" := Z.quot (at level 35) : Z_scope. Infix "`rem`" := Z.rem (at level 35) : Z_scope. `````` Robbert Krebbers committed Jun 17, 2013 254 255 ``````Infix "≪" := Z.shiftl (at level 35) : Z_scope. Infix "≫" := Z.shiftr (at level 35) : Z_scope. `````` Robbert Krebbers committed Jan 05, 2013 256 `````` `````` Robbert Krebbers committed Aug 04, 2016 257 ``````Instance Zpos_inj : Inj (=) (=) Zpos. `````` Robbert Krebbers committed May 02, 2014 258 ``````Proof. by injection 1. Qed. `````` Robbert Krebbers committed Aug 04, 2016 259 ``````Instance Zneg_inj : Inj (=) (=) Zneg. `````` Robbert Krebbers committed May 02, 2014 260 261 ``````Proof. by injection 1. Qed. `````` Robbert Krebbers committed Aug 04, 2016 262 263 264 ``````Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat. Proof. intros n1 n2. apply Nat2Z.inj. Qed. `````` Robbert Krebbers committed Sep 20, 2016 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. `````` Robbert Krebbers committed Jun 17, 2013 268 ``````Instance Z_inhabited: Inhabited Z := populate 1. `````` Robbert Krebbers committed Sep 20, 2016 269 ``````Instance Z_le_po : PartialOrder (≤). `````` Robbert Krebbers committed Aug 12, 2013 270 271 272 ``````Proof. repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm. Qed. `````` Robbert Krebbers committed Jun 17, 2013 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 |]. `````` Ralf Jung committed Feb 20, 2016 283 `````` split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia. `````` Robbert Krebbers committed Jun 17, 2013 284 ``````Qed. `````` Robbert Krebbers committed Jun 11, 2012 285 `````` `````` Robbert Krebbers committed Mar 14, 2013 286 ``````(* Note that we cannot disable simpl for [Z.of_nat] as that would break `````` Robbert Krebbers committed Jun 17, 2013 287 ``````tactics as [lia]. *) `````` Robbert Krebbers committed Sep 08, 2017 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. `````` Robbert Krebbers committed Mar 14, 2013 297 `````` `````` Robbert Krebbers committed Aug 26, 2014 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. `````` Robbert Krebbers committed May 07, 2013 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. `````` Robbert Krebbers committed Jun 17, 2013 308 309 ``````Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos. Hint Resolve Z_mod_pos Z.div_pos : zpos. `````` Robbert Krebbers committed May 07, 2013 310 311 ``````Hint Extern 1000 => lia : zpos. `````` Robbert Krebbers committed Feb 01, 2015 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. `````` Robbert Krebbers committed Jun 17, 2013 314 315 ``````Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y. Proof. `````` Robbert Krebbers committed Feb 01, 2015 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. `````` Robbert Krebbers committed Jun 17, 2013 319 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2015 320 321 322 ``````Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat. Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 323 `````` - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i). `````` Robbert Krebbers committed Feb 01, 2015 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. `````` Robbert Krebbers committed Feb 17, 2016 327 `````` - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul. `````` Robbert Krebbers committed Feb 01, 2015 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. `````` Robbert Krebbers committed Jun 17, 2013 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. `````` Johannes Kloos committed Oct 31, 2017 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. *) `````` Robbert Krebbers committed Feb 19, 2013 358 ``````(** * Notations and properties of [Qc] *) `````` Robbert Krebbers committed Aug 21, 2013 359 ``````Open Scope Qc_scope. `````` Robbert Krebbers committed May 02, 2014 360 361 ``````Delimit Scope Qc_scope with Qc. Notation "1" := (Q2Qc 1) : Qc_scope. `````` Robbert Krebbers committed Aug 21, 2013 362 ``````Notation "2" := (1+1) : Qc_scope. `````` Robbert Krebbers committed May 02, 2014 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. `````` Robbert Krebbers committed Feb 19, 2013 367 ``````Infix "≤" := Qcle : Qc_scope. `````` Robbert Krebbers committed Aug 21, 2013 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. `````` Robbert Krebbers committed May 02, 2014 372 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope. `````` Robbert Krebbers committed Feb 19, 2013 373 374 375 ``````Notation "(≤)" := Qcle (only parsing) : Qc_scope. Notation "(<)" := Qclt (only parsing) : Qc_scope. `````` Robbert Krebbers committed May 02, 2014 376 ``````Hint Extern 1 (_ ≤ _) => reflexivity || discriminate. `````` Robbert Krebbers committed Sep 08, 2017 377 ``````Arguments Qred : simpl never. `````` Robbert Krebbers committed May 02, 2014 378 `````` `````` Robbert Krebbers committed Sep 20, 2016 379 ``````Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec. `````` 380 ``````Program Instance Qc_le_dec: RelDecision Qcle := λ x y, `````` Robbert Krebbers committed Feb 19, 2013 381 `````` if Qclt_le_dec y x then right _ else left _. `````` Robbert Krebbers committed Jan 12, 2016 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, `````` Robbert Krebbers committed Feb 19, 2013 385 `````` if Qclt_le_dec x y then left _ else right _. `````` Robbert Krebbers committed Jan 12, 2016 386 387 ``````Solve Obligations with done. Next Obligation. intros x y; apply Qcle_not_lt. Qed. `````` Robbert Krebbers committed Feb 19, 2013 388 `````` `````` Robbert Krebbers committed Aug 21, 2013 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. `````` Robbert Krebbers committed May 02, 2014 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. `````` Robbert Krebbers committed Feb 26, 2016 401 402 ``````Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc. Proof. ring. Qed. `````` Robbert Krebbers committed Aug 21, 2013 403 ``````Lemma Qcle_ngt (x y : Qc) : x ≤ y ↔ ¬y < x. `````` Robbert Krebbers committed Feb 19, 2013 404 ``````Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed. `````` Robbert Krebbers committed Aug 21, 2013 405 ``````Lemma Qclt_nge (x y : Qc) : x < y ↔ ¬y ≤ x. `````` Robbert Krebbers committed Feb 19, 2013 406 ``````Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed. `````` Robbert Krebbers committed Aug 21, 2013 407 ``````Lemma Qcplus_le_mono_l (x y z : Qc) : x ≤ y ↔ z + x ≤ z + y. `````` Robbert Krebbers committed Feb 19, 2013 408 409 ``````Proof. split; intros. `````` Robbert Krebbers committed Feb 17, 2016 410 411 `````` - by apply Qcplus_le_compat. - replace x with ((0 - z) + (z + x)) by ring. `````` Robbert Krebbers committed Aug 21, 2013 412 `````` replace y with ((0 - z) + (z + y)) by ring. `````` Robbert Krebbers committed Feb 19, 2013 413 414 `````` by apply Qcplus_le_compat. Qed. `````` Robbert Krebbers committed Aug 21, 2013 415 ``````Lemma Qcplus_le_mono_r (x y z : Qc) : x ≤ y ↔ x + z ≤ y + z. `````` Robbert Krebbers committed Feb 19, 2013 416 ``````Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed. `````` Robbert Krebbers committed Aug 21, 2013 417 ``````Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y ↔ z + x < z + y. `````` Robbert Krebbers committed Feb 19, 2013 418 ``````Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed. `````` Robbert Krebbers committed Aug 21, 2013 419 ``````Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y ↔ x + z < y + z. `````` Robbert Krebbers committed Feb 19, 2013 420 ``````Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed. `````` Robbert Krebbers committed Apr 05, 2018 421 ``````Instance Qcopp_inj : Inj (=) (=) Qcopp. `````` Robbert Krebbers committed Aug 21, 2013 422 423 424 ``````Proof. intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive. Qed. `````` Robbert Krebbers committed Apr 05, 2018 425 ``````Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z). `````` Robbert Krebbers committed Aug 21, 2013 426 ``````Proof. `````` Robbert Krebbers committed Apr 05, 2018 427 `````` intros x y H. by apply (anti_symm (≤));rewrite (Qcplus_le_mono_l _ _ z), H. `````` Robbert Krebbers committed Aug 21, 2013 428 ``````Qed. `````` Robbert Krebbers committed Apr 05, 2018 429 ``````Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z). `````` Robbert Krebbers committed May 02, 2014 430 ``````Proof. `````` Robbert Krebbers committed Apr 05, 2018 431 `````` intros x y H. by apply (anti_symm (≤)); rewrite (Qcplus_le_mono_r _ _ z), H. `````` Robbert Krebbers committed May 02, 2014 432 ``````Qed. `````` Robbert Krebbers committed Aug 21, 2013 433 434 435 436 437 438 439 440 441 442 443 ``````Lemma Qcplus_pos_nonneg (x y : Qc) : 0 < x → 0 ≤ y → 0 < x + y. Proof. intros. apply Qclt_le_trans with (x + 0); [by rewrite Qcplus_0_r|]. by apply Qcplus_le_mono_l. Qed. Lemma Qcplus_nonneg_pos (x y : Qc) : 0 ≤ x → 0 < y → 0 < x + y. Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed. Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y. Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed. Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 ≤ x → 0 ≤ y → 0 ≤ x + y. Proof. `````` Ralf Jung committed Feb 20, 2016 444 `````` intros. trans (x + 0); [by rewrite Qcplus_0_r|]. `````` Robbert Krebbers committed Aug 21, 2013 445 446 447 448 449 450 451 452 453 454 455 456 457 `````` by apply Qcplus_le_mono_l. Qed. Lemma Qcplus_neg_nonpos (x y : Qc) : x < 0 → y ≤ 0 → x + y < 0. Proof. intros. apply Qcle_lt_trans with (x + 0); [|by rewrite Qcplus_0_r]. by apply Qcplus_le_mono_l. Qed. Lemma Qcplus_nonpos_neg (x y : Qc) : x ≤ 0 → y < 0 → x + y < 0. Proof. rewrite (Qcplus_comm x). auto using Qcplus_neg_nonpos. Qed. Lemma Qcplus_neg_neg (x y : Qc) : x < 0 → y < 0 → x + y < 0. Proof. auto using Qcplus_nonpos_neg, Qclt_le_weak. Qed. Lemma Qcplus_nonpos_nonpos (x y : Qc) : x ≤ 0 → y ≤ 0 → x + y ≤ 0. Proof. `````` Ralf Jung committed Feb 20, 2016 458 `````` intros. trans (x + 0); [|by rewrite Qcplus_0_r]. `````` Robbert Krebbers committed Aug 21, 2013 459 460 `````` by apply Qcplus_le_mono_l. Qed. `````` Robbert Krebbers committed May 02, 2014 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 ``````Lemma Qcmult_le_mono_nonneg_l x y z : 0 ≤ z → x ≤ y → z * x ≤ z * y. Proof. intros. rewrite !(Qcmult_comm z). by apply Qcmult_le_compat_r. Qed. Lemma Qcmult_le_mono_nonneg_r x y z : 0 ≤ z → x ≤ y → x * z ≤ y * z. Proof. intros. by apply Qcmult_le_compat_r. Qed. Lemma Qcmult_le_mono_pos_l x y z : 0 < z → x ≤ y ↔ z * x ≤ z * y. Proof. split; auto using Qcmult_le_mono_nonneg_l, Qclt_le_weak. rewrite !Qcle_ngt, !(Qcmult_comm z). intuition auto using Qcmult_lt_compat_r. Qed. Lemma Qcmult_le_mono_pos_r x y z : 0 < z → x ≤ y ↔ x * z ≤ y * z. Proof. rewrite !(Qcmult_comm _ z). by apply Qcmult_le_mono_pos_l. Qed. Lemma Qcmult_lt_mono_pos_l x y z : 0 < z → x < y ↔ z * x < z * y. Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_l. Qed. Lemma Qcmult_lt_mono_pos_r x y z : 0 < z → x < y ↔ x * z < y * z. Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_r. Qed. Lemma Qcmult_pos_pos x y : 0 < x → 0 < y → 0 < x * y. Proof. intros. apply Qcle_lt_trans with (0 * y); [by rewrite Qcmult_0_l|]. by apply Qcmult_lt_mono_pos_r. Qed. Lemma Qcmult_nonneg_nonneg x y : 0 ≤ x → 0 ≤ y → 0 ≤ x * y. Proof. `````` Ralf Jung committed Feb 20, 2016 484 `````` intros. trans (0 * y); [by rewrite Qcmult_0_l|]. `````` Robbert Krebbers committed May 02, 2014 485 486 487 488 489 490 491 492 `````` by apply Qcmult_le_mono_nonneg_r. Qed. Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n. Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed. Coercion Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n). Lemma Z2Qc_inj_0 : Qc_of_Z 0 = 0. Proof. by apply Qc_is_canon. Qed. `````` Robbert Krebbers committed Feb 26, 2016 493 494 495 496 ``````Lemma Z2Qc_inj_1 : Qc_of_Z 1 = 1. Proof. by apply Qc_is_canon. Qed. Lemma Z2Qc_inj_2 : Qc_of_Z 2 = 2. Proof. by apply Qc_is_canon. Qed. `````` Robbert Krebbers committed May 02, 2014 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 ``````Lemma Z2Qc_inj n m : Qc_of_Z n = Qc_of_Z m → n = m. Proof. by injection 1. Qed. Lemma Z2Qc_inj_iff n m : Qc_of_Z n = Qc_of_Z m ↔ n = m. Proof. split. auto using Z2Qc_inj. by intros ->. Qed. Lemma Z2Qc_inj_le n m : (n ≤ m)%Z ↔ Qc_of_Z n ≤ Qc_of_Z m. Proof. by rewrite Zle_Qle. Qed. Lemma Z2Qc_inj_lt n m : (n < m)%Z ↔ Qc_of_Z n < Qc_of_Z m. Proof. by rewrite Zlt_Qlt. Qed. Lemma Z2Qc_inj_add n m : Qc_of_Z (n + m) = Qc_of_Z n + Qc_of_Z m. Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_plus. Qed. Lemma Z2Qc_inj_mul n m : Qc_of_Z (n * m) = Qc_of_Z n * Qc_of_Z m. Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_mult. Qed. Lemma Z2Qc_inj_opp n : Qc_of_Z (-n) = -Qc_of_Z n. Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_opp. Qed. Lemma Z2Qc_inj_sub n m : Qc_of_Z (n - m) = Qc_of_Z n - Qc_of_Z m. Proof. apply Qc_is_canon; simpl. by rewrite !Qred_correct, <-inject_Z_opp, <-inject_Z_plus. Qed. `````` Robbert Krebbers committed Aug 21, 2013 516 ``````Close Scope Qc_scope. `````` Robbert Krebbers committed Feb 26, 2016 517 518 519 520 521 522 523 524 `````` (** * Positive rationals *) (** The theory of positive rationals is very incomplete. We merely provide some operations and theorems that are relevant for fractional permissions. *) Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }. Hint Resolve Qp_prf. Delimit Scope Qp_scope with Qp. Bind Scope Qp_scope with Qp. `````` Robbert Krebbers committed Sep 08, 2017 525 ``````Arguments Qp_car _%Qp : assert. `````` Robbert Krebbers committed Feb 26, 2016 526 527 528 529 530 531 532 `````` Definition Qp_one : Qp := mk_Qp 1 eq_refl. Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _. Next Obligation. by intros x y; apply Qcplus_pos_pos. Qed. Definition Qp_minus (x y : Qp) : option Qp := let z := (x - y)%Qc in match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end. `````` Jacques-Henri Jourdan committed Nov 07, 2016 533 534 ``````Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _. Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed. `````` Robbert Krebbers committed Nov 21, 2017 535 536 `````` Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _. `````` Robbert Krebbers committed Feb 26, 2016 537 ``````Next Obligation. `````` Robbert Krebbers committed Nov 21, 2017 538 539 540 `````` intros x y. assert (0 < Zpos y)%Qc. { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. } by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l, `````` Robbert Krebbers committed Feb 26, 2016 541 542 543 544 545 `````` <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r. Qed. Infix "+" := Qp_plus : Qp_scope. Infix "-" := Qp_minus : Qp_scope. `````` Jacques-Henri Jourdan committed Nov 07, 2016 546 ``````Infix "*" := Qp_mult : Qp_scope. `````` Robbert Krebbers committed Feb 26, 2016 547 ``````Infix "/" := Qp_div : Qp_scope. `````` Robbert Krebbers committed May 23, 2018 548 549 550 551 ``````Notation "1" := Qp_one : Qp_scope. Notation "2" := (1 + 1)%Qp : Qp_scope. Notation "3" := (1 + 2)%Qp : Qp_scope. Notation "4" := (1 + 3)%Qp : Qp_scope. `````` Robbert Krebbers committed Feb 26, 2016 552 553 554 555 556 557 `````` Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y. Proof. split; [by intros ->|]. destruct x, y; intros; simplify_eq/=; f_equal; apply (proof_irrel _). Qed. `````` Robbert Krebbers committed Nov 16, 2016 558 559 560 561 562 563 564 `````` Instance Qp_inhabited : Inhabited Qp := populate 1%Qp. Instance Qp_eq_dec : EqDecision Qp. Proof. refine (λ x y, cast_if (decide (Qp_car x = Qp_car y))); by rewrite Qp_eq. Defined. `````` Robbert Krebbers committed Feb 26, 2016 565 566 567 568 ``````Instance Qp_plus_assoc : Assoc (=) Qp_plus. Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed. Instance Qp_plus_comm : Comm (=) Qp_plus. Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed. `````` Robbert Krebbers committed Apr 05, 2018 569 570 571 572 ``````Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p). Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj _). Qed. Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp. Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed. `````` Robbert Krebbers committed Feb 26, 2016 573 574 575 576 577 578 579 580 581 582 `````` Lemma Qp_minus_diag x : (x - x)%Qp = None. Proof. unfold Qp_minus. by rewrite Qcplus_opp_r. Qed. Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y. Proof. unfold Qp_minus; simpl. rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r. destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq. Qed. `````` Jacques-Henri Jourdan committed Nov 07, 2016 583 584 585 586 587 588 589 590 591 592 593 594 595 ``````Instance Qp_mult_assoc : Assoc (=) Qp_mult. Proof. intros x y z; apply Qp_eq, Qcmult_assoc. Qed. Instance Qp_mult_comm : Comm (=) Qp_mult. Proof. intros x y; apply Qp_eq, Qcmult_comm. Qed. Lemma Qp_mult_plus_distr_r x y z: (x * (y + z) = x * y + x * z)%Qp. Proof. apply Qp_eq, Qcmult_plus_distr_r. Qed. Lemma Qp_mult_plus_distr_l x y z: ((x + y) * z = x * z + y * z)%Qp. Proof. apply Qp_eq, Qcmult_plus_distr_l. Qed. Lemma Qp_mult_1_l x: (1 * x)%Qp = x. Proof. apply Qp_eq, Qcmult_1_l. Qed. Lemma Qp_mult_1_r x: (x * 1)%Qp = x. Proof. apply Qp_eq, Qcmult_1_r. Qed. `````` Robbert Krebbers committed Feb 26, 2016 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 ``````Lemma Qp_div_1 x : (x / 1 = x)%Qp. Proof. apply Qp_eq; simpl. rewrite <-(Qcmult_div_r x 1) at 2 by done. by rewrite Qcmult_1_l. Qed. Lemma Qp_div_S x y : (x / (2 * y) + x / (2 * y) = x / y)%Qp. Proof. apply Qp_eq; simpl. rewrite <-Qcmult_plus_distr_l, Pos2Z.inj_mul, Z2Qc_inj_mul, Z2Qc_inj_2. rewrite Qcplus_diag. by field_simplify. Qed. Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp. Proof. change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1. Qed. `````` Robbert Krebbers committed May 23, 2018 611 612 613 614 615 616 ``````Lemma Qp_half_half : (1 / 2 + 1 / 2 = 1)%Qp. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_quarter_three_quarter : (1 / 4 + 3 / 4 = 1)%Qp. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_three_quarter_quarter : (3 / 4 + 1 / 4 = 1)%Qp. Proof. apply (bool_decide_unpack _); by compute. Qed. `````` Jacques-Henri Jourdan committed Sep 09, 2016 617 `````` `````` Robbert Krebbers committed Mar 11, 2017 618 619 620 621 622 623 624 625 626 ``````Lemma Qp_lt_sum (x y : Qp) : (x < y)%Qc ↔ ∃ z, y = (x + z)%Qp. Proof. split. - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl. by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l. - intros [z ->]; simpl. rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf. Qed. `````` Robbert Krebbers committed Sep 09, 2016 627 628 629 630 631 632 633 634 635 636 637 638 639 640 ``````Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp. Proof. revert q1 q2. cut (∀ q1 q2 : Qp, (q1 ≤ q2)%Qc → ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp). { intros help q1 q2. destruct (Qc_le_dec q1 q2) as [LE|LE%Qclt_nge%Qclt_le_weak]; [by eauto|]. destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto. } intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp. assert (0 < q2 - q1 / 2)%Qc as Hq2'. { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq]. replace (q1 - q1 / 2)%Qc with (q1 * (1 - 1/2))%Qc by ring. replace 0%Qc with (0 * (1-1/2))%Qc by ring. by apply Qcmult_lt_compat_r. } exists (mk_Qp (q2 - q1 / 2%Z) Hq2'). split; [by rewrite Qp_div_2|]. apply Qp_eq; simpl. ring. `````` Jacques-Henri Jourdan committed Sep 09, 2016 641 ``````Qed. `````` Zhen Zhang committed Oct 04, 2016 642 `````` `````` Robbert Krebbers committed Apr 05, 2018 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 ``````Lemma Qp_cross_split p a b c d : (a + b = p → c + d = p → ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp. Proof. intros H <-. revert a b c d H. cut (∀ a b c d : Qp, (a < c)%Qc → a + b = c + d → ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp. { intros help a b c d ?. destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq]. - auto. - destruct (help c d a b); [done..|]. naive_solver. - apply (inj _) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->). eauto 10 using (comm_L Qp_plus). } intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj _). destruct (Qp_lower_bound a d) as (q&a'&d'&->&->). eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus). - by rewrite (assoc_L _), (comm_L Qp_plus e). - by rewrite (assoc_L _), (comm_L Qp_plus a'). Qed. `````` Robbert Krebbers committed Jun 10, 2018 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 ``````Lemma Qp_bounded_split (p r : Qp) : ∃ q1 q2 : Qp, (q1 ≤ r)%Qc ∧ p = (q1 + q2)%Qp. Proof. destruct (Qclt_le_dec r p) as [?|?]. - assert (0 < p - r)%Qc as Hpos. { apply (Qcplus_lt_mono_r _ _ r). rewrite <-Qcplus_assoc, (Qcplus_comm (-r)). by rewrite Qcplus_opp_r, Qcplus_0_l, Qcplus_0_r. } exists r, (mk_Qp _ Hpos); simpl; split; [done|]. apply Qp_eq; simpl. rewrite Qcplus_comm, <-Qcplus_assoc, (Qcplus_comm (-r)). by rewrite Qcplus_opp_r, Qcplus_0_r. - exists (p / 2)%Qp, (p / 2)%Qp; split. + trans p; [|done]. apply Qclt_le_weak, Qp_lt_sum. exists (p / 2)%Qp. by rewrite Qp_div_2. + by rewrite Qp_div_2. Qed. `````` Zhen Zhang committed Oct 04, 2016 678 ``````Lemma Qp_not_plus_q_ge_1 (q: Qp): ¬ ((1 + q)%Qp ≤ 1%Qp)%Qc. `````` Zhen Zhang committed Oct 04, 2016 679 680 681 ``````Proof. intros Hle. apply (Qcplus_le_mono_l q 0 1) in Hle. `````` Zhen Zhang committed Oct 04, 2016 682 `````` apply Qcle_ngt in Hle. apply Hle, Qp_prf. `````` Zhen Zhang committed Oct 04, 2016 683 ``````Qed. `````` Zhen Zhang committed Oct 04, 2016 684 685 686 `````` Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc. Proof. apply Qclt_le_weak, Qp_prf. Qed.``````