derived.v 34.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.

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)
  (at level 20, p at level 0, P at level 20, format "□? p  P").

15
16
Definition uPred_except_0 {M} (P : uPred M) : uPred M :=  False  P.
Notation "◇ P" := (uPred_except_0 P)
17
  (at level 20, right associativity) : uPred_scope.
18
19
Instance: Params (@uPred_except_0) 1.
Typeclasses Opaque uPred_except_0.
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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
80
81
82
83
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

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.
Proof. by apply (pure_elim False). Qed.
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.
Lemma impl_entails P Q : (True  P  Q)  P  Q.
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
Lemma entails_impl P Q : (P  Q)  True  P  Q.
Proof. auto using impl_intro_l. Qed.

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.
116
117
118
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
119
120
121
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
122
123
124
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
125
Global Instance exist_mono' A :
126
127
128
129
  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).
130
131
132
133
134
135
136
137
138
139
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
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
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.

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.
202
203
204
205
206
207
208
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.
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259

Lemma pure_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
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.
Lemma pure_iff φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Lemma pure_intro_l φ Q R : φ  ( φ  Q  R)  Q  R.
Proof. intros ? <-; auto using pure_intro. Qed.
Lemma pure_intro_r φ Q R : φ  (Q   φ  R)  Q  R.
Proof. intros ? <-; auto. Qed.
Lemma pure_intro_impl φ Q R : φ  (Q   φ  R)  Q  R.
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Lemma pure_elim_l φ Q R : (φ  Q  R)   φ  Q  R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q   φ  R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_equiv (φ : Prop) : φ   φ  True.
Proof. intros; apply (anti_symm _); auto. Qed.

Lemma pure_and φ1 φ2 :  (φ1  φ2)   φ1   φ2.
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[??]; auto.
  - eapply (pure_elim φ1); [auto|]=> ?. eapply (pure_elim φ2); auto.
Qed.
Lemma pure_or φ1 φ2 :  (φ1  φ2)   φ1   φ2.
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[?|?]; auto.
  - apply or_elim; eapply pure_elim; eauto.
Qed.
Lemma pure_impl φ1 φ2 :  (φ1  φ2)  ( φ1   φ2).
Proof.
  apply (anti_symm _).
  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
  - rewrite -pure_forall_2. apply forall_intro=> ?.
    by rewrite -(left_id True uPred_and (_→_))%I (pure_equiv φ1) // impl_elim_r.
Qed.
Lemma pure_forall {A} (φ : A  Prop) :  ( x, φ x)   x,  φ x.
Proof.
  apply (anti_symm _); auto using pure_forall_2.
  apply forall_intro=> x. eauto using pure_mono.
Qed.
Lemma pure_exist {A} (φ : A  Prop) :  ( x, φ x)   x,  φ x.
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
  - apply exist_elim=> x. eauto using pure_mono.
Qed.

260
261
262
263
Lemma internal_eq_refl' {A : cofeT} (a : A) P : P  a  a.
Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
Hint Resolve internal_eq_refl'.
Lemma equiv_internal_eq {A : cofeT} P (a b : A) : a  b  P  a  b.
264
Proof. by intros ->. Qed.
265
266
Lemma internal_eq_sym {A : cofeT} (a b : A) : a  b  b  a.
Proof. apply (internal_eq_rewrite a b (λ b, b  a)%I); auto. solve_proper. Qed.
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298

Lemma pure_alt φ :  φ   _ : φ, True.
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.
Lemma iff_equiv P Q : (True  P  Q)  (P  Q).
Proof.
  intros HPQ; apply (anti_symm ());
    apply impl_entails; rewrite HPQ /uPred_iff; auto.
Qed.
Lemma equiv_iff P Q : (P  Q)  True  P  Q.
Proof. intros ->; apply iff_refl. Qed.
299
Lemma internal_eq_iff P Q : P  Q  P  Q.
300
Proof.
301
302
  apply (internal_eq_rewrite P Q (λ Q, P  Q))%I;
    first solve_proper; auto using iff_refl.
303
304
305
306
Qed.

(* Derived BI Stuff *)
Hint Resolve sep_mono.
307
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
308
Proof. by intros; apply sep_mono. Qed.
309
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
310
311
312
313
314
315
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.
316
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
317
318
319
320
321
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.
322
323
324
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
325
326
327
328
329
330
331
332
333
334
335
336

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.
337
Lemma sep_elim_l P Q : P  Q  P.
338
Proof. by rewrite (True_intro Q) right_id. Qed.
339
340
341
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.
342
Proof. intros ->; apply sep_elim_l. Qed.
343
Lemma sep_elim_r' P Q R : (Q  R)  P  Q  R.
344
345
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
346
Lemma sep_intro_True_l P Q R : (True  P)  (R  Q)  R  P  Q.
347
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
348
Lemma sep_intro_True_r P Q R : (R  P)  (True  Q)  R  P  Q.
349
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
350
Lemma sep_elim_True_l P Q R : (True  P)  (P  R  Q)  R  Q.
351
Proof. by intros HP; rewrite -HP left_id. Qed.
352
Lemma sep_elim_True_r P Q R : (True  P)  (R  P  Q)  R  Q.
353
Proof. by intros HP; rewrite -HP right_id. Qed.
354
Lemma wand_intro_l P Q R : (Q  P  R)  P  Q - R.
355
Proof. rewrite comm; apply wand_intro_r. Qed.
356
Lemma wand_elim_l P Q : (P - Q)  P  Q.
357
Proof. by apply wand_elim_l'. Qed.
358
Lemma wand_elim_r P Q : P  (P - Q)  Q.
359
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
360
Lemma wand_elim_r' P Q R : (Q  P - R)  P  Q  R.
361
Proof. intros ->; apply wand_elim_r. Qed.
362
Lemma wand_apply P Q R S : (P  Q - R)  (S  P  Q)  S  R.
Ralf Jung's avatar
Ralf Jung committed
363
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
364
Lemma wand_frame_l P Q R : (Q - R)  P  Q - P  R.
365
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
366
Lemma wand_frame_r P Q R : (Q - R)  Q  P - R  P.
367
Proof.
368
  apply wand_intro_l. rewrite ![(_  P)%I]comm -assoc.
369
370
  apply sep_mono_r, wand_elim_r.
Qed.
371
Lemma wand_diag P : (P - P)  True.
372
Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
373
Lemma wand_True P : (True - P)  P.
374
375
376
377
Proof.
  apply (anti_symm _); last by auto using wand_intro_l.
  eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
Qed.
378
Lemma wand_entails P Q : (True  P - Q)  P  Q.
379
380
381
Proof.
  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
382
Lemma entails_wand P Q : (P  Q)  True  P - Q.
383
Proof. auto using wand_intro_l. Qed.
384
Lemma wand_curry P Q R : (P - Q - R)  (P  Q - R).
385
386
387
388
389
390
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.

391
Lemma sep_and P Q : (P  Q)  (P  Q).
392
Proof. auto. Qed.
393
Lemma impl_wand P Q : (P  Q)  P - Q.
394
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
395
Lemma pure_elim_sep_l φ Q R : (φ  Q  R)   φ  Q  R.
396
Proof. intros; apply pure_elim with φ; eauto. Qed.
397
Lemma pure_elim_sep_r φ Q R : (φ  Q  R)  Q   φ  R.
398
399
400
401
402
403
404
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.

405
Lemma sep_and_l P Q R : P  (Q  R)  (P  Q)  (P  R).
406
Proof. auto. Qed.
407
Lemma sep_and_r P Q R : (P  Q)  R  (P  R)  (Q  R).
408
Proof. auto. Qed.
409
Lemma sep_or_l P Q R : P  (Q  R)  (P  Q)  (P  R).
410
411
412
413
Proof.
  apply (anti_symm ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
414
Lemma sep_or_r P Q R : (P  Q)  R  (P  R)  (Q  R).
415
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
416
Lemma sep_exist_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
417
418
419
420
421
422
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.
423
Lemma sep_exist_r {A} (Φ: A  uPred M) Q: ( a, Φ a)  Q   a, Φ a  Q.
424
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
425
Lemma sep_forall_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
426
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
427
Lemma sep_forall_r {A} (Φ : A  uPred M) Q : ( a, Φ a)  Q   a, Φ a  Q.
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
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.

Lemma always_pure φ :   φ   φ.
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.
462
Lemma always_internal_eq {A:cofeT} (a b : A) :  (a  b)  a  b.
463
464
Proof.
  apply (anti_symm ()); auto using always_elim.
465
  apply (internal_eq_rewrite a b (λ b,  (a  b))%I); auto.
466
  { intros n; solve_proper. }
467
  rewrite -(internal_eq_refl a) always_pure; auto.
468
469
Qed.

470
Lemma always_and_sep P Q :  (P  Q)   (P  Q).
471
Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed.
472
Lemma always_and_sep_l' P Q :  P  Q   P  Q.
473
Proof. apply (anti_symm ()); auto using always_and_sep_l_1. Qed.
474
Lemma always_and_sep_r' P Q : P   Q  P   Q.
475
Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
476
Lemma always_sep P Q :  (P  Q)   P   Q.
477
Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
478
Lemma always_sep_dup' P :  P   P   P.
479
480
Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.

481
Lemma always_wand P Q :  (P - Q)   P -  Q.
482
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
483
Lemma always_wand_impl P Q :  (P - Q)   (P  Q).
484
485
486
487
488
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.
489
Lemma always_entails_l' P Q : (P   Q)  P   Q  P.
490
Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
491
Lemma always_entails_r' P Q : (P   Q)  P  P   Q.
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
Proof. intros; rewrite -always_and_sep_r'; auto. Qed.

(* 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.
530
Lemma later_wand P Q :  (P - Q)   P -  Q.
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
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.


(* 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.

Lemma always_if_pure p φ : ?p  φ   φ.
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.
557
Lemma always_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
558
559
560
561
562
563
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 *)
564
Global Instance except_0_ne n : Proper (dist n ==> dist n) (@uPred_except_0 M).
565
Proof. solve_proper. Qed.
566
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
567
Proof. solve_proper. Qed.
568
Global Instance except_0_mono' : Proper (() ==> ()) (@uPred_except_0 M).
569
Proof. solve_proper. Qed.
570
571
Global Instance except_0_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_except_0 M).
572
573
Proof. solve_proper. Qed.

574
575
576
Lemma except_0_intro P : P   P.
Proof. rewrite /uPred_except_0; auto. Qed.
Lemma except_0_mono P Q : (P  Q)   P   Q.
577
Proof. by intros ->. Qed.
578
579
580
581
582
583
584
585
586
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.
587
Lemma except_0_sep P Q :  (P  Q)   P   Q.
588
589
Proof.
  rewrite /uPred_except_0. apply (anti_symm _).
590
591
592
593
  - 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.
594
Lemma except_0_forall {A} (Φ : A  uPred M) :  ( a, Φ a)   a,  Φ a.
595
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
596
Lemma except_0_exist {A} (Φ : A  uPred M) : ( a,  Φ a)    a, Φ a.
597
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
598
599
600
601
602
603
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.
604
Lemma except_0_frame_l P Q : P   Q   (P  Q).
605
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
606
Lemma except_0_frame_r P Q :  P  Q   (P  Q).
607
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631

(* 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.
Proof. apply (anti_symm _); auto using ownM_empty. Qed.
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.
632
Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
633
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
634
Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
635
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
636
Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
637
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
638
Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
639
640
641
642
643
644
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.
645
Lemma except_0_bupd P :  (|==> P)  (|==>  P).
646
Proof.
647
  rewrite /uPred_except_0. apply or_elim; auto using bupd_mono.
648
649
650
651
652
653
654
655
656
657
658
659
  by rewrite -bupd_intro -or_intro_l.
Qed.

(* Timeless instances *)
Global Instance pure_timeless φ : TimelessP ( φ : uPred M)%I.
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).
660
Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed.
661
Global Instance or_timeless P Q : TimelessP P  TimelessP Q  TimelessP (P  Q).
662
Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed.
663
664
665
666
667
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.
668
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
669
670
  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed.
671
Global Instance sep_timeless P Q: TimelessP P  TimelessP Q  TimelessP (P  Q).
672
Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed.
673
Global Instance wand_timeless P Q : TimelessP Q  TimelessP (P - Q).
674
675
676
677
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.
678
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
679
680
681
682
683
684
685
686
687
  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.
688
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
689
690
691
692
693
694
  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.
695
  - rewrite /uPred_except_0; auto.
696
697
698
  - apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
Global Instance always_timeless P : TimelessP P  TimelessP ( P).
699
Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
700
701
702
703
704
705
706
707
Global Instance always_if_timeless p P : TimelessP P  TimelessP (?p P).
Proof. destruct p; apply _. Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) :
  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.
708
  rewrite (timelessP (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
709
710
  apply except_0_mono. rewrite internal_eq_sym.
  apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
711
712
713
714
715
716
717
718
719
720
721
722
723
724
Qed.

(* Persistence *)
Global Instance pure_persistent φ : PersistentP ( φ : uPred M)%I.
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 :
725
  PersistentP P  PersistentP Q  PersistentP (P  Q).
726
727
728
729
730
731
732
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.
733
Global Instance internal_eq_persistent {A : cofeT} (a b : A) :
734
  PersistentP (a  b : uPred M)%I.
735
Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
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.
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.
754
Lemma always_and_sep_l P Q `{!PersistentP P} : P  Q  P  Q.
755
Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
756
Lemma always_and_sep_r P Q `{!PersistentP Q} : P  Q  P  Q.
757
Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
758
Lemma always_sep_dup P `{!PersistentP P} : P  P  P.
759
Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
760
Lemma always_entails_l P Q `{!PersistentP Q} : (P  Q)  P  Q  P.
761
Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
762
Lemma always_entails_r P Q `{!PersistentP Q} : (P  Q)  P  P  Q.
763
764
765
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End derived.
End uPred_derived.