class_instances.v 31.3 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
Import uPred.

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

(* FromAssumption *)
13
14
Global Instance from_assumption_False p P : FromAssumption p False P.
Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
15
16
17
18
19
20
21
22
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
23
24
25
26
27
28
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.
29
Global Instance from_assumption_bupd p P Q :
30
  FromAssumption p P Q  FromAssumption p P (|==> Q)%I.
31
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
32
33
34
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.
35
36

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

Ralf Jung's avatar
Ralf Jung committed
46
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
47
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
48
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
49
Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
50
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
51
Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
52
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
53
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
54
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
55
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
56
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
57
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
58
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
59
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
60
61
62
63
Proof.
  rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
Qed.

Ralf Jung's avatar
Ralf Jung committed
64
Global Instance into_pure_exist {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
65
66
67
68
69
70
  ( 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.

Ralf Jung's avatar
Ralf Jung committed
71
Global Instance into_pure_forall {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
72
73
74
75
76
  ( x, @IntoPure M (Φ x) (φ x))  @IntoPure M ( x, Φ x) ( x, φ x).
Proof.
  rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
Qed.

77
(* FromPure *)
Ralf Jung's avatar
Ralf Jung committed
78
Global Instance from_pure_pure φ : @FromPure M ⌜φ⌝ φ.
79
Proof. done. Qed.
80
Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
81
82
83
84
  @FromPure M (a  b) (a  b).
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply internal_eq_refl'.
Qed.
85
86
Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
  @FromPure M ( a) ( a).
87
88
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ?.
89
  rewrite -cmra_valid_intro //. auto with I.
90
Qed.
91
Global Instance from_pure_bupd P φ : FromPure P φ  FromPure (|==> P) φ.
92
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
93

Ralf Jung's avatar
Ralf Jung committed
94
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
95
  FromPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1  P2) (φ1  φ2).
96
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
97
98
Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  FromPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1  P2) (φ1  φ2).
99
Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
100
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
101
  FromPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1  P2) (φ1  φ2).
102
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
103
104
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1  P2) (φ1  φ2).
105
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
106
107
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 -> FromPure P2 φ2 -> FromPure (P1 - P2) (φ1  φ2).
108
109
110
111
Proof.
  rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
Qed.

Ralf Jung's avatar
Ralf Jung committed
112
Global Instance from_pure_exist {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
113
114
115
116
117
  ( x, @FromPure M (Φ x) (φ x))  @FromPure M ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. apply pure_elim'=>-[x ?]. rewrite -(exist_intro x).
  rewrite -Hx. apply pure_intro. done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
118
Global Instance from_pure_forall {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
119
120
121
122
123
124
  ( x, @FromPure M (Φ x) (φ x))  @FromPure M ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. apply forall_intro=>x. apply pure_elim'=>Hφ.
  rewrite -Hx. apply pure_intro. done.
Qed.

125
126
127
128
129
130
131
132
133
134
135
(* 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 *)
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
(* 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 _ _ _ {_}.

166
167
Global Instance into_laterN_default n P : IntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.
168
169
170
171
Global Instance into_laterN_progress P Q :
  ProgIntoLaterN n P Q  IntoLaterN n P Q.
Proof. done. Qed.

172
Global Instance into_laterN_later n P Q :
173
174
175
  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.
176
Proof. done. Qed.
177
Global Instance into_laterN_laterN_plus n m P Q :
178
179
  IntoLaterN m P Q  ProgIntoLaterN (n + m) (^n P) Q.
Proof. rewrite /IntoLaterN /ProgIntoLaterN=>->. by rewrite laterN_plus. Qed.
180

181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
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).
205
Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
206
207
208
209
210
211
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.
212
213

Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat  A  uPred M) (l: list A) :
214
215
  ( x k, ProgIntoLaterN n (Φ k x) (Ψ k x)) 
  ProgIntoLaterN n ([ list] k  x  l, Φ k x) ([ list] k  x  l, Ψ k x).
216
Proof.
217
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepL_laterN. by apply big_sepL_mono.
218
219
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
220
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
221
222
  ( x k, ProgIntoLaterN n (Φ k x) (Ψ k x)) 
  ProgIntoLaterN n ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
223
Proof.
224
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepM_laterN; by apply big_sepM_mono.
225
Qed.
226
Global Instance into_laterN_big_sepS n `{Countable A}
227
    (Φ Ψ : A  uPred M) (X : gset A) :
228
229
  ( x, ProgIntoLaterN n (Φ x) (Ψ x)) 
  ProgIntoLaterN n ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
230
Proof.
231
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepS_laterN; by apply big_sepS_mono.
232
233
234
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
    (Φ Ψ : A  uPred M) (X : gmultiset A) :
235
236
  ( x, ProgIntoLaterN n (Φ x) (Ψ x)) 
  ProgIntoLaterN n ([ mset] x  X, Φ x) ([ mset] x  X, Ψ x).
237
Proof.
238
  rewrite /ProgIntoLaterN=> ?. rewrite big_sepMS_laterN; by apply big_sepMS_mono.
239
240
241
Qed.

(* FromLater *)
242
Global Instance from_laterN_later P :FromLaterN 1 ( P) P | 0.
243
Proof. done. Qed.
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
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.
267
268

(* IntoWand *)
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
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.
301

302
303
304
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.
305
306
Global Instance into_wand_always R P Q : IntoWand R P Q  IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
307

Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
310
311
312
313
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.
314
Global Instance into_wand_bupd R P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
315
  IntoWand R P Q  IntoWand (|==> R) (|==> P) (|==> Q).
316
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
318
Qed.
319
320
321
322
323

(* 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 :
324
  PersistentP P1  FromAnd (P1  P2) P1 P2 | 9.
325
326
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
327
  PersistentP P2  FromAnd (P1  P2) P1 P2 | 10.
328
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
329
330
Global Instance from_and_pure φ ψ : @FromAnd M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.
331
332
333
334
335
336
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.
337
338
339
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.
340
341

(* FromSep *)
342
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
343
Proof. done. Qed.
344
345
346
347
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.
348
349
Global Instance from_sep_pure φ ψ : @FromSep M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.
350
351
352
353
354
355
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.
356
357
358
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.
359
Global Instance from_sep_bupd P Q1 Q2 :
360
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
361
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
362

363
364
365
366
367
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.
368
369
370
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)) 
371
372
  FromSep ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
373
Proof. rewrite /FromSep=>?. rewrite -big_sepM_sepM. by apply big_sepM_mono. Qed.
374
375
Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) X :
  ( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) 
376
  FromSep ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
377
378
379
380
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).
381
Proof.
382
  rewrite /FromSep=> ?. rewrite -big_sepMS_sepMS. by apply big_sepMS_mono.
383
384
Qed.

385
386
387
388
389
390
391
392
393
394
395
396
397
398
(* 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.

399
400
401
402
403
404
405
406
407
408
409
410
411
412
(* 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.

413
(* IntoAnd *)
414
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
415
416
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
417
  IntoOp a b1 b2 
418
419
  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.
420

421
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
422
Proof. done. Qed.
423
424
425
426
427
428
429
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.

430
431
432
433
434
435
436
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.
437
438
439
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.
440
441
442
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.
443

444
445
446
447
448
449
450
451
452
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.
453
Global Instance into_and_big_sepM
454
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) p m :
455
  ( k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
456
457
  IntoAnd p ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
458
Proof.
459
  rewrite /IntoAnd=> HΦ. destruct p.
460
  - rewrite -big_sepM_and. apply big_sepM_mono; auto.
461
  - rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
462
Qed.
463
464
Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) p X :
  ( x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) 
465
  IntoAnd p ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
466
Proof.
467
  rewrite /IntoAnd=> HΦ. destruct p.
468
  - rewrite -big_sepS_and. apply big_sepS_mono; auto.
469
  - rewrite -big_sepS_sepS. apply big_sepS_mono; auto.
470
Qed.
471
472
473
474
475
476
477
478
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.
479
480
481
482

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

486
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
487
488
489
490
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.
491
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
492
493
Proof. done. Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
494
  Frame R P1 Q  MakeSep Q P2 Q'  Frame R (P1  P2) Q' | 9.
495
496
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
Global Instance frame_sep_r R P1 P2 Q Q' :
497
  Frame R P2 Q  MakeSep P1 Q Q'  Frame R (P1  P2) Q' | 10.
498
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
499
500
501
502
503
504

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.
505
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
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 :
526
  Frame R P2 Q2  Frame R (P1 - P2) (P1 - Q2).
527
528
529
530
531
532
533
534
535
536
537
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.

538
Global Instance frame_later R R' P Q Q' :
539
  IntoLaterN 1 R' R  Frame R P Q  MakeLater Q Q'  Frame R' ( P) Q'.
540
Proof.
541
542
543
544
545
546
547
548
549
550
551
552
553
  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.
554
555
Qed.

556
557
558
559
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.
560
561
Proof. done. Qed.

562
563
Global Instance frame_except_0 R P Q Q' :
  Frame R P Q  MakeExcept0 Q Q'  Frame R ( P) Q'.
564
Proof.
565
566
  rewrite /Frame /MakeExcept0=><- <-.
  by rewrite except_0_sep -(except_0_intro R).
567
568
Qed.

569
570
571
572
573
574
575
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.

576
Global Instance frame_bupd R P Q : Frame R P Q  Frame R (|==> P) (|==> Q).
577
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
578

579
580
581
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. done. Qed.
582
Global Instance from_or_bupd P Q1 Q2 :
583
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
584
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
585
586
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
587
588
589
Global Instance from_or_always P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
590
591
Global Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
592
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
593
594
595
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.
596
597
598
599

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
600
601
602
603
604
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.
605
606
607
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
608
609
610
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.
611
612

(* FromExist *)
613
Global Instance from_exist_exist {A} (Φ : A  uPred M): FromExist ( a, Φ a) Φ.
614
Proof. done. Qed.
615
Global Instance from_exist_bupd {A} P (Φ : A  uPred M) :
616
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
617
618
619
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
620
621
622
623
624
625
626
627
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.
628
629
Global Instance from_exist_later {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
630
631
632
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
Qed.
633
634
635
636
637
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.
638
639
640
641

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  uPred M) : IntoExist ( a, Φ a) Φ.
Proof. done. Qed.
642
643
644
Global Instance into_exist_pure {A} (φ : A  Prop) :
  @IntoExist M A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
645
646
647
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.
648
649
650
651
652
653
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.
654

655
656
657
658
659
660
661
(* 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.

662
663
(* FromModal *)
Global Instance from_modal_later P : FromModal ( P) P.
664
Proof. apply later_intro. Qed.
665
Global Instance from_modal_bupd P : FromModal (|==> P) P.
666
Proof. apply bupd_intro. Qed.
667
Global Instance from_modal_except_0 P : FromModal ( P) P.
668
669
670
Proof. apply except_0_intro. Qed.

(* ElimModal *)
671
Global Instance elim_modal_wand P P' Q Q' R :
672
  ElimModal P P' Q Q'  ElimModal P P' (R - Q) (R - Q').
673
674
675
676
677
678
679
680
681
682
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
683
684
685
Global Instance elim_modal_always P Q : ElimModal ( P) P Q Q.
Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.

686
687
688
689
690
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.
691
  intros. rewrite /ElimModal (except_0_intro (_ - _)).
692
693
694
695
696
  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.
697
  intros. rewrite /ElimModal (except_0_intro (_ - _)) (timelessP P).
698
699
  by rewrite -except_0_sep wand_elim_r.
Qed.
700
701
702
703
704
705
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.
706

707
708
709
710
711
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).
712
Proof.
713
714
  rewrite /IsExcept0=> HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
715
Qed.
716
End classes.
717
718

Hint Mode ProgIntoLaterN + - ! - : typeclass_instances.