frac.v 9.86 KB
 1 ``````From Coq.QArith Require Import Qcanon. `````` Robbert Krebbers committed Mar 10, 2016 2 3 ``````From iris.algebra Require Export cmra. From iris.algebra Require Import upred. `````` Robbert Krebbers committed Feb 26, 2016 4 5 6 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. `````` Ralf Jung committed Mar 11, 2016 7 8 9 10 ``````Inductive frac {A : Type} := | Frac : Qp → A → frac | FracUnit : frac. Arguments frac _ : clear implicits. `````` Robbert Krebbers committed Feb 26, 2016 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 ``````Instance maybe_Frac {A} : Maybe2 (@Frac A) := λ x, match x with Frac q a => Some (q,a) | _ => None end. Instance: Params (@Frac) 2. Section cofe. Context {A : cofeT}. Implicit Types a b : A. Implicit Types x y : frac A. (* Cofe *) Inductive frac_equiv : Equiv (frac A) := | Frac_equiv q1 q2 a b : q1 = q2 → a ≡ b → Frac q1 a ≡ Frac q2 b | FracUnit_equiv : FracUnit ≡ FracUnit. Existing Instance frac_equiv. Inductive frac_dist : Dist (frac A) := | Frac_dist q1 q2 a b n : q1 = q2 → a ≡{n}≡ b → Frac q1 a ≡{n}≡ Frac q2 b | FracUnit_dist n : FracUnit ≡{n}≡ FracUnit. Existing Instance frac_dist. Global Instance Frac_ne q n : Proper (dist n ==> dist n) (@Frac A q). Proof. by constructor. Qed. Global Instance Frac_proper q : Proper ((≡) ==> (≡)) (@Frac A q). Proof. by constructor. Qed. Global Instance Frac_inj : Inj2 (=) (≡) (≡) (@Frac A). Proof. by inversion_clear 1. Qed. Global Instance Frac_dist_inj n : Inj2 (=) (dist n) (dist n) (@Frac A). Proof. by inversion_clear 1. Qed. Program Definition frac_chain (c : chain (frac A)) (q : Qp) (a : A) `````` Ralf Jung committed Feb 29, 2016 40 `````` (H : maybe2 Frac (c 0) = Some (q,a)) : chain A := `````` Robbert Krebbers committed Feb 26, 2016 41 42 `````` {| chain_car n := match c n return _ with Frac _ b => b | _ => a end |}. Next Obligation. `````` Ralf Jung committed Feb 29, 2016 43 44 45 `````` intros c q a ? n i ?; simpl. destruct (c 0) eqn:?; simplify_eq/=. by feed inversion (chain_cauchy c n i). `````` Robbert Krebbers committed Feb 26, 2016 46 47 ``````Qed. Instance frac_compl : Compl (frac A) := λ c, `````` Ralf Jung committed Feb 29, 2016 48 `````` match Some_dec (maybe2 Frac (c 0)) with `````` Robbert Krebbers committed Feb 26, 2016 49 `````` | inleft (exist (q,a) H) => Frac q (compl (frac_chain c q a H)) `````` Ralf Jung committed Feb 29, 2016 50 `````` | inright _ => c 0 `````` Robbert Krebbers committed Feb 26, 2016 51 52 53 54 55 56 57 58 59 60 61 62 63 64 `````` end. Definition frac_cofe_mixin : CofeMixin (frac A). Proof. split. - intros mx my; split. + by destruct 1; subst; constructor; try apply equiv_dist. + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done. apply equiv_dist=> n; by feed inversion (Hxy n). - intros n; split. + by intros [q a|]; constructor. + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; done || apply dist_S. - intros n c; unfold compl, frac_compl. `````` Ralf Jung committed Feb 29, 2016 65 66 67 68 `````` destruct (Some_dec (maybe2 Frac (c 0))) as [[[q a] Hx]|]. { assert (c 0 = Frac q a) by (by destruct (c 0); simplify_eq/=). assert (∃ b, c n = Frac q b) as [y Hy]. { feed inversion (chain_cauchy c 0 n); `````` Robbert Krebbers committed Feb 26, 2016 69 70 71 `````` eauto with lia congruence f_equal. } rewrite Hy; constructor; auto. by rewrite (conv_compl n (frac_chain c q a Hx)) /= Hy. } `````` Ralf Jung committed Feb 29, 2016 72 73 `````` feed inversion (chain_cauchy c 0 n); first lia; constructor; destruct (c 0); simplify_eq/=. `````` Robbert Krebbers committed Feb 26, 2016 74 ``````Qed. `````` Robbert Krebbers committed May 25, 2016 75 ``````Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin. `````` Robbert Krebbers committed Feb 26, 2016 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 ``````Global Instance frac_discrete : Discrete A → Discrete fracC. Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. Global Instance frac_leibniz : LeibnizEquiv A → LeibnizEquiv (frac A). Proof. by destruct 2; f_equal; done || apply leibniz_equiv. Qed. Global Instance Frac_timeless q (a : A) : Timeless a → Timeless (Frac q a). Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. Global Instance FracUnit_timeless : Timeless (@FracUnit A). Proof. by inversion_clear 1; constructor. Qed. End cofe. Arguments fracC : clear implicits. (* Functor on COFEs *) Definition frac_map {A B} (f : A → B) (x : frac A) : frac B := match x with | Frac q a => Frac q (f a) | FracUnit => FracUnit end. Instance: Params (@frac_map) 2. Lemma frac_map_id {A} (x : frac A) : frac_map id x = x. Proof. by destruct x. Qed. Lemma frac_map_compose {A B C} (f : A → B) (g : B → C) (x : frac A) : frac_map (g ∘ f) x = frac_map g (frac_map f x). Proof. by destruct x. Qed. Lemma frac_map_ext {A B : cofeT} (f g : A → B) x : (∀ x, f x ≡ g x) → frac_map f x ≡ frac_map g x. Proof. by destruct x; constructor. Qed. Instance frac_map_cmra_ne {A B : cofeT} n : Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@frac_map A B). Proof. intros f f' Hf; destruct 1; constructor; by try apply Hf. Qed. Definition fracC_map {A B} (f : A -n> B) : fracC A -n> fracC B := CofeMor (frac_map f). Instance fracC_map_ne A B n : Proper (dist n ==> dist n) (@fracC_map A B). Proof. intros f f' Hf []; constructor; by try apply Hf. Qed. Section cmra. Context {A : cmraT}. Implicit Types a b : A. Implicit Types x y : frac A. (* CMRA *) Instance frac_valid : Valid (frac A) := λ x, match x with Frac q a => (q ≤ 1)%Qc ∧ ✓ a | FracUnit => True end. Instance frac_validN : ValidN (frac A) := λ n x, match x with Frac q a => (q ≤ 1)%Qc ∧ ✓{n} a | FracUnit => True end. `````` Robbert Krebbers committed May 27, 2016 122 ``````Instance frac_core : Core (frac A) := λ _, FracUnit. `````` Robbert Krebbers committed Feb 26, 2016 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 ``````Instance frac_op : Op (frac A) := λ x y, match x, y with | Frac q1 a, Frac q2 b => Frac (q1 + q2) (a ⋅ b) | Frac q a, FracUnit | FracUnit, Frac q a => Frac q a | FracUnit, FracUnit => FracUnit end. Lemma Frac_op q1 q2 a b : Frac q1 a ⋅ Frac q2 b = Frac (q1 + q2) (a ⋅ b). Proof. done. Qed. Definition frac_cmra_mixin : CMRAMixin (frac A). Proof. split. - intros n []; destruct 1; constructor; by cofe_subst. - constructor. - do 2 destruct 1; split; by cofe_subst. - intros [q a|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O. - intros n [q a|]; destruct 1; split; auto using cmra_validN_S. - intros [q1 a1|] [q2 a2|] [q3 a3|]; constructor; by rewrite ?assoc. - intros [q1 a1|] [q2 a2|]; constructor; by rewrite 1?comm ?[(q1+_)%Qp]comm. - intros []; by constructor. - done. - by exists FracUnit. - intros n [q1 a1|] [q2 a2|]; destruct 1; split; eauto using cmra_validN_op_l. trans (q1 + q2)%Qp; simpl; last done. rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak. - intros n [q a|] y1 y2 Hx Hx'; last first. `````` Robbert Krebbers committed May 27, 2016 150 `````` { by exists (FracUnit, FracUnit); destruct y1, y2; inversion_clear Hx'. } `````` Robbert Krebbers committed Feb 26, 2016 151 152 153 154 `````` destruct Hx, y1 as [q1 b1|], y2 as [q2 b2|]. + apply (inj2 Frac) in Hx'; destruct Hx' as [-> ?]. destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto. exists (Frac q1 z1,Frac q2 z2); by repeat constructor. `````` Robbert Krebbers committed May 27, 2016 155 156 `````` + exists (Frac q a, FracUnit); inversion_clear Hx'; by repeat constructor. + exists (FracUnit, Frac q a); inversion_clear Hx'; by repeat constructor. `````` Robbert Krebbers committed Feb 26, 2016 157 158 `````` + exfalso; inversion_clear Hx'. Qed. `````` Robbert Krebbers committed May 27, 2016 159 ``````Canonical Structure fracR := `````` Robbert Krebbers committed May 25, 2016 160 `````` CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin. `````` Robbert Krebbers committed May 27, 2016 161 `````` `````` Robbert Krebbers committed Mar 01, 2016 162 ``````Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR. `````` Robbert Krebbers committed Feb 26, 2016 163 164 165 166 167 ``````Proof. split; first apply _. intros [q a|]; destruct 1; split; auto using cmra_discrete_valid. Qed. `````` Robbert Krebbers committed May 27, 2016 168 169 170 171 172 173 ``````Instance frac_empty : Empty (frac A) := FracUnit. Definition frac_ucmra_mixin : UCMRAMixin (frac A). Proof. split. done. by intros []. apply _. Qed. Canonical Structure fracUR := UCMRAT (frac A) frac_cofe_mixin frac_cmra_mixin frac_ucmra_mixin. `````` Robbert Krebbers committed Feb 26, 2016 174 175 176 177 178 179 180 181 182 183 ``````Lemma frac_validN_inv_l n y a : ✓{n} (Frac 1 a ⋅ y) → y = ∅. Proof. destruct y as [q b|]; [|done]=> -[Hq ?]; destruct (Qcle_not_lt _ _ Hq). by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. Qed. Lemma frac_valid_inv_l y a : ✓ (Frac 1 a ⋅ y) → y = ∅. Proof. intros. by apply frac_validN_inv_l with 0 a, cmra_valid_validN. Qed. (** Internalized properties *) Lemma frac_equivI {M} (x y : frac A) : `````` Ralf Jung committed Mar 10, 2016 184 `````` (x ≡ y) ⊣⊢ (match x, y with `````` Robbert Krebbers committed Feb 26, 2016 185 186 187 `````` | Frac q1 a, Frac q2 b => q1 = q2 ∧ a ≡ b | FracUnit, FracUnit => True | _, _ => False `````` Ralf Jung committed Mar 10, 2016 188 `````` end : uPred M). `````` Robbert Krebbers committed Feb 26, 2016 189 190 191 192 193 ``````Proof. uPred.unseal; do 2 split; first by destruct 1. by destruct x, y; destruct 1; try constructor. Qed. Lemma frac_validI {M} (x : frac A) : `````` Ralf Jung committed Mar 10, 2016 194 `````` (✓ x) ⊣⊢ (if x is Frac q a then ■ (q ≤ 1)%Qc ∧ ✓ a else True : uPred M). `````` Robbert Krebbers committed Feb 26, 2016 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 ``````Proof. uPred.unseal. by destruct x. Qed. (** ** Local updates *) Global Instance frac_local_update_full p a : LocalUpdate (λ x, if x is Frac q _ then q = 1%Qp else False) (λ _, Frac p a). Proof. split; first by intros ???. by intros n [q b|] y; [|done]=> -> /frac_validN_inv_l ->. Qed. Global Instance frac_local_update `{!LocalUpdate Lv L} : LocalUpdate (λ x, if x is Frac _ a then Lv a else False) (frac_map L). Proof. split; first apply _. intros n [p a|] [q b|]; simpl; try done. intros ? [??]; constructor; [done|by apply (local_updateN L)]. Qed. (** Updates *) Lemma frac_update_full (a1 a2 : A) : ✓ a2 → Frac 1 a1 ~~> Frac 1 a2. Proof. move=> ? n y /frac_validN_inv_l ->. split. done. by apply cmra_valid_validN. Qed. Lemma frac_update (a1 a2 : A) p : a1 ~~> a2 → Frac p a1 ~~> Frac p a2. Proof. intros Ha n [q b|] [??]; split; auto. `````` Ralf Jung committed Mar 08, 2016 219 `````` apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r. `````` Robbert Krebbers committed Feb 26, 2016 220 221 222 ``````Qed. End cmra. `````` Robbert Krebbers committed Mar 01, 2016 223 ``````Arguments fracR : clear implicits. `````` Robbert Krebbers committed May 27, 2016 224 ``````Arguments fracUR : clear implicits. `````` Robbert Krebbers committed Feb 26, 2016 225 226 227 228 229 230 231 232 `````` (* Functor *) Instance frac_map_cmra_monotone {A B : cmraT} (f : A → B) : CMRAMonotone f → CMRAMonotone (frac_map f). Proof. split; try apply _. - intros n [p a|]; destruct 1; split; auto using validN_preserving. - intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx]; `````` Robbert Krebbers committed May 27, 2016 233 `````` inversion Hx; setoid_subst; try apply: ucmra_unit_least; auto. `````` Robbert Krebbers committed Feb 26, 2016 234 235 236 237 238 `````` destruct (included_preserving f a1 (a1 ⋅ a3)) as [b ?]. { by apply cmra_included_l. } by exists (Frac q3 b); constructor. Qed. `````` Robbert Krebbers committed May 27, 2016 239 240 241 ``````Program Definition fracURF (F : rFunctor) : urFunctor := {| urFunctor_car A B := fracUR (rFunctor_car F A B); urFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg) `````` Robbert Krebbers committed Feb 26, 2016 242 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 243 244 245 ``````Next Obligation. by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne. Qed. `````` Robbert Krebbers committed Feb 26, 2016 246 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 247 248 `````` intros F A B x. rewrite /= -{2}(frac_map_id x). apply frac_map_ext=>y; apply rFunctor_id. `````` Robbert Krebbers committed Feb 26, 2016 249 250 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 251 252 `````` intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -frac_map_compose. apply frac_map_ext=>y; apply rFunctor_compose. `````` Robbert Krebbers committed Feb 26, 2016 253 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 254 `````` `````` Robbert Krebbers committed May 27, 2016 255 256 ``````Instance fracURF_contractive F : rFunctorContractive F → urFunctorContractive (fracURF F). `````` Ralf Jung committed Mar 07, 2016 257 258 259 ``````Proof. by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive. Qed.``````