derived.v 55.5 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
Definition uPred_persistently_if {M} (p : bool) (P : uPred M) : uPred M :=
20
  (if p then  P else P)%I.
21
22
23
Instance: Params (@uPred_persistently_if) 2.
Arguments uPred_persistently_if _ !_ _/.
Notation "□? p P" := (uPred_persistently_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
Class Timeless {M} (P : uPred M) := timelessP :  P   P.
33
Arguments timelessP {_} _ {_}.
34
35
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.
36

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

42
43
44
45
46
Class Plain {M} (P : uPred M) := plain : P   P.
Arguments plain {_} _ {_}.
Hint Mode Plain + ! : typeclass_instances.
Instance: Params (@Plain) 1.

47
Module uPred.
48
49
50
51
52
53
54
55
56
57
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.
58
Proof. by apply (pure_elim' False). Qed.
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
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.
90
Lemma impl_entails P Q : (P  Q)%I  P  Q.
91
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
92
93
Lemma entails_impl P Q : (P  Q)  (P  Q)%I.
Proof. intro. apply impl_intro_l. auto. Qed.
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
131
132
133
134
135

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.
136
137
138
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
139
140
141
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
142
143
144
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
145
Global Instance exist_mono' A :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
146
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
147
148
149
Proof. intros P1 P2; apply exist_mono. Qed.
Global Instance exist_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_exist M A).
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
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.
186
187
188
189
190
Lemma False_impl P : (False  P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.
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
222
223
224
225
226

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.
227
228
229
230
231
232
233
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.
234

235
Lemma pure_elim φ Q R : (Q  ⌜φ⌝)  (φ  Q  R)  Q  R.
236
237
238
239
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
240
Lemma pure_mono φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
241
242
243
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
244
245
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
246
Lemma pure_iff φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
247
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
248
Lemma pure_intro_l φ Q R : φ  (⌜φ⌝  Q  R)  Q  R.
249
Proof. intros ? <-; auto using pure_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
250
Lemma pure_intro_r φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
251
Proof. intros ? <-; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
252
Lemma pure_intro_impl φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
253
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
254
Lemma pure_elim_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
255
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
256
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
257
Proof. intros; apply pure_elim with φ; eauto. Qed.
258

Ralf Jung's avatar
Ralf Jung committed
259
Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
260
Proof. intros; apply (anti_symm _); auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
261
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
262
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
263

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

295
Lemma internal_eq_refl' {A : ofeT} (a : A) P : P  a  a.
296
297
Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
Hint Resolve internal_eq_refl'.
298
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
299
Proof. by intros ->. Qed.
300
Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
301
Proof.
302
303
  rewrite (internal_eq_rewrite a b (λ b, b  a)%I ltac:(solve_proper)).
  by rewrite -internal_eq_refl True_impl.
304
Qed.
305
306
307
308
309
310
311
312
313
Lemma f_equiv {A B : ofeT} (f : A  B) `{!NonExpansive f} x y :
  x  y  f x  f y.
Proof.
  rewrite (internal_eq_rewrite x y (λ y, f x  f y)%I ltac:(solve_proper)).
  by rewrite -internal_eq_refl True_impl.
Qed.
Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A  uPred M)
  {HΨ : Contractive Ψ} :  (a  b)  Ψ a  Ψ b.
Proof. move: HΨ=> /contractiveI ->. by rewrite (internal_eq_rewrite _ _ id). Qed.
314

Ralf Jung's avatar
Ralf Jung committed
315
Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
316
317
Proof.
  apply (anti_symm _).
318
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
319
320
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Ralf Jung's avatar
Ralf Jung committed
321
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
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.

338
Global Instance iff_ne : NonExpansive2 (@uPred_iff M).
339
340
341
342
343
344
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.
345
Lemma iff_equiv P Q : (P  Q)%I  (P  Q).
346
347
Proof.
  intros HPQ; apply (anti_symm ());
348
    apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto.
349
Qed.
350
Lemma equiv_iff P Q : (P  Q)  (P  Q)%I.
351
Proof. intros ->; apply iff_refl. Qed.
352
Lemma internal_eq_iff P Q : P  Q  P  Q.
353
Proof.
354
355
  rewrite (internal_eq_rewrite P Q (λ Q, P  Q)%I ltac:(solve_proper)).
  by rewrite -(iff_refl True) True_impl.
356
357
358
359
Qed.

(* Derived BI Stuff *)
Hint Resolve sep_mono.
360
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
361
Proof. by intros; apply sep_mono. Qed.
362
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
363
364
365
366
367
368
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.
369
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
370
371
372
373
374
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.
375
376
377
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
378
379
380
381
382
383
384
385
386
387
388
389

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

444
Lemma sep_and P Q : (P  Q)  (P  Q).
445
Proof. auto. Qed.
446
Lemma impl_wand_1 P Q : (P  Q)  P - Q.
447
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
448
Lemma pure_elim_sep_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
449
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
450
Lemma pure_elim_sep_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
451
452
453
454
455
456
457
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.

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

485
486
487
488
489
490
491
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
530
531
532
533
534
535
536
537
538
539
(* Plainness modality *)
Global Instance plainly_mono' : Proper (() ==> ()) (@uPred_plainly M).
Proof. intros P Q; apply plainly_mono. Qed.
Global Instance naugth_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_plainly M).
Proof. intros P Q; apply plainly_mono. Qed.

Lemma plainly_elim P :  P  P.
Proof. by rewrite plainly_elim' persistently_elim. Qed.
Hint Resolve plainly_mono plainly_elim.
Lemma plainly_intro' P Q : ( P  Q)   P   Q.
Proof. intros <-. apply plainly_idemp. Qed.
Lemma plainly_idemp P :   P   P.
Proof. apply (anti_symm _); auto using plainly_idemp. Qed.

Lemma persistently_plainly P :   P   P.
Proof.
  apply (anti_symm _); auto using persistently_elim.
  by rewrite -plainly_elim' plainly_idemp.
Qed.
Lemma plainly_persistently P :   P   P.
Proof.
  apply (anti_symm _); auto using plainly_mono, persistently_elim.
  by rewrite -plainly_elim' plainly_idemp.
Qed.

Lemma plainly_pure φ :  ⌜φ⌝  ⌜φ⌝.
Proof.
  apply (anti_symm _); auto.
  apply pure_elim'=> Hφ.
  trans ( x : False,  True : uPred M)%I; [by apply forall_intro|].
  rewrite plainly_forall_2. auto using plainly_mono, pure_intro.
Qed.
Lemma plainly_forall {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
Proof.
  apply (anti_symm _); auto using plainly_forall_2.
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma plainly_exist {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
Proof.
  apply (anti_symm _); auto using plainly_exist_1.
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Lemma plainly_and P Q :  (P  Q)   P   Q.
Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
Lemma plainly_or P Q :  (P  Q)   P   Q.
Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
Lemma plainly_impl P Q :  (P  Q)   P   Q.
Proof.
  apply impl_intro_l; rewrite -plainly_and.
  apply plainly_mono, impl_elim with P; auto.
Qed.
Lemma plainly_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
Proof.
  apply (anti_symm ()); auto using persistently_elim.
540
541
  rewrite {1}(internal_eq_rewrite a b (λ b,  (a  b))%I ltac:(solve_proper)).
  by rewrite -internal_eq_refl plainly_pure True_impl.
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
571
572
573
574
575
576
577
578
579
580
581
Qed.

Lemma plainly_and_sep_l_1 P Q :  P  Q   P  Q.
Proof. by rewrite -persistently_plainly persistently_and_sep_l_1. Qed.
Lemma plainly_and_sep_l' P Q :  P  Q   P  Q.
Proof. apply (anti_symm ()); auto using plainly_and_sep_l_1. Qed.
Lemma plainly_and_sep_r' P Q : P   Q  P   Q.
Proof. by rewrite !(comm _ P) plainly_and_sep_l'. Qed.
Lemma plainly_sep_dup' P :  P   P   P.
Proof. by rewrite -plainly_and_sep_l' idemp. Qed.

Lemma plainly_and_sep P Q :  (P  Q)   (P  Q).
Proof.
  apply (anti_symm ()); auto.
  rewrite -{1}plainly_idemp plainly_and plainly_and_sep_l'; auto.
Qed.
Lemma plainly_sep P Q :  (P  Q)   P   Q.
Proof. by rewrite -plainly_and_sep -plainly_and_sep_l' plainly_and. Qed.

Lemma plainly_wand P Q :  (P - Q)   P -  Q.
Proof. by apply wand_intro_r; rewrite -plainly_sep wand_elim_l. Qed.
Lemma plainly_impl_wand P Q :  (P  Q)   (P - Q).
Proof.
  apply (anti_symm ()); [by rewrite -impl_wand_1|].
  apply plainly_intro', impl_intro_r.
  by rewrite plainly_and_sep_l' plainly_elim wand_elim_l.
Qed.
Lemma wand_impl_plainly P Q : ( P - Q)  ( P  Q).
Proof.
  apply (anti_symm ()); [|by rewrite -impl_wand_1].
  apply impl_intro_l. by rewrite plainly_and_sep_l' wand_elim_r.
Qed.
Lemma plainly_entails_l' P Q : (P   Q)  P   Q  P.
Proof. intros; rewrite -plainly_and_sep_l'; auto. Qed.
Lemma plainly_entails_r' P Q : (P   Q)  P  P   Q.
Proof. intros; rewrite -plainly_and_sep_r'; auto. Qed.

Lemma plainly_laterN n P :  ^n P  ^n  P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite plainly_later IH. Qed.

582
(* Always derived *)
583
584
585
586
587
588
Hint Resolve persistently_mono persistently_elim.
Global Instance persistently_mono' : Proper (() ==> ()) (@uPred_persistently M).
Proof. intros P Q; apply persistently_mono. Qed.
Global Instance persistently_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_persistently M).
Proof. intros P Q; apply persistently_mono. Qed.
589

590
591
592
593
Lemma persistently_intro' P Q : ( P  Q)   P   Q.
Proof. intros <-. apply persistently_idemp_2. Qed.
Lemma persistently_idemp P :   P   P.
Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed.
594

595
Lemma persistently_pure φ :  ⌜φ⌝  ⌜φ⌝.
596
Proof. by rewrite -plainly_pure persistently_plainly. Qed.
597
Lemma persistently_forall {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
598
Proof.
599
  apply (anti_symm _); auto using persistently_forall_2.
600
601
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
602
Lemma persistently_exist {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
603
Proof.
604
  apply (anti_symm _); auto using persistently_exist_1.
605
606
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
607
608
609
610
611
Lemma persistently_and P Q :  (P  Q)   P   Q.
Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
Lemma persistently_or P Q :  (P  Q)   P   Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
Lemma persistently_impl P Q :  (P  Q)   P   Q.
612
Proof.
613
614
  apply impl_intro_l; rewrite -persistently_and.
  apply persistently_mono, impl_elim with P; auto.
615
Qed.
616
Lemma persistently_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
617
Proof. by rewrite -plainly_internal_eq persistently_plainly. Qed.
618

619
Lemma persistently_and_sep_l P Q :  P  Q   P  Q.
620
Proof. apply (anti_symm ()); auto using persistently_and_sep_l_1. Qed.
621
622
623
624
Lemma persistently_and_sep_r P Q : P   Q  P   Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
Lemma persistently_sep_dup P :  P   P   P.
Proof. by rewrite -persistently_and_sep_l idemp. Qed.
625

626
Lemma persistently_and_sep P Q :  (P  Q)   (P  Q).
627
628
Proof.
  apply (anti_symm ()); auto.
629
  rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l; auto.
630
Qed.
631
Lemma persistently_sep P Q :  (P  Q)   P   Q.
632
Proof. by rewrite -persistently_and_sep -persistently_and_sep_l persistently_and. Qed.
633

634
635
Lemma persistently_wand P Q :  (P - Q)   P -  Q.
Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
636
Lemma persistently_impl_wand P Q :  (P  Q)   (P - Q).
637
Proof.
638
  apply (anti_symm ()); [by rewrite -impl_wand_1|].
639
  apply persistently_intro', impl_intro_r.
640
  by rewrite persistently_and_sep_l persistently_elim wand_elim_l.
641
Qed.
642
Lemma impl_wand_persistently P Q : ( P  Q)  ( P - Q).
Ralf Jung's avatar
Ralf Jung committed
643
Proof.
644
645
  apply (anti_symm ()); [by rewrite -impl_wand_1|].
  apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
Ralf Jung's avatar
Ralf Jung committed
646
Qed.
647
648
649
650
Lemma persistently_entails_l P Q : (P   Q)  P   Q  P.
Proof. intros; rewrite -persistently_and_sep_l; auto. Qed.
Lemma persistently_entails_r P Q : (P   Q)  P  P   Q.
Proof. intros; rewrite -persistently_and_sep_r; auto. Qed.
651

652
653
Lemma persistently_laterN n P :  ^n P  ^n  P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
654

655
656
657
658
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).
659
    apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
660
    by rewrite wand_elim_r right_id.
661
  - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r.
662
    by rewrite persistently_elim impl_elim_r.
663
664
665
666
667
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).
668
    apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
669
    by rewrite impl_elim_r right_id.
670
  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
671
    by rewrite persistently_elim wand_elim_r.
672
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
673

674
(* Later derived *)
675
Hint Resolve later_mono.
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
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
695
696
Lemma later_exist_2 {A} (Φ : A  uPred M) : ( a,  Φ a)   ( a, Φ a).
Proof. apply exist_elim; eauto using exist_intro. Qed.
697
698
699
Lemma later_exist `{Inhabited A} (Φ : A  uPred M) :
   ( a, Φ a)  ( a,  Φ a).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
700
  apply: anti_symm; [|apply later_exist_2].
701
702
703
704
705
706
707
708
709
  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.
710
Lemma later_wand P Q :  (P - Q)   P -  Q.
711
712
713
714
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
715
(* Iterated later modality *)
716
Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
Robbert Krebbers's avatar
Robbert Krebbers committed
717
718
719
720
721
722
723
724
725
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.
726
Proof. induction n; f_equiv/=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
727
Lemma laterN_plus n1 n2 P : ^(n1 + n2) P  ^n1 ^n2 P.
728
Proof. induction n1; f_equiv/=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
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).
746
Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
747
748
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
749
750
Lemma laterN_exist `{Inhabited A} n (Φ : A  uPred M) :
  (^n  a, Φ a)   a, ^n Φ a.
751
Proof. induction n as [|n IH]; simpl; rewrite -?later_exist ?IH; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
752
Lemma laterN_and n P Q : ^n (P  Q)  ^n P  ^n Q.
753
Proof. induction n as [|n IH]; simpl; rewrite -?later_and ?IH; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
754
Lemma laterN_or n P Q : ^n (P  Q)  ^n P  ^n Q.
755
Proof. induction n as [|n IH]; simpl; rewrite -?later_or ?IH; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
756
757
758
759
760
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.
761
Proof. induction n as [|n IH]; simpl; rewrite -?later_sep ?IH; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
762
763
764
765
766
767
768
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.

769
770
(* Conditional persistently *)
Global Instance persistently_if_ne p : NonExpansive (@uPred_persistently_if M p).
771
Proof. solve_proper. Qed.
772
Global Instance persistently_if_proper p : Proper (() ==> ()) (@uPred_persistently_if M p).
773
Proof. solve_proper. Qed.
774
Global Instance persistently_if_mono p : Proper (() ==> ()) (@uPred_persistently_if M p).
775
776
Proof. solve_proper. Qed.

777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
Lemma persistently_if_elim p P : ?p P  P.
Proof. destruct p; simpl; auto using persistently_elim. Qed.
Lemma persistently_elim_if p P :  P  ?p P.
Proof. destruct p; simpl; auto using persistently_elim. Qed.

Lemma persistently_if_pure p φ : ?p ⌜φ⌝  ⌜φ⌝.
Proof. destruct p; simpl; auto using persistently_pure. Qed.
Lemma persistently_if_and p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using persistently_and. Qed.
Lemma persistently_if_or p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using persistently_or. Qed.
Lemma persistently_if_exist {A} p (Ψ : A  uPred M) : (?p  a, Ψ a)   a, ?p Ψ a.
Proof. destruct p; simpl; auto using persistently_exist. Qed.
Lemma persistently_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using persistently_sep. Qed.
Lemma persistently_if_later p P : ?p  P   ?p P.
Proof. destruct p; simpl; auto using persistently_later. Qed.
Lemma persistently_if_laterN p n P : ?p ^n P  ^n ?p P.
Proof. destruct p; simpl; auto using persistently_laterN. Qed.
796
797

(* True now *)
798
Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
799
Proof. solve_proper. Qed.
800
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
801
Proof. solve_proper. Qed.
802
Global Instance except_0_mono' : Proper (() ==> ()) (@uPred_except_0 M).
803
Proof. solve_proper. Qed.
804
805
Global Instance except_0_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_except_0 M).
806
807
Proof. solve_proper. Qed.

808
809
810
Lemma except_0_intro P : P   P.
Proof. rewrite /uPred_except_0; auto. Qed.
Lemma except_0_mono P Q : (P  Q)   P   Q.
811
Proof. by intros ->. Qed.
812
813
814
815
816
817
818
819
820
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.
821
Lemma except_0_sep P Q :  (P  Q)   P   Q.
822
823
Proof.
  rewrite /uPred_except_0. apply (anti_symm _).
824
  - apply or_elim; last by auto.
825
    by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup.
826
827
  - rewrite sep_or_r sep_elim_l sep_or_l;