plainly.v 23.3 KB
Newer Older
1
From iris.bi Require Import derived_laws_sbi.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.algebra Require Import monoid.
3
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5
6
7

Class Plainly (A : Type) := plainly : A  A.
Hint Mode Plainly ! : typeclass_instances.
Instance: Params (@plainly) 2.
8
Notation "■ P" := (plainly P) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

Robbert Krebbers's avatar
Robbert Krebbers committed
10
(* Mixins allow us to create instances easily without having to use Program *)
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
13
14
Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
  bi_plainly_mixin_plainly_ne : NonExpansive plainly;

  bi_plainly_mixin_plainly_mono P Q : (P  Q)   P   Q;
15
  bi_plainly_mixin_plainly_elim_persistently P :  P  <pers> P;
Robbert Krebbers's avatar
Robbert Krebbers committed
16
17
18
19
20
21
22
23
24
  bi_plainly_mixin_plainly_idemp_2 P :  P    P;

  bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A  PROP) :
    ( a,  (Ψ a))   ( a, Ψ a);

  (* The following two laws are very similar, and indeed they hold not just
     for persistently and plainly, but for any modality defined as `M P n x :=
     ∀ y, R x y → P n y`. *)
  bi_plainly_mixin_persistently_impl_plainly P Q :
25
    ( P  <pers> Q)  <pers> ( P  Q);
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
  bi_plainly_mixin_plainly_impl_plainly P Q : ( P   Q)   ( P  Q);

  bi_plainly_mixin_plainly_emp_intro P : P   emp;
  bi_plainly_mixin_plainly_absorb P Q :  P  Q   P;

  bi_plainly_mixin_prop_ext P Q :  ((P - Q)  (Q - P))  P  Q;

  bi_plainly_mixin_later_plainly_1 P :   P    P;
  bi_plainly_mixin_later_plainly_2 P :   P    P;
}.

Class BiPlainly (PROP : sbi) := {
  bi_plainly_plainly :> Plainly PROP;
  bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
}.
Hint Mode BiPlainly ! : typeclass_instances.
Arguments bi_plainly_plainly : simpl never.

Class BiPlainlyExist `{!BiPlainly PROP} :=
  plainly_exist_1 A (Ψ : A  PROP) :
     ( a, Ψ a)   a,  (Ψ a).
Arguments BiPlainlyExist : clear implicits.
Arguments BiPlainlyExist _ {_}.
Arguments plainly_exist_1 _ {_ _} _.
50
Hint Mode BiPlainlyExist ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
53
54
55
56
57
58
59
60

Section plainly_laws.
  Context `{BiPlainly PROP}.
  Implicit Types P Q : PROP.

  Global Instance plainly_ne : NonExpansive (@plainly PROP _).
  Proof. eapply bi_plainly_mixin_plainly_ne, bi_plainly_mixin. Qed.

  Lemma plainly_mono P Q : (P  Q)   P   Q.
  Proof. eapply bi_plainly_mixin_plainly_mono, bi_plainly_mixin. Qed.
61
  Lemma plainly_elim_persistently P :  P  <pers> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
65
66
  Proof. eapply bi_plainly_mixin_plainly_elim_persistently, bi_plainly_mixin. Qed.
  Lemma plainly_idemp_2 P :  P    P.
  Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed.
  Lemma plainly_forall_2 {A} (Ψ : A  PROP) : ( a,  (Ψ a))   ( a, Ψ a).
  Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed.
67
  Lemma persistently_impl_plainly P Q : ( P  <pers> Q)  <pers> ( P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
  Proof. eapply bi_plainly_mixin_persistently_impl_plainly, bi_plainly_mixin. Qed.
  Lemma plainly_impl_plainly P Q : ( P   Q)   ( P  Q).
  Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed.
  Lemma plainly_absorb P Q :  P  Q   P.
  Proof. eapply bi_plainly_mixin_plainly_absorb, bi_plainly_mixin. Qed.
  Lemma plainly_emp_intro P : P   emp.
  Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed.

  Lemma prop_ext P Q :  ((P - Q)  (Q - P))  P  Q.
  Proof. eapply bi_plainly_mixin_prop_ext, bi_plainly_mixin. Qed.

  Lemma later_plainly_1 P :   P   ( P).
  Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed.
  Lemma later_plainly_2 P :   P    P.
  Proof. eapply bi_plainly_mixin_later_plainly_2, bi_plainly_mixin. Qed.
End plainly_laws.

(* Derived properties and connectives *)
Class Plain `{BiPlainly PROP} (P : PROP) := plain : P   P.
Arguments Plain {_ _} _%I : simpl never.
Arguments plain {_ _} _%I {_}.
89
Hint Mode Plain + - ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
92
93
94
95
96
97
Instance: Params (@Plain) 1.

Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
  (if p then  P else P)%I.
Arguments plainly_if {_ _} !_ _%I /.
Instance: Params (@plainly_if) 2.
Typeclasses Opaque plainly_if.

98
Notation "■? p P" := (plainly_if p P) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117

(* Derived laws *)
Section plainly_derived.
Context `{BiPlainly PROP}.
Implicit Types P : PROP.

Hint Resolve pure_intro forall_intro.
Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.

Global Instance plainly_proper :
  Proper (() ==> ()) (@plainly PROP _) := ne_proper _.

Global Instance plainly_mono' : Proper (() ==> ()) (@plainly PROP _).
Proof. intros P Q; apply plainly_mono. Qed.
Global Instance plainly_flip_mono' :
  Proper (flip () ==> flip ()) (@plainly PROP _).
Proof. intros P Q; apply plainly_mono. Qed.

118
Lemma affinely_plainly_elim P : <affine>  P  P.
119
Proof. by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
120

Ralf Jung's avatar
Ralf Jung committed
121
Lemma persistently_elim_plainly P : <pers>  P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
Proof.
  apply (anti_symm _).
Ralf Jung's avatar
Ralf Jung committed
124
  - by rewrite persistently_into_absorbingly /bi_absorbingly comm plainly_absorb.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
126
  - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
Qed.
Ralf Jung's avatar
Ralf Jung committed
127
128
Lemma persistently_if_elim_plainly P p : <pers>?p  P   P.
Proof. destruct p; last done. exact: persistently_elim_plainly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
129

Ralf Jung's avatar
Ralf Jung committed
130
Lemma plainly_persistently_elim P :  <pers> P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
132
133
134
135
136
137
138
Proof.
  apply (anti_symm _).
  - rewrite -{1}(left_id True%I bi_and ( _)%I) (plainly_emp_intro True%I).
    rewrite -{2}(persistently_and_emp_elim P).
    rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
  - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
Qed.

Ralf Jung's avatar
Ralf Jung committed
139
140
Lemma absorbingly_elim_plainly P : <absorb>  P   P.
Proof. by rewrite -(persistently_elim_plainly P) absorbingly_elim_persistently. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
143
144

Lemma plainly_and_sep_elim P Q :  P  Q - (emp  P)  Q.
Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
Lemma plainly_and_sep_assoc P Q R :  P  (Q  R)  ( P  Q)  R.
Ralf Jung's avatar
Ralf Jung committed
145
Proof. by rewrite -(persistently_elim_plainly P) persistently_and_sep_assoc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
Lemma plainly_and_emp_elim P : emp   P  P.
Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
Ralf Jung's avatar
Ralf Jung committed
148
149
Lemma plainly_into_absorbingly P :  P  <absorb> P.
Proof. by rewrite plainly_elim_persistently persistently_into_absorbingly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
Lemma plainly_elim P `{!Absorbing P} :  P  P.
Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.

Lemma plainly_idemp_1 P :   P   P.
Ralf Jung's avatar
Ralf Jung committed
154
Proof. by rewrite plainly_into_absorbingly absorbingly_elim_plainly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
158
159
160
Lemma plainly_idemp P :   P   P.
Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.

Lemma plainly_intro' P Q : ( P  Q)   P   Q.
Proof. intros <-. apply plainly_idemp_2. Qed.

161
Lemma plainly_pure φ :  ⌜φ⌝ @{PROP} ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
164
165
166
Proof.
  apply (anti_symm _); auto.
  - by rewrite plainly_elim_persistently persistently_pure.
  - apply pure_elim'=> Hφ.
    trans ( x : False,  True : PROP)%I; [by apply forall_intro|].
167
    rewrite plainly_forall_2. by rewrite -(pure_intro φ).
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
Qed.
Lemma plainly_forall {A} (Ψ : A  PROP) :  ( 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_2 {A} (Ψ : A  PROP) : ( a,  (Ψ a))   ( a, Ψ a).
Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed.
Lemma plainly_exist `{!BiPlainlyExist PROP} {A} (Ψ : A  PROP) :
   ( a, Ψ a)   a,  (Ψ a).
Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed.
Lemma plainly_and P Q :  (P  Q)   P   Q.
Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
Lemma plainly_or_2 P Q :  P   Q   (P  Q).
Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed.
Lemma plainly_or `{!BiPlainlyExist PROP} 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.

191
192
193
Lemma plainly_emp_2 : emp @{PROP}  emp.
Proof. apply plainly_emp_intro. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
196
197
Lemma plainly_sep_dup P :  P   P   P.
Proof.
  apply (anti_symm _).
  - rewrite -{1}(idemp bi_and ( _)%I).
198
    by rewrite -{2}(emp_sep ( _)%I) plainly_and_sep_assoc and_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
201
202
  - by rewrite plainly_absorb.
Qed.

Lemma plainly_and_sep_l_1 P Q :  P  Q   P  Q.
203
Proof. by rewrite -{1}(emp_sep Q%I) plainly_and_sep_assoc and_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
206
Lemma plainly_and_sep_r_1 P Q : P   Q  P   Q.
Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.

207
Lemma plainly_True_emp :  True @{PROP}  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
209
210
211
Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
Lemma plainly_and_sep P Q :  (P  Q)   (P  Q).
Proof.
  rewrite plainly_and.
212
  rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
  by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
Qed.

Ralf Jung's avatar
Ralf Jung committed
216
Lemma plainly_affinely_elim P :  <affine> P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218
Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.

219
220
221
222
Lemma intuitionistically_plainly_elim P :   P -  P.
Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
Lemma intuitionistically_plainly P :   P -   P.
Proof.
Ralf Jung's avatar
Ralf Jung committed
223
224
  rewrite /bi_intuitionistically plainly_affinely_elim affinely_elim.
  rewrite persistently_elim_plainly plainly_persistently_elim. done.
225
226
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
230
231
232
233
234
235
236
237
238
Lemma and_sep_plainly P Q :  P   Q   P   Q.
Proof.
  apply (anti_symm _); auto using plainly_and_sep_l_1.
  apply and_intro.
  - by rewrite plainly_absorb.
  - by rewrite comm plainly_absorb.
Qed.
Lemma plainly_sep_2 P Q :  P   Q   (P  Q).
Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
Lemma plainly_sep `{BiPositive PROP} P Q :  (P  Q)   P   Q.
Proof.
  apply (anti_symm _); auto using plainly_sep_2.
Ralf Jung's avatar
Ralf Jung committed
239
  rewrite -(plainly_affinely_elim (_  _)%I) affinely_sep -and_sep_plainly. apply and_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
  - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
  - by rewrite (affinely_elim_emp P) left_id affinely_elim.
Qed.

Lemma plainly_wand P Q :  (P - Q)   P -  Q.
Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed.

Lemma plainly_entails_l P Q : (P   Q)  P   Q  P.
Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed.
Lemma plainly_entails_r P Q : (P   Q)  P  P   Q.
Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.

Lemma plainly_impl_wand_2 P Q :  (P - Q)   (P  Q).
Proof.
  apply plainly_intro', impl_intro_r.
255
  rewrite -{2}(emp_sep P%I) plainly_and_sep_assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
257
258
259
260
261
  by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
Qed.

Lemma impl_wand_plainly_2 P Q : ( P - Q)  ( P  Q).
Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.

262
Lemma impl_wand_affinely_plainly P Q : ( P  Q)  (<affine>  P - Q).
Ralf Jung's avatar
Ralf Jung committed
263
Proof. by rewrite -(persistently_elim_plainly P) impl_wand_intuitionistically. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
264

265
266
267
268
269
270
271
272
Lemma persistently_wand_affinely_plainly P Q :
  (<affine>  P - <pers> Q)  <pers> (<affine>  P - Q).
Proof. rewrite -!impl_wand_affinely_plainly. apply persistently_impl_plainly. Qed.

Lemma plainly_wand_affinely_plainly P Q :
  (<affine>  P -  Q)   (<affine>  P - Q).
Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
273
274
275
Section plainly_affine_bi.
  Context `{BiAffine PROP}.

276
  Lemma plainly_emp :  emp @{PROP} emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
  Proof. by rewrite -!True_emp plainly_pure. Qed.

  Lemma plainly_and_sep_l P Q :  P  Q   P  Q.
  Proof.
    apply (anti_symm ());
      eauto using plainly_and_sep_l_1, sep_and with typeclass_instances.
  Qed.
  Lemma plainly_and_sep_r P Q : P   Q  P   Q.
  Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed.

  Lemma plainly_impl_wand P Q :  (P  Q)   (P - Q).
  Proof.
    apply (anti_symm ()); auto using plainly_impl_wand_2.
    apply plainly_intro', wand_intro_l.
    by rewrite -plainly_and_sep_r plainly_elim impl_elim_r.
  Qed.

  Lemma impl_wand_plainly P Q : ( P  Q)  ( P - Q).
  Proof.
    apply (anti_symm ()). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2.
  Qed. 
End plainly_affine_bi.

(* Conditional plainly *)
Global Instance plainly_if_ne p : NonExpansive (@plainly_if PROP _ p).
Proof. solve_proper. Qed.
Global Instance plainly_if_proper p : Proper (() ==> ()) (@plainly_if PROP _ p).
Proof. solve_proper. Qed.
Global Instance plainly_if_mono' p : Proper (() ==> ()) (@plainly_if PROP _ p).
Proof. solve_proper. Qed.
Global Instance plainly_if_flip_mono' p :
  Proper (flip () ==> flip ()) (@plainly_if PROP _ p).
Proof. solve_proper. Qed.

Lemma plainly_if_mono p P Q : (P  Q)  ?p P  ?p Q.
Proof. by intros ->. Qed.

314
Lemma plainly_if_pure p φ : ?p ⌜φ⌝ @{PROP} ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
Proof. destruct p; simpl; auto using plainly_pure. Qed.
Lemma plainly_if_and p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using plainly_and. Qed.
Lemma plainly_if_or_2 p P Q : ?p P  ?p Q  ?p (P  Q).
Proof. destruct p; simpl; auto using plainly_or_2. Qed.
Lemma plainly_if_or `{!BiPlainlyExist PROP} p P Q : ?p (P  Q)  ?p P  ?p Q.
Proof. destruct p; simpl; auto using plainly_or. Qed.
Lemma plainly_if_exist_2 {A} p (Ψ : A  PROP) : ( a, ?p (Ψ a))  ?p ( a, Ψ a).
Proof. destruct p; simpl; auto using plainly_exist_2. Qed.
Lemma plainly_if_exist `{!BiPlainlyExist PROP} {A} p (Ψ : A  PROP) :
  ?p ( a, Ψ a)   a, ?p (Ψ a).
Proof. destruct p; simpl; auto using plainly_exist. Qed.
Lemma plainly_if_sep_2 `{!BiPositive PROP} p P Q : ?p P  ?p Q   ?p (P  Q).
Proof. destruct p; simpl; auto using plainly_sep_2. Qed.

Lemma plainly_if_idemp p P : ?p ?p P  ?p P.
Proof. destruct p; simpl; auto using plainly_idemp. Qed.

(* Properties of plain propositions *)
Global Instance Plain_proper : Proper (() ==> iff) (@Plain PROP _).
Proof. solve_proper. Qed.

Lemma plain_plainly_2 P `{!Plain P} : P   P.
Proof. done. Qed.
Lemma plain_plainly P `{!Plain P, !Absorbing P} :  P  P.
Proof. apply (anti_symm _), plain_plainly_2, _. by apply plainly_elim. Qed.
Lemma plainly_intro P Q `{!Plain P} : (P  Q)  P   Q.
Proof. by intros <-. Qed.

(* Typeclass instances *)
Global Instance plainly_absorbing P : Absorbing ( P).
Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorb. Qed.
Global Instance plainly_if_absorbing P p :
  Absorbing P  Absorbing (plainly_if p P).
Proof. intros; destruct p; simpl; apply _. Qed.

(* Not an instance, see the bottom of this file *)
Lemma plain_persistent P : Plain P  Persistent P.
Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.

(* Not an instance, see the bottom of this file *)
Lemma impl_persistent P Q :
  Absorbing P  Plain P  Persistent Q  Persistent (P  Q).
Proof.
  intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
Ralf Jung's avatar
Ralf Jung committed
360
                     -(persistent Q) (plainly_into_absorbingly P) absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
361
362
363
Qed.

Global Instance plainly_persistent P : Persistent ( P).
Ralf Jung's avatar
Ralf Jung committed
364
Proof. by rewrite /Persistent persistently_elim_plainly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
365
366
367
368

Global Instance wand_persistent P Q :
  Plain P  Persistent Q  Absorbing Q  Persistent (P - Q).
Proof.
369
  intros. rewrite /Persistent {2}(plain P). trans (<pers> ( P  Q))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
  - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
    by rewrite affinely_plainly_elim.
  - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
Qed.

(* Instances for big operators *)
Global Instance plainly_and_homomorphism :
  MonoidHomomorphism bi_and bi_and () (@plainly PROP _).
Proof.
  split; [split|]; try apply _. apply plainly_and. apply plainly_pure.
Qed.

Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} :
  MonoidHomomorphism bi_or bi_or () (@plainly PROP _).
Proof.
  split; [split|]; try apply _. apply plainly_or. apply plainly_pure.
Qed.

Global Instance plainly_sep_weak_homomorphism `{!BiPositive PROP, !BiAffine PROP} :
  WeakMonoidHomomorphism bi_sep bi_sep () (@plainly PROP _).
Proof. split; try apply _. apply plainly_sep. Qed.

Global Instance plainly_sep_homomorphism `{BiAffine PROP} :
  MonoidHomomorphism bi_sep bi_sep () (@plainly PROP _).
Proof. split. apply _. apply plainly_emp. Qed.

Global Instance plainly_sep_entails_weak_homomorphism :
  WeakMonoidHomomorphism bi_sep bi_sep (flip ()) (@plainly PROP _).
Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed.

Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} :
  MonoidHomomorphism bi_sep bi_sep (flip ()) (@plainly PROP _).
Proof. split. apply _. simpl. rewrite plainly_emp. done. Qed.

Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A  PROP) :
  NonExpansive Φ  LimitPreserving (λ x, Plain (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.

(* Plainness instances *)
409
Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
Proof. by rewrite /Plain plainly_pure. Qed.
Global Instance emp_plain : Plain (PROP:=PROP) emp.
Proof. apply plainly_emp_intro. Qed.
Global Instance and_plain P Q : Plain P  Plain Q  Plain (P  Q).
Proof. intros. by rewrite /Plain plainly_and -!plain. Qed.
Global Instance or_plain P Q : Plain P  Plain Q  Plain (P  Q).
Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed.
Global Instance forall_plain {A} (Ψ : A  PROP) :
  ( x, Plain (Ψ x))  Plain ( x, Ψ x).
Proof.
  intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain.
Qed.
Global Instance exist_plain {A} (Ψ : A  PROP) :
  ( x, Plain (Ψ x))  Plain ( x, Ψ x).
Proof.
  intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
Qed.

Global Instance impl_plain P Q : Absorbing P  Plain P  Plain Q  Plain (P  Q).
Proof.
  intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
Ralf Jung's avatar
Ralf Jung committed
431
                     (plainly_into_absorbingly P) absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
432
433
434
435
436
437
438
439
440
441
442
443
444
445
Qed.
Global Instance wand_plain P Q :
  Plain P  Plain Q  Absorbing Q  Plain (P - Q).
Proof.
  intros. rewrite /Plain {2}(plain P). trans ( ( P  Q))%I.
  - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q).
    by rewrite affinely_plainly_elim.
  - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
Qed.
Global Instance sep_plain P Q : Plain P  Plain Q  Plain (P  Q).
Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.

Global Instance plainly_plain P : Plain ( P).
Proof. by rewrite /Plain plainly_idemp. Qed.
446
Global Instance persistently_plain P : Plain P  Plain (<pers> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
447
Proof.
Ralf Jung's avatar
Ralf Jung committed
448
  rewrite /Plain=> HP. rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
Qed.
450
Global Instance affinely_plain P : Plain P  Plain (<affine> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
451
Proof. rewrite /bi_affinely. apply _. Qed.
452
453
Global Instance intuitionistically_plain P : Plain P  Plain ( P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
454
Global Instance absorbingly_plain P : Plain P  Plain (<absorb> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
455
456
457
458
459
460
Proof. rewrite /bi_absorbingly. apply _. Qed.
Global Instance from_option_plain {A} P (Ψ : A  PROP) (mx : option A) :
  ( x, Plain (Ψ x))  Plain P  Plain (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.

(* Interaction with equality *)
461
Lemma plainly_internal_eq {A:ofeT} (a b : A) :  (a  b) @{PROP} a  b.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
463
464
465
466
467
468
Proof.
  apply (anti_symm ()).
  { by rewrite plainly_elim. }
  apply (internal_eq_rewrite' a b (λ  b,  (a  b))%I); [solve_proper|done|].
  rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
Qed.

469
Lemma plainly_alt P :  P  <affine> P  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
470
Proof.
Ralf Jung's avatar
Ralf Jung committed
471
  rewrite -plainly_affinely_elim. apply (anti_symm ()).
Robbert Krebbers's avatar
Robbert Krebbers committed
472
473
474
475
476
477
478
479
480
481
482
483
484
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
  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
    + by rewrite affinely_elim_emp left_id.
    + by rewrite left_id.
  - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
    by rewrite -plainly_True_emp plainly_pure True_impl.
Qed.

Lemma plainly_alt_absorbing P `{!Absorbing P} :  P  P  True.
Proof.
  apply (anti_symm ()).
  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
  - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly).
    by rewrite plainly_pure True_impl.
Qed.

Lemma plainly_True_alt P :  (True - P)  P  True.
Proof.
  apply (anti_symm ()).
  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
    by rewrite wand_elim_r.
  - rewrite internal_eq_sym (internal_eq_rewrite _ _
      (λ Q,  (True - Q))%I ltac:(shelve)); last solve_proper.
    by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
Qed.

(* Interaction with ▷ *)
Lemma later_plainly P :   P    P.
Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed.
Lemma laterN_plainly n P : ^n  P   ^n P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed.

Lemma later_plainly_if p P :  ?p P  ?p  P.
Proof. destruct p; simpl; auto using later_plainly. Qed.
Lemma laterN_plainly_if n p P : ^n ?p P  ?p (^n P).
Proof. destruct p; simpl; auto using laterN_plainly. Qed.

Lemma except_0_plainly_1 P :   P    P.
Proof. by rewrite /sbi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed.
Lemma except_0_plainly `{!BiPlainlyExist PROP} P :   P    P.
Proof. by rewrite /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed.

Global Instance internal_eq_plain {A : ofeT} (a b : A) :
514
  Plain (PROP:=PROP) (a  b).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
540
541
542
543
544
545
Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.

Global Instance later_plain P : Plain P  Plain ( P).
Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed.
Global Instance laterN_plain n P : Plain P  Plain (^n P).
Proof. induction n; apply _. Qed.
Global Instance except_0_plain P : Plain P  Plain ( P).
Proof. rewrite /sbi_except_0; apply _. Qed.

Global Instance plainly_timeless P  `{!BiPlainlyExist PROP} :
  Timeless P  Timeless ( P).
Proof.
  intros. rewrite /Timeless /sbi_except_0 later_plainly_1.
  by rewrite (timeless P) /sbi_except_0 plainly_or {1}plainly_elim.
Qed.
End plainly_derived.

(* When declared as an actual instance, [plain_persistent] will cause
failing proof searches to take exponential time, as Coq will try to
apply it the instance at any node in the proof search tree.

To avoid that, we declare it using a [Hint Immediate], so that it will
only be used at the leaves of the proof search tree, i.e. when the
premise of the hint can be derived from just the current context. *)
Hint Immediate plain_persistent : typeclass_instances.

(* Not defined using an ordinary [Instance] because the default
[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [coreP_persistent] for an
example where it would fail with a regular [Instance].*)
Hint Extern 4 (Persistent (_  _)) => eapply @impl_persistent : typeclass_instances.