one_shot.v 10.3 KB
 Ralf Jung committed Mar 11, 2016 1 2 ``````From iris.algebra Require Export cmra. From iris.algebra Require Import upred. `````` Robbert Krebbers committed May 28, 2016 3 4 ``````Local Arguments pcore _ _ !_ /. Local Arguments cmra_pcore _ !_ /. `````` Ralf Jung committed Mar 11, 2016 5 6 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. `````` Ralf Jung committed Mar 11, 2016 7 8 ``````Local Arguments cmra_validN _ _ !_ /. Local Arguments cmra_valid _ !_ /. `````` Ralf Jung committed Mar 11, 2016 9 `````` `````` Ralf Jung committed Mar 11, 2016 10 ``````(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *) `````` Robbert Krebbers committed May 28, 2016 11 12 13 14 15 16 17 18 ``````Inductive one_shot (A : Type) := | OneShotPending : one_shot A | Shot : A → one_shot A | OneShotBot : one_shot A. Arguments OneShotPending {_}. Arguments Shot {_} _. Arguments OneShotBot {_}. `````` Ralf Jung committed Mar 11, 2016 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 ``````Instance maybe_Shot {A} : Maybe (@Shot A) := λ x, match x with Shot a => Some a | _ => None end. Instance: Params (@Shot) 1. Section cofe. Context {A : cofeT}. Implicit Types a b : A. Implicit Types x y : one_shot A. (* Cofe *) Inductive one_shot_equiv : Equiv (one_shot A) := | OneShotPending_equiv : OneShotPending ≡ OneShotPending | OneShot_equiv a b : a ≡ b → Shot a ≡ Shot b | OneShotBot_equiv : OneShotBot ≡ OneShotBot. Existing Instance one_shot_equiv. Inductive one_shot_dist : Dist (one_shot A) := | OneShotPending_dist n : OneShotPending ≡{n}≡ OneShotPending | OneShot_dist n a b : a ≡{n}≡ b → Shot a ≡{n}≡ Shot b | OneShotBot_dist n : OneShotBot ≡{n}≡ OneShotBot. Existing Instance one_shot_dist. Global Instance One_Shot_ne n : Proper (dist n ==> dist n) (@Shot A). Proof. by constructor. Qed. Global Instance One_Shot_proper : Proper ((≡) ==> (≡)) (@Shot A). Proof. by constructor. Qed. Global Instance One_Shot_inj : Inj (≡) (≡) (@Shot A). Proof. by inversion_clear 1. Qed. Global Instance One_Shot_dist_inj n : Inj (dist n) (dist n) (@Shot A). Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed Mar 19, 2016 49 ``````Program Definition one_shot_chain (c : chain (one_shot A)) (a : A) : chain A := `````` Ralf Jung committed Mar 11, 2016 50 `````` {| chain_car n := match c n return _ with Shot b => b | _ => a end |}. `````` Robbert Krebbers committed Mar 19, 2016 51 ``````Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed. `````` Ralf Jung committed Mar 11, 2016 52 ``````Instance one_shot_compl : Compl (one_shot A) := λ c, `````` Robbert Krebbers committed Mar 19, 2016 53 `````` match c 0 with Shot a => Shot (compl (one_shot_chain c a)) | x => x end. `````` Ralf Jung committed Mar 11, 2016 54 55 56 57 58 59 60 61 ``````Definition one_shot_cofe_mixin : CofeMixin (one_shot 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 62 `````` + by intros [|a|]; constructor. `````` Ralf Jung committed Mar 11, 2016 63 64 65 `````` + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; done || apply dist_S. `````` Robbert Krebbers committed Mar 19, 2016 66 67 68 `````` - intros n c; rewrite /compl /one_shot_compl. feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. rewrite (conv_compl n (one_shot_chain c _)) /=. destruct (c n); naive_solver. `````` Ralf Jung committed Mar 11, 2016 69 ``````Qed. `````` Robbert Krebbers committed May 25, 2016 70 ``````Canonical Structure one_shotC : cofeT := CofeT (one_shot A) one_shot_cofe_mixin. `````` Ralf Jung committed Mar 11, 2016 71 72 73 74 75 76 77 78 79 80 81 ``````Global Instance one_shot_discrete : Discrete A → Discrete one_shotC. Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. Global Instance one_shot_leibniz : LeibnizEquiv A → LeibnizEquiv (one_shot A). Proof. by destruct 2; f_equal; done || apply leibniz_equiv. Qed. Global Instance Shot_timeless (a : A) : Timeless a → Timeless (Shot a). Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. End cofe. Arguments one_shotC : clear implicits. `````` Ralf Jung committed Mar 11, 2016 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 122 123 124 ``````(* Functor on COFEs *) Definition one_shot_map {A B} (f : A → B) (x : one_shot A) : one_shot B := match x with | OneShotPending => OneShotPending | Shot a => Shot (f a) | OneShotBot => OneShotBot end. Instance: Params (@one_shot_map) 2. Lemma one_shot_map_id {A} (x : one_shot A) : one_shot_map id x = x. Proof. by destruct x. Qed. Lemma one_shot_map_compose {A B C} (f : A → B) (g : B → C) (x : one_shot A) : one_shot_map (g ∘ f) x = one_shot_map g (one_shot_map f x). Proof. by destruct x. Qed. Lemma one_shot_map_ext {A B : cofeT} (f g : A → B) x : (∀ x, f x ≡ g x) → one_shot_map f x ≡ one_shot_map g x. Proof. by destruct x; constructor. Qed. Instance one_shot_map_cmra_ne {A B : cofeT} n : Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@one_shot_map A B). Proof. intros f f' Hf; destruct 1; constructor; by try apply Hf. Qed. Definition one_shotC_map {A B} (f : A -n> B) : one_shotC A -n> one_shotC B := CofeMor (one_shot_map f). Instance one_shotC_map_ne A B n : Proper (dist n ==> dist n) (@one_shotC_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 : one_shot A. (* CMRA *) Instance one_shot_valid : Valid (one_shot A) := λ x, match x with | OneShotPending => True | Shot a => ✓ a | OneShotBot => False end. Instance one_shot_validN : ValidN (one_shot A) := λ n x, match x with | OneShotPending => True | Shot a => ✓{n} a | OneShotBot => False end. `````` Robbert Krebbers committed May 28, 2016 125 ``````Instance one_shot_pcore : PCore (one_shot A) := λ x, `````` Ralf Jung committed Mar 11, 2016 126 `````` match x with `````` Robbert Krebbers committed May 28, 2016 127 128 129 `````` | OneShotPending => None | Shot a => Shot <\$> pcore a | OneShotBot => Some OneShotBot `````` Ralf Jung committed Mar 11, 2016 130 131 132 133 134 135 136 137 138 `````` end. Instance one_shot_op : Op (one_shot A) := λ x y, match x, y with | Shot a, Shot b => Shot (a ⋅ b) | _, _ => OneShotBot end. Lemma Shot_op a b : Shot a ⋅ Shot b = Shot (a ⋅ b). Proof. done. Qed. `````` Robbert Krebbers committed Mar 15, 2016 139 `````` `````` Robbert Krebbers committed May 28, 2016 140 141 ``````Lemma one_shot_included x y : x ≼ y ↔ y = OneShotBot ∨ ∃ a b, x = Shot a ∧ y = Shot b ∧ a ≼ b. `````` Ralf Jung committed Mar 11, 2016 142 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 143 144 145 146 147 148 149 150 `````` split. - intros [z Hy]; destruct x as [|a|], z as [|b|]; inversion_clear Hy; auto. right; eexists _, _; split_and!; eauto. setoid_subst; eauto using cmra_included_l. - intros [->|(a&b&->&->&c&?)]. + destruct x; exists OneShotBot; constructor. + exists (Shot c); by constructor. Qed. `````` Ralf Jung committed Mar 11, 2016 151 `````` `````` Robbert Krebbers committed May 27, 2016 152 ``````Lemma one_shot_cmra_mixin : CMRAMixin (one_shot A). `````` Ralf Jung committed Mar 11, 2016 153 154 155 ``````Proof. split. - intros n []; destruct 1; constructor; by cofe_subst. `````` Robbert Krebbers committed May 28, 2016 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 `````` - intros ???? [n|n a b Hab|n] [=]; subst; eauto. destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. destruct (cmra_pcore_ne n a b ca) as (cb&->&?); auto. exists (Shot cb); by repeat constructor. - intros ? [|a|] [|b|] H; inversion_clear H; cofe_subst; done. - intros [|a|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O. - intros n [|a|]; simpl; auto using cmra_validN_S. - intros [|a1|] [|a2|] [|a3|]; constructor; by rewrite ?assoc. - intros [|a1|] [|a2|]; constructor; by rewrite 1?comm. - intros [|a|] ? [=]; subst; auto. destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. constructor; eauto using cmra_pcore_l. - intros [|a|] ? [=]; subst; auto. destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto. - intros x y ? [->|(a&b&->&->&?)]%one_shot_included [=]. { exists OneShotBot. rewrite one_shot_included; eauto. } destruct (pcore a) as [ca|] eqn:?; simplify_option_eq. destruct (cmra_pcore_preserving a b ca) as (cb&->&?); auto. exists (Shot cb). rewrite one_shot_included; eauto 10. - intros n [|a1|] [|a2|]; simpl; eauto using cmra_validN_op_l; done. - intros n [|a|] y1 y2 Hx Hx'. + destruct y1, y2; exfalso; by inversion_clear Hx'. + destruct y1 as [|b1|], y2 as [|b2|]; try (exfalso; by inversion_clear Hx'). apply (inj Shot) in Hx'. destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto. exists (Shot z1, Shot z2). by repeat constructor. `````` Ralf Jung committed Mar 11, 2016 183 184 `````` + by exists (OneShotBot, OneShotBot); destruct y1, y2; inversion_clear Hx'. Qed. `````` Robbert Krebbers committed May 27, 2016 185 ``````Canonical Structure one_shotR := `````` Robbert Krebbers committed May 25, 2016 186 `````` CMRAT (one_shot A) one_shot_cofe_mixin one_shot_cmra_mixin. `````` Robbert Krebbers committed May 28, 2016 187 `````` `````` Ralf Jung committed Mar 11, 2016 188 189 190 ``````Global Instance one_shot_cmra_discrete : CMRADiscrete A → CMRADiscrete one_shotR. Proof. split; first apply _. `````` Robbert Krebbers committed May 28, 2016 191 `````` intros [|a|]; simpl; auto using cmra_discrete_valid. `````` Ralf Jung committed Mar 11, 2016 192 193 ``````Qed. `````` Robbert Krebbers committed Mar 15, 2016 194 ``````Global Instance Shot_persistent a : Persistent a → Persistent (Shot a). `````` Robbert Krebbers committed May 28, 2016 195 ``````Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed. `````` Ralf Jung committed Mar 11, 2016 196 197 198 `````` (** Internalized properties *) Lemma one_shot_equivI {M} (x y : one_shot A) : `````` Robbert Krebbers committed May 31, 2016 199 200 201 202 203 204 `````` x ≡ y ⊣⊢ (match x, y with | OneShotPending, OneShotPending => True | Shot a, Shot b => a ≡ b | OneShotBot, OneShotBot => True | _, _ => False end : uPred M). `````` Ralf Jung committed Mar 11, 2016 205 206 207 208 209 ``````Proof. uPred.unseal; do 2 split; first by destruct 1. by destruct x, y; try destruct 1; try constructor. Qed. Lemma one_shot_validI {M} (x : one_shot A) : `````` Robbert Krebbers committed May 31, 2016 210 211 212 213 214 `````` ✓ x ⊣⊢ (match x with | Shot a => ✓ a | OneShotBot => False | _ => True end : uPred M). `````` Ralf Jung committed Mar 11, 2016 215 216 217 218 ``````Proof. uPred.unseal. by destruct x. Qed. (** Updates *) Lemma one_shot_update_shoot (a : A) : ✓ a → OneShotPending ~~> Shot a. `````` Robbert Krebbers committed May 28, 2016 219 ``````Proof. move=> ? n [y|] //= ?. by apply cmra_valid_validN. Qed. `````` Ralf Jung committed Mar 11, 2016 220 221 ``````Lemma one_shot_update (a1 a2 : A) : a1 ~~> a2 → Shot a1 ~~> Shot a2. Proof. `````` Robbert Krebbers committed May 28, 2016 222 223 224 `````` intros Ha n [[|b|]|] ?; simpl in *; auto. - by apply (Ha n (Some b)). - by apply (Ha n None). `````` Ralf Jung committed Mar 11, 2016 225 ``````Qed. `````` Ralf Jung committed Mar 11, 2016 226 227 228 ``````Lemma one_shot_updateP (P : A → Prop) (Q : one_shot A → Prop) a : a ~~>: P → (∀ b, P b → Q (Shot b)) → Shot a ~~>: Q. Proof. `````` Robbert Krebbers committed May 28, 2016 229 230 231 `````` intros Hx HP n mf Hm. destruct mf as [[|b|]|]; try by destruct Hm. - destruct (Hx n (Some b)) as (c&?&?); naive_solver. - destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l. `````` Ralf Jung committed Mar 11, 2016 232 233 234 235 ``````Qed. Lemma one_shot_updateP' (P : A → Prop) a : a ~~>: P → Shot a ~~>: λ m', ∃ b, m' = Shot b ∧ P b. Proof. eauto using one_shot_updateP. Qed. `````` Ralf Jung committed Mar 11, 2016 236 237 238 239 240 241 242 243 244 ``````End cmra. Arguments one_shotR : clear implicits. (* Functor *) Instance one_shot_map_cmra_monotone {A B : cmraT} (f : A → B) : CMRAMonotone f → CMRAMonotone (one_shot_map f). Proof. split; try apply _. `````` Robbert Krebbers committed May 28, 2016 245 246 247 `````` - intros n [|a|]; simpl; auto using validN_preserving. - intros x y; rewrite !one_shot_included. intros [->|(a&b&->&->&?)]; simpl; eauto 10 using included_preserving. `````` Ralf Jung committed Mar 11, 2016 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 ``````Qed. Program Definition one_shotRF (F : rFunctor) : rFunctor := {| rFunctor_car A B := one_shotR (rFunctor_car F A B); rFunctor_map A1 A2 B1 B2 fg := one_shotC_map (rFunctor_map F fg) |}. Next Obligation. by intros F A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_ne. Qed. Next Obligation. intros F A B x. rewrite /= -{2}(one_shot_map_id x). apply one_shot_map_ext=>y; apply rFunctor_id. Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -one_shot_map_compose. apply one_shot_map_ext=>y; apply rFunctor_compose. Qed. Instance one_shotRF_contractive F : rFunctorContractive F → rFunctorContractive (one_shotRF F). Proof. by intros ? A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_contractive. Qed.``````