derived.v 45.6 KB
Newer Older
1
From iris.base_logic Require Export primitive.
2
Set Default Proof Using "Type".
3
Import upred.uPred primitive.uPred.
4
5
6
7
8

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
9
10
11
12
13
14
15
16
17
18
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.

19
20
21
22
23
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
24
  (at level 20, p at level 9, P at level 20, format "□? p  P").
25

26
27
Definition uPred_except_0 {M} (P : uPred M) : uPred M :=  False  P.
Notation "◇ P" := (uPred_except_0 P)
28
  (at level 20, right associativity) : uPred_scope.
29
30
Instance: Params (@uPred_except_0) 1.
Typeclasses Opaque uPred_except_0.
31
32
33

Class TimelessP {M} (P : uPred M) := timelessP :  P   P.
Arguments timelessP {_} _ {_}.
34
Hint Mode TimelessP + ! : typeclass_instances.
35
Instance: Params (@TimelessP) 1.
36
37
38

Class PersistentP {M} (P : uPred M) := persistentP : P   P.
Arguments persistentP {_} _ {_}.
39
Hint Mode PersistentP + ! : typeclass_instances.
40
Instance: Params (@PersistentP) 1.
41

42
Module uPred.
43
44
45
46
47
48
49
50
51
52
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.
53
Proof. by apply (pure_elim' False). Qed.
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
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.
85
Lemma impl_entails P Q : (P  Q)%I  P  Q.
86
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
87
88
Lemma entails_impl P Q : (P  Q)  (P  Q)%I.
Proof. intro. apply impl_intro_l. auto. Qed.
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
126
127
128
129
130

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.
131
132
133
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
134
135
136
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
137
138
139
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
140
Global Instance exist_mono' A :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
141
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
142
143
144
Proof. intros P1 P2; apply exist_mono. Qed.
Global Instance exist_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_exist M A).
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
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.
181
182
183
184
185
Lemma False_impl P : (False  P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.
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
217
218
219
220
221

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.
222
223
224
225
226
227
228
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.
229

230
Lemma pure_elim φ Q R : (Q  ⌜φ⌝)  (φ  Q  R)  Q  R.
231
232
233
234
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
235
Lemma pure_mono φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
236
237
238
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.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
239
240
Global Instance pure_flip_mono : Proper (flip impl ==> flip ()) (@uPred_pure M).
Proof. intros φ1 φ2; apply pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
241
Lemma pure_iff φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
242
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
243
Lemma pure_intro_l φ Q R : φ  (⌜φ⌝  Q  R)  Q  R.
244
Proof. intros ? <-; auto using pure_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
245
Lemma pure_intro_r φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
246
Proof. intros ? <-; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
247
Lemma pure_intro_impl φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
248
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
249
Lemma pure_elim_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
250
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
251
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
252
Proof. intros; apply pure_elim with φ; eauto. Qed.
253

Ralf Jung's avatar
Ralf Jung committed
254
Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
255
Proof. intros; apply (anti_symm _); auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
256
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
257
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
258

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

290
Lemma internal_eq_refl' {A : ofeT} (a : A) P : P  a  a.
291
292
Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
Hint Resolve internal_eq_refl'.
293
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
294
Proof. by intros ->. Qed.
295
Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
296
Proof. apply (internal_eq_rewrite a b (λ b, b  a)%I); auto. solve_proper. Qed.
297
298
299
Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A  uPred M) P
  {HΨ : Contractive Ψ} : (P   (a  b))  (P  Ψ a)  P  Ψ b.
Proof.
300
301
  move: HΨ=> /contractiveI HΨ Heq ?.
  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
302
Qed.
303

Ralf Jung's avatar
Ralf Jung committed
304
Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
305
306
Proof.
  apply (anti_symm _).
307
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
308
309
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Ralf Jung's avatar
Ralf Jung committed
310
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
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.

327
Global Instance iff_ne : NonExpansive2 (@uPred_iff M).
328
329
330
331
332
333
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.
334
Lemma iff_equiv P Q : (P  Q)%I  (P  Q).
335
336
Proof.
  intros HPQ; apply (anti_symm ());
337
    apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto.
338
Qed.
339
Lemma equiv_iff P Q : (P  Q)  (P  Q)%I.
340
Proof. intros ->; apply iff_refl. Qed.
341
Lemma internal_eq_iff P Q : P  Q  P  Q.
342
Proof.
343
344
  apply (internal_eq_rewrite P Q (λ Q, P  Q))%I;
    first solve_proper; auto using iff_refl.
345
346
347
348
Qed.

(* Derived BI Stuff *)
Hint Resolve sep_mono.
349
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
350
Proof. by intros; apply sep_mono. Qed.
351
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
352
353
354
355
356
357
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.
358
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
359
360
361
362
363
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.
364
365
366
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
367
368
369
370
371
372
373
374
375
376
377
378

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.
379
Lemma sep_elim_l P Q : P  Q  P.
380
Proof. by rewrite (True_intro Q) right_id. Qed.
381
382
383
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.
384
Proof. intros ->; apply sep_elim_l. Qed.
385
Lemma sep_elim_r' P Q R : (Q  R)  P  Q  R.
386
387
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
388
Lemma sep_intro_True_l P Q R : P%I  (R  Q)  R  P  Q.
389
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
390
Lemma sep_intro_True_r P Q R : (R  P)  Q%I  R  P  Q.
391
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
392
Lemma sep_elim_True_l P Q R : P  (P  R  Q)  R  Q.
393
Proof. by intros HP; rewrite -HP left_id. Qed.
394
Lemma sep_elim_True_r P Q R : P  (R  P  Q)  R  Q.
395
Proof. by intros HP; rewrite -HP right_id. Qed.
396
Lemma wand_intro_l P Q R : (Q  P  R)  P  Q - R.
397
Proof. rewrite comm; apply wand_intro_r. Qed.
398
Lemma wand_elim_l P Q : (P - Q)  P  Q.
399
Proof. by apply wand_elim_l'. Qed.
400
Lemma wand_elim_r P Q : P  (P - Q)  Q.
401
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
402
Lemma wand_elim_r' P Q R : (Q  P - R)  P  Q  R.
403
Proof. intros ->; apply wand_elim_r. Qed.
404
Lemma wand_apply P Q R S : (P  Q - R)  (S  P  Q)  S  R.
Ralf Jung's avatar
Ralf Jung committed
405
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
406
Lemma wand_frame_l P Q R : (Q - R)  P  Q - P  R.
407
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
408
Lemma wand_frame_r P Q R : (Q - R)  Q  P - R  P.
409
Proof.
410
  apply wand_intro_l. rewrite ![(_  P)%I]comm -assoc.
411
412
  apply sep_mono_r, wand_elim_r.
Qed.
413
Lemma wand_diag P : (P - P)  True.
414
Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
415
Lemma wand_True P : (True - P)  P.
416
417
Proof.
  apply (anti_symm _); last by auto using wand_intro_l.
418
  eapply sep_elim_True_l; last by apply wand_elim_r. done.
419
Qed.
420
Lemma wand_entails P Q : (P - Q)%I  P  Q.
421
422
423
Proof.
  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
424
425
Lemma entails_wand P Q : (P  Q)  (P - Q)%I.
Proof. intro. apply wand_intro_l. auto. Qed.
426
Lemma wand_curry P Q R : (P - Q - R)  (P  Q - R).
427
428
429
430
431
432
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.

433
Lemma sep_and P Q : (P  Q)  (P  Q).
434
Proof. auto. Qed.
435
Lemma impl_wand P Q : (P  Q)  P - Q.
436
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
437
Lemma pure_elim_sep_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
438
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
439
Lemma pure_elim_sep_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
440
441
442
443
444
445
446
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.

447
Lemma entails_equiv_and P Q : (P  Q  P)  (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
448
Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed.
449
Lemma sep_and_l P Q R : P  (Q  R)  (P  Q)  (P  R).
450
Proof. auto. Qed.
451
Lemma sep_and_r P Q R : (P  Q)  R  (P  R)  (Q  R).
452
Proof. auto. Qed.
453
Lemma sep_or_l P Q R : P  (Q  R)  (P  Q)  (P  R).
454
455
456
457
Proof.
  apply (anti_symm ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
458
Lemma sep_or_r P Q R : (P  Q)  R  (P  R)  (Q  R).
459
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
460
Lemma sep_exist_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
461
462
463
464
465
466
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.
467
Lemma sep_exist_r {A} (Φ: A  uPred M) Q: ( a, Φ a)  Q   a, Φ a  Q.
468
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
469
Lemma sep_forall_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
470
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
471
Lemma sep_forall_r {A} (Φ : A  uPred M) Q : ( a, Φ a)  Q   a, Φ a  Q.
472
473
474
475
476
477
478
479
480
481
482
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.
483
Proof. intros <-. apply always_idemp_2. Qed.
484
Lemma always_idemp P :   P   P.
485
Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
486

Ralf Jung's avatar
Ralf Jung committed
487
Lemma always_pure φ :  ⌜φ⌝  ⌜φ⌝.
488
489
490
491
492
493
Proof.
  apply (anti_symm _); auto.
  apply pure_elim'=> Hφ.
  trans ( x : False,  True : uPred M)%I; [by apply forall_intro|].
  rewrite always_forall_2. auto using always_mono, pure_intro.
Qed.
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
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.
513
Lemma always_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
514
515
Proof.
  apply (anti_symm ()); auto using always_elim.
516
  apply (internal_eq_rewrite a b (λ b,  (a  b))%I); auto.
517
  { intros n; solve_proper. }
518
  rewrite -(internal_eq_refl a) always_pure; auto.
519
520
Qed.

521
Lemma always_and_sep_l' P Q :  P  Q   P  Q.
522
Proof. apply (anti_symm ()); auto using always_and_sep_l_1. Qed.
523
Lemma always_and_sep_r' P Q : P   Q  P   Q.
524
Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
525
526
527
528
529
530
531
532
Lemma always_sep_dup' P :  P   P   P.
Proof. by rewrite -always_and_sep_l' idemp. Qed.

Lemma always_and_sep P Q :  (P  Q)   (P  Q).
Proof.
  apply (anti_symm ()); auto.
  rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
Qed.
533
Lemma always_sep P Q :  (P  Q)   P   Q.
534
535
Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.

536
Lemma always_wand P Q :  (P - Q)   P -  Q.
537
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
538
Lemma always_wand_impl P Q :  (P - Q)   (P  Q).
539
540
541
542
543
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.
Ralf Jung's avatar
Ralf Jung committed
544
545
546
547
548
Lemma wand_impl_always P Q : (( P) - Q)  (( P)  Q).
Proof.
  apply (anti_symm ()); [|by rewrite -impl_wand].
  apply impl_intro_l. by rewrite always_and_sep_l' wand_elim_r.
Qed.
549
Lemma always_entails_l' P Q : (P   Q)  P   Q  P.
550
Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
551
Lemma always_entails_r' P Q : (P   Q)  P  P   Q.
552
553
Proof. intros; rewrite -always_and_sep_r'; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
556
Lemma always_laterN n P :  ^n P  ^n  P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.

557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
Lemma wand_alt P Q : (P - Q)   R, R   (P  R  Q).
Proof.
  apply (anti_symm ()).
  - rewrite -(right_id True%I uPred_sep (P - Q)%I) -(exist_intro (P - Q)%I).
    apply sep_mono_r. rewrite -always_pure. apply always_mono, impl_intro_l.
    by rewrite wand_elim_r right_id.
  - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -always_and_sep_r'.
    by rewrite always_elim impl_elim_r.
Qed.
Lemma impl_alt P Q : (P  Q)   R, R   (P  R - Q).
Proof.
  apply (anti_symm ()).
  - rewrite -(right_id True%I uPred_and (P  Q)%I) -(exist_intro (P  Q)%I).
    apply and_mono_r. rewrite -always_pure. apply always_mono, wand_intro_l.
    by rewrite impl_elim_r right_id.
  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc always_and_sep_r'.
    by rewrite always_elim wand_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
575

576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
(* 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
600
Lemma later_exist_2 {A} (Φ : A  uPred M) : ( a,  Φ a)   ( a, Φ a).
Proof. apply exist_elim; eauto using exist_intro. Qed.
601
602
603
Lemma later_exist `{Inhabited A} (Φ : A  uPred M) :
   ( a, Φ a)  ( a,  Φ a).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
  apply: anti_symm; [|apply later_exist_2].
605
606
607
608
609
610
611
612
613
  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.
614
Lemma later_wand P Q :  (P - Q)   P -  Q.
615
616
617
618
619
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
620
(* Iterated later modality *)
621
Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
652
653
Lemma laterN_exist_2 {A} n (Φ : A  uPred M) : ( a, ^n Φ a)  ^n ( a, Φ a).
Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
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.

674
(* Conditional always *)
675
Global Instance always_if_ne p : NonExpansive (@uPred_always_if M p).
676
677
678
679
680
681
682
683
684
685
686
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
687
Lemma always_if_pure p φ : ?p ⌜φ⌝  ⌜φ⌝.
688
689
690
691
692
693
694
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.
695
Lemma always_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
696
697
698
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.
699
700
Lemma always_if_laterN p n P : ?p ^n P  ^n ?p P.
Proof. destruct p; simpl; auto using always_laterN. Qed.
701
702

(* True now *)
703
Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
704
Proof. solve_proper. Qed.
705
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
706
Proof. solve_proper. Qed.
707
Global Instance except_0_mono' : Proper (() ==> ()) (@uPred_except_0 M).
708
Proof. solve_proper. Qed.
709
710
Global Instance except_0_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_except_0 M).
711
712
Proof. solve_proper. Qed.

713
714
715
Lemma except_0_intro P : P   P.
Proof. rewrite /uPred_except_0; auto. Qed.
Lemma except_0_mono P Q : (P  Q)   P   Q.
716
Proof. by intros ->. Qed.
717
718
719
720
721
722
723
724
725
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.
726
Lemma except_0_sep P Q :  (P  Q)   P   Q.
727
728
Proof.
  rewrite /uPred_except_0. apply (anti_symm _).
729
730
731
732
  - 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.
733
Lemma except_0_forall {A} (Φ : A  uPred M) :  ( a, Φ a)   a,  Φ a.
734
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
735
Lemma except_0_exist_2 {A} (Φ : A  uPred M) : ( a,  Φ a)    a, Φ a.
736
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
737
738
739
740
741
742
743
Lemma except_0_exist `{Inhabited A} (Φ : A  uPred M) :
   ( a, Φ a)  ( a,  Φ a).
Proof.
  apply (anti_symm _); [|by apply except_0_exist_2]. apply or_elim.
  - rewrite -(exist_intro inhabitant). by apply or_intro_l.
  - apply exist_mono=> a. apply except_0_intro.
Qed.
744
745
746
747
748
749
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.
750
Lemma except_0_frame_l P Q : P   Q   (P  Q).
751
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
752
Lemma except_0_frame_r P Q :  P  Q   (P  Q).
753
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
754
755

(* Own and valid derived *)
756
Lemma always_ownM (a : M) : CoreId a   uPred_ownM a  uPred_ownM a.
757
758
Proof.
  intros; apply (anti_symm _); first by apply:always_elim.
759
  by rewrite {1}always_ownM_core core_id_core.
760
761
762
763
764
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
765
766
Lemma ownM_unit' : uPred_ownM ε  True.
Proof. apply (anti_symm _); first by auto. apply ownM_unit. Qed.
767
768
769
770
771
772
773
774
775
776
777
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.
778
Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
779
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
780
Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
781
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
782
Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
783
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
784
Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
785
786
787
788
789
790
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.
791
Lemma except_0_bupd P :  (|==> P)  (|==>  P).
792
Proof.
793
  rewrite /uPred_except_0. apply or_elim; auto using bupd_mono.
794
795
796
  by rewrite -bupd_intro -or_intro_l.
Qed.

797
(* Discrete instances *)
798
799
Global Instance TimelessP_proper : Proper (() ==> iff) (@TimelessP M).
Proof. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
800
Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
801
802
803
Proof.
  rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
Qed.
804
Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
805
806
807
  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).
808
Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed.
809
Global Instance or_timeless P Q : TimelessP P  TimelessP Q  TimelessP (P  Q).
810
Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed.
811
812
813
814
815
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.
816
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
817
818
  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed.