numbers.v 51.6 KB
 Robbert Krebbers committed Oct 19, 2012 1 2 3 ``````(** 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 4 ``````From Coq Require Export EqdepFacts PArith NArith ZArith NPeano. `````` Robbert Krebbers committed Feb 13, 2016 5 6 ``````From Coq Require Import QArith Qcanon. From stdpp Require Export base decidable option. `````` Ralf Jung committed Sep 16, 2020 7 ``````From stdpp Require Import options. `````` Jacques-Henri Jourdan committed Sep 11, 2019 8 ``````Local Open Scope nat_scope. `````` Robbert Krebbers committed Jun 11, 2012 9 `````` `````` Ralf Jung committed Jan 07, 2021 10 ``````Global Instance comparison_eq_dec : EqDecision comparison. `````` Robbert Krebbers committed Feb 26, 2016 11 ``````Proof. solve_decision. Defined. `````` Robbert Krebbers committed Feb 01, 2013 12 `````` `````` Robbert Krebbers committed Feb 19, 2013 13 ``````(** * Notations and properties of [nat] *) `````` Ralf Jung committed Jan 07, 2021 14 15 ``````Global Arguments minus !_ !_ / : assert. Global Arguments Nat.max : simpl nomatch. `````` 16 `````` `````` Robbert Krebbers committed May 08, 2019 17 18 ``````Typeclasses Opaque lt. `````` Robbert Krebbers committed Nov 12, 2012 19 20 21 22 ``````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 23 24 ``````Reserved Notation "x ≤ y ≤ z ≤ z'" (at level 70, y at next level, z at next level). `````` Robbert Krebbers committed Nov 12, 2012 25 `````` `````` Robbert Krebbers committed Aug 21, 2012 26 ``````Infix "≤" := le : nat_scope. `````` Robbert Krebbers committed Nov 12, 2012 27 28 29 ``````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 30 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_scope. `````` Robbert Krebbers committed Nov 12, 2012 31 32 33 ``````Notation "(≤)" := le (only parsing) : nat_scope. Notation "(<)" := lt (only parsing) : nat_scope. `````` Robbert Krebbers committed Feb 01, 2017 34 35 ``````Infix "`div`" := Nat.div (at level 35) : nat_scope. Infix "`mod`" := Nat.modulo (at level 35) : nat_scope. `````` Robbert Krebbers committed Jul 03, 2016 36 37 ``````Infix "`max`" := Nat.max (at level 35) : nat_scope. Infix "`min`" := Nat.min (at level 35) : nat_scope. `````` Robbert Krebbers committed Nov 12, 2012 38 `````` `````` Ralf Jung committed Jan 07, 2021 39 40 41 42 43 ``````Global Instance nat_eq_dec: EqDecision nat := eq_nat_dec. Global Instance nat_le_dec: RelDecision le := le_dec. Global Instance nat_lt_dec: RelDecision lt := lt_dec. Global Instance nat_inhabited: Inhabited nat := populate 0%nat. Global Instance S_inj: Inj (=) (=) S. `````` Robbert Krebbers committed Jun 17, 2013 44 ``````Proof. by injection 1. Qed. `````` Ralf Jung committed Jan 07, 2021 45 ``````Global Instance nat_le_po: PartialOrder (≤). `````` Robbert Krebbers committed Jun 17, 2013 46 ``````Proof. repeat split; repeat intro; auto with lia. Qed. `````` Ralf Jung committed Jan 07, 2021 47 ``````Global Instance nat_le_total: Total (≤). `````` Robbert Krebbers committed May 08, 2019 48 ``````Proof. repeat intro; lia. Qed. `````` Robbert Krebbers committed Oct 19, 2012 49 `````` `````` Ralf Jung committed Jan 07, 2021 50 ``````Global Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y). `````` Robbert Krebbers committed May 07, 2013 51 52 53 ``````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 54 `````` { fix FIX 3. intros x ? [|y p] ? [|y' q]. `````` Robbert Krebbers committed Feb 17, 2016 55 `````` - done. `````` Robbert Krebbers committed Apr 27, 2018 56 57 58 `````` - 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 59 `````` intros x y p q. `````` Robbert Krebbers committed Feb 13, 2016 60 `````` by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux. `````` Robbert Krebbers committed May 07, 2013 61 ``````Qed. `````` Ralf Jung committed Jan 07, 2021 62 ``````Global Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y). `````` Robbert Krebbers committed May 08, 2019 63 ``````Proof. unfold lt. apply _. Qed. `````` Robbert Krebbers committed May 07, 2013 64 `````` `````` Robbert Krebbers committed Mar 11, 2017 65 ``````Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z. `````` Tej Chajed committed Sep 15, 2020 66 ``````Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed. `````` Robbert Krebbers committed Jan 05, 2013 67 `````` `````` Robbert Krebbers committed Jun 17, 2013 68 69 70 ``````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 71 72 `````` x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2. Proof. `````` Robbert Krebbers committed Jun 17, 2013 73 `````` intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |]. `````` Robbert Krebbers committed May 07, 2013 74 75 `````` revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia. Qed. `````` Robbert Krebbers committed Jun 17, 2013 76 77 78 ``````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 79 `````` `````` Robbert Krebbers committed May 02, 2014 80 81 82 ``````Notation lcm := Nat.lcm. Notation divide := Nat.divide. Notation "( x | y )" := (divide x y) : nat_scope. `````` Ralf Jung committed Jan 07, 2021 83 ``````Global Instance Nat_divide_dec : RelDecision Nat.divide. `````` Robbert Krebbers committed Nov 15, 2014 84 ``````Proof. `````` 85 `````` refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff. `````` Robbert Krebbers committed Nov 15, 2014 86 ``````Defined. `````` Ralf Jung committed May 25, 2021 87 ``````Global Instance: PartialOrder divide. `````` Robbert Krebbers committed May 02, 2014 88 89 90 ``````Proof. repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia. Qed. `````` Tej Chajed committed Nov 20, 2020 91 ``````Global Hint Extern 0 (_ | _) => reflexivity : core. `````` Robbert Krebbers committed May 02, 2014 92 93 94 ``````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 95 96 97 ``````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 committed Nov 09, 2018 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. `````` Ralf Jung committed Feb 09, 2021 102 103 104 105 106 107 ``````Lemma Nat_iter_mul {A} n1 n2 (f : A → A) x : Nat.iter (n1 * n2) f x = Nat.iter n1 (Nat.iter n2 f) x. Proof. intros. induction n1 as [|n1 IHn1]; [done|]. simpl. by rewrite Nat_iter_add, IHn1. Qed. `````` Robbert Krebbers committed Nov 09, 2018 108 `````` `````` Robbert Krebbers committed Mar 11, 2017 109 ``````Lemma Nat_iter_ind {A} (P : A → Prop) f x k : `````` Robbert Krebbers committed Mar 09, 2017 110 111 `````` 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 112 `````` `````` Michael Sammler committed Mar 31, 2020 113 `````` `````` Robbert Krebbers committed Feb 19, 2013 114 ``````(** * Notations and properties of [positive] *) `````` Jacques-Henri Jourdan committed Sep 11, 2019 115 ``````Local Open Scope positive_scope. `````` Robbert Krebbers committed Feb 19, 2013 116 `````` `````` Robbert Krebbers committed May 08, 2019 117 118 119 ``````Typeclasses Opaque Pos.le. Typeclasses Opaque Pos.lt. `````` Robbert Krebbers committed Jun 17, 2013 120 ``````Infix "≤" := Pos.le : positive_scope. `````` Robbert Krebbers committed May 02, 2014 121 122 123 124 ``````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 125 126 ``````Notation "(≤)" := Pos.le (only parsing) : positive_scope. Notation "(<)" := Pos.lt (only parsing) : positive_scope. `````` Robbert Krebbers committed Jun 11, 2012 127 128 129 ``````Notation "(~0)" := xO (only parsing) : positive_scope. Notation "(~1)" := xI (only parsing) : positive_scope. `````` Ralf Jung committed Jan 07, 2021 130 131 ``````Global Arguments Pos.of_nat : simpl never. Global Arguments Pmult : simpl never. `````` Robbert Krebbers committed Feb 26, 2016 132 `````` `````` Ralf Jung committed Jan 07, 2021 133 134 ``````Global Instance positive_eq_dec: EqDecision positive := Pos.eq_dec. Global Instance positive_le_dec: RelDecision Pos.le. `````` 135 ``````Proof. refine (λ x y, decide ((x ?= y) ≠ Gt)). Defined. `````` Ralf Jung committed Jan 07, 2021 136 ``````Global Instance positive_lt_dec: RelDecision Pos.lt. `````` 137 ``````Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined. `````` Ralf Jung committed Jan 07, 2021 138 ``````Global Instance positive_le_total: Total Pos.le. `````` Robbert Krebbers committed May 08, 2019 139 140 ``````Proof. repeat intro; lia. Qed. `````` Ralf Jung committed Jan 07, 2021 141 ``````Global Instance positive_inhabited: Inhabited positive := populate 1. `````` Robbert Krebbers committed Jun 17, 2013 142 `````` `````` Ralf Jung committed Jan 07, 2021 143 144 145 ``````Global Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end. Global Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end. Global Instance xO_inj : Inj (=) (=) (~0). `````` Robbert Krebbers committed Jan 05, 2013 146 ``````Proof. by injection 1. Qed. `````` Ralf Jung committed Jan 07, 2021 147 ``````Global Instance xI_inj : Inj (=) (=) (~1). `````` Robbert Krebbers committed Jan 05, 2013 148 149 ``````Proof. by injection 1. Qed. `````` Robbert Krebbers committed Feb 19, 2013 150 151 152 153 154 155 156 157 158 159 160 ``````(** 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. `````` Robbert Krebbers committed Sep 19, 2019 161 162 ``````Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope. Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope. `````` Robbert Krebbers committed Feb 19, 2013 163 164 165 166 167 168 169 170 171 `````` 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 172 ``````Global Instance Papp_1_l : LeftId (=) 1 (++). `````` Robbert Krebbers committed Feb 17, 2016 173 ``````Proof. intros p. by induction p; intros; f_equal/=. Qed. `````` Robbert Krebbers committed Mar 11, 2017 174 ``````Global Instance Papp_1_r : RightId (=) 1 (++). `````` Robbert Krebbers committed Feb 19, 2013 175 ``````Proof. done. Qed. `````` Robbert Krebbers committed Mar 11, 2017 176 ``````Global Instance Papp_assoc : Assoc (=) (++). `````` Robbert Krebbers committed Feb 17, 2016 177 ``````Proof. intros ?? p. by induction p; intros; f_equal/=. Qed. `````` Robbert Krebbers committed Sep 19, 2019 178 ``````Global Instance Papp_inj p : Inj (=) (=) (.++ p). `````` Robbert Krebbers committed Mar 11, 2017 179 ``````Proof. intros ???. induction p; simplify_eq; auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 180 181 182 183 `````` Lemma Preverse_go_app p1 p2 p3 : Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2. Proof. `````` Robbert Krebbers committed Dec 08, 2015 184 185 186 187 `````` revert p3 p1 p2. cut (∀ p1 p2 p3, Preverse_go (p2 ++ p3) p1 = p2 ++ Preverse_go p3 p1). { by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. } intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto. `````` Robbert Krebbers committed Feb 17, 2016 188 189 `````` - apply (IH _ (_~1)). - apply (IH _ (_~0)). `````` Robbert Krebbers committed Feb 19, 2013 190 ``````Qed. `````` Robbert Krebbers committed Dec 08, 2015 191 ``````Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1. `````` Robbert Krebbers committed Feb 19, 2013 192 193 194 195 196 197 ``````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). `````` Jakob Botsch Nielsen committed Mar 16, 2019 198 199 200 201 202 203 204 205 ``````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. `````` Michael Sammler committed Mar 31, 2020 206 `````` `````` Ralf Jung committed Jan 07, 2021 207 ``````Global Instance Preverse_inj : Inj (=) (=) Preverse. `````` Jakob Botsch Nielsen committed Mar 16, 2019 208 209 210 211 212 213 214 ``````Proof. intros p q eq. rewrite <- (Preverse_involutive p). rewrite <- (Preverse_involutive q). by rewrite eq. Qed. `````` Robbert Krebbers committed Feb 19, 2013 215 ``````Fixpoint Plength (p : positive) : nat := `````` Robbert Krebbers committed May 02, 2014 216 `````` match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end. `````` Robbert Krebbers committed Dec 08, 2015 217 ``````Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat. `````` Robbert Krebbers committed Feb 17, 2016 218 ``````Proof. by induction p2; f_equal/=. Qed. `````` Robbert Krebbers committed Feb 19, 2013 219 `````` `````` Robbert Krebbers committed Mar 11, 2017 220 221 222 223 224 225 226 ``````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. `````` Jakob Botsch Nielsen committed Mar 16, 2019 227 228 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 ``````(** 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. `````` Ralf Jung committed Jan 07, 2021 256 ``````Global Instance Pdup_inj : Inj (=) (=) Pdup. `````` Jakob Botsch Nielsen committed Mar 16, 2019 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 ``````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. `````` Jacques-Henri Jourdan committed Sep 11, 2019 280 ``````Local Close Scope positive_scope. `````` Robbert Krebbers committed Feb 19, 2013 281 282 `````` (** * Notations and properties of [N] *) `````` Robbert Krebbers committed May 08, 2019 283 284 285 ``````Typeclasses Opaque N.le. Typeclasses Opaque N.lt. `````` Robbert Krebbers committed Jun 11, 2012 286 ``````Infix "≤" := N.le : N_scope. `````` Robbert Krebbers committed Nov 12, 2012 287 288 289 ``````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 290 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope. `````` Robbert Krebbers committed Jun 11, 2012 291 ``````Notation "(≤)" := N.le (only parsing) : N_scope. `````` Robbert Krebbers committed Oct 19, 2012 292 ``````Notation "(<)" := N.lt (only parsing) : N_scope. `````` Robbert Krebbers committed May 30, 2019 293 `````` `````` Robbert Krebbers committed Nov 12, 2012 294 295 ``````Infix "`div`" := N.div (at level 35) : N_scope. Infix "`mod`" := N.modulo (at level 35) : N_scope. `````` Robbert Krebbers committed May 30, 2019 296 297 ``````Infix "`max`" := N.max (at level 35) : N_scope. Infix "`min`" := N.min (at level 35) : N_scope. `````` Robbert Krebbers committed Nov 12, 2012 298 `````` `````` Ralf Jung committed Jan 07, 2021 299 ``````Global Arguments N.add : simpl never. `````` Robbert Krebbers committed Jun 16, 2014 300 `````` `````` Ralf Jung committed Jan 07, 2021 301 ``````Global Instance Npos_inj : Inj (=) (=) Npos. `````` Robbert Krebbers committed Jan 05, 2013 302 303 ``````Proof. by injection 1. Qed. `````` Ralf Jung committed Jan 07, 2021 304 ``````Global Instance N_eq_dec: EqDecision N := N.eq_dec. `````` Ralf Jung committed May 25, 2021 305 ``````Global Program Instance N_le_dec : RelDecision N.le := λ x y, `````` Robbert Krebbers committed Mar 08, 2018 306 `````` match N.compare x y with Gt => right _ | _ => left _ end. `````` Robbert Krebbers committed Jan 12, 2016 307 ``````Solve Obligations with naive_solver. `````` Ralf Jung committed May 25, 2021 308 ``````Global Program Instance N_lt_dec : RelDecision N.lt := λ x y, `````` Robbert Krebbers committed Mar 08, 2018 309 `````` match N.compare x y with Lt => left _ | _ => right _ end. `````` Robbert Krebbers committed Jan 12, 2016 310 ``````Solve Obligations with naive_solver. `````` Ralf Jung committed Jan 07, 2021 311 312 ``````Global Instance N_inhabited: Inhabited N := populate 1%N. Global Instance N_lt_pi x y : ProofIrrel (x < y)%N. `````` Robbert Krebbers committed May 08, 2019 313 314 ``````Proof. unfold N.lt. apply _. Qed. `````` Ralf Jung committed Jan 07, 2021 315 ``````Global Instance N_le_po: PartialOrder (≤)%N. `````` Robbert Krebbers committed Aug 12, 2013 316 ``````Proof. `````` Tej Chajed committed Sep 15, 2020 317 `````` repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm]. `````` Robbert Krebbers committed Aug 12, 2013 318 ``````Qed. `````` Ralf Jung committed Jan 07, 2021 319 ``````Global Instance N_le_total: Total (≤)%N. `````` Robbert Krebbers committed May 08, 2019 320 321 ``````Proof. repeat intro; lia. Qed. `````` Tej Chajed committed Nov 20, 2020 322 ``````Global Hint Extern 0 (_ ≤ _)%N => reflexivity : core. `````` Robbert Krebbers committed Jun 11, 2012 323 `````` `````` Robbert Krebbers committed Feb 19, 2013 324 ``````(** * Notations and properties of [Z] *) `````` Jacques-Henri Jourdan committed Sep 11, 2019 325 ``````Local Open Scope Z_scope. `````` Robbert Krebbers committed Jun 17, 2013 326 `````` `````` Robbert Krebbers committed May 08, 2019 327 328 329 ``````Typeclasses Opaque Z.le. Typeclasses Opaque Z.lt. `````` Robbert Krebbers committed Jun 11, 2012 330 ``````Infix "≤" := Z.le : Z_scope. `````` Robbert Krebbers committed Jun 17, 2013 331 332 333 334 ``````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 335 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope. `````` Robbert Krebbers committed Jun 11, 2012 336 ``````Notation "(≤)" := Z.le (only parsing) : Z_scope. `````` Robbert Krebbers committed Oct 19, 2012 337 ``````Notation "(<)" := Z.lt (only parsing) : Z_scope. `````` Robbert Krebbers committed Nov 12, 2012 338 `````` `````` Robbert Krebbers committed Jan 05, 2013 339 340 ``````Infix "`div`" := Z.div (at level 35) : Z_scope. Infix "`mod`" := Z.modulo (at level 35) : Z_scope. `````` Robbert Krebbers committed Mar 14, 2013 341 342 ``````Infix "`quot`" := Z.quot (at level 35) : Z_scope. Infix "`rem`" := Z.rem (at level 35) : Z_scope. `````` Robbert Krebbers committed Jun 17, 2013 343 344 ``````Infix "≪" := Z.shiftl (at level 35) : Z_scope. Infix "≫" := Z.shiftr (at level 35) : Z_scope. `````` Robbert Krebbers committed May 30, 2019 345 346 ``````Infix "`max`" := Z.max (at level 35) : Z_scope. Infix "`min`" := Z.min (at level 35) : Z_scope. `````` Robbert Krebbers committed Jan 05, 2013 347 `````` `````` Ralf Jung committed Jan 07, 2021 348 ``````Global Instance Zpos_inj : Inj (=) (=) Zpos. `````` Robbert Krebbers committed May 02, 2014 349 ``````Proof. by injection 1. Qed. `````` Ralf Jung committed Jan 07, 2021 350 ``````Global Instance Zneg_inj : Inj (=) (=) Zneg. `````` Robbert Krebbers committed May 02, 2014 351 352 ``````Proof. by injection 1. Qed. `````` Ralf Jung committed Jan 07, 2021 353 ``````Global Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat. `````` Robbert Krebbers committed Aug 04, 2016 354 355 ``````Proof. intros n1 n2. apply Nat2Z.inj. Qed. `````` Ralf Jung committed Jan 07, 2021 356 357 358 359 360 361 362 ``````Global Instance Z_eq_dec: EqDecision Z := Z.eq_dec. Global Instance Z_le_dec: RelDecision Z.le := Z_le_dec. Global Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec. Global Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec. Global Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec. Global Instance Z_inhabited: Inhabited Z := populate 1. Global Instance Z_lt_pi x y : ProofIrrel (x < y). `````` Robbert Krebbers committed May 08, 2019 363 364 ``````Proof. unfold Z.lt. apply _. Qed. `````` Ralf Jung committed Jan 07, 2021 365 ``````Global Instance Z_le_po : PartialOrder (≤). `````` Robbert Krebbers committed Aug 12, 2013 366 ``````Proof. `````` Tej Chajed committed Sep 15, 2020 367 `````` repeat split; red; [apply Z.le_refl | apply Z.le_trans | apply Z.le_antisymm]. `````` Robbert Krebbers committed Aug 12, 2013 368 ``````Qed. `````` Ralf Jung committed Jan 07, 2021 369 ``````Global Instance Z_le_total: Total Z.le. `````` Robbert Krebbers committed May 08, 2019 370 ``````Proof. repeat intro; lia. Qed. `````` Robbert Krebbers committed Jun 17, 2013 371 372 373 `````` Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m. Proof. `````` Tej Chajed committed Sep 15, 2020 374 `````` intros. rewrite <-Z.pow_succ_r, Z.succ_pred; [done|]. by apply Z.lt_le_pred. `````` Robbert Krebbers committed Jun 17, 2013 375 376 377 378 379 380 ``````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 |]. `````` Tej Chajed committed Sep 15, 2020 381 382 `````` split; [apply Z.quot_pos; lia|]. trans x; auto. apply Z.quot_lt; lia. `````` Robbert Krebbers committed Jun 17, 2013 383 ``````Qed. `````` Robbert Krebbers committed Jun 11, 2012 384 `````` `````` Ralf Jung committed Jan 07, 2021 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 ``````Global Arguments Z.pred : simpl never. Global Arguments Z.succ : simpl never. Global Arguments Z.of_nat : simpl never. Global Arguments Z.to_nat : simpl never. Global Arguments Z.mul : simpl never. Global Arguments Z.add : simpl never. Global Arguments Z.sub : simpl never. Global Arguments Z.opp : simpl never. Global Arguments Z.pow : simpl never. Global Arguments Z.div : simpl never. Global Arguments Z.modulo : simpl never. Global Arguments Z.quot : simpl never. Global Arguments Z.rem : simpl never. Global Arguments Z.shiftl : simpl never. Global Arguments Z.shiftr : simpl never. Global Arguments Z.gcd : simpl never. Global Arguments Z.lcm : simpl never. Global Arguments Z.min : simpl never. Global Arguments Z.max : simpl never. Global Arguments Z.lor : simpl never. Global Arguments Z.land : simpl never. Global Arguments Z.lxor : simpl never. Global Arguments Z.lnot : simpl never. Global Arguments Z.square : simpl never. Global Arguments Z.abs : simpl never. `````` Robbert Krebbers committed Mar 14, 2013 410 `````` `````` Robbert Krebbers committed Aug 26, 2014 411 412 413 414 415 ``````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 416 417 ``````Proof. apply Z.mod_pos_bound. Qed. `````` Tej Chajed committed Nov 20, 2020 418 419 420 421 422 423 ``````Global Hint Resolve Z.lt_le_incl : zpos. Global Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos. Global Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos. Global Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos. Global Hint Resolve Z_mod_pos Z.div_pos : zpos. Global Hint Extern 1000 => lia : zpos. `````` Robbert Krebbers committed May 07, 2013 424 `````` `````` Robbert Krebbers committed Feb 01, 2015 425 426 ``````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. `````` Ralf Jung committed Apr 29, 2021 427 ``````Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y). `````` Robbert Krebbers committed Jun 17, 2013 428 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2015 429 430 431 `````` 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 432 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2015 433 434 435 ``````Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat. Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 436 `````` - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i). `````` Robbert Krebbers committed Feb 01, 2015 437 438 439 `````` 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 440 `````` - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul. `````` Robbert Krebbers committed Feb 01, 2015 441 442 443 444 ``````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. `````` Ralf Jung committed Apr 29, 2021 445 ``````Lemma Nat2Z_inj_div x y : Z.of_nat (x `div` y) = (Z.of_nat x) `div` (Z.of_nat y). `````` Robbert Krebbers committed Jun 17, 2013 446 447 ``````Proof. destruct (decide (y = 0%nat)); [by subst; destruct x |]. `````` Ralf Jung committed Apr 29, 2021 448 `````` apply Z.div_unique with (Z.of_nat \$ x `mod` y)%nat. `````` Robbert Krebbers committed Jun 17, 2013 449 450 451 452 `````` { 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. `````` Ralf Jung committed Apr 29, 2021 453 ``````Lemma Nat2Z_inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y). `````` Robbert Krebbers committed Jun 17, 2013 454 455 ``````Proof. destruct (decide (y = 0%nat)); [by subst; destruct x |]. `````` Ralf Jung committed Apr 29, 2021 456 `````` apply Z.mod_unique with (Z.of_nat \$ x `div` y)%nat. `````` Robbert Krebbers committed Jun 17, 2013 457 458 459 460 `````` { 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. `````` Michael Sammler committed May 12, 2020 461 ``````Lemma Z2Nat_inj_div x y : `````` Michael Sammler committed May 12, 2020 462 463 464 `````` 0 ≤ x → 0 ≤ y → Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat. Proof. `````` Ralf Jung committed Apr 29, 2021 465 `````` intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|]. `````` Michael Sammler committed May 12, 2020 466 `````` pose proof (Z.div_pos x y). `````` Michael Sammler committed May 12, 2020 467 `````` apply (inj Z.of_nat). by rewrite Nat2Z_inj_div, !Z2Nat.id by lia. `````` Michael Sammler committed May 12, 2020 468 ``````Qed. `````` Michael Sammler committed May 12, 2020 469 ``````Lemma Z2Nat_inj_mod x y : `````` Michael Sammler committed May 12, 2020 470 471 472 `````` 0 ≤ x → 0 ≤ y → Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat. Proof. `````` Ralf Jung committed Apr 29, 2021 473 `````` intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|]. `````` Michael Sammler committed May 12, 2020 474 `````` pose proof (Z_mod_pos x y). `````` Michael Sammler committed May 12, 2020 475 `````` apply (inj Z.of_nat). by rewrite Nat2Z_inj_mod, !Z2Nat.id by lia. `````` Michael Sammler committed May 12, 2020 476 ``````Qed. `````` Simon Spies committed Jun 28, 2019 477 478 479 480 481 482 ``````Lemma Z_succ_pred_induction y (P : Z → Prop) : P y → (∀ x, y ≤ x → P x → P (Z.succ x)) → (∀ x, x ≤ y → P x → P (Z.pred x)) → (∀ x, P x). Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed. `````` Michael Sammler committed Mar 31, 2020 483 484 485 486 ``````Lemma Zmod_in_range q a c : q * c ≤ a < (q + 1) * c → a `mod` c = a - q * c. Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed. `````` Simon Spies committed Jun 28, 2019 487 `````` `````` Michael Sammler committed May 04, 2021 488 489 490 491 492 493 494 495 496 ``````Lemma Z_ones_spec n m: 0 ≤ m → 0 ≤ n → Z.testbit (Z.ones n) m = bool_decide (m < n). Proof. intros. case_bool_decide. - by rewrite Z.ones_spec_low by lia. - by rewrite Z.ones_spec_high by lia. Qed. `````` Fengmin Zhu committed Apr 19, 2021 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 ``````Lemma Z_bounded_iff_bits_nonneg k n : 0 ≤ k → 0 ≤ n → n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false. Proof. intros. destruct (decide (n = 0)) as [->|]. { naive_solver eauto using Z.bits_0, Z.pow_pos_nonneg with lia. } split. { intros Hb%Z.log2_lt_pow2 l Hl; [|lia]. apply Z.bits_above_log2; lia. } intros Hl. apply Z.nle_gt; intros ?. assert (Z.testbit n (Z.log2 n) = false) as Hbit. { apply Hl, Z.log2_le_pow2; lia. } by rewrite Z.bit_log2 in Hbit by lia. Qed. (* Goals of the form [0 ≤ n ≤ 2^k] appear often. So we also define the derived version [Z_bounded_iff_bits_nonneg'] that does not require proving [0 ≤ n] twice in that case. *) Lemma Z_bounded_iff_bits_nonneg' k n : 0 ≤ k → 0 ≤ n → 0 ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false. Proof. intros ??. rewrite <-Z_bounded_iff_bits_nonneg; lia. Qed. Lemma Z_bounded_iff_bits k n : 0 ≤ k → -2^k ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = bool_decide (n < 0). Proof. intros Hk. case_bool_decide; [ | rewrite <-Z_bounded_iff_bits_nonneg; lia]. assert(n = - Z.abs n)%Z as -> by lia. split. { intros [? _] l Hl. rewrite Z.bits_opp, negb_true_iff by lia. apply Z_bounded_iff_bits_nonneg with k; lia. } intros Hbit. split. - rewrite <-Z.opp_le_mono, <-Z.lt_pred_le. apply Z_bounded_iff_bits_nonneg; [lia..|]. intros l Hl. rewrite <-negb_true_iff, <-Z.bits_opp by lia. by apply Hbit. - etrans; [|apply Z.pow_pos_nonneg]; lia. Qed. `````` Jacques-Henri Jourdan committed Sep 11, 2019 539 ``````Local Close Scope Z_scope. `````` Robbert Krebbers committed Jun 17, 2013 540 `````` `````` Johannes Kloos committed Oct 31, 2017 541 ``````(** * Injectivity of casts *) `````` Ralf Jung committed Jan 07, 2021 542 543 544 545 546 ``````Global Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj. Global Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj. Global Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj. Global Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj. Global Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj. `````` Johannes Kloos committed Oct 31, 2017 547 548 ``````(* Add others here. *) `````` Robbert Krebbers committed Feb 19, 2013 549 ``````(** * Notations and properties of [Qc] *) `````` Robbert Krebbers committed May 08, 2019 550 551 552 ``````Typeclasses Opaque Qcle. Typeclasses Opaque Qclt. `````` Jacques-Henri Jourdan committed Sep 11, 2019 553 ``````Local Open Scope Qc_scope. `````` Robbert Krebbers committed May 02, 2014 554 555 ``````Delimit Scope Qc_scope with Qc. Notation "1" := (Q2Qc 1) : Qc_scope. `````` Robbert Krebbers committed Aug 21, 2013 556 ``````Notation "2" := (1+1) : Qc_scope. `````` Robbert Krebbers committed May 02, 2014 557 558 ``````Notation "- 1" := (Qcopp 1) : Qc_scope. Notation "- 2" := (Qcopp 2) : Qc_scope. `````` Robbert Krebbers committed Feb 19, 2013 559 ``````Infix "≤" := Qcle : Qc_scope. `````` Robbert Krebbers committed Aug 21, 2013 560 561 562 563 ``````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 564 ``````Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope. `````` Robbert Krebbers committed Feb 19, 2013 565 566 567 ``````Notation "(≤)" := Qcle (only parsing) : Qc_scope. Notation "(<)" := Qclt (only parsing) : Qc_scope. `````` Tej Chajed committed Nov 20, 2020 568 ``````Global Hint Extern 1 (_ ≤ _) => reflexivity || discriminate : core. `````` Ralf Jung committed Jan 07, 2021 569 ``````Global Arguments Qred : simpl never. `````` Robbert Krebbers committed May 02, 2014 570 `````` `````` Ralf Jung committed Apr 29, 2021 571 572 573 574 ``````Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n. Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed. Definition Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n). `````` Ralf Jung committed Jan 07, 2021 575 ``````Global Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec. `````` Ralf Jung committed May 25, 2021 576 ``````Global Program Instance Qc_le_dec: RelDecision Qcle := λ x y, `````` Robbert Krebbers committed Feb 19, 2013 577 `````` if Qclt_le_dec y x then right _ else left _. `````` Robbert Krebbers committed Jan 12, 2016 578 579 ``````Next Obligation. intros x y; apply Qclt_not_le. Qed. Next Obligation. done. Qed. `````` Ralf Jung committed May 25, 2021 580 ``````Global Program Instance Qc_lt_dec: RelDecision Qclt := λ x y, `````` Robbert Krebbers committed Feb 19, 2013 581 `````` if Qclt_le_dec x y then left _ else right _. `````` Ralf Jung committed Feb 20, 2019 582 ``````Next Obligation. done. Qed. `````` Robbert Krebbers committed Jan 12, 2016 583 ``````Next Obligation. intros x y; apply Qcle_not_lt. Qed. `````` Ralf Jung committed Jan 07, 2021 584 ``````Global Instance Qc_lt_pi x y : ProofIrrel (x < y). `````` Robbert Krebbers committed May 08, 2019 585 ``````Proof. unfold Qclt. apply _. Qed. `````` Robbert Krebbers committed Feb 19, 2013 586 `````` `````` Ralf Jung committed Jan 07, 2021 587 ``````Global Instance Qc_le_po: PartialOrder (≤). `````` Robbert Krebbers committed Aug 21, 2013 588 ``````Proof. `````` Tej Chajed committed Sep 15, 2020 589 `````` repeat split; red; [apply Qcle_refl | apply Qcle_trans | apply Qcle_antisym]. `````` Robbert Krebbers committed Aug 21, 2013 590 ``````Qed. `````` Ralf Jung committed Jan 07, 2021 591 ``````Global Instance Qc_lt_strict: StrictOrder (<). `````` Robbert Krebbers committed Aug 21, 2013 592 ``````Proof. `````` Tej Chajed committed Sep 15, 2020 593 594 `````` split; red; [|apply Qclt_trans]. intros x Hx. by destruct (Qclt_not_eq x x). `````` Robbert Krebbers committed Aug 21, 2013 595 ``````Qed. `````` Ralf Jung committed Jan 07, 2021 596 ``````Global Instance Qc_le_total: Total Qcle. `````` Robbert Krebbers committed May 08, 2019 597 598 ``````Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed. `````` Robbert Krebbers committed May 02, 2014 599 600 601 602 ``````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 603 604 ``````Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc. Proof. ring. Qed. `````` Robbert Krebbers committed Aug 21, 2013 605 ``````Lemma Qcle_ngt (x y : Qc) : x ≤ y ↔ ¬y < x. `````` Robbert Krebbers committed Feb 19, 2013 606 ``````Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed. `````` Robbert Krebbers committed Aug 21, 2013 607 ``````Lemma Qclt_nge (x y : Qc) : x < y ↔ ¬y ≤ x. `````` Robbert Krebbers committed Feb 19, 2013 608 ``````Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed. `````` Robbert Krebbers committed Aug 21, 2013 609 ``````Lemma Qcplus_le_mono_l (x y z : Qc) : x ≤ y ↔ z + x ≤ z + y. `````` Robbert Krebbers committed Feb 19, 2013 610 611 ``````Proof. split; intros. `````` Robbert Krebbers committed Feb 17, 2016 612 613 `````` - by apply Qcplus_le_compat. - replace x with ((0 - z) + (z + x)) by ring. `````` Robbert Krebbers committed Aug 21, 2013 614 `````` replace y with ((0 - z) + (z + y)) by ring. `````` Robbert Krebbers committed Feb 19, 2013 615 616 `````` by apply Qcplus_le_compat. Qed. `````` Robbert Krebbers committed Aug 21, 2013 617 ``````Lemma Qcplus_le_mono_r (x y z : Qc) : x ≤ y ↔ x + z ≤ y + z. `````` Robbert Krebbers committed Feb 19, 2013 618 ``````Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed. `````` Robbert Krebbers committed Aug 21, 2013 619 ``````Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y ↔ z + x < z + y. `````` Robbert Krebbers committed Feb 19, 2013 620 ``````Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed. `````` Robbert Krebbers committed Aug 21, 2013 621 ``````Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y ↔ x + z < y + z. `````` Robbert Krebbers committed Feb 19, 2013 622 ``````Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed. `````` Ralf Jung committed Jan 07, 2021 623 ``````Global Instance Qcopp_inj : Inj (=) (=) Qcopp. `````` Robbert Krebbers committed Aug 21, 2013 624 625 626 ``````Proof. intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive. Qed. `````` Ralf Jung committed Jan 07, 2021 627 ``````Global Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z). `````` Robbert Krebbers committed Aug 21, 2013 628 ``````Proof. `````` Robbert Krebbers committed Apr 05, 2018 629 `````` intros x y H. by apply (anti_symm (≤));rewrite (Qcplus_le_mono_l _ _ z), H. `````` Robbert Krebbers committed Aug 21, 2013 630 ``````Qed. `````` Ralf Jung committed Jan 07, 2021 631 ``````Global Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z). `````` Robbert Krebbers committed May 02, 2014 632 ``````Proof. `````` Robbert Krebbers committed Apr 05, 2018 633 `````` intros x y H. by apply (anti_symm (≤)); rewrite (Qcplus_le_mono_r _ _ z), H. `````` Robbert Krebbers committed May 02, 2014 634 ``````Qed. `````` Robbert Krebbers committed Aug 21, 2013 635 636 637 638 639 640 ``````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. `````` Michael Sammler committed Mar 31, 2020 641 ``````Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed. `````` Robbert Krebbers committed Aug 21, 2013 642 643 644 645 ``````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 646 `````` intros. trans (x + 0); [by rewrite Qcplus_0_r|]. `````` Robbert Krebbers committed Aug 21, 2013 647 648 649 650 651 652 653 654 655 656 657 658 659 `````` 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 660 `````` intros. trans (x + 0); [|by rewrite Qcplus_0_r]. `````` Robbert Krebbers committed Aug 21, 2013 661 662 `````` by apply Qcplus_le_mono_l. Qed. `````` Robbert Krebbers committed May 02, 2014 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 ``````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 686 `````` intros. trans (0 * y); [by rewrite Qcmult_0_l|]. `````` Robbert Krebbers committed May 02, 2014 687 688 689 `````` by apply Qcmult_le_mono_nonneg_r. Qed. `````` Robbert Krebbers committed Oct 29, 2020 690 691 692 693 694 695 ``````Lemma Qcinv_pos x : 0 < x → 0 < /x. Proof. intros. assert (0 ≠ x) by (by apply Qclt_not_eq). by rewrite (Qcmult_lt_mono_pos_r _ _ x), Qcmult_0_l, Qcmult_inv_l by done. Qed. `````` Robbert Krebbers committed May 02, 2014 696 697 ``````Lemma Z2Qc_inj_0 : Qc_of_Z 0 = 0. Proof. by apply Qc_is_canon. Qed. `````` Robbert Krebbers committed Feb 26, 2016 698 699 700 701 ``````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 702 703 704 ``````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. `````` Tej Chajed committed Sep 15, 2020 705 ``````Proof. split; [ auto using Z2Qc_inj | by intros -> ]. Qed. `````` Robbert Krebbers committed May 02, 2014 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 ``````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. `````` Jacques-Henri Jourdan committed Sep 11, 2019 721 ``````Local Close Scope Qc_scope. `````` Robbert Krebbers committed Feb 26, 2016 722 723 `````` (** * Positive rationals *) `````` Ralf Jung committed Oct 06, 2020 724 725 726 ``````Declare Scope Qp_scope. Delimit Scope Qp_scope with Qp. `````` Robbert Krebbers committed Oct 29, 2020 727 728 ``````Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }. Add Printing Constructor Qp. `````` Ralf Jung committed Oct 06, 2020 729 ``````Bind Scope Qp_scope with Qp. `````` Ralf Jung committed Jan 07, 2021 730 ``````Global Arguments Qp_to_Qc _%Qp : assert. `````` Robbert Krebbers committed Feb 26, 2016 731 `````` `````` Simon Friis Vindum committed Aug 31, 2020 732 733 ``````Local Open Scope Qp_scope. `````` 734 735 736 737 738 ``````Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q. Proof. split; [|by intros ->]. destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _). Qed. `````` Ralf Jung committed Jan 07, 2021 739 ``````Global Instance Qp_eq_dec : EqDecision Qp. `````` 740 741 742 743 744 ``````Proof. refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q))); by rewrite <-Qp_to_Qc_inj_iff. Defined. `````` 745 ``````Definition Qp_add (p q : Qp) : Qp := `````` Robbert Krebbers committed Oct 29, 2020 746 747 `````` let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq). `````` Ralf Jung committed Jan 07, 2021 748 ``````Global Arguments Qp_add : simpl never. `````` Robbert Krebbers committed Oct 29, 2020 749 `````` `````` 750 ``````Definition Qp_sub (p q : Qp) : option Qp := `````` Robbert Krebbers committed Oct 29, 2020 751 752 753 `````` let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in let pq := (p - q)%Qc in guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq). `````` Ralf Jung committed Jan 07, 2021 754 ``````Global Arguments Qp_sub : simpl never. `````` Robbert Krebbers committed Oct 29, 2020 755 `````` `````` 756 ``````Definition Qp_mul (p q : Qp) : Qp := `````` Robbert Krebbers committed Oct 29, 2020 757 758 `````` let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq). `````` Ralf Jung committed Jan 07, 2021 759 ``````Global Arguments Qp_mul : simpl never. `````` Robbert Krebbers committed Oct 29, 2020 760 `````` `````` Robbert Krebbers committed Oct 29, 2020 761 762 763 ``````Definition Qp_inv (q : Qp) : Qp := let 'mk_Qp q Hq := q return _ in mk_Qp (/ q)%Qc (Qcinv_pos _ Hq). `````` Ralf Jung committed Jan 07, 2021 764 ``````Global Arguments Qp_inv : simpl never. `````` Robbert Krebbers committed Oct 29, 2020 765 `````` `````` 766 ``````Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q). `````` Robbert Krebbers committed Oct 29, 2020 767 ``````Typeclasses Opaque Qp_div. `````` Ralf Jung committed Jan 07, 2021 768 ``````Global Arguments Qp_div : simpl never. `````` Simon Friis Vindum committed Aug 31, 2020 769 `````` `````` 770 771 772 ``````Infix "+" := Qp_add : Qp_scope. Infix "-" := Qp_sub : Qp_scope. Infix "*" := Qp_mul : Qp_scope. `````` Robbert Krebbers committed Oct 29, 2020 773 ``````Notation "/ q" := (Qp_inv q) : Qp_scope. ``````