frac.v 8.4 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 May 28, 2016 4 ``````Local Arguments op _ _ !_ !_ /. `````` Robbert Krebbers committed Feb 26, 2016 5 6 7 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. `````` Robbert Krebbers committed May 28, 2016 8 9 10 11 12 ``````Inductive frac A := Frac { frac_perm : Qp ; frac_car : A }. Add Printing Constructor frac. Arguments Frac {_} _ _. Arguments frac_perm {_} _. Arguments frac_car {_} _. `````` Robbert Krebbers committed Feb 26, 2016 13 14 15 16 17 18 19 20 ``````Instance: Params (@Frac) 2. Section cofe. Context {A : cofeT}. Implicit Types a b : A. Implicit Types x y : frac A. (* Cofe *) `````` Robbert Krebbers committed May 28, 2016 21 22 23 24 ``````Instance frac_equiv : Equiv (frac A) := λ x y, frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y. Instance frac_dist : Dist (frac A) := λ n x y, frac_perm x = frac_perm y ∧ frac_car x ≡{n}≡ frac_car y. `````` Robbert Krebbers committed Feb 26, 2016 25 26 27 28 29 30 `````` 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). `````` Robbert Krebbers committed May 28, 2016 31 ``````Proof. by destruct 1. Qed. `````` Robbert Krebbers committed Feb 26, 2016 32 ``````Global Instance Frac_dist_inj n : Inj2 (=) (dist n) (dist n) (@Frac A). `````` Robbert Krebbers committed May 28, 2016 33 34 35 36 37 38 39 40 41 42 43 44 45 ``````Proof. by destruct 1. Qed. Global Instance frac_perm_ne n : Proper (dist n ==> (=)) (@frac_perm A). Proof. by destruct 1. Qed. Global Instance frac_car_ne n : Proper (dist n ==> dist n) (@frac_car A). Proof. by destruct 1. Qed. Global Instance frac_perm_proper : Proper ((≡) ==> (=)) (@frac_perm A). Proof. by destruct 1. Qed. Global Instance frac_car_proper : Proper ((≡) ==> (≡)) (@frac_car A). Proof. by destruct 1. Qed. Program Definition frac_chain (c : chain (frac A)) : chain A := {| chain_car n := match c n return _ with Frac _ b => b end |}. `````` Robbert Krebbers committed Feb 26, 2016 46 ``````Next Obligation. `````` Robbert Krebbers committed May 28, 2016 47 `````` intros c n i ?; simpl. destruct (c 0) eqn:?; simplify_eq/=. `````` Ralf Jung committed Feb 29, 2016 48 `````` by feed inversion (chain_cauchy c n i). `````` Robbert Krebbers committed Feb 26, 2016 49 50 ``````Qed. Instance frac_compl : Compl (frac A) := λ c, `````` Robbert Krebbers committed May 28, 2016 51 `````` Frac (frac_perm (c 0)) (compl (frac_chain c)). `````` Robbert Krebbers committed Feb 26, 2016 52 53 54 55 56 57 58 59 ``````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. `````` Robbert Krebbers committed May 28, 2016 60 `````` + by intros [q a]; constructor. `````` Robbert Krebbers committed Feb 26, 2016 61 62 63 `````` + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; done || apply dist_S. `````` Robbert Krebbers committed May 28, 2016 64 65 66 `````` - intros n c; constructor; simpl. + destruct (chain_cauchy c 0 n); auto with lia. + apply (conv_compl n (frac_chain c)). `````` Robbert Krebbers committed Feb 26, 2016 67 ``````Qed. `````` Robbert Krebbers committed May 25, 2016 68 ``````Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin. `````` Robbert Krebbers committed Feb 26, 2016 69 70 71 ``````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). `````` Robbert Krebbers committed May 28, 2016 72 ``````Proof. intros ? [??] [??] [??]; f_equal; done || by apply leibniz_equiv. Qed. `````` Robbert Krebbers committed Feb 26, 2016 73 74 75 76 77 78 79 80 81 `````` Global Instance Frac_timeless q (a : A) : Timeless a → Timeless (Frac q a). Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. End cofe. Arguments fracC : clear implicits. (* Functor on COFEs *) Definition frac_map {A B} (f : A → B) (x : frac A) : frac B := `````` Robbert Krebbers committed May 28, 2016 82 `````` match x with Frac q a => Frac q (f a) end. `````` Robbert Krebbers committed Feb 26, 2016 83 84 85 86 87 88 89 90 91 ``````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. `````` Robbert Krebbers committed May 28, 2016 92 ``````Proof. destruct x; constructor; simpl; auto. Qed. `````` Robbert Krebbers committed Feb 26, 2016 93 94 ``````Instance frac_map_cmra_ne {A B : cofeT} n : Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@frac_map A B). `````` Robbert Krebbers committed May 28, 2016 95 ``````Proof. intros f f' Hf [??] [??] [??]; constructor; by try apply Hf. Qed. `````` Robbert Krebbers committed Feb 26, 2016 96 97 98 99 100 101 102 103 104 105 106 ``````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. Instance frac_valid : Valid (frac A) := λ x, `````` Robbert Krebbers committed May 28, 2016 107 108 `````` (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x. Global Arguments frac_valid !_/. `````` Robbert Krebbers committed Feb 26, 2016 109 ``````Instance frac_validN : ValidN (frac A) := λ n x, `````` Robbert Krebbers committed May 28, 2016 110 111 112 `````` (frac_perm x ≤ 1)%Qc ∧ ✓{n} frac_car x. Global Arguments frac_validN _ !_/. Instance frac_pcore : PCore (frac A) := λ _, None. `````` Robbert Krebbers committed Feb 26, 2016 113 ``````Instance frac_op : Op (frac A) := λ x y, `````` Robbert Krebbers committed May 28, 2016 114 115 `````` Frac (frac_perm x + frac_perm y) (frac_car x ⋅ frac_car y). Global Arguments frac_op !_ !_ /. `````` Robbert Krebbers committed Feb 26, 2016 116 117 118 119 120 121 `````` 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. `````` Robbert Krebbers committed May 28, 2016 122 123 124 125 126 127 128 129 `````` split; try discriminate. - intros n [??] [??] [??] [??]; constructor; by cofe_subst. - intros ? [??] [??] [??] [??]; split; by cofe_subst. - intros [??]; 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 n [q1 a1] [q2 a2]; destruct 1; split; eauto using cmra_validN_op_l. `````` Robbert Krebbers committed Feb 26, 2016 130 131 `````` trans (q1 + q2)%Qp; simpl; last done. rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak. `````` Robbert Krebbers committed May 28, 2016 132 133 134 135 136 `````` - intros n [q a] y1 y2 Hx Hx'. 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 Feb 26, 2016 137 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 138 ``````Canonical Structure fracR := CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin. `````` Robbert Krebbers committed May 27, 2016 139 `````` `````` Robbert Krebbers committed Mar 01, 2016 140 ``````Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR. `````` Robbert Krebbers committed Feb 26, 2016 141 142 ``````Proof. split; first apply _. `````` Robbert Krebbers committed May 28, 2016 143 `````` intros [q a]; destruct 1; split; auto using cmra_discrete_valid. `````` Robbert Krebbers committed Feb 26, 2016 144 145 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 146 ``````Lemma frac_validN_inv_l n x y : ✓{n} (x ⋅ y) → frac_perm x ≠ 1%Qp. `````` Robbert Krebbers committed Feb 26, 2016 147 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 148 149 `````` intros [Hq _] Hx; simpl in *; destruct (Qcle_not_lt _ _ Hq). by rewrite Hx -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. `````` Robbert Krebbers committed Feb 26, 2016 150 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 151 152 ``````Lemma frac_valid_inv_l x y : ✓ (x ⋅ y) → frac_perm x ≠ 1%Qp. Proof. intros. by apply frac_validN_inv_l with 0 y, cmra_valid_validN. Qed. `````` Robbert Krebbers committed Feb 26, 2016 153 154 155 `````` (** Internalized properties *) Lemma frac_equivI {M} (x y : frac A) : `````` Robbert Krebbers committed May 28, 2016 156 157 `````` (x ≡ y) ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M). Proof. by uPred.unseal. Qed. `````` Robbert Krebbers committed Feb 26, 2016 158 ``````Lemma frac_validI {M} (x : frac A) : `````` Robbert Krebbers committed May 28, 2016 159 160 `````` ✓ x ⊣⊢ (■ (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x : uPred M). Proof. by uPred.unseal. Qed. `````` Robbert Krebbers committed Feb 26, 2016 161 162 163 `````` (** ** Local updates *) Global Instance frac_local_update_full p a : `````` Robbert Krebbers committed May 28, 2016 164 165 `````` LocalUpdate (λ x, frac_perm x = 1%Qp) (λ _, Frac p a). Proof. split; first by intros ???. by intros n x y ? ?%frac_validN_inv_l. Qed. `````` Robbert Krebbers committed Feb 26, 2016 166 ``````Global Instance frac_local_update `{!LocalUpdate Lv L} : `````` Robbert Krebbers committed May 28, 2016 167 `````` LocalUpdate (λ x, Lv (frac_car x)) (frac_map L). `````` Robbert Krebbers committed Feb 26, 2016 168 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 169 `````` split; first apply _. intros n [p a] [q b]; simpl. `````` Robbert Krebbers committed Feb 26, 2016 170 171 172 173 174 175 `````` 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. `````` Robbert Krebbers committed May 28, 2016 176 177 `````` move=> ? n [y|]; last (intros; by apply cmra_valid_validN). by intros ?%frac_validN_inv_l. `````` Robbert Krebbers committed Feb 26, 2016 178 179 180 ``````Qed. Lemma frac_update (a1 a2 : A) p : a1 ~~> a2 → Frac p a1 ~~> Frac p a2. Proof. `````` Robbert Krebbers committed May 28, 2016 181 182 `````` intros Ha n mz [??]; split; first by destruct mz. pose proof (Ha n (frac_car <\$> mz)); destruct mz; naive_solver. `````` Robbert Krebbers committed Feb 26, 2016 183 184 185 ``````Qed. End cmra. `````` Robbert Krebbers committed Mar 01, 2016 186 ``````Arguments fracR : clear implicits. `````` Robbert Krebbers committed Feb 26, 2016 187 188 189 190 191 192 `````` (* Functor *) Instance frac_map_cmra_monotone {A B : cmraT} (f : A → B) : CMRAMonotone f → CMRAMonotone (frac_map f). Proof. split; try apply _. `````` Robbert Krebbers committed May 28, 2016 193 194 `````` - intros n [p a]; destruct 1; split; simpl in *; auto using validN_preserving. - intros [q1 a1] [q2 a2] [[q3 a3] [??]]; setoid_subst. `````` Robbert Krebbers committed Feb 26, 2016 195 196 197 198 199 `````` 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 28, 2016 200 201 202 ``````Program Definition fracRF (F : rFunctor) : rFunctor := {| rFunctor_car A B := fracR (rFunctor_car F A B); rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg) `````` Robbert Krebbers committed Feb 26, 2016 203 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 204 205 206 ``````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 207 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 208 209 `````` 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 210 211 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 212 213 `````` 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 214 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 215 `````` `````` Robbert Krebbers committed May 28, 2016 216 217 ``````Instance fracRF_contractive F : rFunctorContractive F → rFunctorContractive (fracRF F). `````` Ralf Jung committed Mar 07, 2016 218 219 220 ``````Proof. by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive. Qed.``````