interface.v 19.2 KB
Newer Older
1
From iris.algebra Require Export ofe.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.bi Require Export notation.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.prelude Require Import options.
4
Set Primitive Projections.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6

Section bi_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  Context {PROP : Type} `{Dist PROP, Equiv PROP}.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
14
15
16
17
18
19
  Context (bi_entails : PROP  PROP  Prop).
  Context (bi_emp : PROP).
  Context (bi_pure : Prop  PROP).
  Context (bi_and : PROP  PROP  PROP).
  Context (bi_or : PROP  PROP  PROP).
  Context (bi_impl : PROP  PROP  PROP).
  Context (bi_forall :  A, (A  PROP)  PROP).
  Context (bi_exist :  A, (A  PROP)  PROP).
  Context (bi_sep : PROP  PROP  PROP).
  Context (bi_wand : PROP  PROP  PROP).
  Context (bi_persistently : PROP  PROP).

20
  Bind Scope bi_scope with PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  Local Infix "⊢" := bi_entails.
22
23
24
25
26
27
28
  Local Notation "'emp'" := bi_emp : bi_scope.
  Local Notation "'True'" := (bi_pure True) : bi_scope.
  Local Notation "'False'" := (bi_pure False) : bi_scope.
  Local Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
  Local Infix "∧" := bi_and : bi_scope.
  Local Infix "∨" := bi_or : bi_scope.
  Local Infix "→" := bi_impl : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  Local Notation "∀ x .. y , P" :=
30
    (bi_forall _ (λ x, .. (bi_forall _ (λ y, P%I)) ..)) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  Local Notation "∃ x .. y , P" :=
32
33
34
35
    (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
  Local Infix "∗" := bi_sep : bi_scope.
  Local Infix "-∗" := bi_wand : bi_scope.
  Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

Ralf Jung's avatar
Ralf Jung committed
37
38
39
40
41
42
  (** * Axioms for a general BI (logic of bunched implications) *)

  (** The following axioms are satisifed by both affine and linear BIs, and BIs
  that combine both kinds of resources. In particular, we have an "ordered RA"
  model satisfying all these axioms. For this model, we extend RAs with an
  arbitrary partial order, and up-close resources wrt. that order (instead of
43
  extension order).  We demand composition to be monotone wrt. the order: [x1 ≼
44
45
46
  x2 → x1 ⋅ y ≼ x2 ⋅ y].  We define [emp := λ r, ε ≼ r]; persistently is still
  defined with the core: [persistently P := λ r, P (core r)].  This is uplcosed
  because the core is monotone.  *)
Ralf Jung's avatar
Ralf Jung committed
47

Ralf Jung's avatar
Ralf Jung committed
48
  Record BiMixin := {
Robbert Krebbers's avatar
Robbert Krebbers committed
49
    bi_mixin_entails_po : PreOrder bi_entails;
50
    bi_mixin_equiv_entails P Q : (P  Q)  (P  Q)  (Q  P);
Robbert Krebbers's avatar
Robbert Krebbers committed
51

52
    (** Non-expansiveness *)
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
56
57
58
59
60
61
62
63
64
    bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure;
    bi_mixin_and_ne : NonExpansive2 bi_and;
    bi_mixin_or_ne : NonExpansive2 bi_or;
    bi_mixin_impl_ne : NonExpansive2 bi_impl;
    bi_mixin_forall_ne A n :
      Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A);
    bi_mixin_exist_ne A n :
      Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
    bi_mixin_sep_ne : NonExpansive2 bi_sep;
    bi_mixin_wand_ne : NonExpansive2 bi_wand;
    bi_mixin_persistently_ne : NonExpansive bi_persistently;

65
    (** Higher-order logic *)
66
    bi_mixin_pure_intro (φ : Prop) P : φ  P   φ ;
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
    bi_mixin_pure_elim' (φ : Prop) P : (φ  True  P)   φ   P;

    bi_mixin_and_elim_l P Q : P  Q  P;
    bi_mixin_and_elim_r P Q : P  Q  Q;
    bi_mixin_and_intro P Q R : (P  Q)  (P  R)  P  Q  R;

    bi_mixin_or_intro_l P Q : P  P  Q;
    bi_mixin_or_intro_r P Q : Q  P  Q;
    bi_mixin_or_elim P Q R : (P  R)  (Q  R)  P  Q  R;

    bi_mixin_impl_intro_r P Q R : (P  Q  R)  P  Q  R;
    bi_mixin_impl_elim_l' P Q R : (P  Q  R)  P  Q  R;

    bi_mixin_forall_intro {A} P (Ψ : A  PROP) : ( a, P  Ψ a)  P   a, Ψ a;
    bi_mixin_forall_elim {A} {Ψ : A  PROP} a : ( a, Ψ a)  Ψ a;

    bi_mixin_exist_intro {A} {Ψ : A  PROP} a : Ψ a   a, Ψ a;
    bi_mixin_exist_elim {A} (Φ : A  PROP) Q : ( a, Φ a  Q)  ( a, Φ a)  Q;

86
    (** BI connectives *)
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
89
90
91
92
93
94
    bi_mixin_sep_mono P P' Q Q' : (P  Q)  (P'  Q')  P  P'  Q  Q';
    bi_mixin_emp_sep_1 P : P  emp  P;
    bi_mixin_emp_sep_2 P : emp  P  P;
    bi_mixin_sep_comm' P Q : P  Q  Q  P;
    bi_mixin_sep_assoc' P Q R : (P  Q)  R  P  (Q  R);
    bi_mixin_wand_intro_r P Q R : (P  Q  R)  P  Q - R;
    bi_mixin_wand_elim_l' P Q R : (P  Q - R)  P  Q  R;

95
    (** Persistently *)
96
    (* In the ordered RA model: Holds without further assumptions. *)
97
    bi_mixin_persistently_mono P Q : (P  Q)  <pers> P  <pers> Q;
98
    (* In the ordered RA model: `core` is idempotent *)
99
    bi_mixin_persistently_idemp_2 P : <pers> P  <pers> <pers> P;
Robbert Krebbers's avatar
Robbert Krebbers committed
100

Ralf Jung's avatar
Ralf Jung committed
101
    (* In the ordered RA model: [ε ≼ core x]. *)
102
    bi_mixin_persistently_emp_2 : emp  <pers> emp;
103

104
105
106
    (* The laws of a "frame" (https://ncatlab.org/nlab/show/frame, not to be
    confused with separation logic terminology): commuting with finite
    conjunction and infinite disjunction.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
    The null-ary case, [persistently_True : True ⊢ <pers> True], is derivable from the
    other laws. *)
109
    bi_mixin_persistently_and_2 (P Q : PROP) :
Ralf Jung's avatar
Ralf Jung committed
110
      (<pers> P)  (<pers> Q)  <pers> (P  Q);
Robbert Krebbers's avatar
Robbert Krebbers committed
111
    bi_mixin_persistently_exist_1 {A} (Ψ : A  PROP) :
112
      <pers> ( a, Ψ a)   a, <pers> (Ψ a);
Robbert Krebbers's avatar
Robbert Krebbers committed
113

114
    (* In the ordered RA model: [core x ≼ core (x ⋅ y)]. *)
115
    bi_mixin_persistently_absorbing P Q : <pers> P  Q  <pers> P;
Ralf Jung's avatar
typo    
Ralf Jung committed
116
    (* In the ordered RA model: [x ⋅ core x = x]. *)
117
    bi_mixin_persistently_and_sep_elim P Q : <pers> P  Q  P  Q;
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
  }.

120
121
122
123
124
125
  (** We equip any BI with a later modality. This avoids an additional layer in
  the BI hierachy and improves performance significantly (see Iris issue #303).

  For non step-indexed BIs the later modality can simply be defined as the
  identity function, as the Löb axiom or contractiveness of later is not part of
  [BiLaterMixin]. For step-indexed BIs one should separately prove an instance
126
127
  of the class [BiLaterContractive PROP] or [BiLöb PROP]. (Note that there is an
  instance [BiLaterContractive PROP → BiLöb PROP] in [derived_laws_later].)
128
129
130

  For non step-indexed BIs one can get a "free" instance of [BiLaterMixin] using
  the smart constructor [bi_later_mixin_id] below. *)
131
132
  Context (bi_later : PROP  PROP).
  Local Notation "▷ P" := (bi_later P) : bi_scope.
133

134
135
  Record BiLaterMixin := {
    bi_mixin_later_ne : NonExpansive bi_later;
Robbert Krebbers's avatar
Robbert Krebbers committed
136

137
138
    bi_mixin_later_mono P Q : (P  Q)   P   Q;
    bi_mixin_later_intro P : P   P;
Robbert Krebbers's avatar
Robbert Krebbers committed
139

140
141
    bi_mixin_later_forall_2 {A} (Φ : A  PROP) : ( a,  Φ a)    a, Φ a;
    bi_mixin_later_exist_false {A} (Φ : A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
142
      (  a, Φ a)   False  ( a,  Φ a);
143
144
145
146
    bi_mixin_later_sep_1 P Q :  (P  Q)   P   Q;
    bi_mixin_later_sep_2 P Q :  P   Q   (P  Q);
    bi_mixin_later_persistently_1 P :  <pers> P  <pers>  P;
    bi_mixin_later_persistently_2 P : <pers>  P   <pers> P;
Robbert Krebbers's avatar
Robbert Krebbers committed
147

148
    bi_mixin_later_false_em P :  P   False  ( False  P);
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  }.
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164

  Lemma bi_later_mixin_id :
    ( (P : PROP), ( P)%I = P) 
    BiMixin  BiLaterMixin.
  Proof.
    intros Hlater Hbi. pose proof (bi_mixin_entails_po Hbi).
    split; repeat intro; rewrite ?Hlater ?Hequiv //.
    - apply (bi_mixin_forall_intro Hbi)=> a.
      etrans; [apply (bi_mixin_forall_elim Hbi a)|]. by rewrite Hlater.
    - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
      apply (bi_mixin_exist_elim Hbi)=> a.
      etrans; [|apply (bi_mixin_exist_intro Hbi a)]. by rewrite /= Hlater.
    - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
      apply (bi_mixin_impl_intro_r Hbi), (bi_mixin_and_elim_l Hbi).
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
End bi_mixin.

167
168
169
170
171
172
173
Module Import universes.
  (** The universe of the logic (PROP). *)
  Universe Logic.
  (** The universe of quantifiers in the logic. *)
  Universe Quant.
End universes.

Ralf Jung's avatar
Ralf Jung committed
174
Structure bi := Bi {
175
  bi_car :> Type@{Logic};
Robbert Krebbers's avatar
Robbert Krebbers committed
176
177
178
179
180
181
182
183
  bi_dist : Dist bi_car;
  bi_equiv : Equiv bi_car;
  bi_entails : bi_car  bi_car  Prop;
  bi_emp : bi_car;
  bi_pure : Prop  bi_car;
  bi_and : bi_car  bi_car  bi_car;
  bi_or : bi_car  bi_car  bi_car;
  bi_impl : bi_car  bi_car  bi_car;
184
185
  bi_forall :  A : Type@{Quant}, (A  bi_car)  bi_car;
  bi_exist :  A : Type@{Quant}, (A  bi_car)  bi_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
  bi_sep : bi_car  bi_car  bi_car;
  bi_wand : bi_car  bi_car  bi_car;
  bi_persistently : bi_car  bi_car;
189
  bi_later : bi_car  bi_car;
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  bi_ofe_mixin : OfeMixin bi_car;
191
  bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin);
192
  bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
Robbert Krebbers's avatar
Robbert Krebbers committed
193
                        bi_exist bi_sep bi_wand bi_persistently;
194
195
  bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                   bi_forall bi_exist bi_sep bi_persistently bi_later;
Robbert Krebbers's avatar
Robbert Krebbers committed
196
}.
197
Bind Scope bi_scope with bi_car.
Robbert Krebbers's avatar
Robbert Krebbers committed
198

199
Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
200
Canonical Structure bi_ofeO.
201
202
203
204
205
206

(** The projection [bi_cofe_aux] is not registered as an instance because it has
the wrong type. Its result type is unfolded, i.e., [Cofe (Ofe PROP ...)], and
thus should never be used. The instance [bi_cofe] has the proper result type
[Cofe (bi_ofeO PROP)]. *)
Global Instance bi_cofe (PROP : bi) : Cofe PROP := bi_cofe_aux PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
207

208
209
210
211
212
213
214
215
216
217
218
219
Global Instance: Params (@bi_entails) 1 := {}.
Global Instance: Params (@bi_emp) 1 := {}.
Global Instance: Params (@bi_pure) 1 := {}.
Global Instance: Params (@bi_and) 1 := {}.
Global Instance: Params (@bi_or) 1 := {}.
Global Instance: Params (@bi_impl) 1 := {}.
Global Instance: Params (@bi_forall) 2 := {}.
Global Instance: Params (@bi_exist) 2 := {}.
Global Instance: Params (@bi_sep) 1 := {}.
Global Instance: Params (@bi_wand) 1 := {}.
Global Instance: Params (@bi_persistently) 1 := {}.
Global Instance: Params (@bi_later) 1  := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
220

Ralf Jung's avatar
Ralf Jung committed
221
222
223
Global Arguments bi_car : simpl never.
Global Arguments bi_dist : simpl never.
Global Arguments bi_equiv : simpl never.
224
Global Arguments bi_entails {PROP} _ _ : simpl never, rename.
Ralf Jung's avatar
Ralf Jung committed
225
226
Global Arguments bi_emp {PROP} : simpl never, rename.
Global Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
227
228
229
Global Arguments bi_and {PROP} _ _ : simpl never, rename.
Global Arguments bi_or {PROP} _ _ : simpl never, rename.
Global Arguments bi_impl {PROP} _ _ : simpl never, rename.
Ralf Jung's avatar
Ralf Jung committed
230
231
Global Arguments bi_forall {PROP _} _%I : simpl never, rename.
Global Arguments bi_exist {PROP _} _%I : simpl never, rename.
232
233
234
235
Global Arguments bi_sep {PROP} _ _ : simpl never, rename.
Global Arguments bi_wand {PROP} _ _ : simpl never, rename.
Global Arguments bi_persistently {PROP} _ : simpl never, rename.
Global Arguments bi_later {PROP} _ : simpl never, rename.
Robbert Krebbers's avatar
Robbert Krebbers committed
236

237
Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
238
239
240
241
242
(** We set this rewrite relation's priority below the stdlib's 
  ([impl], [iff], [eq], ...) and [≡] but above [⊑].
  [eq] (at 100) < [≡] (at 150) < [bi_entails _] (at 170) < [⊑] (at 200)
*)
Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) | 170 := {}.
243
Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
Robbert Krebbers's avatar
Robbert Krebbers committed
244

245
Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
246
Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
247
Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
248
Notation "'(⊢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
249

250
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
251
Notation "P '⊣⊢@{' PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
252
Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
253
254
255
Notation "'(⊣⊢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
Notation "( P ⊣⊢.)" := (equiv (A:=bi_car _) P) (only parsing) : stdpp_scope.
Notation "(.⊣⊢ Q )" := (λ P, P @{bi_car _} Q) (only parsing) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
256

257
Notation "P -∗ Q" := (P  Q) : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
259

Notation "'emp'" := (bi_emp) : bi_scope.
260
Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
262
263
264
265
266
267
Notation "'True'" := (bi_pure True) : bi_scope.
Notation "'False'" := (bi_pure False) : bi_scope.
Infix "∧" := bi_and : bi_scope.
Notation "(∧)" := bi_and (only parsing) : bi_scope.
Infix "∨" := bi_or : bi_scope.
Notation "(∨)" := bi_or (only parsing) : bi_scope.
Infix "→" := bi_impl : bi_scope.
268
Notation "¬ P" := (P  False)%I : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
272
Infix "∗" := bi_sep : bi_scope.
Notation "(∗)" := bi_sep (only parsing) : bi_scope.
Notation "P -∗ Q" := (bi_wand P Q) : bi_scope.
Notation "∀ x .. y , P" :=
Ralf Jung's avatar
Ralf Jung committed
273
  (bi_forall (λ x, .. (bi_forall (λ y, P%I)) ..)) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
Notation "∃ x .. y , P" :=
Ralf Jung's avatar
Ralf Jung committed
275
  (bi_exist (λ x, .. (bi_exist (λ y, P%I)) ..)) : bi_scope.
276
Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
277

278
Notation "▷ P" := (bi_later P) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
279

Gregory Malecha's avatar
Gregory Malecha committed
280
Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
281

Ralf Jung's avatar
Ralf Jung committed
282
Global Arguments bi_emp_valid {_} _%I : simpl never.
Ralf Jung's avatar
Ralf Jung committed
283
Typeclasses Opaque bi_emp_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
284

Gregory Malecha's avatar
Gregory Malecha committed
285
286
Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
Notation "'⊢@{' PROP } Q" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
287
288
289
290
(** Work around parsing issues: see [notation.v] for details. *)
Notation "'(⊢@{' PROP } Q )" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
Notation "(.⊢ Q )" := (λ P, P  Q) (only parsing) : stdpp_scope.
Notation "( P ⊢.)" := (bi_entails P) (only parsing) : stdpp_scope.
Gregory Malecha's avatar
Gregory Malecha committed
291

Robbert Krebbers's avatar
Robbert Krebbers committed
292
293
294
295
296
297
298
299
300
301
Module bi.
Section bi_laws.
Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
Implicit Types A : Type.

(* About the entailment *)
Global Instance entails_po : PreOrder (@bi_entails PROP).
Proof. eapply bi_mixin_entails_po, bi_bi_mixin. Qed.
302
303
Lemma equiv_entails P Q : P  Q  (P  Q)  (Q  P).
Proof. eapply bi_mixin_equiv_entails, bi_bi_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327

(* Non-expansiveness *)
Global Instance pure_ne n : Proper (iff ==> dist n) (@bi_pure PROP).
Proof. eapply bi_mixin_pure_ne, bi_bi_mixin. Qed.
Global Instance and_ne : NonExpansive2 (@bi_and PROP).
Proof. eapply bi_mixin_and_ne, bi_bi_mixin. Qed.
Global Instance or_ne : NonExpansive2 (@bi_or PROP).
Proof. eapply bi_mixin_or_ne, bi_bi_mixin. Qed.
Global Instance impl_ne : NonExpansive2 (@bi_impl PROP).
Proof. eapply bi_mixin_impl_ne, bi_bi_mixin. Qed.
Global Instance forall_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_forall PROP A).
Proof. eapply bi_mixin_forall_ne, bi_bi_mixin. Qed.
Global Instance exist_ne A n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_exist PROP A).
Proof. eapply bi_mixin_exist_ne, bi_bi_mixin. Qed.
Global Instance sep_ne : NonExpansive2 (@bi_sep PROP).
Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed.
Global Instance wand_ne : NonExpansive2 (@bi_wand PROP).
Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed.
Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed.

(* Higher-order logic *)
328
Lemma pure_intro (φ : Prop) P : φ  P   φ .
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
Lemma pure_elim' (φ : Prop) P : (φ  True  P)   φ   P.
Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.

Lemma and_elim_l P Q : P  Q  P.
Proof. eapply bi_mixin_and_elim_l, bi_bi_mixin. Qed.
Lemma and_elim_r P Q : P  Q  Q.
Proof. eapply bi_mixin_and_elim_r, bi_bi_mixin. Qed.
Lemma and_intro P Q R : (P  Q)  (P  R)  P  Q  R.
Proof. eapply bi_mixin_and_intro, bi_bi_mixin. Qed.

Lemma or_intro_l P Q : P  P  Q.
Proof. eapply bi_mixin_or_intro_l, bi_bi_mixin. Qed.
Lemma or_intro_r P Q : Q  P  Q.
Proof. eapply bi_mixin_or_intro_r, bi_bi_mixin. Qed.
Lemma or_elim P Q R : (P  R)  (Q  R)  P  Q  R.
Proof. eapply bi_mixin_or_elim, bi_bi_mixin. Qed.

Lemma impl_intro_r P Q R : (P  Q  R)  P  Q  R.
Proof. eapply bi_mixin_impl_intro_r, bi_bi_mixin. Qed.
Lemma impl_elim_l' P Q R : (P  Q  R)  P  Q  R.
Proof. eapply bi_mixin_impl_elim_l', bi_bi_mixin. Qed.

Lemma forall_intro {A} P (Ψ : A  PROP) : ( a, P  Ψ a)  P   a, Ψ a.
Proof. eapply bi_mixin_forall_intro, bi_bi_mixin. Qed.
Lemma forall_elim {A} {Ψ : A  PROP} a : ( a, Ψ a)  Ψ a.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
355
Proof. eapply (bi_mixin_forall_elim bi_entails), bi_bi_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
357
358
359
360
361
362
363
364
365
366
367
368
369

Lemma exist_intro {A} {Ψ : A  PROP} a : Ψ a   a, Ψ a.
Proof. eapply bi_mixin_exist_intro, bi_bi_mixin. Qed.
Lemma exist_elim {A} (Φ : A  PROP) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
Proof. eapply bi_mixin_exist_elim, bi_bi_mixin. Qed.

(* BI connectives *)
Lemma sep_mono P P' Q Q' : (P  Q)  (P'  Q')  P  P'  Q  Q'.
Proof. eapply bi_mixin_sep_mono, bi_bi_mixin. Qed.
Lemma emp_sep_1 P : P  emp  P.
Proof. eapply bi_mixin_emp_sep_1, bi_bi_mixin. Qed.
Lemma emp_sep_2 P : emp  P  P.
Proof. eapply bi_mixin_emp_sep_2, bi_bi_mixin. Qed.
Lemma sep_comm' P Q : P  Q  Q  P.
370
Proof. eapply (bi_mixin_sep_comm' bi_entails), bi_bi_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
371
372
373
374
375
376
377
378
Lemma sep_assoc' P Q R : (P  Q)  R  P  (Q  R).
Proof. eapply bi_mixin_sep_assoc', bi_bi_mixin. Qed.
Lemma wand_intro_r P Q R : (P  Q  R)  P  Q - R.
Proof. eapply bi_mixin_wand_intro_r, bi_bi_mixin. Qed.
Lemma wand_elim_l' P Q R : (P  Q - R)  P  Q  R.
Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.

(* Persistently *)
379
Lemma persistently_mono P Q : (P  Q)  <pers> P  <pers> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
380
Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
381
Lemma persistently_idemp_2 P : <pers> P  <pers> <pers> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.

384
Lemma persistently_emp_2 : emp @{PROP} <pers> emp.
385
Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
386

387
388
389
Lemma persistently_and_2 (P Q : PROP) :
  ((<pers> P)  (<pers> Q))  <pers> (P  Q).
Proof. eapply bi_mixin_persistently_and_2, bi_bi_mixin. Qed.
390
Lemma persistently_exist_1 {A} (Ψ : A  PROP) :
391
  <pers> ( a, Ψ a)   a, <pers> (Ψ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
392
393
Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.

394
Lemma persistently_absorbing P Q : <pers> P  Q  <pers> P.
395
Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
396
Lemma persistently_and_sep_elim P Q : <pers> P  Q  P  Q.
397
Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
398
399

(* Later *)
400
Global Instance later_ne : NonExpansive (@bi_later PROP).
401
Proof. eapply bi_mixin_later_ne, bi_bi_later_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
403

Lemma later_mono P Q : (P  Q)   P   Q.
404
Proof. eapply bi_mixin_later_mono, bi_bi_later_mixin. Qed.
405
Lemma later_intro P : P   P.
406
Proof. eapply bi_mixin_later_intro, bi_bi_later_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
408

Lemma later_forall_2 {A} (Φ : A  PROP) : ( a,  Φ a)    a, Φ a.
409
Proof. eapply bi_mixin_later_forall_2, bi_bi_later_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
411
Lemma later_exist_false {A} (Φ : A  PROP) :
  (  a, Φ a)   False  ( a,  Φ a).
412
Proof. eapply bi_mixin_later_exist_false, bi_bi_later_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
Lemma later_sep_1 P Q :  (P  Q)   P   Q.
414
Proof. eapply bi_mixin_later_sep_1, bi_bi_later_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
Lemma later_sep_2 P Q :  P   Q   (P  Q).
416
Proof. eapply bi_mixin_later_sep_2, bi_bi_later_mixin. Qed.
417
Lemma later_persistently_1 P :  <pers> P  <pers>  P.
418
Proof. eapply (bi_mixin_later_persistently_1 bi_entails), bi_bi_later_mixin. Qed.
419
Lemma later_persistently_2 P : <pers>  P   <pers> P.
420
Proof. eapply (bi_mixin_later_persistently_2 bi_entails), bi_bi_later_mixin. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422

Lemma later_false_em P :  P   False  ( False  P).
423
424
Proof. eapply bi_mixin_later_false_em, bi_bi_later_mixin. Qed.
End bi_laws.
Robbert Krebbers's avatar
Robbert Krebbers committed
425
End bi.