class_instances.v 27.3 KB
Newer Older
1
From iris.proofmode Require Export classes.
2
From iris.algebra Require Import gmap.
3
From iris.prelude Require Import gmultiset.
4
From iris.base_logic Require Import big_op.
5
Set Default Proof Using "Type".
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Import uPred.

Section classes.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.

(* FromAssumption *)
Global Instance from_assumption_exact p P : FromAssumption p P P.
Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
Global Instance from_assumption_always_l p P Q :
  FromAssumption p P Q  FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
Global Instance from_assumption_always_r P Q :
  FromAssumption true P Q  FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
21
Global Instance from_assumption_bupd p P Q :
22
  FromAssumption p P Q  FromAssumption p P (|==> Q)%I.
23
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
24
25
26
Global Instance from_assumption_forall {A} p (Φ : A  uPred M) Q x :
  FromAssumption p (Φ x) Q  FromAssumption p ( x, Φ x) Q.
Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
27
28

(* IntoPure *)
Ralf Jung's avatar
Ralf Jung committed
29
Global Instance into_pure_pure φ : @IntoPure M ⌜φ⌝ φ.
30
Proof. done. Qed.
31
Global Instance into_pure_eq {A : ofeT} (a b : A) :
32
33
  Timeless a  @IntoPure M (a  b) (a  b).
Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
34
35
Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
  @IntoPure M ( a) ( a).
36
37
Proof. by rewrite /IntoPure discrete_valid. Qed.

38
39
40
41
42
43
44
45
46
47
48
49
50
Global Instance into_pure_exist {X : Type} (Φ : X  uPred M) φ :
  ( x, @IntoPure M (Φ x) (φ x))  @IntoPure M ( x, Φ x) ( x, φ x).
Proof.
  rewrite /IntoPure=>Hx. apply exist_elim=>x. rewrite Hx.
  apply pure_elim'=>Hφ. apply pure_intro. eauto.
Qed.

Global Instance into_pure_forall {X : Type} (Φ : X  uPred M) φ :
  ( x, @IntoPure M (Φ x) (φ x))  @IntoPure M ( x, Φ x) ( x, φ x).
Proof.
  rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
Qed.

51
(* FromPure *)
Ralf Jung's avatar
Ralf Jung committed
52
Global Instance from_pure_pure φ : @FromPure M ⌜φ⌝ φ.
53
Proof. done. Qed.
54
Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
55
56
57
58
  @FromPure M (a  b) (a  b).
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply internal_eq_refl'.
Qed.
59
60
Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
  @FromPure M ( a) ( a).
61
62
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ?.
63
  rewrite -cmra_valid_intro //. auto with I.
64
Qed.
65
Global Instance from_pure_bupd P φ : FromPure P φ  FromPure (|==> P) φ.
66
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
67
68
69
70
71
72
73
74
75
76
77
78

(* IntoPersistentP *)
Global Instance into_persistentP_always_trans P Q :
  IntoPersistentP P Q  IntoPersistentP ( P) Q | 0.
Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
Global Instance into_persistentP_always P : IntoPersistentP ( P) P | 1.
Proof. done. Qed.
Global Instance into_persistentP_persistent P :
  PersistentP P  IntoPersistentP P P | 100.
Proof. done. Qed.

(* IntoLater *)
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
(* The class [IntoLaterN] has only two instances:

- The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [ProgIntoLaterN n P Q → IntoLaterN n P Q], where [ProgIntoLaterN]
  is identical to [IntoLaterN], but computationally is supposed to make
  progress, i.e. its instances should actually strip a later.

The point of using the auxilary class [ProgIntoLaterN] is to ensure that the
default instance is not applied deeply in the term, which may cause in too many
definitions being unfolded (see issue #55).

For binary connectives we have the following instances:

<<
ProgIntoLaterN n P P'       IntoLaterN n Q Q'
---------------------------------------------
ProgIntoLaterN n (P /\ Q) (P' /\ Q')


   ProgIntoLaterN n Q Q'
--------------------------------
IntoLaterN n (P /\ Q) (P /\ Q')
>>

That is, to make progress, a later _should_ be stripped on either the left- or
right-hand side of the binary connective. *)
Class ProgIntoLaterN (n : nat) (P Q : uPred M) :=
  prog_into_laterN : P  ^n Q.
Global Arguments prog_into_laterN _ _ _ {_}.

109
110
Global Instance into_laterN_default n P : IntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.
111
112
113
114
Global Instance into_laterN_progress P Q :
  ProgIntoLaterN n P Q  IntoLaterN n P Q.
Proof. done. Qed.

115
Global Instance into_laterN_later n P Q :
116
117
118
  IntoLaterN n P Q  ProgIntoLaterN (S n) ( P) Q.
Proof. by rewrite /IntoLaterN /ProgIntoLaterN=>->. Qed.
Global Instance into_laterN_laterN n P : ProgIntoLaterN n (^n P) P.
119
Proof. done. Qed.
120
Global Instance into_laterN_laterN_plus n m P Q :
121
122
  IntoLaterN m P Q  ProgIntoLaterN (n + m) (^n P) Q.
Proof. rewrite /IntoLaterN /ProgIntoLaterN=>->. by rewrite laterN_plus. Qed.
123

124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
  ProgIntoLaterN n P1 Q1  IntoLaterN n P2 Q2 
  IntoLaterN n (P1  P2) (Q1  Q2).
Proof. rewrite /ProgIntoLaterN /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
Global Instance into_laterN_and_r n P P2 Q2 :
  ProgIntoLaterN n P2 Q2  ProgIntoLaterN n (P  P2) (P  Q2).
Proof.
  rewrite /ProgIntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Qed.

Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
  ProgIntoLaterN n P1 Q1  IntoLaterN n P2 Q2 
  IntoLaterN n (P1  P2) (Q1  Q2).
Proof. rewrite /ProgIntoLaterN /IntoLaterN=> -> ->. by rewrite laterN_or. Qed.
Global Instance into_laterN_or_r n P P2 Q2 :
  ProgIntoLaterN n P2 Q2 
  ProgIntoLaterN n (P  P2) (P  Q2).
Proof.
  rewrite /ProgIntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
Qed.

Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
  ProgIntoLaterN n P1 Q1  IntoLaterN n P2 Q2 
  IntoLaterN n (P1  P2) (Q1  Q2).
148
Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
149
150
151
152
153
154
Global Instance into_laterN_sep_r n P P2 Q2 :
  ProgIntoLaterN n P2 Q2 
  ProgIntoLaterN n (P  P2) (P  Q2).
Proof.
  rewrite /ProgIntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
Qed.
155
156

Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat  A  uPred M) (l: list A) :
157
158
  ( x k, ProgIntoLaterN n (Φ k x) (Ψ k x)) 
  ProgIntoLaterN n ([ list] k  x  l, Φ k x) ([ list] k  x  l, Ψ k x).
159
Proof.
160
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepL_laterN. by apply big_sepL_mono.
161
162
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
163
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
164
165
  ( x k, ProgIntoLaterN n (Φ k x) (Ψ k x)) 
  ProgIntoLaterN n ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
166
Proof.
167
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepM_laterN; by apply big_sepM_mono.
168
Qed.
169
Global Instance into_laterN_big_sepS n `{Countable A}
170
    (Φ Ψ : A  uPred M) (X : gset A) :
171
172
  ( x, ProgIntoLaterN n (Φ x) (Ψ x)) 
  ProgIntoLaterN n ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
173
Proof.
174
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepS_laterN; by apply big_sepS_mono.
175
176
177
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
    (Φ Ψ : A  uPred M) (X : gmultiset A) :
178
179
  ( x, ProgIntoLaterN n (Φ x) (Ψ x)) 
  ProgIntoLaterN n ([ mset] x  X, Φ x) ([ mset] x  X, Ψ x).
180
Proof.
181
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepMS_laterN; by apply big_sepMS_mono.
182
183
184
Qed.

(* FromLater *)
185
Global Instance from_laterN_later P :FromLaterN 1 ( P) P | 0.
186
Proof. done. Qed.
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
Global Instance from_laterN_laterN n P : FromLaterN n (^n P) P | 0.
Proof. done. Qed.

(* The instances below are used when stripping a specific number of laters, or
to balance laters in different branches of ∧, ∨ and ∗. *)
Global Instance from_laterN_0 P : FromLaterN 0 P P | 100. (* fallthrough *)
Proof. done. Qed.
Global Instance from_laterN_later_S n P Q :
  FromLaterN n P Q  FromLaterN (S n) ( P) Q.
Proof. by rewrite /FromLaterN=><-. Qed.
Global Instance from_laterN_later_plus n m P Q :
  FromLaterN m P Q  FromLaterN (n + m) (^n P) Q.
Proof. rewrite /FromLaterN=><-. by rewrite laterN_plus. Qed.

Global Instance from_later_and n P1 P2 Q1 Q2 :
  FromLaterN n P1 Q1  FromLaterN n P2 Q2  FromLaterN n (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite laterN_and; apply and_mono. Qed.
Global Instance from_later_or n P1 P2 Q1 Q2 :
  FromLaterN n P1 Q1  FromLaterN n P2 Q2  FromLaterN n (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite laterN_or; apply or_mono. Qed.
Global Instance from_later_sep n P1 P2 Q1 Q2 :
  FromLaterN n P1 Q1  FromLaterN n P2 Q2  FromLaterN n (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
210
211

(* IntoWand *)
212
Global Instance into_wand_wand P Q Q' :
213
  FromAssumption false Q Q'  IntoWand (P - Q) P Q'.
214
215
216
217
Proof. by rewrite /FromAssumption /IntoWand /= => ->. Qed.
Global Instance into_wand_impl P Q Q' :
  FromAssumption false Q Q'  IntoWand (P  Q) P Q'.
Proof. rewrite /FromAssumption /IntoWand /= => ->. by rewrite impl_wand. Qed.
218
219
220
221
Global Instance into_wand_iff_l P Q : IntoWand (P  Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance into_wand_iff_r P Q : IntoWand (P  Q) Q P.
Proof. apply and_elim_r', impl_wand. Qed.
222

223
224
225
Global Instance into_wand_forall {A} (Φ : A  uPred M) P Q x :
  IntoWand (Φ x) P Q  IntoWand ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
226
227
Global Instance into_wand_always R P Q : IntoWand R P Q  IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
228

229
Global Instance into_wand_later (R1 R2 P Q : uPred M) :
230
231
232
233
  IntoLaterN 1 R1 R2  IntoWand R2 P Q  IntoWand' R1 ( P) ( Q) | 99.
Proof.
  rewrite /IntoLaterN /IntoWand' /IntoWand=> -> ->. by rewrite -later_wand.
Qed.
234
Global Instance into_wand_laterN n (R1 R2 P Q : uPred M) :
235
236
237
238
  IntoLaterN n R1 R2  IntoWand R2 P Q  IntoWand' R1 (^n P) (^n Q) | 100.
Proof.
  rewrite /IntoLaterN /IntoWand' /IntoWand=> -> ->. by rewrite -laterN_wand.
Qed.
239
Global Instance into_wand_bupd R P Q :
240
241
242
243
  IntoWand R P Q  IntoWand' R (|==> P) (|==> Q) | 98.
Proof.
  rewrite /IntoWand' /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_wand_r.
Qed.
244
245
246
247
248

(* FromAnd *)
Global Instance from_and_and P1 P2 : FromAnd (P1  P2) P1 P2.
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
249
  PersistentP P1  FromAnd (P1  P2) P1 P2 | 9.
250
251
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
252
  PersistentP P2  FromAnd (P1  P2) P1 P2 | 10.
253
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
254
255
Global Instance from_and_pure φ ψ : @FromAnd M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.
256
257
258
259
260
261
Global Instance from_and_always P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
Global Instance from_and_later P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
262
263
264
Global Instance from_and_laterN n P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromAnd=> <-. by rewrite laterN_and. Qed.
265
266

(* FromSep *)
267
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
268
Proof. done. Qed.
269
270
271
272
Global Instance from_sep_ownM (a b1 b2 : M) :
  FromOp a b1 b2 
  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromSep -ownM_op from_op. Qed.
273
274
Global Instance from_sep_pure φ ψ : @FromSep M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.
275
276
277
278
279
280
Global Instance from_sep_always P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
Global Instance from_sep_later P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
281
282
283
Global Instance from_sep_laterN n P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
284
Global Instance from_sep_bupd P Q1 Q2 :
285
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
286
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
287

288
289
290
291
292
Global Instance from_sep_big_sepL {A} (Φ Ψ1 Ψ2 : nat  A  uPred M) l :
  ( k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
  FromSep ([ list] k  x  l, Φ k x)
    ([ list] k  x  l, Ψ1 k x) ([ list] k  x  l, Ψ2 k x).
Proof. rewrite /FromSep=>?. rewrite -big_sepL_sepL. by apply big_sepL_mono. Qed.
293
294
295
Global Instance from_sep_big_sepM
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) m :
  ( k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
296
297
  FromSep ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
298
Proof. rewrite /FromSep=>?. rewrite -big_sepM_sepM. by apply big_sepM_mono. Qed.
299
300
Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) X :
  ( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) 
301
  FromSep ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
302
303
304
305
Proof. rewrite /FromSep=>?. rewrite -big_sepS_sepS. by apply big_sepS_mono. Qed.
Global Instance from_sep_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) X :
  ( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) 
  FromSep ([ mset] x  X, Φ x) ([ mset] x  X, Ψ1 x) ([ mset] x  X, Ψ2 x).
306
Proof.
307
  rewrite /FromSep=> ?. rewrite -big_sepMS_sepMS. by apply big_sepMS_mono.
308
309
Qed.

310
311
312
313
314
315
316
317
318
319
320
321
322
323
(* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a  b) a b.
Proof. by rewrite /FromOp. Qed.
Global Instance from_op_persistent {A : cmraT} (a : A) :
  Persistent a  FromOp a a a.
Proof. intros. by rewrite /FromOp -(persistent_dup a). Qed.
Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
  FromOp a b1 b2  FromOp a' b1' b2' 
  FromOp (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
Global Instance from_op_Some {A : cmraT} (a : A) b1 b2 :
  FromOp a b1 b2  FromOp (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.

324
325
326
327
328
329
330
331
332
333
334
335
336
337
(* IntoOp *)
Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a  b) a b.
Proof. by rewrite /IntoOp. Qed.
Global Instance into_op_persistent {A : cmraT} (a : A) :
  Persistent a  IntoOp a a a.
Proof. intros; apply (persistent_dup a). Qed.
Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
  IntoOp a b1 b2  IntoOp a' b1' b2' 
  IntoOp (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
  IntoOp a b1 b2  IntoOp (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.

338
(* IntoAnd *)
339
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
340
341
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
342
  IntoOp a b1 b2 
343
344
  IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) ownM_op. Qed.
345

346
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
347
Proof. done. Qed.
348
349
350
351
352
353
354
Global Instance into_and_and_persistent_l P Q :
  PersistentP P  IntoAnd false (P  Q) P Q.
Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed.
Global Instance into_and_and_persistent_r P Q :
  PersistentP Q  IntoAnd false (P  Q) P Q.
Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.

355
356
357
358
359
360
361
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_into_and_sep. by rewrite pure_and always_and_sep_r. Qed.
Global Instance into_and_always p P Q1 Q2 :
  IntoAnd true P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd=>->. destruct p; by rewrite ?always_and always_and_sep_r.
Qed.
362
363
364
Global Instance into_and_later p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?later_and ?later_sep. Qed.
365
366
367
Global Instance into_and_laterN n p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p (^n P) (^n Q1) (^n Q2).
Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?laterN_and ?laterN_sep. Qed.
368

369
370
371
372
373
374
375
376
377
Global Instance into_and_big_sepL {A} (Φ Ψ1 Ψ2 : nat  A  uPred M) p l :
  ( k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
  IntoAnd p ([ list] k  x  l, Φ k x)
    ([ list] k  x  l, Ψ1 k x) ([ list] k  x  l, Ψ2 k x).
Proof.
  rewrite /IntoAnd=> HΦ. destruct p.
  - rewrite -big_sepL_and. apply big_sepL_mono; auto.
  - rewrite -big_sepL_sepL. apply big_sepL_mono; auto.
Qed.
378
Global Instance into_and_big_sepM
379
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) p m :
380
  ( k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
381
382
  IntoAnd p ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
383
Proof.
384
  rewrite /IntoAnd=> HΦ. destruct p.
385
  - rewrite -big_sepM_and. apply big_sepM_mono; auto.
386
  - rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
387
Qed.
388
389
Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) p X :
  ( x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) 
390
  IntoAnd p ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
391
Proof.
392
  rewrite /IntoAnd=> HΦ. destruct p.
393
  - rewrite -big_sepS_and. apply big_sepS_mono; auto.
394
  - rewrite -big_sepS_sepS. apply big_sepS_mono; auto.
395
Qed.
396
397
398
399
400
401
402
403
Global Instance into_and_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) p X :
  ( x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) 
  IntoAnd p ([ mset] x  X, Φ x) ([ mset] x  X, Ψ1 x) ([ mset] x  X, Ψ2 x).
Proof.
  rewrite /IntoAnd=> HΦ. destruct p.
  - rewrite -big_sepMS_and. apply big_sepMS_mono; auto.
  - rewrite -big_sepMS_sepMS. apply big_sepMS_mono; auto.
Qed.
404
405
406
407

(* Frame *)
Global Instance frame_here R : Frame R R True.
Proof. by rewrite /Frame right_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
408
Global Instance frame_here_pure φ Q : FromPure Q φ  Frame ⌜φ⌝ Q True.
409
Proof. rewrite /FromPure /Frame=> ->. by rewrite right_id. Qed.
410

411
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
412
413
414
415
Global Instance make_sep_true_l P : MakeSep True P P.
Proof. by rewrite /MakeSep left_id. Qed.
Global Instance make_sep_true_r P : MakeSep P True P.
Proof. by rewrite /MakeSep right_id. Qed.
416
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
417
418
Proof. done. Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
419
  Frame R P1 Q  MakeSep Q P2 Q'  Frame R (P1  P2) Q' | 9.
420
421
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
Global Instance frame_sep_r R P1 P2 Q Q' :
422
  Frame R P2 Q  MakeSep P1 Q Q'  Frame R (P1  P2) Q' | 10.
423
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
424
425
426
427
428
429

Class MakeAnd (P Q PQ : uPred M) := make_and : P  Q  PQ.
Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed.
Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed.
430
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
Proof. done. Qed.
Global Instance frame_and_l R P1 P2 Q Q' :
  Frame R P1 Q  MakeAnd Q P2 Q'  Frame R (P1  P2) Q' | 9.
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
Global Instance frame_and_r R P1 P2 Q Q' :
  Frame R P2 Q  MakeAnd P1 Q Q'  Frame R (P1  P2) Q' | 10.
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.

Class MakeOr (P Q PQ : uPred M) := make_or : P  Q  PQ.
Global Instance make_or_true_l P : MakeOr True P True.
Proof. by rewrite /MakeOr left_absorb. Qed.
Global Instance make_or_true_r P : MakeOr P True True.
Proof. by rewrite /MakeOr right_absorb. Qed.
Global Instance make_or_default P Q : MakeOr P Q (P  Q) | 100.
Proof. done. Qed.
Global Instance frame_or R P1 P2 Q1 Q2 Q :
  Frame R P1 Q1  Frame R P2 Q2  MakeOr Q1 Q2 Q  Frame R (P1  P2) Q.
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

Global Instance frame_wand R P1 P2 Q2 :
451
  Frame R P2 Q2  Frame R (P1 - P2) (P1 - Q2).
452
453
454
455
456
457
458
459
460
461
462
Proof.
  rewrite /Frame=> ?. apply wand_intro_l.
  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.

Class MakeLater (P lP : uPred M) := make_later :  P  lP.
Global Instance make_later_true : MakeLater True True.
Proof. by rewrite /MakeLater later_True. Qed.
Global Instance make_later_default P : MakeLater P ( P) | 100.
Proof. done. Qed.

463
Global Instance frame_later R R' P Q Q' :
464
  IntoLaterN 1 R' R  Frame R P Q  MakeLater Q Q'  Frame R' ( P) Q'.
465
Proof.
466
467
468
469
470
471
472
473
474
475
476
477
478
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite later_sep.
Qed.

Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ^n P  lP.
Global Instance make_laterN_true n : MakeLaterN n True True.
Proof. by rewrite /MakeLaterN laterN_True. Qed.
Global Instance make_laterN_default P : MakeLaterN n P (^n P) | 100.
Proof. done. Qed.

Global Instance frame_laterN n R R' P Q Q' :
  IntoLaterN n R' R  Frame R P Q  MakeLaterN n Q Q'  Frame R' (^n P) Q'.
Proof.
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite laterN_sep.
479
480
Qed.

481
482
483
484
Class MakeExcept0 (P Q : uPred M) := make_except_0 :  P  Q.
Global Instance make_except_0_True : MakeExcept0 True True.
Proof. by rewrite /MakeExcept0 except_0_True. Qed.
Global Instance make_except_0_default P : MakeExcept0 P ( P) | 100.
485
486
Proof. done. Qed.

487
488
Global Instance frame_except_0 R P Q Q' :
  Frame R P Q  MakeExcept0 Q Q'  Frame R ( P) Q'.
489
Proof.
490
491
  rewrite /Frame /MakeExcept0=><- <-.
  by rewrite except_0_sep -(except_0_intro R).
492
493
Qed.

494
495
496
497
498
499
500
Global Instance frame_exist {A} R (Φ Ψ : A  uPred M) :
  ( a, Frame R (Φ a) (Ψ a))  Frame R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
Global Instance frame_forall {A} R (Φ Ψ : A  uPred M) :
  ( a, Frame R (Φ a) (Ψ a))  Frame R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

501
Global Instance frame_bupd R P Q : Frame R P Q  Frame R (|==> P) (|==> Q).
502
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
503

504
505
506
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. done. Qed.
507
Global Instance from_or_bupd P Q1 Q2 :
508
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
509
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
510
511
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
512
513
514
Global Instance from_or_always P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
515
516
Global Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
517
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
518
519
520
Global Instance from_or_laterN n P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromOr=><-. by rewrite laterN_or. Qed.
521
522
523
524

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
525
526
527
528
529
Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoOr pure_or. Qed.
Global Instance into_or_always P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
530
531
532
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
533
534
535
Global Instance into_or_laterN n P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr (^n P) (^n Q1) (^n Q2).
Proof. rewrite /IntoOr=>->. by rewrite laterN_or. Qed.
536
537

(* FromExist *)
538
Global Instance from_exist_exist {A} (Φ : A  uPred M): FromExist ( a, Φ a) Φ.
539
Proof. done. Qed.
540
Global Instance from_exist_bupd {A} P (Φ : A  uPred M) :
541
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
542
543
544
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
545
546
547
548
549
550
551
552
Global Instance from_exist_pure {A} (φ : A  Prop) :
  @FromExist M A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
Global Instance from_exist_always {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply always_mono, exist_intro.
Qed.
553
554
Global Instance from_exist_later {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
555
556
557
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
Qed.
558
559
560
561
562
Global Instance from_exist_laterN {A} n P (Φ : A  uPred M) :
  FromExist P Φ  FromExist (^n P) (λ a, ^n (Φ a))%I.
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply laterN_mono, exist_intro.
Qed.
563
564
565
566

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  uPred M) : IntoExist ( a, Φ a) Φ.
Proof. done. Qed.
567
568
569
Global Instance into_exist_pure {A} (φ : A  Prop) :
  @IntoExist M A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
570
571
572
Global Instance into_exist_always {A} P (Φ : A  uPred M) :
  IntoExist P Φ  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
573
574
575
576
577
578
Global Instance into_exist_later {A} P (Φ : A  uPred M) :
  IntoExist P Φ  Inhabited A  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
Global Instance into_exist_laterN {A} n P (Φ : A  uPred M) :
  IntoExist P Φ  Inhabited A  IntoExist (^n P) (λ a, ^n (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
579

580
581
(* FromModal *)
Global Instance from_modal_later P : FromModal ( P) P.
582
Proof. apply later_intro. Qed.
583
Global Instance from_modal_bupd P : FromModal (|==> P) P.
584
Proof. apply bupd_intro. Qed.
585
Global Instance from_modal_except_0 P : FromModal ( P) P.
586
587
588
Proof. apply except_0_intro. Qed.

(* ElimModal *)
589
Global Instance elim_modal_wand P P' Q Q' R :
590
  ElimModal P P' Q Q'  ElimModal P P' (R - Q) (R - Q').
591
592
593
594
595
596
597
598
599
600
Proof.
  rewrite /ElimModal=> H. apply wand_intro_r.
  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
Qed.
Global Instance forall_modal_wand {A} P P' (Φ Ψ : A  uPred M) :
  ( x, ElimModal P P' (Φ x) (Ψ x))  ElimModal P P' ( x, Φ x) ( x, Ψ x).
Proof.
  rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
601
602
603
Global Instance elim_modal_always P Q : ElimModal ( P) P Q Q.
Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.

604
605
606
607
608
Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.

Global Instance elim_modal_except_0 P Q : IsExcept0 Q  ElimModal ( P) P Q Q.
Proof.
609
  intros. rewrite /ElimModal (except_0_intro (_ - _)).
610
611
612
613
614
  by rewrite -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_timeless_bupd P Q :
  TimelessP P  IsExcept0 Q  ElimModal ( P) P Q Q.
Proof.
615
  intros. rewrite /ElimModal (except_0_intro (_ - _)) (timelessP P).
616
617
  by rewrite -except_0_sep wand_elim_r.
Qed.
618
619
620
621
622
623
Global Instance elim_modal_timeless_bupd' p P Q :
  TimelessP P  IsExcept0 Q  ElimModal (?p P) P Q Q.
Proof.
  destruct p; simpl; auto using elim_modal_timeless_bupd.
  intros _ _. by rewrite /ElimModal wand_elim_r.
Qed.
624

625
626
627
628
629
Global Instance is_except_0_except_0 P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
Global Instance is_except_0_later P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_later. Qed.
Global Instance is_except_0_bupd P : IsExcept0 P  IsExcept0 (|==> P).
630
Proof.
631
632
  rewrite /IsExcept0=> HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
633
Qed.
634
End classes.
635
636

Hint Mode ProgIntoLaterN + - ! - : typeclass_instances.