class_instances.v 28.6 KB
Newer Older
1
From iris.proofmode Require Export classes.
2
From iris.algebra Require Import gmap.
Ralf Jung's avatar
Ralf Jung committed
3
From stdpp 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
26
Global Instance from_assumption_later p P Q :
  FromAssumption p P Q  FromAssumption p P ( Q)%I.
Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
Global Instance from_assumption_laterN n p P Q :
  FromAssumption p P Q  FromAssumption p P (^n Q)%I.
Proof. rewrite /FromAssumption=>->. apply laterN_intro. Qed.
27
Global Instance from_assumption_bupd p P Q :
28
  FromAssumption p P Q  FromAssumption p P (|==> Q)%I.
29
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
30
31
32
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.
33
34

(* IntoPure *)
Ralf Jung's avatar
Ralf Jung committed
35
Global Instance into_pure_pure φ : @IntoPure M ⌜φ⌝ φ.
36
Proof. done. Qed.
37
Global Instance into_pure_eq {A : ofeT} (a b : A) :
38
39
  Timeless a  @IntoPure M (a  b) (a  b).
Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
40
41
Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
  @IntoPure M ( a) ( a).
42
43
Proof. by rewrite /IntoPure discrete_valid. Qed.

44
45
46
47
48
49
50
51
52
53
54
55
56
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.

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

(* 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 *)
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
(* 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 _ _ _ {_}.

115
116
Global Instance into_laterN_default n P : IntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.
117
118
119
120
Global Instance into_laterN_progress P Q :
  ProgIntoLaterN n P Q  IntoLaterN n P Q.
Proof. done. Qed.

121
Global Instance into_laterN_later n P Q :
122
123
124
  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.
125
Proof. done. Qed.
126
Global Instance into_laterN_laterN_plus n m P Q :
127
128
  IntoLaterN m P Q  ProgIntoLaterN (n + m) (^n P) Q.
Proof. rewrite /IntoLaterN /ProgIntoLaterN=>->. by rewrite laterN_plus. Qed.
129

130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
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).
154
Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
155
156
157
158
159
160
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.
161
162

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

(* FromLater *)
191
Global Instance from_laterN_later P :FromLaterN 1 ( P) P | 0.
192
Proof. done. Qed.
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
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.
216
217

(* IntoWand *)
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
Global Instance wand_weaken_exact P Q : WandWeaken P Q P Q.
Proof. done. Qed.
Global Instance wand_weaken_later P Q P' Q' :
  WandWeaken P Q P' Q'  WandWeaken' P Q ( P') ( Q').
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -later_wand -later_intro.
Qed.
Global Instance wand_weaken_laterN n P Q P' Q' :
  WandWeaken P Q P' Q'  WandWeaken' P Q (^n P') (^n Q').
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -laterN_wand -laterN_intro.
Qed.
Global Instance bupd_weaken_laterN P Q P' Q' :
  WandWeaken P Q P' Q'  WandWeaken' P Q (|==> P') (|==> Q').
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->.
  apply wand_intro_l. by rewrite bupd_wand_r.
Qed.

Global Instance into_wand_wand P P' Q Q' :
  WandWeaken P Q P' Q'  IntoWand (P - Q) P' Q'.
Proof. done. Qed.
Global Instance into_wand_impl P P' Q Q' :
  WandWeaken P Q P' Q'  IntoWand (P  Q) P' Q'.
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand. Qed.

Global Instance into_wand_iff_l P P' Q Q' :
  WandWeaken P Q P' Q'  IntoWand (P  Q) P' Q'.
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand. Qed.
Global Instance into_wand_iff_r P P' Q Q' :
  WandWeaken Q P Q' P'  IntoWand (P  Q) Q' P'.
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
250

251
252
253
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.
254
255
Global Instance into_wand_always R P Q : IntoWand R P Q  IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
256

Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
259
260
261
262
Global Instance into_wand_later R P Q :
  IntoWand R P Q  IntoWand ( R) ( P) ( Q).
Proof. rewrite /IntoWand=> ->. by rewrite -later_wand. Qed.
Global Instance into_wand_laterN n R P Q :
  IntoWand R P Q  IntoWand (^n R) (^n P) (^n Q).
Proof. rewrite /IntoWand=> ->. by rewrite -laterN_wand. Qed.
263
Global Instance into_wand_bupd R P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
264
  IntoWand R P Q  IntoWand (|==> R) (|==> P) (|==> Q).
265
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
266
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
267
Qed.
268
269
270
271
272

(* 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 :
273
  PersistentP P1  FromAnd (P1  P2) P1 P2 | 9.
274
275
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
276
  PersistentP P2  FromAnd (P1  P2) P1 P2 | 10.
277
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
278
279
Global Instance from_and_pure φ ψ : @FromAnd M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.
280
281
282
283
284
285
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.
286
287
288
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.
289
290

(* FromSep *)
291
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
292
Proof. done. Qed.
293
294
295
296
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.
297
298
Global Instance from_sep_pure φ ψ : @FromSep M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.
299
300
301
302
303
304
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.
305
306
307
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.
308
Global Instance from_sep_bupd P Q1 Q2 :
309
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
310
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
311

312
313
314
315
316
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.
317
318
319
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)) 
320
321
  FromSep ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
322
Proof. rewrite /FromSep=>?. rewrite -big_sepM_sepM. by apply big_sepM_mono. Qed.
323
324
Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) X :
  ( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) 
325
  FromSep ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
326
327
328
329
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).
330
Proof.
331
  rewrite /FromSep=> ?. rewrite -big_sepMS_sepMS. by apply big_sepMS_mono.
332
333
Qed.

334
335
336
337
338
339
340
341
342
343
344
345
346
347
(* 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.

348
349
350
351
352
353
354
355
356
357
358
359
360
361
(* 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.

362
(* IntoAnd *)
363
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
364
365
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
366
  IntoOp a b1 b2 
367
368
  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.
369

370
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
371
Proof. done. Qed.
372
373
374
375
376
377
378
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.

379
380
381
382
383
384
385
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.
386
387
388
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.
389
390
391
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.
392

393
394
395
396
397
398
399
400
401
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.
402
Global Instance into_and_big_sepM
403
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) p m :
404
  ( k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
405
406
  IntoAnd p ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
407
Proof.
408
  rewrite /IntoAnd=> HΦ. destruct p.
409
  - rewrite -big_sepM_and. apply big_sepM_mono; auto.
410
  - rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
411
Qed.
412
413
Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) p X :
  ( x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) 
414
  IntoAnd p ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
415
Proof.
416
  rewrite /IntoAnd=> HΦ. destruct p.
417
  - rewrite -big_sepS_and. apply big_sepS_mono; auto.
418
  - rewrite -big_sepS_sepS. apply big_sepS_mono; auto.
419
Qed.
420
421
422
423
424
425
426
427
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.
428
429
430
431

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

435
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
436
437
438
439
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.
440
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
441
442
Proof. done. Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
443
  Frame R P1 Q  MakeSep Q P2 Q'  Frame R (P1  P2) Q' | 9.
444
445
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
Global Instance frame_sep_r R P1 P2 Q Q' :
446
  Frame R P2 Q  MakeSep P1 Q Q'  Frame R (P1  P2) Q' | 10.
447
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
448
449
450
451
452
453

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.
454
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
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 :
475
  Frame R P2 Q2  Frame R (P1 - P2) (P1 - Q2).
476
477
478
479
480
481
482
483
484
485
486
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.

487
Global Instance frame_later R R' P Q Q' :
488
  IntoLaterN 1 R' R  Frame R P Q  MakeLater Q Q'  Frame R' ( P) Q'.
489
Proof.
490
491
492
493
494
495
496
497
498
499
500
501
502
  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.
503
504
Qed.

505
506
507
508
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.
509
510
Proof. done. Qed.

511
512
Global Instance frame_except_0 R P Q Q' :
  Frame R P Q  MakeExcept0 Q Q'  Frame R ( P) Q'.
513
Proof.
514
515
  rewrite /Frame /MakeExcept0=><- <-.
  by rewrite except_0_sep -(except_0_intro R).
516
517
Qed.

518
519
520
521
522
523
524
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.

525
Global Instance frame_bupd R P Q : Frame R P Q  Frame R (|==> P) (|==> Q).
526
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
527

528
529
530
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. done. Qed.
531
Global Instance from_or_bupd P Q1 Q2 :
532
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
533
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
534
535
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
536
537
538
Global Instance from_or_always P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
539
540
Global Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
541
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
542
543
544
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.
545
546
547
548

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
549
550
551
552
553
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.
554
555
556
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
557
558
559
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.
560
561

(* FromExist *)
562
Global Instance from_exist_exist {A} (Φ : A  uPred M): FromExist ( a, Φ a) Φ.
563
Proof. done. Qed.
564
Global Instance from_exist_bupd {A} P (Φ : A  uPred M) :
565
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
566
567
568
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
569
570
571
572
573
574
575
576
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.
577
578
Global Instance from_exist_later {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
579
580
581
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
Qed.
582
583
584
585
586
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.
587
588
589
590

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  uPred M) : IntoExist ( a, Φ a) Φ.
Proof. done. Qed.
591
592
593
Global Instance into_exist_pure {A} (φ : A  Prop) :
  @IntoExist M A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
594
595
596
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.
597
598
599
600
601
602
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.
603

604
605
606
607
608
609
610
(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A  uPred M) : IntoForall ( a, Φ a) Φ.
Proof. done. Qed.
Global Instance into_forall_always {A} P (Φ : A  uPred M) :
  IntoForall P Φ  IntoForall ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.

611
612
(* FromModal *)
Global Instance from_modal_later P : FromModal ( P) P.
613
Proof. apply later_intro. Qed.
614
Global Instance from_modal_bupd P : FromModal (|==> P) P.
615
Proof. apply bupd_intro. Qed.
616
Global Instance from_modal_except_0 P : FromModal ( P) P.
617
618
619
Proof. apply except_0_intro. Qed.

(* ElimModal *)
620
Global Instance elim_modal_wand P P' Q Q' R :
621
  ElimModal P P' Q Q'  ElimModal P P' (R - Q) (R - Q').
622
623
624
625
626
627
628
629
630
631
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
632
633
634
Global Instance elim_modal_always P Q : ElimModal ( P) P Q Q.
Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.

635
636
637
638
639
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.
640
  intros. rewrite /ElimModal (except_0_intro (_ - _)).
641
642
643
644
645
  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.
646
  intros. rewrite /ElimModal (except_0_intro (_ - _)) (timelessP P).
647
648
  by rewrite -except_0_sep wand_elim_r.
Qed.
649
650
651
652
653
654
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.
655

656
657
658
659
660
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).
661
Proof.
662
663
  rewrite /IsExcept0=> HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
664
Qed.
665
End classes.
666
667

Hint Mode ProgIntoLaterN + - ! - : typeclass_instances.