derived.v 39.1 KB
Newer Older
1
2
3
4
5
6
7
From iris.base_logic Require Export primitive.
Import uPred_entails uPred_primitive.

Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Instance: Params (@uPred_iff) 1.
Infix "↔" := uPred_iff : uPred_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
14
15
16
17
Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
  Nat.iter n uPred_later P.
Instance: Params (@uPred_laterN) 2.
Notation "▷^ n P" := (uPred_laterN n P)
  (at level 20, n at level 9, P at level 20,
   format "▷^ n  P") : uPred_scope.
Notation "▷? p P" := (uPred_laterN (Nat.b2n p) P)
  (at level 20, p at level 9, P at level 20,
   format "▷? p  P") : uPred_scope.

18
19
20
21
22
Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
  (if p then  P else P)%I.
Instance: Params (@uPred_always_if) 2.
Arguments uPred_always_if _ !_ _/.
Notation "□? p P" := (uPred_always_if p P)
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  (at level 20, p at level 9, P at level 20, format "□? p  P").
24

25
26
Definition uPred_except_0 {M} (P : uPred M) : uPred M :=  False  P.
Notation "◇ P" := (uPred_except_0 P)
27
  (at level 20, right associativity) : uPred_scope.
28
29
Instance: Params (@uPred_except_0) 1.
Typeclasses Opaque uPred_except_0.
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

Class TimelessP {M} (P : uPred M) := timelessP :  P   P.
Arguments timelessP {_} _ {_}.

Class PersistentP {M} (P : uPred M) := persistentP : P   P.
Arguments persistentP {_} _ {_}.

Module uPred_derived.
Section derived.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)

(* Derived logical stuff *)
Lemma False_elim P : False  P.
48
Proof. by apply (pure_elim' False). Qed.
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
Lemma True_intro P : P  True.
Proof. by apply pure_intro. Qed.

Lemma and_elim_l' P Q R : (P  R)  P  Q  R.
Proof. by rewrite and_elim_l. Qed.
Lemma and_elim_r' P Q R : (Q  R)  P  Q  R.
Proof. by rewrite and_elim_r. Qed.
Lemma or_intro_l' P Q R : (P  Q)  P  Q  R.
Proof. intros ->; apply or_intro_l. Qed.
Lemma or_intro_r' P Q R : (P  R)  P  Q  R.
Proof. intros ->; apply or_intro_r. Qed.
Lemma exist_intro' {A} P (Ψ : A  uPred M) a : (P  Ψ a)  P   a, Ψ a.
Proof. intros ->; apply exist_intro. Qed.
Lemma forall_elim' {A} P (Ψ : A  uPred M) : (P   a, Ψ a)   a, P  Ψ a.
Proof. move=> HP a. by rewrite HP forall_elim. Qed.

Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.

Lemma impl_intro_l P Q R : (Q  P  R)  P  Q  R.
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
Lemma impl_elim_l P Q : (P  Q)  P  Q.
Proof. apply impl_elim with P; auto. Qed.
Lemma impl_elim_r P Q : P  (P  Q)  Q.
Proof. apply impl_elim with P; auto. Qed.
Lemma impl_elim_l' P Q R : (P  Q  R)  P  Q  R.
Proof. intros; apply impl_elim with Q; auto. Qed.
Lemma impl_elim_r' P Q R : (Q  P  R)  P  Q  R.
Proof. intros; apply impl_elim with P; auto. Qed.
80
Lemma impl_entails P Q : (P  Q)%I  P  Q.
81
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
82
83
Lemma entails_impl P Q : (P  Q)  (P  Q)%I.
Proof. intro. apply impl_intro_l. auto. Qed.
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

Lemma and_mono P P' Q Q' : (P  Q)  (P'  Q')  P  P'  Q  Q'.
Proof. auto. Qed.
Lemma and_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
Proof. by intros; apply and_mono. Qed.
Lemma and_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
Proof. by apply and_mono. Qed.

Lemma or_mono P P' Q Q' : (P  Q)  (P'  Q')  P  P'  Q  Q'.
Proof. auto. Qed.
Lemma or_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
Proof. by intros; apply or_mono. Qed.
Lemma or_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
Proof. by apply or_mono. Qed.

Lemma impl_mono P P' Q Q' : (Q  P)  (P'  Q')  (P  P')  Q  Q'.
Proof.
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
  apply impl_elim with P; eauto.
Qed.
Lemma forall_mono {A} (Φ Ψ : A  uPred M) :
  ( a, Φ a  Ψ a)  ( a, Φ a)   a, Ψ a.
Proof.
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
Qed.
Lemma exist_mono {A} (Φ Ψ : A  uPred M) :
  ( a, Φ a  Ψ a)  ( a, Φ a)   a, Ψ a.
Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.

Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance and_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance or_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
126
127
128
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
129
130
131
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
132
133
134
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
135
Global Instance exist_mono' A :
136
137
138
139
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_exist M A).
Proof. intros P1 P2; apply exist_mono. Qed.
Global Instance exist_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_exist M A).
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
Proof. intros P1 P2; apply exist_mono. Qed.

Global Instance and_idem : IdemP () (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_idem : IdemP () (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_comm : Comm () (@uPred_and M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance True_and : LeftId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_True : RightId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance False_or : LeftId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_False : RightId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_assoc : Assoc () (@uPred_and M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance or_comm : Comm () (@uPred_or M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance or_assoc : Assoc () (@uPred_or M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.
  intros P; apply (anti_symm ()).
  - by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
Qed.
176
177
178
179
180
Lemma False_impl P : (False  P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216

Lemma exists_impl_forall {A} P (Ψ : A  uPred M) :
  (( x : A, Ψ x)  P)   x : A, Ψ x  P.
Proof.
  apply equiv_spec; split.
  - apply forall_intro=>x. by rewrite -exist_intro.
  - apply impl_intro_r, impl_elim_r', exist_elim=>x.
    apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
Qed.

Lemma or_and_l P Q R : P  Q  R  (P  Q)  (P  R).
Proof.
  apply (anti_symm ()); first auto.
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
Qed.
Lemma or_and_r P Q R : P  Q  R  (P  R)  (Q  R).
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
Lemma and_or_l P Q R : P  (Q  R)  P  Q  P  R.
Proof.
  apply (anti_symm ()); last auto.
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
Qed.
Lemma and_or_r P Q R : (P  Q)  R  P  R  Q  R.
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
Lemma and_exist_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
Proof.
  apply (anti_symm ()).
  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
    by rewrite -(exist_intro a) and_elim_r.
Qed.
Lemma and_exist_r {A} P (Φ: A  uPred M) : ( a, Φ a)  P   a, Φ a  P.
Proof.
  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
Qed.
217
218
219
220
221
222
223
Lemma or_exist {A} (Φ Ψ : A  uPred M) :
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
Proof.
  apply (anti_symm ()).
  - apply exist_elim=> a. by rewrite -!(exist_intro a).
  - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto.
Qed.
224

225
Lemma pure_elim φ Q R : (Q  ⌜φ⌝)  (φ  Q  R)  Q  R.
226
227
228
229
Proof.
  intros HQ HQR. rewrite -(idemp uPred_and Q) {1}HQ.
  apply impl_elim_l', pure_elim'=> ?. by apply entails_impl, HQR.
Qed.
Ralf Jung's avatar
Ralf Jung committed
230
Lemma pure_mono φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
231
232
233
Proof. intros; apply pure_elim with φ1; eauto. Qed.
Global Instance pure_mono' : Proper (impl ==> ()) (@uPred_pure M).
Proof. intros φ1 φ2; apply pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
234
Lemma pure_iff φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
235
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
236
Lemma pure_intro_l φ Q R : φ  (⌜φ⌝  Q  R)  Q  R.
237
Proof. intros ? <-; auto using pure_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
238
Lemma pure_intro_r φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
239
Proof. intros ? <-; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
240
Lemma pure_intro_impl φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
241
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
242
Lemma pure_elim_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
243
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
244
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
245
Proof. intros; apply pure_elim with φ; eauto. Qed.
246

Ralf Jung's avatar
Ralf Jung committed
247
Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
248
Proof. intros; apply (anti_symm _); auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
249
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
250
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
251

Ralf Jung's avatar
Ralf Jung committed
252
Lemma pure_and φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
253
254
255
256
257
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[??]; auto.
  - eapply (pure_elim φ1); [auto|]=> ?. eapply (pure_elim φ2); auto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
258
Lemma pure_or φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
259
260
261
262
263
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[?|?]; auto.
  - apply or_elim; eapply pure_elim; eauto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
264
Lemma pure_impl φ1 φ2 : ⌜φ1  φ2  (⌜φ1  ⌜φ2).
265
266
267
268
Proof.
  apply (anti_symm _).
  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
  - rewrite -pure_forall_2. apply forall_intro=> ?.
269
    by rewrite -(left_id True uPred_and (_→_))%I (pure_True φ1) // impl_elim_r.
270
Qed.
Ralf Jung's avatar
Ralf Jung committed
271
Lemma pure_forall {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
272
273
274
275
Proof.
  apply (anti_symm _); auto using pure_forall_2.
  apply forall_intro=> x. eauto using pure_mono.
Qed.
Ralf Jung's avatar
Ralf Jung committed
276
Lemma pure_exist {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
277
278
279
280
281
282
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
  - apply exist_elim=> x. eauto using pure_mono.
Qed.

283
Lemma internal_eq_refl' {A : ofeT} (a : A) P : P  a  a.
284
285
Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
Hint Resolve internal_eq_refl'.
286
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
287
Proof. by intros ->. Qed.
288
Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
289
Proof. apply (internal_eq_rewrite a b (λ b, b  a)%I); auto. solve_proper. Qed.
290
291
292
293
294
295
296
297
Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A  uPred M) P
  {HΨ : Contractive Ψ} : (P   (a  b))  (P  Ψ a)  P  Ψ b.
Proof.
  rewrite -later_equivI. intros Heq.
  change ((P  (Ψ  later_car) (Next a))  P  (Ψ  later_car) (Next b)).
  apply internal_eq_rewrite; last done.
  exact: later_car_compose_ne.
Qed.
298

Ralf Jung's avatar
Ralf Jung committed
299
Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
300
301
Proof.
  apply (anti_symm _).
302
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
303
304
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Ralf Jung's avatar
Ralf Jung committed
305
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
Proof.
  apply (anti_symm _).
  - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto.
  - by apply exist_elim, pure_intro.
Qed.
Lemma and_alt P Q : P  Q   b : bool, if b then P else Q.
Proof.
  apply (anti_symm _); first apply forall_intro=> -[]; auto.
  apply and_intro. by rewrite (forall_elim true). by rewrite (forall_elim false).
Qed.
Lemma or_alt P Q : P  Q   b : bool, if b then P else Q.
Proof.
  apply (anti_symm _); last apply exist_elim=> -[]; auto.
  apply or_elim. by rewrite -(exist_intro true). by rewrite -(exist_intro false).
Qed.

Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper :
  Proper (() ==> () ==> ()) (@uPred_iff M) := ne_proper_2 _.

Lemma iff_refl Q P : Q  P  P.
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
329
Lemma iff_equiv P Q : (P  Q)%I  (P  Q).
330
331
Proof.
  intros HPQ; apply (anti_symm ());
332
    apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto.
333
Qed.
334
Lemma equiv_iff P Q : (P  Q)  (P  Q)%I.
335
Proof. intros ->; apply iff_refl. Qed.
336
Lemma internal_eq_iff P Q : P  Q  P  Q.
337
Proof.
338
339
  apply (internal_eq_rewrite P Q (λ Q, P  Q))%I;
    first solve_proper; auto using iff_refl.
340
341
342
343
Qed.

(* Derived BI Stuff *)
Hint Resolve sep_mono.
344
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
345
Proof. by intros; apply sep_mono. Qed.
346
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
347
348
349
350
351
352
Proof. by apply sep_mono. Qed.
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Global Instance sep_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
353
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
354
355
356
357
358
Proof.
  intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
Qed.
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
359
360
361
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
362
363
364
365
366
367
368
369
370
371
372
373

Global Instance sep_comm : Comm () (@uPred_sep M).
Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.
Global Instance sep_assoc : Assoc () (@uPred_sep M).
Proof.
  intros P Q R; apply (anti_symm _); auto using sep_assoc'.
  by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'.
Qed.
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto using True_sep_1, True_sep_2. Qed.
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Proof. by intros P; rewrite comm left_id. Qed.
374
Lemma sep_elim_l P Q : P  Q  P.
375
Proof. by rewrite (True_intro Q) right_id. Qed.
376
377
378
Lemma sep_elim_r P Q : P  Q  Q.
Proof. by rewrite (comm ())%I; apply sep_elim_l. Qed.
Lemma sep_elim_l' P Q R : (P  R)  P  Q  R.
379
Proof. intros ->; apply sep_elim_l. Qed.
380
Lemma sep_elim_r' P Q R : (Q  R)  P  Q  R.
381
382
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
383
Lemma sep_intro_True_l P Q R : P%I  (R  Q)  R  P  Q.
384
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
385
Lemma sep_intro_True_r P Q R : (R  P)  Q%I  R  P  Q.
386
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
387
Lemma sep_elim_True_l P Q R : P  (P  R  Q)  R  Q.
388
Proof. by intros HP; rewrite -HP left_id. Qed.
389
Lemma sep_elim_True_r P Q R : P  (R  P  Q)  R  Q.
390
Proof. by intros HP; rewrite -HP right_id. Qed.
391
Lemma wand_intro_l P Q R : (Q  P  R)  P  Q - R.
392
Proof. rewrite comm; apply wand_intro_r. Qed.
393
Lemma wand_elim_l P Q : (P - Q)  P  Q.
394
Proof. by apply wand_elim_l'. Qed.
395
Lemma wand_elim_r P Q : P  (P - Q)  Q.
396
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
397
Lemma wand_elim_r' P Q R : (Q  P - R)  P  Q  R.
398
Proof. intros ->; apply wand_elim_r. Qed.
399
Lemma wand_apply P Q R S : (P  Q - R)  (S  P  Q)  S  R.
Ralf Jung's avatar
Ralf Jung committed
400
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
401
Lemma wand_frame_l P Q R : (Q - R)  P  Q - P  R.
402
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
403
Lemma wand_frame_r P Q R : (Q - R)  Q  P - R  P.
404
Proof.
405
  apply wand_intro_l. rewrite ![(_  P)%I]comm -assoc.
406
407
  apply sep_mono_r, wand_elim_r.
Qed.
408
Lemma wand_diag P : (P - P)  True.
409
Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
410
Lemma wand_True P : (True - P)  P.
411
412
Proof.
  apply (anti_symm _); last by auto using wand_intro_l.
413
  eapply sep_elim_True_l; last by apply wand_elim_r. done.
414
Qed.
415
Lemma wand_entails P Q : (P - Q)%I  P  Q.
416
417
418
Proof.
  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
419
420
Lemma entails_wand P Q : (P  Q)  (P - Q)%I.
Proof. intro. apply wand_intro_l. auto. Qed.
421
Lemma wand_curry P Q R : (P - Q - R)  (P  Q - R).
422
423
424
425
426
427
Proof.
  apply (anti_symm _).
  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
Qed.

428
Lemma sep_and P Q : (P  Q)  (P  Q).
429
Proof. auto. Qed.
430
Lemma impl_wand P Q : (P  Q)  P - Q.
431
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
432
Lemma pure_elim_sep_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
433
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
434
Lemma pure_elim_sep_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
435
436
437
438
439
440
441
Proof. intros; apply pure_elim with φ; eauto. Qed.

Global Instance sep_False : LeftAbsorb () False%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto. Qed.
Global Instance False_sep : RightAbsorb () False%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto. Qed.

442
Lemma sep_and_l P Q R : P  (Q  R)  (P  Q)  (P  R).
443
Proof. auto. Qed.
444
Lemma sep_and_r P Q R : (P  Q)  R  (P  R)  (Q  R).
445
Proof. auto. Qed.
446
Lemma sep_or_l P Q R : P  (Q  R)  (P  Q)  (P  R).
447
448
449
450
Proof.
  apply (anti_symm ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
451
Lemma sep_or_r P Q R : (P  Q)  R  (P  R)  (Q  R).
452
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
453
Lemma sep_exist_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
454
455
456
457
458
459
Proof.
  intros; apply (anti_symm ()).
  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
Qed.
460
Lemma sep_exist_r {A} (Φ: A  uPred M) Q: ( a, Φ a)  Q   a, Φ a  Q.
461
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
462
Lemma sep_forall_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
463
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
464
Lemma sep_forall_r {A} (Φ : A  uPred M) Q : ( a, Φ a)  Q   a, Φ a  Q.
465
466
467
468
469
470
471
472
473
474
475
476
477
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.

(* Always derived *)
Hint Resolve always_mono always_elim.
Global Instance always_mono' : Proper (() ==> ()) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.
Global Instance always_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.

Lemma always_intro' P Q : ( P  Q)   P   Q.
Proof. intros <-. apply always_idemp. Qed.

Ralf Jung's avatar
Ralf Jung committed
478
Lemma always_pure φ :  ⌜φ⌝  ⌜φ⌝.
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
Proof. apply (anti_symm _); auto using always_pure_2. Qed.
Lemma always_forall {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
Proof.
  apply (anti_symm _); auto using always_forall_2.
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma always_exist {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
Proof.
  apply (anti_symm _); auto using always_exist_1.
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Lemma always_and P Q :  (P  Q)   P   Q.
Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
Lemma always_or P Q :  (P  Q)   P   Q.
Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
Lemma always_impl P Q :  (P  Q)   P   Q.
Proof.
  apply impl_intro_l; rewrite -always_and.
  apply always_mono, impl_elim with P; auto.
Qed.
499
Lemma always_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
500
501
Proof.
  apply (anti_symm ()); auto using always_elim.
502
  apply (internal_eq_rewrite a b (λ b,  (a  b))%I); auto.
503
  { intros n; solve_proper. }
504
  rewrite -(internal_eq_refl a) always_pure; auto.
505
506
Qed.

507
Lemma always_and_sep P Q :  (P  Q)   (P  Q).
508
Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed.
509
Lemma always_and_sep_l' P Q :  P  Q   P  Q.
510
Proof. apply (anti_symm ()); auto using always_and_sep_l_1. Qed.
511
Lemma always_and_sep_r' P Q : P   Q  P   Q.
512
Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
513
Lemma always_sep P Q :  (P  Q)   P   Q.
514
Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
515
Lemma always_sep_dup' P :  P   P   P.
516
517
Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.

518
Lemma always_wand P Q :  (P - Q)   P -  Q.
519
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
520
Lemma always_wand_impl P Q :  (P - Q)   (P  Q).
521
522
523
524
525
Proof.
  apply (anti_symm ()); [|by rewrite -impl_wand].
  apply always_intro', impl_intro_r.
  by rewrite always_and_sep_l' always_elim wand_elim_l.
Qed.
526
Lemma always_entails_l' P Q : (P   Q)  P   Q  P.
527
Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
528
Lemma always_entails_r' P Q : (P   Q)  P  P   Q.
529
530
Proof. intros; rewrite -always_and_sep_r'; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
531
532
533
534
Lemma always_laterN n P :  ^n P  ^n  P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.


535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
(* Later derived *)
Lemma later_proper P Q : (P  Q)   P   Q.
Proof. by intros ->. Qed.
Hint Resolve later_mono later_proper.
Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.

Lemma later_intro P : P   P.
Proof.
  rewrite -(and_elim_l ( P) P) -(löb ( P  P)).
  apply impl_intro_l. by rewrite {1}(and_elim_r ( P)).
Qed.

Lemma later_True :  True  True.
Proof. apply (anti_symm ()); auto using later_intro. Qed.
Lemma later_forall {A} (Φ : A  uPred M) : (  a, Φ a)  ( a,  Φ a).
Proof.
  apply (anti_symm _); auto using later_forall_2.
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma later_exist `{Inhabited A} (Φ : A  uPred M) :
   ( a, Φ a)  ( a,  Φ a).
Proof.
  apply: anti_symm; [|apply exist_elim; eauto using exist_intro].
  rewrite later_exist_false. apply or_elim; last done.
  rewrite -(exist_intro inhabitant); auto.
Qed.
Lemma later_and P Q :  (P  Q)   P   Q.
Proof. rewrite !and_alt later_forall. by apply forall_proper=> -[]. Qed.
Lemma later_or P Q :  (P  Q)   P   Q.
Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed.
Lemma later_impl P Q :  (P  Q)   P   Q.
Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed.
571
Lemma later_wand P Q :  (P - Q)   P -  Q.
572
573
574
575
576
Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed.
Lemma later_iff P Q :  (P  Q)   P   Q.
Proof. by rewrite /uPred_iff later_and !later_impl. Qed.


Robbert Krebbers's avatar
Robbert Krebbers committed
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
(* Iterated later modality *)
Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m).
Proof. induction m; simpl. by intros ???. solve_proper. Qed.
Global Instance laterN_proper m :
  Proper (() ==> ()) (@uPred_laterN M m) := ne_proper _.

Lemma laterN_0 P : ^0 P  P.
Proof. done. Qed.
Lemma later_laterN n P : ^(S n) P   ^n P.
Proof. done. Qed.
Lemma laterN_later n P : ^(S n) P  ^n  P.
Proof. induction n; simpl; auto. Qed.
Lemma laterN_plus n1 n2 P : ^(n1 + n2) P  ^n1 ^n2 P.
Proof. induction n1; simpl; auto. Qed.
Lemma laterN_le n1 n2 P : n1  n2  ^n1 P  ^n2 P.
Proof. induction 1; simpl; by rewrite -?later_intro. Qed.

Lemma laterN_mono n P Q : (P  Q)  ^n P  ^n Q.
Proof. induction n; simpl; auto. Qed.
Global Instance laterN_mono' n : Proper (() ==> ()) (@uPred_laterN M n).
Proof. intros P Q; apply laterN_mono. Qed.
Global Instance laterN_flip_mono' n :
  Proper (flip () ==> flip ()) (@uPred_laterN M n).
Proof. intros P Q; apply laterN_mono. Qed.

Lemma laterN_intro n P : P  ^n P.
Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.

Lemma laterN_True n : ^n True  True.
Proof. apply (anti_symm ()); auto using laterN_intro. Qed.
Lemma laterN_forall {A} n (Φ : A  uPred M) : (^n  a, Φ a)  ( a, ^n Φ a).
Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
Lemma laterN_exist `{Inhabited A} n (Φ : A  uPred M) :
  (^n  a, Φ a)   a, ^n Φ a.
Proof. induction n as [|n IH]; simpl; rewrite -?later_exist; auto. Qed.
Lemma laterN_and n P Q : ^n (P  Q)  ^n P  ^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed.
Lemma laterN_or n P Q : ^n (P  Q)  ^n P  ^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed.
Lemma laterN_impl n P Q : ^n (P  Q)  ^n P  ^n Q.
Proof.
  apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono.
Qed.
Lemma laterN_sep n P Q : ^n (P  Q)  ^n P  ^n Q.
Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed.
Lemma laterN_wand n P Q : ^n (P - Q)  ^n P - ^n Q.
Proof.
  apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono.
Qed.
Lemma laterN_iff n P Q : ^n (P  Q)  ^n P  ^n Q.
Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.

629
630
631
632
633
634
635
636
637
638
639
640
641
(* Conditional always *)
Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
Proof. solve_proper. Qed.
Global Instance always_if_proper p : Proper (() ==> ()) (@uPred_always_if M p).
Proof. solve_proper. Qed.
Global Instance always_if_mono p : Proper (() ==> ()) (@uPred_always_if M p).
Proof. solve_proper. Qed.

Lemma always_if_elim p P : ?p P  P.
Proof. destruct p; simpl; auto using always_elim. Qed.
Lemma always_elim_if p P :  P  ?p P.
Proof. destruct p; simpl; auto using always_elim. Qed.

Ralf Jung's avatar
Ralf Jung committed
642
Lemma always_if_pure p φ : ?p ⌜φ⌝  ⌜φ⌝.
643
644
645
646
647
648
649
Proof. destruct p; simpl; auto using always_pure. Qed.
Lemma always_if_and p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using always_and. Qed.
Lemma always_if_or p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using always_or. Qed.
Lemma always_if_exist {A} p (Ψ : A  uPred M) : (?p  a, Ψ a)   a, ?p Ψ a.
Proof. destruct p; simpl; auto using always_exist. Qed.
650
Lemma always_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
651
652
653
654
655
656
Proof. destruct p; simpl; auto using always_sep. Qed.
Lemma always_if_later p P : ?p  P   ?p P.
Proof. destruct p; simpl; auto using always_later. Qed.


(* True now *)
657
Global Instance except_0_ne n : Proper (dist n ==> dist n) (@uPred_except_0 M).
658
Proof. solve_proper. Qed.
659
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
660
Proof. solve_proper. Qed.
661
Global Instance except_0_mono' : Proper (() ==> ()) (@uPred_except_0 M).
662
Proof. solve_proper. Qed.
663
664
Global Instance except_0_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_except_0 M).
665
666
Proof. solve_proper. Qed.

667
668
669
Lemma except_0_intro P : P   P.
Proof. rewrite /uPred_except_0; auto. Qed.
Lemma except_0_mono P Q : (P  Q)   P   Q.
670
Proof. by intros ->. Qed.
671
672
673
674
675
676
677
678
679
Lemma except_0_idemp P :   P   P.
Proof. rewrite /uPred_except_0; auto. Qed.

Lemma except_0_True :  True  True.
Proof. rewrite /uPred_except_0. apply (anti_symm _); auto. Qed.
Lemma except_0_or P Q :  (P  Q)   P   Q.
Proof. rewrite /uPred_except_0. apply (anti_symm _); auto. Qed.
Lemma except_0_and P Q :  (P  Q)   P   Q.
Proof. by rewrite /uPred_except_0 or_and_l. Qed.
680
Lemma except_0_sep P Q :  (P  Q)   P   Q.
681
682
Proof.
  rewrite /uPred_except_0. apply (anti_symm _).
683
684
685
686
  - apply or_elim; last by auto.
    by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
  - rewrite sep_or_r sep_elim_l sep_or_l; auto.
Qed.
687
Lemma except_0_forall {A} (Φ : A  uPred M) :  ( a, Φ a)   a,  Φ a.
688
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
689
Lemma except_0_exist {A} (Φ : A  uPred M) : ( a,  Φ a)    a, Φ a.
690
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
691
692
693
694
695
696
Lemma except_0_later P :   P   P.
Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
Lemma except_0_always P :   P    P.
Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed.
Lemma except_0_always_if p P :  ?p P  ?p  P.
Proof. destruct p; simpl; auto using except_0_always. Qed.
697
Lemma except_0_frame_l P Q : P   Q   (P  Q).
698
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
699
Lemma except_0_frame_r P Q :  P  Q   (P  Q).
700
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
701
702
703
704
705
706
707
708
709
710
711
712

(* Own and valid derived *)
Lemma always_ownM (a : M) : Persistent a   uPred_ownM a  uPred_ownM a.
Proof.
  intros; apply (anti_symm _); first by apply:always_elim.
  by rewrite {1}always_ownM_core persistent_core.
Qed.
Lemma ownM_invalid (a : M) : ¬ {0} a  uPred_ownM a  False.
Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
Global Instance ownM_mono : Proper (flip () ==> ()) (@uPred_ownM M).
Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
Lemma ownM_empty' : uPred_ownM   True.
713
Proof. apply (anti_symm _); first by auto. apply ownM_empty. Qed.
714
715
716
717
718
719
720
721
722
723
724
Lemma always_cmra_valid {A : cmraT} (a : A) :   a   a.
Proof.
  intros; apply (anti_symm _); first by apply:always_elim.
  apply:always_cmra_valid_1.
Qed.

(** * Derived rules *)
Global Instance bupd_mono' : Proper (() ==> ()) (@uPred_bupd M).
Proof. intros P Q; apply bupd_mono. Qed.
Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (@uPred_bupd M).
Proof. intros P Q; apply bupd_mono. Qed.
725
Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
726
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
727
Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
728
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
729
Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
730
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
731
Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
732
733
734
735
736
737
Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
Lemma bupd_ownM_update x y : x ~~> y  uPred_ownM x  |==> uPred_ownM y.
Proof.
  intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
  by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
Qed.
738
Lemma except_0_bupd P :  (|==> P)  (|==>  P).
739
Proof.
740
  rewrite /uPred_except_0. apply or_elim; auto using bupd_mono.
741
742
743
744
  by rewrite -bupd_intro -or_intro_l.
Qed.

(* Timeless instances *)
Ralf Jung's avatar
Ralf Jung committed
745
Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
746
747
748
749
750
751
752
Proof.
  rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
Qed.
Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
  TimelessP ( a : uPred M)%I.
Proof. rewrite /TimelessP !discrete_valid. apply (timelessP _). Qed.
Global Instance and_timeless P Q: TimelessP P  TimelessP Q  TimelessP (P  Q).
753
Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed.
754
Global Instance or_timeless P Q : TimelessP P  TimelessP Q  TimelessP (P  Q).
755
Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed.
756
757
758
759
760
Global Instance impl_timeless P Q : TimelessP Q  TimelessP (P  Q).
Proof.
  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
  apply or_mono, impl_intro_l; first done.
  rewrite -{2}(löb Q); apply impl_intro_l.
761
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
762
763
  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed.
764
Global Instance sep_timeless P Q: TimelessP P  TimelessP Q  TimelessP (P  Q).
765
Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed.
766
Global Instance wand_timeless P Q : TimelessP Q  TimelessP (P - Q).
767
768
769
770
Proof.
  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
  apply or_mono, wand_intro_l; first done.
  rewrite -{2}(löb Q); apply impl_intro_l.
771
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
772
773
774
775
776
777
778
779
780
  rewrite -(always_pure) -always_later always_and_sep_l'.
  by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
Qed.
Global Instance forall_timeless {A} (Ψ : A  uPred M) :
  ( x, TimelessP (Ψ x))  TimelessP ( x, Ψ x).
Proof.
  rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
  apply or_mono; first done. apply forall_intro=> x.
  rewrite -(löb (Ψ x)); apply impl_intro_l.
781
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
782
783
784
785
786
787
  by rewrite impl_elim_r (forall_elim x).
Qed.
Global Instance exist_timeless {A} (Ψ : A  uPred M) :
  ( x, TimelessP (Ψ x))  TimelessP ( x, Ψ x).
Proof.
  rewrite /TimelessP=> ?. rewrite later_exist_false. apply or_elim.
788
  - rewrite /uPred_except_0; auto.
789
790
791
  - apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
Global Instance always_timeless P : TimelessP P  TimelessP ( P).
792
Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
793
794
Global Instance always_if_timeless p P : TimelessP P  TimelessP (?p P).
Proof. destruct p; apply _. Qed.
795
Global Instance eq_timeless {A : ofeT} (a b : A) :
796
797
798
799
800
  Timeless a  TimelessP (a  b : uPred M)%I.
Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
Global Instance ownM_timeless (a : M) : Timeless a  TimelessP (uPred_ownM a).
Proof.
  intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b.
801
  rewrite (timelessP (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
802
803
  apply except_0_mono. rewrite internal_eq_sym.
  apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
804
Qed.
805
806
807
Global Instance from_option_timeless {A} P (Ψ : A  uPred M) (mx : option A) :
  ( x, TimelessP (Ψ x))  TimelessP P  TimelessP (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
808
809

(* Persistence *)
Ralf Jung's avatar
Ralf Jung committed
810
Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
811
812
813
814
815
816
817
818
819
820
Proof. by rewrite /PersistentP always_pure. Qed.
Global Instance always_persistent P : PersistentP ( P).
Proof. by intros; apply always_intro'. Qed.
Global Instance and_persistent P Q :
  PersistentP P  PersistentP Q  PersistentP (P  Q).
Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
Global Instance or_persistent P Q :
  PersistentP P  PersistentP Q  PersistentP (P  Q).
Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
Global Instance sep_persistent P Q :
821
  PersistentP P  PersistentP Q  PersistentP (P  Q).
822
823
824
825
826
827
828
Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
Global Instance forall_persistent {A} (Ψ : A  uPred M) :
  ( x, PersistentP (Ψ x))  PersistentP ( x, Ψ x).
Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
Global Instance exist_persistent {A} (Ψ : A  uPred M) :
  ( x, PersistentP (Ψ x))  PersistentP ( x, Ψ x).
Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
829
Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
830
  PersistentP (a  b : uPred M)%I.
831
Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
832
833
834
835
836
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
  PersistentP ( a : uPred M)%I.
Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
Global Instance later_persistent P : PersistentP P  PersistentP ( P).
Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
837
838
Global Instance laterN_persistent n P : PersistentP P  PersistentP (^n P).
Proof. induction n; apply _. Qed.
839
840
841
842
843
844
845
846
847
848
849
850
851
Global Instance ownM_persistent : Persistent a  PersistentP (@uPred_ownM M a).
Proof. intros. by rewrite /PersistentP always_ownM. Qed.
Global Instance from_option_persistent {A} P (Ψ : A  uPred M) (mx : option A) :
  ( x, PersistentP (Ψ x))  PersistentP P  PersistentP (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.

(* Derived lemmas for persistence *)
Lemma always_always P `{!PersistentP P} :  P  P.
Proof. apply (anti_symm ()); auto using always_elim. Qed.
Lemma always_if_always p P `{!PersistentP P} : ?p P  P.
Proof. destruct p; simpl; auto using always_always. Qed.
Lemma always_intro P Q `{!PersistentP P} : (P  Q)  P   Q.
Proof. rewrite -(always_always P); apply always_intro'. Qed.
852
Lemma always_and_sep_l P Q `{!PersistentP P} : P  Q  P  Q.
853
Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
854
Lemma always_and_sep_r P Q `{!PersistentP Q} : P  Q  P  Q.
855
Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
856
Lemma always_sep_dup P `{!PersistentP P} : P  P  P.
857
Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
858
Lemma always_entails_l P Q `{!PersistentP Q} : (P  Q)  P  Q  P.
859
Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
860
Lemma always_entails_r P Q `{!PersistentP Q} : (P  Q)  P  P  Q.