1 ``````From fri.algebra Require Export cmra. `````` Robbert Krebbers committed Jun 16, 2016 2 3 `````` (** * Frame preserving updates *) `````` Ralf Jung committed Jun 23, 2016 4 5 6 7 ``````(* This quantifies over [option A] for the frame. That is necessary to make the following hold: x ~~> P → Some c ~~> Some P *) `````` Robbert Krebbers committed Jun 16, 2016 8 9 ``````Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz, ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz). `````` Robbert Krebbers committed May 20, 2019 10 ``````Instance: Params (@cmra_updateP) 1 := {}. `````` Robbert Krebbers committed Jun 16, 2016 11 12 13 14 15 ``````Infix "~~>:" := cmra_updateP (at level 70). Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz, ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz). Infix "~~>" := cmra_update (at level 70). `````` Robbert Krebbers committed May 20, 2019 16 ``````Instance: Params (@cmra_update) 1 := {}. `````` Robbert Krebbers committed Jun 16, 2016 17 `````` `````` Joseph Tassarotti committed Jul 27, 2016 18 19 20 ``````Definition cmra_step_updateP {A : cmraT} (x : A) (xl: A) (P : A → A → Prop) := ∀ n mz, ✓{n} (x ⋅ xl ⋅? mz) → ∃ y yl, P y yl ∧ ✓{n} (y ⋅ yl ⋅? mz) ∧ xl ⤳_(n) yl. Notation "x # y ~~>>: P" := (cmra_step_updateP x y P) (at level 70). `````` Robbert Krebbers committed May 20, 2019 21 ``````Instance: Params (@cmra_step_updateP) 1 := {}. `````` Joseph Tassarotti committed Jul 27, 2016 22 23 24 `````` Definition cmra_step_update {A : cmraT} (x xl y yl : A) := ∀ n mz, ✓{n} (x ⋅ xl ⋅? mz) → ✓{n} (y ⋅ yl ⋅? mz) ∧ xl ⤳_(n) yl. `````` Joseph Tassarotti committed Nov 30, 2017 25 ``````Notation "x # xl ~~>> y #' yl " := (cmra_step_update x xl y yl) (at level 70). `````` Robbert Krebbers committed May 20, 2019 26 ``````Instance: Params (@cmra_step_update) 1 := {}. `````` Joseph Tassarotti committed Jul 27, 2016 27 28 `````` `````` Robbert Krebbers committed Jul 25, 2016 29 ``````Section updates. `````` Robbert Krebbers committed Jun 16, 2016 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 ``````Context {A : cmraT}. Implicit Types x y : A. Global Instance cmra_updateP_proper : Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A). Proof. rewrite /pointwise_relation /cmra_updateP=> x x' Hx P P' HP; split=> ? n mz; setoid_subst; naive_solver. Qed. Global Instance cmra_update_proper : Proper ((≡) ==> (≡) ==> iff) (@cmra_update A). Proof. rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto. Qed. `````` Robbert Krebbers committed Sep 20, 2019 45 ``````Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =.). `````` Robbert Krebbers committed Jun 16, 2016 46 47 48 49 50 51 52 53 54 ``````Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed. Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P. Proof. intros ? n mz ?; eauto. Qed. Lemma cmra_updateP_compose (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q. Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed. Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q. Proof. rewrite cmra_update_updateP. `````` Robbert Krebbers committed Sep 20, 2019 55 `````` intros; apply cmra_updateP_compose with (y =.); naive_solver. `````` Robbert Krebbers committed Jun 16, 2016 56 57 58 59 60 61 62 63 64 65 66 67 68 ``````Qed. Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q. Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed. Global Instance cmra_update_preorder : PreOrder (@cmra_update A). Proof. split. - intros x. by apply cmra_update_updateP, cmra_updateP_id. - intros x y z. rewrite !cmra_update_updateP. eauto using cmra_updateP_compose with subst. Qed. Lemma cmra_update_exclusive `{!Exclusive x} y: ✓ y → x ~~> y. `````` Robbert Krebbers committed Jun 16, 2016 69 ``````Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed. `````` Robbert Krebbers committed Jun 16, 2016 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 `````` Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. Proof. intros Hx1 Hx2 Hy n mz ?. destruct (Hx1 n (Some (x2 ⋅? mz))) as (y1&?&?). { by rewrite /= -cmra_opM_assoc. } destruct (Hx2 n (Some (y1 ⋅? mz))) as (y2&?&?). { by rewrite /= -cmra_opM_assoc (comm _ x2) cmra_opM_assoc. } exists (y1 ⋅ y2); split; last rewrite (comm _ y1) cmra_opM_assoc; auto. Qed. Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 : x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2. Proof. eauto 10 using cmra_updateP_op. Qed. Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2. Proof. rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence. Qed. `````` 90 91 92 93 94 95 96 ``````Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y. Proof. intros H n mz Hmz. apply H, Hmz. apply (cmra_validN_le n); last lia. destruct mz. eapply cmra_validN_op_l, Hmz. apply Hmz. Qed. `````` Robbert Krebbers committed Jun 16, 2016 97 `````` `````` Joseph Tassarotti committed Jul 27, 2016 98 ``````Lemma cmra_step_stepP (x xl y yl: A) : `````` Joseph Tassarotti committed Nov 30, 2017 99 `````` x # xl ~~>> y #' yl ↔ (x # xl ~~>>: (λ x xl, y = x ∧ yl = xl)). `````` Joseph Tassarotti committed Jul 27, 2016 100 101 102 103 104 105 106 107 108 109 110 111 112 113 ``````Proof. split. - by intros Hx n z ?; exists y, yl; destruct (Hx n z) as (?&?); auto. - intros Hx n z ?. destruct (Hx n z) as (?&?&(<-&<-)&?); auto. Qed. Lemma cmra_step_updateP_weaken (P Q : A → A → Prop) x xl: x # xl ~~>>: P → (∀ y yl, P y yl → Q y yl) → x # xl ~~>>: Q. Proof. intros Hs HPQ n z Hval. edestruct (Hs n z Hval) as (y&yl&HP&Hval'&Hs'). exists y, yl. split_and!; eauto. Qed. `````` Robbert Krebbers committed Jun 16, 2016 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 ``````(** ** Frame preserving updates for total CMRAs *) Section total_updates. Context `{CMRATotal A}. Lemma cmra_total_updateP x (P : A → Prop) : x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z). Proof. split=> Hup; [intros n z; apply (Hup n (Some z))|]. intros n [z|] ?; simpl; [by apply Hup|]. destruct (Hup n (core x)) as (y&?&?); first by rewrite cmra_core_r. eauto using cmra_validN_op_l. Qed. Lemma cmra_total_update x y : x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z). Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed. `````` Joseph Tassarotti committed Jul 27, 2016 129 130 131 132 133 134 135 136 137 138 139 `````` Lemma cmra_total_step_updateP (x : A) (xl: A) (P : A → A → Prop) : x # xl ~~>>: P ↔ ∀ n z, ✓{n} (x ⋅ xl ⋅ z) → ∃ y yl, P y yl ∧ ✓{n} (y ⋅ yl ⋅ z) ∧ xl ⤳_(n) yl. Proof. split=> Hup; [intros n z; apply (Hup n (Some z))|]. intros n [z|] ?; simpl; [by apply Hup|]. destruct (Hup n (core (x ⋅ xl))) as (y&yl&?&?&?); first by rewrite cmra_core_r. do 2 eexists. split_and!; eauto using cmra_validN_op_l. Qed. Lemma cmra_total_step_update (x xl y yl : A) : `````` Joseph Tassarotti committed Nov 30, 2017 140 `````` (x # xl ~~>> y #' yl) ↔ `````` Joseph Tassarotti committed Jul 27, 2016 141 142 143 144 `````` ∀ n z, ✓{n} (x ⋅ xl ⋅ z) → ✓{n} (y ⋅ yl ⋅ z) ∧ xl ⤳_(n) yl. Proof. rewrite cmra_step_stepP cmra_total_step_updateP. naive_solver. Qed. `````` Robbert Krebbers committed Jun 16, 2016 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 `````` Context `{CMRADiscrete A}. Lemma cmra_discrete_updateP (x : A) (P : A → Prop) : x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z). Proof. rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using 0. Qed. Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) : x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z). Proof. rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using 0. Qed. End total_updates. `````` Robbert Krebbers committed Jul 25, 2016 160 ``````End updates. `````` Robbert Krebbers committed Jun 16, 2016 161 `````` `````` Joseph Tassarotti committed Jul 27, 2016 162 163 164 165 166 167 ``````Section unit_updates. Context {A: ucmraT}. Implicit Types x y : A. Lemma ucmra_update_unit x : x ~~> ∅. Proof. apply cmra_total_update=>n z. rewrite left_id; apply cmra_validN_op_r. Qed. Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y. `````` Joseph Tassarotti committed Nov 30, 2017 168 `````` Proof. split; [intros; trans (∅ : A)|]; auto using ucmra_update_unit. Qed. `````` Joseph Tassarotti committed Jul 27, 2016 169 170 171 ``````End unit_updates. `````` Robbert Krebbers committed Jun 16, 2016 172 ``````(** * Transport *) `````` Robbert Krebbers committed Jun 16, 2016 173 174 175 176 177 178 179 180 181 ``````Section cmra_transport. Context {A B : cmraT} (H : A = B). Notation T := (cmra_transport H). Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x : x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q. Proof. destruct H; eauto using cmra_updateP_weaken. Qed. Lemma cmra_transport_updateP' (P : A → Prop) x : x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'. Proof. eauto using cmra_transport_updateP. Qed. `````` Joseph Tassarotti committed Jul 27, 2016 182 183 184 185 186 187 188 189 190 191 192 193 `````` Lemma cmra_transport_update x y : x ~~> y → T x ~~> T y. Proof. destruct H; eauto using cmra_updateP_weaken. Qed. Lemma cmra_transport_step_updateP (P : A → A → Prop) (Q : B → B → Prop) x xl : x # xl ~~>>: P → (∀ y yl, P y yl → Q (T y) (T yl)) → T x # T xl ~~>>: Q. Proof. destruct H. eauto using cmra_step_updateP_weaken. Qed. Lemma cmra_transport_step_updateP' (P : A → A → Prop) (Q : B → B → Prop) x xl : x # xl ~~>>: P → T x # T xl ~~>>: (λ y yl, ∃ y' yl', y = cmra_transport H y' ∧ yl = cmra_transport H yl' ∧ P y' yl'). Proof. intros. eapply cmra_transport_step_updateP; eauto. Qed. Lemma cmra_transport_step_update x xl y yl : `````` Joseph Tassarotti committed Nov 30, 2017 194 `````` x # xl ~~>> y #' yl → T x # T xl ~~>> T y #' T yl. `````` Joseph Tassarotti committed Jul 27, 2016 195 `````` Proof. destruct H; eauto using cmra_updateP_weaken. Qed. `````` Robbert Krebbers committed Jun 16, 2016 196 197 ``````End cmra_transport. `````` Joseph Tassarotti committed Jul 27, 2016 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 ``````(** * ucmra Transport *) Section ucmra_transport. Context {A B : ucmraT} (H : A = B). Notation T := (ucmra_transport H). Lemma ucmra_transport_updateP (P : A → Prop) (Q : B → Prop) x : x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q. Proof. destruct H; eauto using cmra_updateP_weaken. Qed. Lemma ucmra_transport_updateP' (P : A → Prop) x : x ~~>: P → T x ~~>: λ y, ∃ y', y = ucmra_transport H y' ∧ P y'. Proof. eauto using ucmra_transport_updateP. Qed. Lemma ucmra_transport_update x y : x ~~> y → T x ~~> T y. Proof. destruct H; eauto using cmra_updateP_weaken. Qed. Lemma ucmra_transport_step_updateP (P : A → A → Prop) (Q : B → B → Prop) x xl : x # xl ~~>>: P → (∀ y yl, P y yl → Q (T y) (T yl)) → T x # T xl ~~>>: Q. Proof. destruct H. eauto using cmra_step_updateP_weaken. Qed. Lemma ucmra_transport_step_updateP' (P : A → A → Prop) (Q : B → B → Prop) x xl : x # xl ~~>>: P → T x # T xl ~~>>: (λ y yl, ∃ y' yl', y = ucmra_transport H y' ∧ yl = ucmra_transport H yl' ∧ P y' yl'). Proof. intros. eapply ucmra_transport_step_updateP; eauto. Qed. Lemma ucmra_transport_step_update x xl y yl : `````` Joseph Tassarotti committed Nov 30, 2017 220 `````` x # xl ~~>> y #' yl → T x # T xl ~~>> T y #' T yl. `````` Joseph Tassarotti committed Jul 27, 2016 221 222 223 `````` Proof. destruct H; eauto using cmra_updateP_weaken. Qed. End ucmra_transport. `````` Robbert Krebbers committed Jun 16, 2016 224 225 226 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 256 257 258 259 260 261 262 263 ``````(** * Product *) Section prod. Context {A B : cmraT}. Implicit Types x : A * B. Lemma prod_updateP P1 P2 (Q : A * B → Prop) x : x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q. Proof. intros Hx1 Hx2 HP n mz [??]; simpl in *. destruct (Hx1 n (fst <\$> mz)) as (a&?&?); first by destruct mz. destruct (Hx2 n (snd <\$> mz)) as (b&?&?); first by destruct mz. exists (a,b); repeat split; destruct mz; auto. Qed. Lemma prod_updateP' P1 P2 x : x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2). Proof. eauto using prod_updateP. Qed. Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y. Proof. rewrite !cmra_update_updateP. destruct x, y; eauto using prod_updateP with subst. Qed. End prod. (** * Option *) Section option. Context {A : cmraT}. Implicit Types x y : A. Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x : x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q. Proof. intros Hx Hy; apply cmra_total_updateP=> n [y|] ?. { destruct (Hx n (Some y)) as (y'&?&?); auto. exists (Some y'); auto. } destruct (Hx n None) as (y'&?&?); rewrite ?cmra_core_r; auto. by exists (Some y'); auto. Qed. Lemma option_updateP' (P : A → Prop) x : x ~~>: P → Some x ~~>: from_option P False. Proof. eauto using option_updateP. Qed. Lemma option_update x y : x ~~> y → Some x ~~> Some y. `````` Robbert Krebbers committed Jun 16, 2016 264 `````` Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed. `````` Robbert Krebbers committed Jun 16, 2016 265 ``End option.``