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

Ralf Jung's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
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.
 *)

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

53 54
  uPred_mono n1 n2 x1 x2 :
    uPred_holds n1 x1  x1 {n1} x2  n2  n1  uPred_holds n2 x2
55
}.
56 57
Bind Scope bi_scope with uPred.
Arguments uPred_holds {_} _%I _ _ : simpl never.
58
Add Printing Constructor uPred.
59
Instance: Params (@uPred_holds) 3 := {}.
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'.
70
  Definition uPred_ofe_mixin : OfeMixin (uPred M).
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.
83 84 85
  Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.

  Program Definition uPred_compl : Compl uPredC := λ c,
86
    {| uPred_holds n x :=  n', n'  n  {n'}x  c n' n' x |}.
87
  Next Obligation.
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.
91 92 93
  Qed.
  Global Program Instance uPred_cofe : Cofe uPredC := {| compl := uPred_compl |}.
  Next Obligation.
94 95
    intros n c; split=>i x Hin Hv.
    etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|].
96
    repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono.
97
  Qed.
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.
111
  intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
112 113
Qed.

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.
129 130 131 132
Qed.

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

Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
138
  `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
139 140
Proof.
  intros x1 x2 Hx; split=> n' y ??.
141
  split; apply Hx; auto using cmra_morphism_validN.
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)
146
    `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
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)
150
      `{!CmraMorphism f} `{!CmraMorphism g}:
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.
153
Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
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)
156
    `{!CmraMorphism f, !CmraMorphism g} n :
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.
183 184
  intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
  destruct n; split; by apply HPQ.
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 }.
190
Hint Resolve uPred_mono : uPred_def.
191

Robbert Krebbers's avatar
Robbert Krebbers committed
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.
197
Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Definition uPred_pure_eq :
199
  @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
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.
219
  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
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.
224
Definition uPred_impl {M} := uPred_impl_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Definition uPred_impl_eq :
226
  @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
232
Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
Definition uPred_forall_eq :
234
  @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
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.
247
Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
Definition uPred_internal_eq_eq:
249
  @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
254
  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
  exists x1, (x2  z); split_and?; eauto using uPred_mono, cmra_includedN_l.
256
  eapply dist_le, Hn. by rewrite Hy Hx assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258
Qed.
Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed.
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's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
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.
271
Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
Definition uPred_wand_eq :
273
  @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
274

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 :=
279
  {| uPred_holds n x := P n ε |}.
280
Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
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).
285

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

Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
  {| uPred_holds n x := a {n} x |}.
Next Obligation.
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's avatar
Robbert Krebbers committed
311 312
Qed.
Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. Qed.
313
Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M.
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Definition uPred_ownM_eq :
315
  @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
321
Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A.
Robbert Krebbers's avatar
Robbert Krebbers committed
322
Definition uPred_cmra_valid_eq :
323
  @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
329
  intros M Q n1 n2 x1 x2 HQ [x3 Hx] Hn k yf Hk.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
333
  eauto using uPred_mono, cmra_includedN_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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,
350
  uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
351
  uPred_cmra_valid_eq, @uPred_bupd_eq).
352
Ltac unseal :=
353
  rewrite !unseal_eqs /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 {_} !_ _ _ /.
361
Hint Immediate uPred_in_entails : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
416 417
Qed.

418
Lemma or_ne : NonExpansive2 (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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.
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's avatar
Ralf Jung committed
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).
486
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
487 488
  intros n a b Ha.
  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
489 490
Qed.

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

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.
740 741
Qed.

742
(** Own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
754
Proof.
755
  split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
Robbert Krebbers's avatar
Robbert Krebbers committed
756
Qed.
757
Lemma ownM_unit P : P  (uPred_ownM ε).
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
760
Proof.
761
  unseal; split=> -[|n] x /= ? Hax; first by eauto using ucmra_unit_leastN.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
787
Proof. by unseal. Qed.
788
Lemma cmra_valid_weaken {A : cmraT} (a b : A) :  (a  b)   a.
Robbert Krebbers's avatar
Robbert Krebbers committed
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's avatar
Robbert Krebbers committed
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.
799

800
Lemma ofe_fun_validI {A} {B : A  ucmraT} (g : ofe_fun B) :  g   i,  g i.
801 802
Proof. by unseal. Qed.

803
(** Consistency/soundness statement *)
Ralf Jung's avatar
Ralf Jung committed
804
Lemma pure_soundness φ : (True   φ )  φ.
805 806
Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.

Ralf Jung's avatar
Ralf Jung committed
807
Lemma later_soundness P : (True   P)  (True  P).
808
Proof.
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.
812
Qed.
813 814
End primitive.
End uPred_primitive.