upred.v 33 KB
Newer Older
1
From stdpp Require Import finite.
2 3
From iris.bi Require Import notation.
From iris.algebra Require Export cmra updates.
4
Set Default Proof Using "Type".
Tej Chajed's avatar
Tej Chajed committed
5 6 7
Local Hint Extern 1 (_  _) => etrans; [eassumption|] : core.
Local Hint Extern 1 (_  _) => etrans; [|eassumption] : core.
Local Hint Extern 10 (_  _) => lia : core.
8

Ralf Jung's avatar
Ralf Jung committed
9 10 11 12 13
(** 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's avatar
Ralf Jung committed
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
(* 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's avatar
Ralf Jung committed
32 33 34 35 36
     ∀ 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's avatar
Ralf Jung committed
37 38 39 40 41 42 43 44 45 46 47 48
     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.
 *)

49
Record uPred (M : ucmraT) : Type := UPred {
50
  uPred_holds :> nat  M  Prop;
51

52 53
  uPred_mono n1 n2 x1 x2 :
    uPred_holds n1 x1  x1 {n1} x2  n2  n1  uPred_holds n2 x2
54
}.
55 56
Bind Scope bi_scope with uPred.
Arguments uPred_holds {_} _%I _ _ : simpl never.
57
Add Printing Constructor uPred.
58
Instance: Params (@uPred_holds) 3 := {}.
59 60 61 62 63 64 65 66 67 68

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'.
69
  Definition uPred_ofe_mixin : OfeMixin (uPred M).
70 71 72 73 74 75 76 77 78 79 80 81
  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.
82
  Canonical Structure uPredO : ofeT := OfeT (uPred M) uPred_ofe_mixin.
83

84
  Program Definition uPred_compl : Compl uPredO := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    {| uPred_holds n x :=  n', n'  n  {n'} x  c n' n' x |}.
86
  Next Obligation.
87 88 89
    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.
90
  Qed.
91
  Global Program Instance uPred_cofe : Cofe uPredO := {| compl := uPred_compl |}.
92
  Next Obligation.
93 94
    intros n c; split=>i x Hin Hv.
    etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|].
95
    repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono.
96
  Qed.
97
End cofe.
98
Arguments uPredO : clear implicits.
99 100 101 102 103 104 105 106 107 108 109

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.
110
  intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
111 112
Qed.

113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
(* 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.
128 129 130 131
Qed.

(** functor *)
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
132
  `{!CmraMorphism f} (P : uPred M1) :
133
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
134
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
135 136

Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
137
  `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
138 139
Proof.
  intros x1 x2 Hx; split=> n' y ??.
140
  split; apply Hx; auto using cmra_morphism_validN.
141 142 143 144
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)
145
    `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
146 147 148
  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)
149
      `{!CmraMorphism f} `{!CmraMorphism g}:
150 151
  ( 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.
152 153 154
Definition uPredO_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
  uPredO M1 -n> uPredO M2 := OfeMor (uPred_map f : uPredO M1  uPredO M2).
Lemma uPredO_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
155
    `{!CmraMorphism f, !CmraMorphism g} n :
156
  f {n} g  uPredO_map f {n} uPredO_map g.
157 158 159 160 161
Proof.
  by intros Hfg P; split=> n' y ??;
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.

162 163 164
Program Definition uPredOF (F : urFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := uPredO (urFunctor_car F B A);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := uPredO_map (urFunctor_map F (fg.2, fg.1))
165 166
|}.
Next Obligation.
167
  intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
168
  apply uPredO_map_ne, urFunctor_map_ne; split; by apply HPQ.
169 170
Qed.
Next Obligation.
171
  intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
172
  apply uPred_map_ext=>y. by rewrite urFunctor_map_id.
173 174
Qed.
Next Obligation.
175
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' P; simpl. rewrite -uPred_map_compose.
176
  apply uPred_map_ext=>y; apply urFunctor_map_compose.
177 178
Qed.

179 180
Instance uPredOF_contractive F :
  urFunctorContractive F  oFunctorContractive (uPredOF F).
181
Proof.
182 183
  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
  apply uPredO_map_ne, urFunctor_map_contractive. destruct n; split; by apply HPQ.
184 185 186 187 188
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 }.
189
Hint Resolve uPred_mono : uPred_def.
190

Robbert Krebbers's avatar
Robbert Krebbers committed
191 192 193 194
(** logical connectives *)
Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
  {| uPred_holds n x := φ |}.
Solve Obligations with done.
195
Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
196
Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Definition uPred_pure_eq :
198
  @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200 201 202

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.
203
Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
204 205
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's avatar
Robbert Krebbers committed
206 207 208 209

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.
210
Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
211 212
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's avatar
Robbert Krebbers committed
213 214 215 216 217

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.
218
  intros M P Q n1 n1' x1 x1' HPQ [x2 Hx1'] Hn1 n2 x3 [x4 Hx3] ?; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
219 220 221
  rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
  eapply HPQ; auto. exists (x2  x4); by rewrite assoc.
Qed.
222
Definition uPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.
223
Definition uPred_impl {M} := uPred_impl_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
Definition uPred_impl_eq :
225
  @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
226 227 228 229

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.
230
Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
231
Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
Definition uPred_forall_eq :
233
  @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
234 235 236 237

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.
238
Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
239 240
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's avatar
Robbert Krebbers committed
241 242 243 244

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)).
245
Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
246
Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Definition uPred_internal_eq_eq:
248
  @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252

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.
253
  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
  exists x1, (x2  z); split_and?; eauto using uPred_mono, cmra_includedN_l.
255
  eapply dist_le, Hn. by rewrite Hy Hx assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
Qed.
257
Definition uPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.
258 259
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's avatar
Robbert Krebbers committed
260 261 262 263 264

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.
265 266
  intros M P Q n1 n1' x1 x1' HPQ ? Hn n3 x3 ???; simpl in *.
  eapply uPred_mono with n3 (x1  x3);
Robbert Krebbers's avatar
Robbert Krebbers committed
267 268
    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
269
Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
270
Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Definition uPred_wand_eq :
272
  @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
273

274 275 276
(* 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. *)
277
Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
278
  {| uPred_holds n x := P n ε |}.
279
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
280
Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
281 282 283
Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M.
Definition uPred_plainly_eq :
  @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
284

Robbert Krebbers's avatar
Robbert Krebbers committed
285 286 287 288 289
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.
290
Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
291
Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
Definition uPred_persistently_eq :
293
  @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295 296 297

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.
298
  intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Qed.
300
Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
301
Definition uPred_later {M} := uPred_later_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
Definition uPred_later_eq :
303
  @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
304 305 306 307

Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
  {| uPred_holds n x := a {n} x |}.
Next Obligation.
308 309
  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's avatar
Robbert Krebbers committed
310
Qed.
311
Definition uPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.
312
Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
Definition uPred_ownM_eq :
314
  @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
315 316 317 318

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.
319
Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
320
Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
Definition uPred_cmra_valid_eq :
322
  @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
323 324 325 326 327

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.
328
  intros M Q n1 n2 x1 x2 HQ [x3 Hx] Hn k yf Hk.
Robbert Krebbers's avatar
Robbert Krebbers committed
329 330 331
  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.
332
  eauto using uPred_mono, cmra_includedN_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
333
Qed.
334
Definition uPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.
335 336 337 338 339 340
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's avatar
Robbert Krebbers committed
341

342
(** Primitive logical rules.
343 344 345
    These are not directly usable later because they do not refer to the BI
    connectives. *)
Module uPred_primitive.
Robbert Krebbers's avatar
Robbert Krebbers committed
346 347 348
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,
349
  uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
350
  uPred_cmra_valid_eq, @uPred_bupd_eq).
351
Ltac unseal :=
352
  rewrite !unseal_eqs /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
353

354 355 356 357 358 359
Section primitive.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Arguments uPred_holds {_} !_ _ _ /.
Tej Chajed's avatar
Tej Chajed committed
360
Hint Immediate uPred_in_entails : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
361

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
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's avatar
Robbert Krebbers committed
387 388
Proof.
  split.
389 390 391 392 393 394
  - 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's avatar
Robbert Krebbers committed
395 396
Proof.
  split.
397 398 399
  - intros HPQ; split; split=> x i; apply HPQ.
  - intros [??]. exact: entails_anti_sym.
Qed.
400
Lemma entails_lim (cP cQ : chain (uPredO M)) :
401 402 403
  ( n, cP n  cQ n)  compl cP  compl cQ.
Proof.
  intros Hlim; split=> n m ? HP.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
  eapply uPred_holds_ne, Hlim, HP; rewrite ?conv_compl; eauto.
405
Qed.
406

407 408 409 410 411
(** 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's avatar
Robbert Krebbers committed
412
Proof.
413 414
  intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
  split; (intros [??]; split; [by apply HP|by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
415 416
Qed.

417
Lemma or_ne : NonExpansive2 (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
418
Proof.
419 420
  intros n P P' HP Q Q' HQ; split=> x n' ??.
  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
421 422
Qed.

423 424 425 426 427 428
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.
429

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
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's avatar
Ralf Jung committed
468
  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia.
469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484
  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).
485
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
486 487
  intros n a b Ha.
  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
488 489
Qed.

490
Lemma cmra_valid_ne {A : cmraT} :
Robbert Krebbers's avatar
Robbert Krebbers committed
491
  NonExpansive (@uPred_cmra_valid M A).
492
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
493 494
  intros n a b Ha; unseal; split=> n' x ? /=.
  by rewrite (dist_le _ _ _ _ Ha); last lia.
495
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
496

497 498 499 500 501 502 503 504 505 506 507 508 509 510 511
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.
512

513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533
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.
534

535 536 537 538
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.
539

540 541 542 543 544 545 546
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'.
547
Proof.
548 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
  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.

619
Lemma prop_ext_2 P Q :  ((P - Q)  (Q - P))  P  Q.
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
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.

695
Lemma fun_ext {A} {B : A  ofeT} (g1 g2 : discrete_fun B) :
696 697
  ( i, g1 i  g2 i)  g1  g2.
Proof. by unseal. Qed.
698
Lemma sig_eq {A : ofeT} (P : A  Prop) (x y : sigO P) :
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
  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.
739 740
Qed.

741
(** Own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
742 743 744
Lemma ownM_op (a1 a2 : M) :
  uPred_ownM (a1  a2)  uPred_ownM a1  uPred_ownM a2.
Proof.
745
  unseal; split=> n x ?; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
746 747 748 749 750 751
  - 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.
752
Lemma persistently_ownM_core (a : M) : uPred_ownM a   uPred_ownM (core a).
Robbert Krebbers's avatar
Robbert Krebbers committed
753
Proof.
754
  split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
Robbert Krebbers's avatar
Robbert Krebbers committed
755
Qed.
756
Lemma ownM_unit P : P  (uPred_ownM ε).
Robbert Krebbers's avatar
Robbert Krebbers committed
757
Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
758
Lemma later_ownM a :  uPred_ownM a   b, uPred_ownM b   (a  b).
Robbert Krebbers's avatar
Robbert Krebbers committed
759
Proof.
760
  unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
Robbert Krebbers's avatar
Robbert Krebbers committed
761 762 763 764 765
  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.

766 767 768 769 770 771 772 773 774 775 776
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's avatar
Robbert Krebbers committed
777 778 779 780
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.
781
Lemma cmra_valid_intro {A : cmraT} P (a : A) :  a  P  ( a).
Robbert Krebbers's avatar
Robbert Krebbers committed
782
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
783 784 785
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's avatar
Robbert Krebbers committed
786
Proof. by unseal. Qed.
787
Lemma cmra_valid_weaken {A : cmraT} (a b : A) :  (a  b)   a.
Robbert Krebbers's avatar
Robbert Krebbers committed
788 789
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.

790
Lemma prod_validI {A B : cmraT} (x : A * B) :  x   x.1   x.2.
Robbert Krebbers's avatar
Robbert Krebbers committed
791 792 793 794 795
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.

796 797
Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) :  a  ⌜✓ a.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
798

799
Lemma discrete_fun_validI {A} {B : A  ucmraT} (g : discrete_fun B) :  g   i,  g i.
800 801
Proof. by unseal. Qed.

802
(** Consistency/soundness statement *)
803 804
(** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
instance of [siProp] soundness in the future. *)
Ralf Jung's avatar
Ralf Jung committed
805
Lemma pure_soundness φ : (True   φ )  φ.
806 807
Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.

808 809 810 811 812 813
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True  x  y)  x  y.
Proof.
  unseal=> -[H]. apply equiv_dist=> n.
  by apply (H n ε); eauto using ucmra_unit_validN.
Qed.

Ralf Jung's avatar
Ralf Jung committed
814
Lemma later_soundness P : (True   P)  (True  P).
815
Proof.
816 817 818
  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.
819
Qed.
820 821
End primitive.
End uPred_primitive.