plainly.v 23.7 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

Class Plainly (A : Type) := plainly : A  A.
Hint Mode Plainly ! : typeclass_instances.
7
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
Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
12
  bi_plainly_mixin_plainly_ne : NonExpansive (plainly (A:=PROP));
Robbert Krebbers's avatar
Robbert Krebbers committed
13

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

  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`. *)
24
  bi_plainly_mixin_persistently_impl_plainly (P Q : PROP) :
25
    ( P  <pers> Q)  <pers> ( P  Q);
26
27
  bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
    ( P   Q)   ( P  Q);
Robbert Krebbers's avatar
Robbert Krebbers committed
28

29
30
  bi_plainly_mixin_plainly_emp_intro (P : PROP) : P   emp;
  bi_plainly_mixin_plainly_absorb (P Q : PROP) :  P  Q   P;
Robbert Krebbers's avatar
Robbert Krebbers committed
31

32
  bi_plainly_mixin_prop_ext_2 (P Q : PROP) :  ((P - Q)  (Q - P))  P  Q;
Robbert Krebbers's avatar
Robbert Krebbers committed
33

34
35
  bi_plainly_mixin_later_plainly_1 (P : PROP) :   P    P;
  bi_plainly_mixin_later_plainly_2 (P : PROP) :   P    P;
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
}.

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 _ {_ _} _.
51
Hint Mode BiPlainlyExist ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
55
56
57
58
59
60
61

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.
62
  Lemma plainly_elim_persistently P :  P  <pers> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
65
66
67
  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.
68
  Lemma persistently_impl_plainly P Q : ( P  <pers> Q)  <pers> ( P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
69
70
71
72
73
74
75
76
  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.

77
78
  Lemma prop_ext_2 P Q :  ((P - Q)  (Q - P))  P  Q.
  Proof. eapply bi_plainly_mixin_prop_ext_2, bi_plainly_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
81
82
83
84
85
86
87
88
89

  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 {_}.
90
Hint Mode Plain + - ! : typeclass_instances.
91
Instance: Params (@Plain) 1 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
95

Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
  (if p then  P else P)%I.
Arguments plainly_if {_ _} !_ _%I /.
96
Instance: Params (@plainly_if) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
Typeclasses Opaque plainly_if.

99
Notation "■? p P" := (plainly_if p P) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103
104
105

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

Tej Chajed's avatar
Tej Chajed committed
106
107
108
Hint Resolve pure_intro forall_intro : core.
Hint Resolve or_elim or_intro_l' or_intro_r' : core.
Hint Resolve and_intro and_elim_l' and_elim_r' : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
113
114
115
116
117
118

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.

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

Ralf Jung's avatar
Ralf Jung committed
122
Lemma persistently_elim_plainly P : <pers>  P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
Proof.
  apply (anti_symm _).
Ralf Jung's avatar
Ralf Jung committed
125
  - by rewrite persistently_into_absorbingly /bi_absorbingly comm plainly_absorb.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
  - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
Qed.
Ralf Jung's avatar
Ralf Jung committed
128
129
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
130

Ralf Jung's avatar
Ralf Jung committed
131
Lemma plainly_persistently_elim P :  <pers> P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
134
135
136
137
138
139
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
140
141
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
142
143
144
145

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
146
Proof. by rewrite -(persistently_elim_plainly P) persistently_and_sep_assoc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
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
149
150
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
151
152
153
154
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
155
Proof. by rewrite plainly_into_absorbingly absorbingly_elim_plainly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
160
161
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.

162
Lemma plainly_pure φ :  ⌜φ⌝ @{PROP} ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
166
167
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|].
168
    rewrite plainly_forall_2. by rewrite -(pure_intro φ).
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
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.

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

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

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

208
Lemma plainly_True_emp :  True @{PROP}  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
210
211
212
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.
213
  rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
216
  by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
Qed.

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

220
221
222
223
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
224
225
  rewrite /bi_intuitionistically plainly_affinely_elim affinely_elim.
  rewrite persistently_elim_plainly plainly_persistently_elim. done.
226
227
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
230
231
232
233
234
235
236
237
238
239
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
240
  rewrite -(plainly_affinely_elim (_  _)%I) affinely_sep -and_sep_plainly. apply and_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
  - 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.
256
  rewrite -{2}(emp_sep P%I) plainly_and_sep_assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
259
260
261
262
  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.

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

266
267
268
269
270
271
272
273
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
274
275
276
Section plainly_affine_bi.
  Context `{BiAffine PROP}.

277
  Lemma plainly_emp :  emp @{PROP} emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
314
  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.

315
Lemma plainly_if_pure p φ : ?p ⌜φ⌝ @{PROP} ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
360
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
361
                     -(persistent Q) (plainly_into_absorbingly P) absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
363
364
Qed.

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

Global Instance wand_persistent P Q :
  Plain P  Persistent Q  Absorbing Q  Persistent (P - Q).
Proof.
370
  intros. rewrite /Persistent {2}(plain P). trans (<pers> ( P  Q))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
409
  - 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 *)
410
Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
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
432
                     (plainly_into_absorbingly P) absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
434
435
436
437
438
439
440
441
442
443
444
445
446
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.
447
Global Instance persistently_plain P : Plain P  Plain (<pers> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
448
Proof.
Ralf Jung's avatar
Ralf Jung committed
449
  rewrite /Plain=> HP. rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
Robbert Krebbers's avatar
Robbert Krebbers committed
450
Qed.
451
Global Instance affinely_plain P : Plain P  Plain (<affine> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
452
Proof. rewrite /bi_affinely. apply _. Qed.
453
454
Global Instance intuitionistically_plain P : Plain P  Plain ( P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
455
Global Instance absorbingly_plain P : Plain P  Plain (<absorb> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
456
457
458
459
460
461
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 *)
462
Lemma plainly_internal_eq {A:ofeT} (a b : A) :  (a  b) @{PROP} a  b.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
466
467
468
469
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.

470
471
472
473
474
475
476
477
478
Lemma prop_ext P Q : P  Q   (P - Q).
Proof.
  apply (anti_symm ()); last exact: prop_ext_2.
  apply (internal_eq_rewrite' P Q (λ Q,  (P - Q))%I);
    [ solve_proper | done | ].
  rewrite (plainly_emp_intro (P  Q)%I).
  apply plainly_mono, wand_iff_refl.
Qed.

479
Lemma plainly_alt P :  P  <affine> P  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
Proof.
Ralf Jung's avatar
Ralf Jung committed
481
  rewrite -plainly_affinely_elim. apply (anti_symm ()).
482
  - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
484
485
486
487
488
489
490
491
    + 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 ()).
492
  - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
493
494
495
496
497
498
499
  - 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 ()).
500
  - rewrite prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
    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) :
524
  Plain (PROP:=PROP) (a  b).
Robbert Krebbers's avatar
Robbert Krebbers committed
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
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.