upred.v 32.6 KB
 Robbert Krebbers committed Oct 30, 2017 1 ``````From iris.algebra Require Export cmra updates. `````` 2 ``````From iris.bi Require Import notation. `````` Robbert Krebbers committed Dec 02, 2017 3 ``````From stdpp Require Import finite. `````` Ralf Jung committed Jun 05, 2018 4 ``````From Coq.Init Require Import Nat. `````` Ralf Jung committed Jan 05, 2017 5 ``````Set Default Proof Using "Type". `````` Tej Chajed committed Nov 29, 2018 6 7 8 ``````Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core. Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core. Local Hint Extern 10 (_ ≤ _) => lia : core. `````` Robbert Krebbers committed Oct 25, 2016 9 `````` `````` Ralf Jung committed Jan 05, 2017 10 11 12 13 14 ``````(** The basic definition of the uPred type, its metric and functor laws. You probably do not want to import this file. Instead, import base_logic.base_logic; that will also give you all the primitive and many derived laws for the logic. *) `````` Ralf Jung committed Dec 08, 2017 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 ``````(* A good way of understanding this definition of the uPred OFE is to consider the OFE uPred0 of monotonous SProp predicates. That is, uPred0 is the OFE of non-expansive functions from M to SProp that are monotonous with respect to CMRA inclusion. This notion of monotonicity has to be stated in the SProp logic. Together with the usual closedness property of SProp, this gives exactly uPred_mono. Then, we quotient uPred0 *in the sProp logic* with respect to equivalence on valid elements of M. That is, we quotient with respect to the following *sProp* equivalence relation: P1 ≡ P2 := ∀ x, ✓ x → (P1(x) ↔ P2(x)) (1) When seen from the ambiant logic, obtaining this quotient requires definig both a custom Equiv and Dist. It is worth noting that this equivalence relation admits canonical representatives. More precisely, one can show that every equivalence class contains exactly one element P0 such that: `````` Ralf Jung committed Dec 08, 2017 33 34 35 36 37 `````` ∀ x, (✓ x → P0(x)) → P0(x) (2) (Again, this assertion has to be understood in sProp). Intuitively, this says that P0 trivially holds whenever the resource is invalid. Starting from any element P, one can find this canonical representative by choosing: `````` Ralf Jung committed Dec 08, 2017 38 39 40 41 42 43 44 45 46 47 48 49 `````` P0(x) := ✓ x → P(x) (3) Hence, as an alternative definition of uPred, we could use the set of canonical representatives (i.e., the subtype of monotonous sProp predicates that verify (2)). This alternative definition would save us from using a quotient. However, the definitions of the various connectives would get more complicated, because we have to make sure they all verify (2), which sometimes requires some adjustments. We would moreover need to prove one more property for every logical connective. *) `````` Robbert Krebbers committed Jan 18, 2019 50 ``````Record uPred (M : ucmraT) : Type := UPred { `````` Robbert Krebbers committed Oct 25, 2016 51 `````` uPred_holds :> nat → M → Prop; `````` Jacques-Henri Jourdan committed Apr 04, 2017 52 `````` `````` Jacques-Henri Jourdan committed Dec 07, 2017 53 54 `````` uPred_mono n1 n2 x1 x2 : uPred_holds n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → uPred_holds n2 x2 `````` Robbert Krebbers committed Oct 25, 2016 55 ``````}. `````` 56 57 ``````Bind Scope bi_scope with uPred. Arguments uPred_holds {_} _%I _ _ : simpl never. `````` Robbert Krebbers committed Oct 25, 2016 58 ``````Add Printing Constructor uPred. `````` Maxime Dénès committed Jan 24, 2019 59 ``````Instance: Params (@uPred_holds) 3 := {}. `````` Robbert Krebbers committed Oct 25, 2016 60 61 62 63 64 65 66 67 68 69 `````` Section cofe. Context {M : ucmraT}. Inductive uPred_equiv' (P Q : uPred M) : Prop := { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }. Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'. Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop := { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }. Instance uPred_dist : Dist (uPred M) := uPred_dist'. `````` Ralf Jung committed Nov 22, 2016 70 `````` Definition uPred_ofe_mixin : OfeMixin (uPred M). `````` Robbert Krebbers committed Oct 25, 2016 71 72 73 74 75 76 77 78 79 80 81 82 `````` Proof. split. - intros P Q; split. + by intros HPQ n; split=> i x ??; apply HPQ. + intros HPQ; split=> n x ?; apply HPQ with n; auto. - intros n; split. + by intros P; split=> x i. + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ. + intros P Q Q' HP HQ; split=> i x ??. by trans (Q i x);[apply HP|apply HQ]. - intros n P Q HPQ; split=> i x ??; apply HPQ; auto. Qed. `````` Ralf Jung committed Nov 22, 2016 83 84 85 `````` Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin. Program Definition uPred_compl : Compl uPredC := λ c, `````` Jacques-Henri Jourdan committed Dec 06, 2017 86 `````` {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'}x → c n' n' x |}. `````` Ralf Jung committed Nov 22, 2016 87 `````` Next Obligation. `````` Jacques-Henri Jourdan committed Dec 07, 2017 88 89 90 `````` move=> /= c n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv. eapply uPred_mono. eapply HP, cmra_validN_includedN, cmra_includedN_le=>//; lia. eapply cmra_includedN_le=>//; lia. done. `````` Ralf Jung committed Nov 22, 2016 91 92 93 `````` Qed. Global Program Instance uPred_cofe : Cofe uPredC := {| compl := uPred_compl |}. Next Obligation. `````` Jacques-Henri Jourdan committed Dec 06, 2017 94 95 `````` intros n c; split=>i x Hin Hv. etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|]. `````` Jacques-Henri Jourdan committed Dec 07, 2017 96 `````` repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono. `````` Ralf Jung committed Nov 22, 2016 97 `````` Qed. `````` Robbert Krebbers committed Oct 25, 2016 98 99 100 101 102 103 104 105 106 107 108 109 110 ``````End cofe. Arguments uPredC : clear implicits. Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n). Proof. intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx. Qed. Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n). Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed. Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x : P ≡{n2}≡ Q → n2 ≤ n1 → ✓{n2} x → Q n1 x → P n2 x. Proof. `````` Jacques-Henri Jourdan committed Dec 07, 2017 111 `````` intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le. `````` Robbert Krebbers committed Oct 25, 2016 112 113 ``````Qed. `````` Ralf Jung committed Dec 08, 2017 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 ``````(* Equivalence to the definition of uPred in the appendix. *) Lemma uPred_alt {M : ucmraT} (P: nat → M → Prop) : (∀ n1 n2 x1 x2, P n1 x1 → x1 ≼{n1} x2 → n2 ≤ n1 → P n2 x2) ↔ ( (∀ x n1 n2, n2 ≤ n1 → P n1 x → P n2 x) (* Pointwise down-closed *) ∧ (∀ n x1 x2, x1 ≡{n}≡ x2 → ∀ m, m ≤ n → P m x1 ↔ P m x2) (* Non-expansive *) ∧ (∀ n x1 x2, x1 ≼{n} x2 → ∀ m, m ≤ n → P m x1 → P m x2) (* Monotonicity *) ). Proof. (* Provide this lemma to eauto. *) assert (∀ n1 n2 (x1 x2 : M), n2 ≤ n1 → x1 ≡{n1}≡ x2 → x1 ≼{n2} x2). { intros ????? H. eapply cmra_includedN_le; last done. by rewrite H. } (* Now go ahead. *) split. - intros Hupred. repeat split; eauto using cmra_includedN_le. - intros (Hdown & _ & Hmono) **. eapply Hmono; [done..|]. eapply Hdown; done. `````` Robbert Krebbers committed Oct 25, 2016 129 130 131 132 ``````Qed. (** functor *) Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1) `````` Robbert Krebbers committed Oct 25, 2017 133 `````` `{!CmraMorphism f} (P : uPred M1) : `````` Robbert Krebbers committed Oct 25, 2016 134 `````` uPred M2 := {| uPred_holds n x := P n (f x) |}. `````` 135 ``````Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed. `````` Robbert Krebbers committed Oct 25, 2016 136 137 `````` Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1) `````` Robbert Krebbers committed Oct 25, 2017 138 `````` `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f). `````` Robbert Krebbers committed Oct 25, 2016 139 140 ``````Proof. intros x1 x2 Hx; split=> n' y ??. `````` 141 `````` split; apply Hx; auto using cmra_morphism_validN. `````` Robbert Krebbers committed Oct 25, 2016 142 143 144 145 ``````Qed. Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P. Proof. by split=> n x ?. Qed. Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3) `````` Robbert Krebbers committed Oct 25, 2017 146 `````` `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3): `````` Robbert Krebbers committed Oct 25, 2016 147 148 149 `````` uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P). Proof. by split=> n x Hx. Qed. Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2) `````` Robbert Krebbers committed Oct 25, 2017 150 `````` `{!CmraMorphism f} `{!CmraMorphism g}: `````` Robbert Krebbers committed Oct 25, 2016 151 152 `````` (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x. Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed. `````` Robbert Krebbers committed Oct 25, 2017 153 ``````Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} : `````` Robbert Krebbers committed Oct 25, 2016 154 155 `````` uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2). Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1) `````` Robbert Krebbers committed Oct 25, 2017 156 `````` `{!CmraMorphism f, !CmraMorphism g} n : `````` Robbert Krebbers committed Oct 25, 2016 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 `````` f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g. Proof. by intros Hfg P; split=> n' y ??; rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia. Qed. Program Definition uPredCF (F : urFunctor) : cFunctor := {| cFunctor_car A B := uPredC (urFunctor_car F B A); cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1)) |}. Next Obligation. intros F A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ. Qed. Next Obligation. intros F A B P; simpl. rewrite -{2}(uPred_map_id P). apply uPred_map_ext=>y. by rewrite urFunctor_id. Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose. apply uPred_map_ext=>y; apply urFunctor_compose. Qed. Instance uPredCF_contractive F : urFunctorContractive F → cFunctorContractive (uPredCF F). Proof. `````` Robbert Krebbers committed Dec 05, 2016 183 184 `````` intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive. destruct n; split; by apply HPQ. `````` Robbert Krebbers committed Oct 25, 2016 185 186 187 188 189 ``````Qed. (** logical entailement *) Inductive uPred_entails {M} (P Q : uPred M) : Prop := { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }. `````` Jacques-Henri Jourdan committed Dec 07, 2017 190 ``````Hint Resolve uPred_mono : uPred_def. `````` Robbert Krebbers committed Oct 25, 2016 191 `````` `````` Robbert Krebbers committed Oct 30, 2017 192 193 194 195 196 ``````(** logical connectives *) Program Definition uPred_pure_def {M} (φ : Prop) : uPred M := {| uPred_holds n x := φ |}. Solve Obligations with done. Definition uPred_pure_aux : seal (@uPred_pure_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 197 ``````Definition uPred_pure {M} := uPred_pure_aux.(unseal) M. `````` Robbert Krebbers committed Oct 30, 2017 198 ``````Definition uPred_pure_eq : `````` Ralf Jung committed Mar 05, 2018 199 `````` @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 200 201 202 203 204 `````` Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := P n x ∧ Q n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_and_aux : seal (@uPred_and_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 205 206 ``````Definition uPred_and {M} := uPred_and_aux.(unseal) M. Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 207 208 209 210 211 `````` Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := P n x ∨ Q n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 212 213 ``````Definition uPred_or {M} := uPred_or_aux.(unseal) M. Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 214 215 216 217 218 `````` Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ n' x', x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}. Next Obligation. `````` Jacques-Henri Jourdan committed Dec 21, 2017 219 `````` intros M P Q n1 n1' x1 x1' HPQ [x2 Hx1'] Hn1 n2 x3 [x4 Hx3] ?; simpl in *. `````` Robbert Krebbers committed Oct 30, 2017 220 221 222 223 `````` rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??. eapply HPQ; auto. exists (x2 ⋅ x4); by rewrite assoc. Qed. Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 224 ``````Definition uPred_impl {M} := uPred_impl_aux.(unseal) M. `````` Robbert Krebbers committed Oct 30, 2017 225 ``````Definition uPred_impl_eq : `````` Ralf Jung committed Mar 05, 2018 226 `````` @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 227 228 229 230 231 `````` Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M := {| uPred_holds n x := ∀ a, Ψ a n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_forall_aux : seal (@uPred_forall_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 232 ``````Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A. `````` Robbert Krebbers committed Oct 30, 2017 233 ``````Definition uPred_forall_eq : `````` Ralf Jung committed Mar 05, 2018 234 `````` @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 235 236 237 238 239 `````` Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M := {| uPred_holds n x := ∃ a, Ψ a n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. Definition uPred_exist_aux : seal (@uPred_exist_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 240 241 ``````Definition uPred_exist {M A} := uPred_exist_aux.(unseal) M A. Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 242 243 244 245 246 `````` Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M := {| uPred_holds n x := a1 ≡{n}≡ a2 |}. Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)). Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 247 ``````Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A. `````` Robbert Krebbers committed Oct 30, 2017 248 ``````Definition uPred_internal_eq_eq: `````` Ralf Jung committed Mar 05, 2018 249 `````` @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 250 251 252 253 `````` Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}. Next Obligation. `````` Jacques-Henri Jourdan committed Dec 21, 2017 254 `````` intros M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn. `````` Robbert Krebbers committed Oct 30, 2017 255 `````` exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_includedN_l. `````` Jacques-Henri Jourdan committed Dec 21, 2017 256 `````` eapply dist_le, Hn. by rewrite Hy Hx assoc. `````` Robbert Krebbers committed Oct 30, 2017 257 258 ``````Qed. Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 259 260 ``````Definition uPred_sep {M} := uPred_sep_aux.(unseal) M. Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 261 262 263 264 265 `````` Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ n' x', n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}. Next Obligation. `````` Jacques-Henri Jourdan committed Dec 21, 2017 266 267 `````` intros M P Q n1 n1' x1 x1' HPQ ? Hn n3 x3 ???; simpl in *. eapply uPred_mono with n3 (x1 ⋅ x3); `````` Robbert Krebbers committed Oct 30, 2017 268 269 270 `````` eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le. Qed. Definition uPred_wand_aux : seal (@uPred_wand_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 271 ``````Definition uPred_wand {M} := uPred_wand_aux.(unseal) M. `````` Robbert Krebbers committed Oct 30, 2017 272 ``````Definition uPred_wand_eq : `````` Ralf Jung committed Mar 05, 2018 273 `````` @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 274 `````` `````` Jacques-Henri Jourdan committed Nov 03, 2017 275 276 277 ``````(* Equivalently, this could be `∀ y, P n y`. That's closer to the intuition of "embedding the step-indexed logic in Iris", but the two are equivalent because Iris is afine. The following is easier to work with. *) `````` 278 ``````Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M := `````` Jacques-Henri Jourdan committed Nov 03, 2017 279 `````` {| uPred_holds n x := P n ε |}. `````` Jacques-Henri Jourdan committed Dec 21, 2017 280 ``````Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN. `````` Ralf Jung committed Mar 05, 2018 281 282 283 284 ``````Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed. Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M. Definition uPred_plainly_eq : @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq). `````` Jacques-Henri Jourdan committed Nov 03, 2017 285 `````` `````` Robbert Krebbers committed Oct 30, 2017 286 287 288 289 290 291 ``````Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M := {| uPred_holds n x := P n (core x) |}. Next Obligation. intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN. Qed. Definition uPred_persistently_aux : seal (@uPred_persistently_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 292 ``````Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M. `````` Robbert Krebbers committed Oct 30, 2017 293 ``````Definition uPred_persistently_eq : `````` Ralf Jung committed Mar 05, 2018 294 `````` @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 295 296 297 298 `````` Program Definition uPred_later_def {M} (P : uPred M) : uPred M := {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}. Next Obligation. `````` Jacques-Henri Jourdan committed Dec 21, 2017 299 `````` intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia. `````` Robbert Krebbers committed Oct 30, 2017 300 301 ``````Qed. Definition uPred_later_aux : seal (@uPred_later_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 302 ``````Definition uPred_later {M} := uPred_later_aux.(unseal) M. `````` Robbert Krebbers committed Oct 30, 2017 303 ``````Definition uPred_later_eq : `````` Ralf Jung committed Mar 05, 2018 304 `````` @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 305 306 307 308 `````` Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M := {| uPred_holds n x := a ≼{n} x |}. Next Obligation. `````` Jacques-Henri Jourdan committed Dec 21, 2017 309 310 `````` intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn. eapply cmra_includedN_le=>//. exists (a' ⋅ x2). by rewrite Hx(assoc op) Hx1. `````` Robbert Krebbers committed Oct 30, 2017 311 312 ``````Qed. Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 313 ``````Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M. `````` Robbert Krebbers committed Oct 30, 2017 314 ``````Definition uPred_ownM_eq : `````` Ralf Jung committed Mar 05, 2018 315 `````` @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 316 317 318 319 320 `````` Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M := {| uPred_holds n x := ✓{n} a |}. Solve Obligations with naive_solver eauto 2 using cmra_validN_le. Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). by eexists. Qed. `````` Ralf Jung committed Mar 05, 2018 321 ``````Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A. `````` Robbert Krebbers committed Oct 30, 2017 322 ``````Definition uPred_cmra_valid_eq : `````` Ralf Jung committed Mar 05, 2018 323 `````` @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq). `````` Robbert Krebbers committed Oct 30, 2017 324 325 326 327 328 `````` Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M := {| uPred_holds n x := ∀ k yf, k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}. Next Obligation. `````` Jacques-Henri Jourdan committed Dec 21, 2017 329 `````` intros M Q n1 n2 x1 x2 HQ [x3 Hx] Hn k yf Hk. `````` Robbert Krebbers committed Oct 30, 2017 330 331 332 `````` rewrite (dist_le _ _ _ _ Hx); last lia. intros Hxy. destruct (HQ k (x3 ⋅ yf)) as (x'&?&?); [auto|by rewrite assoc|]. exists (x' ⋅ x3); split; first by rewrite -assoc. `````` Jacques-Henri Jourdan committed Dec 21, 2017 333 `````` eauto using uPred_mono, cmra_includedN_l. `````` Robbert Krebbers committed Oct 30, 2017 334 ``````Qed. `````` 335 336 337 338 339 340 341 ``````Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed. Definition uPred_bupd {M} := uPred_bupd_aux.(unseal) M. Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq). (** Global uPred-specific Notation *) Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope. `````` Robbert Krebbers committed Oct 30, 2017 342 `````` `````` 343 344 345 346 ``````(** Promitive logical rules. These are not directly usable later because they do not refer to the BI connectives. *) Module uPred_primitive. `````` Robbert Krebbers committed Oct 30, 2017 347 348 349 ``````Definition unseal_eqs := (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq, uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, `````` Jacques-Henri Jourdan committed Nov 03, 2017 350 `````` uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq, `````` Jacques-Henri Jourdan committed Dec 11, 2017 351 `````` uPred_cmra_valid_eq, @uPred_bupd_eq). `````` Ralf Jung committed Jun 05, 2018 352 ``````Ltac unseal := `````` Robbert Krebbers committed Nov 14, 2017 353 `````` rewrite !unseal_eqs /=. `````` Robbert Krebbers committed Oct 30, 2017 354 `````` `````` 355 356 357 358 359 360 ``````Section primitive. Context {M : ucmraT}. Implicit Types φ : Prop. Implicit Types P Q : uPred M. Implicit Types A : Type. Arguments uPred_holds {_} !_ _ _ /. `````` Tej Chajed committed Nov 29, 2018 361 ``````Hint Immediate uPred_in_entails : core. `````` Robbert Krebbers committed Oct 30, 2017 362 `````` `````` 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 ``````Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope. Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope. Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope. Notation "(⊣⊢)" := (@uPred_equiv M) (only parsing) : stdpp_scope. Notation "'True'" := (uPred_pure True) : bi_scope. Notation "'False'" := (uPred_pure False) : bi_scope. Notation "'⌜' φ '⌝'" := (uPred_pure φ%type%stdpp) : bi_scope. Infix "∧" := uPred_and : bi_scope. Infix "∨" := uPred_or : bi_scope. Infix "→" := uPred_impl : bi_scope. Notation "∀ x .. y , P" := (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope. Notation "∃ x .. y , P" := (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope. Infix "∗" := uPred_sep : bi_scope. Infix "-∗" := uPred_wand : bi_scope. Notation "□ P" := (uPred_persistently P) : bi_scope. Notation "■ P" := (uPred_plainly P) : bi_scope. Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope. Notation "▷ P" := (uPred_later P) : bi_scope. Notation "|==> P" := (uPred_bupd P) : bi_scope. (** Entailment *) Lemma entails_po : PreOrder (⊢). `````` Robbert Krebbers committed Oct 30, 2017 388 389 ``````Proof. split. `````` 390 391 392 393 394 395 `````` - by intros P; split=> x i. - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP. Qed. Lemma entails_anti_sym : AntiSymm (⊣⊢) (⊢). Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed. Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P). `````` Robbert Krebbers committed Oct 30, 2017 396 397 ``````Proof. split. `````` 398 399 400 401 402 403 404 405 406 `````` - intros HPQ; split; split=> x i; apply HPQ. - intros [??]. exact: entails_anti_sym. Qed. Lemma entails_lim (cP cQ : chain (uPredC M)) : (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ. Proof. intros Hlim; split=> n m ? HP. eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl. Qed. `````` Robbert Krebbers committed Oct 25, 2016 407 `````` `````` 408 409 410 411 412 ``````(** Non-expansiveness and setoid morphisms *) Lemma pure_ne n : Proper (iff ==> dist n) (@uPred_pure M). Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|m] ?; try apply Hφ. Qed. Lemma and_ne : NonExpansive2 (@uPred_and M). `````` Robbert Krebbers committed Mar 03, 2018 413 ``````Proof. `````` 414 415 `````` intros n P P' HP Q Q' HQ; unseal; split=> x n' ??. split; (intros [??]; split; [by apply HP|by apply HQ]). `````` Robbert Krebbers committed Mar 03, 2018 416 417 ``````Qed. `````` 418 ``````Lemma or_ne : NonExpansive2 (@uPred_or M). `````` Robbert Krebbers committed Mar 03, 2018 419 ``````Proof. `````` 420 421 `````` intros n P P' HP Q Q' HQ; split=> x n' ??. unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]). `````` Robbert Krebbers committed Mar 03, 2018 422 423 ``````Qed. `````` 424 425 426 427 428 429 ``````Lemma impl_ne : NonExpansive2 (@uPred_impl M). Proof. intros n P P' HP Q Q' HQ; split=> x n' ??. unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 430 `````` `````` 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 ``````Lemma sep_ne : NonExpansive2 (@uPred_sep M). Proof. intros n P P' HP Q Q' HQ; split=> n' x ??. unseal; split; intros (x1&x2&?&?&?); ofe_subst x; exists x1, x2; split_and!; try (apply HP || apply HQ); eauto using cmra_validN_op_l, cmra_validN_op_r. Qed. Lemma wand_ne : NonExpansive2 (@uPred_wand M). Proof. intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???; apply HQ, HPQ, HP; eauto using cmra_validN_op_r. Qed. Lemma internal_eq_ne (A : ofeT) : NonExpansive2 (@uPred_internal_eq M A). Proof. intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *. - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto. - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto. Qed. Lemma forall_ne A n : Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A). Proof. by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ. Qed. Lemma exist_ne A n : Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A). Proof. intros Ψ1 Ψ2 HΨ. unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ. Qed. Lemma later_contractive : Contractive (@uPred_later M). Proof. `````` Ralf Jung committed Jun 20, 2018 469 `````` unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia. `````` 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 `````` apply HPQ; eauto using cmra_validN_S. Qed. Lemma plainly_ne : NonExpansive (@uPred_plainly M). Proof. intros n P1 P2 HP. unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN. Qed. Lemma persistently_ne : NonExpansive (@uPred_persistently M). Proof. intros n P1 P2 HP. unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN. Qed. Lemma ownM_ne : NonExpansive (@uPred_ownM M). `````` Robbert Krebbers committed Oct 25, 2016 486 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 487 488 `````` intros n a b Ha. unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. `````` Robbert Krebbers committed Oct 25, 2016 489 490 ``````Qed. `````` 491 ``````Lemma cmra_valid_ne {A : cmraT} : `````` Robbert Krebbers committed Oct 30, 2017 492 `````` NonExpansive (@uPred_cmra_valid M A). `````` Robbert Krebbers committed Oct 25, 2016 493 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 494 495 `````` intros n a b Ha; unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. `````` Robbert Krebbers committed Oct 25, 2016 496 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 497 `````` `````` 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 ``````Lemma bupd_ne : NonExpansive (@uPred_bupd M). Proof. intros n P Q HPQ. unseal; split=> n' x; split; intros HP k yf ??; destruct (HP k yf) as (x'&?&?); auto; exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l. Qed. (** Introduction and elimination rules *) Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝. Proof. by intros ?; unseal; split. Qed. Lemma pure_elim' φ P : (φ → True ⊢ P) → ⌜φ⌝ ⊢ P. Proof. unseal; intros HP; split=> n x ??. by apply HP. Qed. Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ x : A, ⌜φ x⌝) ⊢ ⌜∀ x : A, φ x⌝. Proof. by unseal. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 513 `````` `````` 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 ``````Lemma and_elim_l P Q : P ∧ Q ⊢ P. Proof. by unseal; split=> n x ? [??]. Qed. Lemma and_elim_r P Q : P ∧ Q ⊢ Q. Proof. by unseal; split=> n x ? [??]. Qed. Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R. Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed. Lemma or_intro_l P Q : P ⊢ P ∨ Q. Proof. unseal; split=> n x ??; left; auto. Qed. Lemma or_intro_r P Q : Q ⊢ P ∨ Q. Proof. unseal; split=> n x ??; right; auto. Qed. Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R. Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed. Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R. Proof. unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ; naive_solver eauto using uPred_mono, cmra_included_includedN. Qed. Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R. Proof. unseal; intros HP ; split=> n x ? [??]; apply HP with n x; auto. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 535 `````` `````` 536 537 538 539 ``````Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a. Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed. Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a. Proof. unseal; split=> n x ? HP; apply HP. Qed. `````` Jacques-Henri Jourdan committed Dec 04, 2017 540 `````` `````` 541 542 543 544 545 546 547 ``````Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a. Proof. unseal; split=> n x ??; by exists a. Qed. Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q. Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed. (** BI connectives *) Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'. `````` Ralf Jung committed Dec 21, 2016 548 ``````Proof. `````` 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 `````` intros HQ HQ'; unseal. split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; ofe_subst x; eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails. Qed. Lemma True_sep_1 P : P ⊢ True ∗ P. Proof. unseal; split; intros n x ??. exists (core x), x. by rewrite cmra_core_l. Qed. Lemma True_sep_2 P : True ∗ P ⊢ P. Proof. unseal; split; intros n x ? (x1&x2&?&_&?); ofe_subst; eauto using uPred_mono, cmra_includedN_r. Qed. Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P. Proof. unseal; split; intros n x ? (x1&x2&?&?&?); exists x2, x1; by rewrite (comm op). Qed. Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R). Proof. unseal; split; intros n x ? (x1&x2&Hx&(y1&y2&Hy&?&?)&?). exists y1, (y2 ⋅ x2); split_and?; auto. + by rewrite (assoc op) -Hy -Hx. + by exists y2, x2. Qed. Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R. Proof. unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto. exists x, x'; split_and?; auto. eapply uPred_mono with n x; eauto using cmra_validN_op_l. Qed. Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R. Proof. unseal =>HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst. eapply HPQR; eauto using cmra_validN_op_l. Qed. (** Persistently *) Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q. Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed. Lemma persistently_elim P : □ P ⊢ P. Proof. unseal; split=> n x ? /=. eauto using uPred_mono, @cmra_included_core, cmra_included_includedN. Qed. Lemma persistently_idemp_2 P : □ P ⊢ □ □ P. Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed. Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a). Proof. by unseal. Qed. Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a). Proof. by unseal. Qed. Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ P ∗ Q. Proof. unseal; split=> n x ? [??]; exists (core x), x; simpl in *. by rewrite cmra_core_l. Qed. (** Plainly *) Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q. Proof. intros HP; unseal; split=> n x ? /=. apply HP, ucmra_unit_validN. Qed. Lemma plainly_elim_persistently P : ■ P ⊢ □ P. Proof. unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. Qed. Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P. Proof. unseal; split=> n x ?? //. Qed. Lemma plainly_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ■ Ψ a) ⊢ (■ ∀ a, Ψ a). Proof. by unseal. Qed. Lemma plainly_exist_1 {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊢ (∃ a, ■ Ψ a). Proof. by unseal. Qed. Lemma prop_ext P Q : ■ ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q. Proof. unseal; split=> n x ? /= HPQ. split=> n' x' ??. move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?. move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver. Qed. (* The following two laws are very similar, and indeed they hold not just for □ and ■, but for any modality defined as `M P n x := ∀ y, R x y → P n y`. *) Lemma persistently_impl_plainly P Q : (■ P → □ Q) ⊢ □ (■ P → Q). Proof. unseal; split=> /= n x ? HPQ n' x' ????. eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN]. apply (HPQ n' x); eauto using cmra_validN_le. Qed. Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q). Proof. unseal; split=> /= n x ? HPQ n' x' ????. eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN]. apply (HPQ n' x); eauto using cmra_validN_le. Qed. (** Later *) Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q. Proof. unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S]. Qed. Lemma later_intro P : P ⊢ ▷ P. Proof. unseal; split=> -[|n] /= x ? HP; first done. apply uPred_mono with (S n) x; eauto using cmra_validN_S. Qed. Lemma later_forall_2 {A} (Φ : A → uPred M) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a. Proof. unseal; by split=> -[|n] x. Qed. Lemma later_exist_false {A} (Φ : A → uPred M) : (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a). Proof. unseal; split=> -[|[|n]] x /=; eauto. Qed. Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q. Proof. unseal; split=> n x ?. destruct n as [|n]; simpl. { by exists x, (core x); rewrite cmra_core_r. } intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2) as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *. exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2]. Qed. Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q). Proof. unseal; split=> n x ?. destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)]. exists x1, x2; eauto using dist_S. Qed. Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P). Proof. unseal; split=> -[|n] x ? /= HP; [by left|right]. intros [|n'] x' ????; eauto using uPred_mono, cmra_included_includedN. Qed. Lemma later_persistently_1 P : ▷ □ P ⊢ □ ▷ P. Proof. by unseal. Qed. Lemma later_persistently_2 P : □ ▷ P ⊢ ▷ □ P. Proof. by unseal. Qed. Lemma later_plainly_1 P : ▷ ■ P ⊢ ■ ▷ P. Proof. by unseal. Qed. Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P. Proof. by unseal. Qed. (** Internal equality *) Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ (a ≡ a). Proof. unseal; by split=> n x ??; simpl. Qed. Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) : NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b. Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed. `````` Ralf Jung committed Mar 05, 2019 696 ``````Lemma fun_ext {A} {B : A → ofeT} (g1 g2 : ofe_fun B) : `````` 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 `````` (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2. Proof. by unseal. Qed. Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sigC P) : proj1_sig x ≡ proj1_sig y ⊢ x ≡ y. Proof. by unseal. Qed. Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y). Proof. by unseal. Qed. Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y. Proof. by unseal. Qed. Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝. Proof. unseal=> ?. split=> n x ?. by apply (discrete_iff n). Qed. (** Basic update modality *) Lemma bupd_intro P : P ⊢ |==> P. Proof. unseal. split=> n x ? HP k yf ?; exists x; split; first done. apply uPred_mono with n x; eauto using cmra_validN_op_l. Qed. Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ⊢ |==> Q. Proof. unseal. intros HPQ; split=> n x ? HP k yf ??. destruct (HP k yf) as (x'&?&?); eauto. exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l. Qed. Lemma bupd_trans P : (|==> |==> P) ⊢ |==> P. Proof. unseal; split; naive_solver. Qed. Lemma bupd_frame_r P R : (|==> P) ∗ R ⊢ |==> P ∗ R. Proof. unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??. destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto. { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. } exists (x' ⋅ x2); split; first by rewrite -assoc. exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r. Qed. Lemma bupd_plainly P : (|==> ■ P) ⊢ P. Proof. unseal; split => n x Hnx /= Hng. destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto. eapply uPred_mono; eauto using ucmra_unit_leastN. `````` Ralf Jung committed Dec 21, 2016 740 741 ``````Qed. `````` 742 ``````(** Own *) `````` Robbert Krebbers committed Oct 30, 2017 743 744 745 ``````Lemma ownM_op (a1 a2 : M) : uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2. Proof. `````` 746 `````` unseal; split=> n x ?; split. `````` Robbert Krebbers committed Oct 30, 2017 747 748 749 750 751 752 `````` - intros [z ?]; exists a1, (a2 ⋅ z); split; [by rewrite (assoc op)|]. split. by exists (core a1); rewrite cmra_core_r. by exists z. - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 ⋅ z2). by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1) -(assoc op _ a2) (comm op z1) -Hy1 -Hy2. Qed. `````` 753 ``````Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a). `````` Robbert Krebbers committed Oct 30, 2017 754 ``````Proof. `````` 755 `````` split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN. `````` Robbert Krebbers committed Oct 30, 2017 756 ``````Qed. `````` 757 ``````Lemma ownM_unit P : P ⊢ (uPred_ownM ε). `````` Robbert Krebbers committed Oct 30, 2017 758 ``````Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed. `````` 759 ``````Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b). `````` Robbert Krebbers committed Oct 30, 2017 760 ``````Proof. `````` 761 `````` unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN. `````` Robbert Krebbers committed Oct 30, 2017 762 763 764 765 766 `````` destruct Hax as [y ?]. destruct (cmra_extend n x a y) as (a'&y'&Hx&?&?); auto using cmra_validN_S. exists a'. rewrite Hx. eauto using cmra_includedN_l. Qed. `````` 767 768 769 770 771 772 773 774 775 776 777 ``````Lemma bupd_ownM_updateP x (Φ : M → Prop) : x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y. Proof. unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??. destruct (Hup k (Some (x3 ⋅ yf))) as (y&?&?); simpl in *. { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. } exists (y ⋅ x3); split; first by rewrite -assoc. exists y; eauto using cmra_includedN_l. Qed. (** Valid *) `````` Robbert Krebbers committed Oct 30, 2017 778 779 780 781 ``````Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a. Proof. unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l. Qed. `````` 782 ``````Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a). `````` Robbert Krebbers committed Oct 30, 2017 783 ``````Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed. `````` 784 785 786 ``````Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False. Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed. Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a. `````` Robbert Krebbers committed Oct 30, 2017 787 ``````Proof. by unseal. Qed. `````` 788 ``````Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a. `````` Robbert Krebbers committed Oct 30, 2017 789 790 ``````Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed. `````` 791 ``````Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2. `````` Robbert Krebbers committed Oct 30, 2017 792 793 794 795 796 ``````Proof. by unseal. Qed. Lemma option_validI {A : cmraT} (mx : option A) : ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end. Proof. unseal. by destruct mx. Qed. `````` 797 798 ``````Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝. Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed. `````` Robbert Krebbers committed Dec 02, 2017 799 `````` `````` Ralf Jung committed Mar 05, 2019 800 ``````Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i. `````` 801 802 ``````Proof. by unseal. Qed. `````` Ralf Jung committed Jun 05, 2018 803 ``````(** Consistency/soundness statement *) `````` Ralf Jung committed Mar 29, 2019 804 ``````Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ. `````` Robbert Krebbers committed Mar 29, 2019 805 806 ``````Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed. `````` Ralf Jung committed Mar 29, 2019 807 ``````Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P). `````` Ralf Jung committed Jun 05, 2018 808 ``````Proof. `````` Robbert Krebbers committed Mar 29, 2019 809 810 811 `````` unseal=> -[HP]; split=> n x Hx _. apply uPred_mono with n ε; eauto using ucmra_unit_leastN. by apply (HP (S n)); eauto using ucmra_unit_validN. `````` Ralf Jung committed Jun 05, 2018 812 ``````Qed. `````` 813 814 ``````End primitive. End uPred_primitive.``````