upred.v 32.5 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".
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
8
Local Hint Extern 1 (_  _) => etrans; [eassumption|].
Local Hint Extern 1 (_  _) => etrans; [|eassumption].
Local Hint Extern 10 (_  _) => omega.
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
51
Record uPred (M : ucmraT) : Type := IProp {
  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
59
60
61
62
63
64
65
66
67
68
69
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.

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
361
Section primitive.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Arguments uPred_holds {_} !_ _ _ /.
Hint Immediate uPred_in_entails.
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
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
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.
  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
  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
696
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
  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.

Lemma fun_ext `{B : A  ofeT} (g1 g2 : ofe_fun B) :
  ( 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
801
802
Lemma ofe_fun_validI `{B : A  ucmraT} (g : ofe_fun B) :  g   i,  g i.
Proof. by unseal. Qed.

803
804
805
806
807
808
809
810
(** Consistency/soundness statement *)
Lemma soundness φ n : (True  iter n uPred_later ( φ )%I)  φ.
Proof.
  cut (iter n (@uPred_later M) ( φ )%I n ε  φ).
  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
  unseal. induction n as [|n IH]=> H; auto.
Qed.

811
812
End primitive.
End uPred_primitive.