class_instances.v 43.4 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 tactics.
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
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
14
Proof. destruct p; by rewrite /FromAssumption /= ?persistently_elim. Qed.
15
Global Instance from_assumption_False p P : FromAssumption p False P | 1.
16
Proof. destruct p; rewrite /FromAssumption /= ?persistently_pure; apply False_elim. Qed.
17

18
Global Instance from_assumption_persistently_r P Q :
19
  FromAssumption true P Q  FromAssumption true P ( Q).
20
Proof. rewrite /FromAssumption=><-. by rewrite persistent_persistently. Qed.
21

22
23
24
Global Instance from_assumption_plainly_l p P Q :
  FromAssumption p P Q  FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite plainly_elim. Qed.
25
Global Instance from_assumption_persistently_l p P Q :
26
  FromAssumption p P Q  FromAssumption p ( P) Q.
27
Proof. rewrite /FromAssumption=><-. by rewrite persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
29
30
31
32
33
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.
34
35
36
Global Instance from_assumption_except_0 p P Q :
  FromAssumption p P Q  FromAssumption p P ( Q)%I.
Proof. rewrite /FromAssumption=>->. apply except_0_intro. Qed.
37
Global Instance from_assumption_bupd p P Q :
38
  FromAssumption p P Q  FromAssumption p P (|==> Q)%I.
39
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
40
41
42
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.
43
44

(* IntoPure *)
Ralf Jung's avatar
Ralf Jung committed
45
Global Instance into_pure_pure φ : @IntoPure M ⌜φ⌝ φ.
46
Proof. done. Qed.
47
Global Instance into_pure_eq {A : ofeT} (a b : A) :
48
49
  Discrete a  @IntoPure M (a  b) (a  b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
50
Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
51
  @IntoPure M ( a) ( a).
52
53
Proof. by rewrite /IntoPure discrete_valid. Qed.

54
55
Global Instance into_pure_plainly P φ : IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite plainly_pure. Qed.
56
57
Global Instance into_pure_persistently P φ : IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite persistently_pure. Qed.
58

Ralf Jung's avatar
Ralf Jung committed
59
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
60
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
61
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
62
Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
63
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
64
Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
65
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
66
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
67
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
68
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
69
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
70
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
71
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
72
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
73
Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
74

Ralf Jung's avatar
Ralf Jung committed
75
Global Instance into_pure_exist {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
76
77
78
79
80
81
  ( 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
82
Global Instance into_pure_forall {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
83
84
85
86
87
  ( x, @IntoPure M (Φ x) (φ x))  @IntoPure M ( x, Φ x) ( x, φ x).
Proof.
  rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
Qed.

88
(* FromPure *)
Ralf Jung's avatar
Ralf Jung committed
89
Global Instance from_pure_pure φ : @FromPure M ⌜φ⌝ φ.
90
Proof. done. Qed.
91
Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
92
93
94
95
  @FromPure M (a  b) (a  b).
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply internal_eq_refl'.
Qed.
96
97
Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
  @FromPure M ( a) ( a).
98
99
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ?.
100
  rewrite -cmra_valid_intro //. auto with I.
101
Qed.
102

103
104
Global Instance from_pure_plainly P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
105
106
Global Instance from_pure_persistently P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
107
108
109
110
111
112
Global Instance from_pure_later P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
Global Instance from_pure_laterN n P φ : FromPure P φ  FromPure (^n P) φ.
Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
Global Instance from_pure_except_0 P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
113
Global Instance from_pure_bupd P φ : FromPure P φ  FromPure (|==> P) φ.
114
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
115

Ralf Jung's avatar
Ralf Jung committed
116
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
117
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
118
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
119
Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
120
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
121
Proof. rewrite /FromPure pure_and and_sep_l. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
122
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
123
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
124
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
125
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
126
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
127
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
128
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
129
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1 - P2) (φ1  φ2).
130
Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
131

Ralf Jung's avatar
Ralf Jung committed
132
Global Instance from_pure_exist {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
133
134
135
136
137
  ( 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
138
Global Instance from_pure_forall {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
139
140
141
142
143
144
  ( 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.

145
146
147
148
149
150
151
152
(* IntoInternalEq *)
Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
  @IntoInternalEq PROP A (x  y) x y.
Proof. by rewrite /IntoInternalEq. Qed.
Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
  IntoInternalEq P x y  IntoInternalEq ( P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.

153
(* IntoPersistent *)
154
Global Instance into_persistent_persistently_trans p P Q :
155
  IntoPersistent true P Q  IntoPersistent p ( P) Q | 0.
156
Proof. rewrite /IntoPersistent /==> ->. by rewrite persistent_persistently_if. Qed.
157
Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
158
Proof. done. Qed.
159
160
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
161
162
Proof. done. Qed.

163
164
165
166
167
168
(* FromAlways *)
Global Instance from_always_persistently P : FromAlways false ( P) P.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_plainly P : FromAlways true ( P) P.
Proof. by rewrite /FromAlways. Qed.

169
(* IntoLater *)
170
Global Instance into_laterN_later n P Q :
171
  IntoLaterN n P Q  IntoLaterN' (S n) ( P) Q | 0.
172
Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
Global Instance into_laterN_later_further n P Q :
174
  IntoLaterN' n P Q  IntoLaterN' n ( P) ( Q) | 1000.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
Proof. rewrite /IntoLaterN' /IntoLaterN =>->. by rewrite -laterN_later. Qed.

177
Global Instance into_laterN_laterN n P : IntoLaterN' n (^n P) P | 0.
178
Proof. done. Qed.
179
Global Instance into_laterN_laterN_plus n m P Q :
180
  IntoLaterN m P Q  IntoLaterN' (n + m) (^n P) Q | 1.
181
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Global Instance into_laterN_laterN_further n m P Q :
183
  IntoLaterN' m P Q  IntoLaterN' m (^n P) (^n Q) | 1000.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
186
Proof.
  rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite -!laterN_plus Nat.add_comm.
Qed.
187

188
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
189
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
191
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
192
Global Instance into_laterN_and_r n P P2 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
193
  IntoLaterN' n P2 Q2  IntoLaterN' n (P  P2) (P  Q2) | 11.
194
Proof.
195
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
196
Qed.
197

Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
201
202
203
204
205
Global Instance into_later_forall {A} n (Φ Ψ : A  uPred M) :
  ( x, IntoLaterN' n (Φ x) (Ψ x))  IntoLaterN' n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN' /IntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
Global Instance into_later_exist {A} n (Φ Ψ : A  uPred M) :
  ( x, IntoLaterN' n (Φ x) (Ψ x)) 
  IntoLaterN' n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.

206
Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
207
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
208
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
209
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_or. Qed.
210
Global Instance into_laterN_or_r n P P2 Q2 :
211
  IntoLaterN' n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  IntoLaterN' n (P  P2) (P  Q2) | 11.
213
Proof.
214
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
215
216
217
Qed.

Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
218
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
221
Global Instance into_laterN_sep_r n P P2 Q2 :
222
  IntoLaterN' n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
223
  IntoLaterN' n (P  P2) (P  Q2) | 11.
224
Proof.
225
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
226
Qed.
227
228

Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat  A  uPred M) (l: list A) :
229
230
  ( x k, IntoLaterN' n (Φ k x) (Ψ k x)) 
  IntoLaterN' n ([ list] k  x  l, Φ k x) ([ list] k  x  l, Ψ k x).
231
Proof.
232
  rewrite /IntoLaterN' /IntoLaterN=> ?.
233
  rewrite big_opL_commute. by apply big_sepL_mono.
234
235
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
236
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
237
238
  ( x k, IntoLaterN' n (Φ k x) (Ψ k x)) 
  IntoLaterN' n ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
239
Proof.
240
  rewrite /IntoLaterN' /IntoLaterN=> ?.
241
  rewrite big_opM_commute; by apply big_sepM_mono.
242
Qed.
243
Global Instance into_laterN_big_sepS n `{Countable A}
244
    (Φ Ψ : A  uPred M) (X : gset A) :
245
246
  ( x, IntoLaterN' n (Φ x) (Ψ x)) 
  IntoLaterN' n ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
247
Proof.
248
  rewrite /IntoLaterN' /IntoLaterN=> ?.
249
  rewrite big_opS_commute; by apply big_sepS_mono.
250
251
252
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
    (Φ Ψ : A  uPred M) (X : gmultiset A) :
253
254
  ( x, IntoLaterN' n (Φ x) (Ψ x)) 
  IntoLaterN' n ([ mset] x  X, Φ x) ([ mset] x  X, Ψ x).
255
Proof.
256
  rewrite /IntoLaterN' /IntoLaterN=> ?.
257
  rewrite big_opMS_commute; by apply big_sepMS_mono.
258
259
260
Qed.

(* FromLater *)
261
Global Instance from_laterN_later P : FromLaterN 1 ( P) P | 0.
262
Proof. done. Qed.
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
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.
286

287
288
289
Global Instance from_later_plainly n P Q :
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
Proof. by rewrite /FromLaterN -plainly_laterN=> ->. Qed.
290
Global Instance from_later_persistently n P Q :
291
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
292
Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
293
294
295
296
297
298
299
300
301

Global Instance from_later_forall {A} n (Φ Ψ : A  uPred M) :
  ( x, FromLaterN n (Φ x) (Ψ x))  FromLaterN n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /FromLaterN laterN_forall=> ?. by apply forall_mono. Qed.
Global Instance from_later_exist {A} n (Φ Ψ : A  uPred M) :
  Inhabited A  ( x, FromLaterN n (Φ x) (Ψ x)) 
  FromLaterN n ( x, Φ x) ( x, Ψ x).
Proof. intros ?. rewrite /FromLaterN laterN_exist=> ?. by apply exist_mono. Qed.

302
(* IntoWand *)
303
304
Global Instance wand_weaken_assumption p P1 P2 Q :
  FromAssumption p P2 P1  WandWeaken p P1 Q P2 Q | 0.
305
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
306
307
Global Instance wand_weaken_later p P Q P' Q' :
  WandWeaken p P Q P' Q'  WandWeaken' p P Q ( P') ( Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Proof.
309
  rewrite /WandWeaken' /WandWeaken=> ->.
310
  by rewrite persistently_if_later -later_wand -later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
Qed.
312
313
Global Instance wand_weaken_laterN p n P Q P' Q' :
  WandWeaken p P Q P' Q'  WandWeaken' p P Q (^n P') (^n Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Proof.
315
  rewrite /WandWeaken' /WandWeaken=> ->.
316
  by rewrite persistently_if_laterN -laterN_wand -laterN_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
Qed.
318
319
Global Instance bupd_weaken_laterN p P Q P' Q' :
  WandWeaken false P Q P' Q'  WandWeaken' p P Q (|==> P') (|==> Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->.
322
  apply wand_intro_l. by rewrite persistently_if_elim bupd_wand_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
324
Qed.

325
326
Global Instance into_wand_wand p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P - Q) P' Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Proof. done. Qed.
328
329
Global Instance into_wand_impl p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
330
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
331

332
333
Global Instance into_wand_iff_l p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
334
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand_1. Qed.
335
336
Global Instance into_wand_iff_r p P P' Q Q' :
  WandWeaken p Q P Q' P'  IntoWand p (P  Q) Q' P'.
337
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
338

Robbert Krebbers's avatar
Robbert Krebbers committed
339
340
341
342
343
344
345
Global Instance into_wand_forall_prop p (φ : Prop) P :
  IntoWand p ( _ : φ, P)  φ  P.
Proof.
  rewrite /FromAssumption /IntoWand persistently_if_pure -pure_impl_forall.
  by apply impl_wand_1.
Qed.

346
347
Global Instance into_wand_forall {A} p (Φ : A  uPred M) P Q x :
  IntoWand p (Φ x) P Q  IntoWand p ( x, Φ x) P Q.
348
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
349
350
351
Global Instance into_wand_plainly p R P Q :
  IntoWand p R P Q  IntoWand p ( R) P Q.
Proof. rewrite /IntoWand=> ->. by rewrite plainly_elim. Qed.
352
Global Instance into_wand_persistently p R P Q :
353
  IntoWand p R P Q  IntoWand p ( R) P Q.
354
Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
355

356
357
Global Instance into_wand_later p R P Q :
  IntoWand p R P Q  IntoWand p ( R) ( P) ( Q).
358
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_later -later_wand. Qed.
359
360
Global Instance into_wand_laterN p n R P Q :
  IntoWand p R P Q  IntoWand p (^n R) (^n P) (^n Q).
361
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_laterN -laterN_wand. Qed.
362

363
Global Instance into_wand_bupd R P Q :
364
  IntoWand false R P Q  IntoWand false (|==> R) (|==> P) (|==> Q).
365
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
367
Qed.
368
369
370
371
372
Global Instance into_wand_bupd_persistent R P Q :
  IntoWand true R P Q  IntoWand true (|==> R) P (|==> Q).
Proof.
  rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.
373
374

(* FromAnd *)
375
376
377
378
Global Instance from_and_and p P1 P2 : FromAnd p (P1  P2) P1 P2 | 100.
Proof. by apply mk_from_and_and. Qed.

Global Instance from_and_sep P1 P2 : FromAnd false (P1  P2) P1 P2 | 100.
379
380
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
381
  Persistent P1  FromAnd true (P1  P2) P1 P2 | 9.
382
Proof. intros. by rewrite /FromAnd and_sep_l. Qed.
383
Global Instance from_and_sep_persistent_r P1 P2 :
384
  Persistent P2  FromAnd true (P1  P2) P1 P2 | 10.
385
Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
386
387
388

Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
389
390
391
392
393
394
Global Instance from_and_plainly p P Q1 Q2 :
  FromAnd false P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof.
  intros. apply mk_from_and_and.
  by rewrite plainly_and_sep_l' -plainly_sep -(from_and _ P).
Qed.
395
Global Instance from_and_persistently p P Q1 Q2 :
396
397
398
  FromAnd false P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof.
  intros. apply mk_from_and_and.
399
  by rewrite persistently_and_sep_l -persistently_sep -(from_and _ P).
400
401
402
403
404
405
406
Qed.
Global Instance from_and_later p P Q1 Q2 :
  FromAnd p P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. destruct p; by rewrite ?later_and ?later_sep. Qed.
Global Instance from_and_laterN p n P Q1 Q2 :
  FromAnd p P Q1 Q2  FromAnd p (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromAnd=> <-. destruct p; by rewrite ?laterN_and ?laterN_sep. Qed.
407
408
409
410
411
Global Instance from_and_except_0 p P Q1 Q2 :
  FromAnd p P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /FromAnd=><-. by destruct p; rewrite ?except_0_and ?except_0_sep.
Qed.
412

413
Global Instance from_sep_ownM (a b1 b2 : M) :
414
  IsOp a b1 b2 
415
  FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
416
Proof. intros. by rewrite /FromAnd -ownM_op -is_op. Qed.
417
Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
418
  IsOp a b1 b2  Or (CoreId b1) (CoreId b2) 
419
420
421
  FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
  intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
422
  by rewrite -ownM_op -is_op.
423
Qed.
424

425
Global Instance from_sep_bupd P Q1 Q2 :
426
427
428
  FromAnd false P Q1 Q2  FromAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.

429
430
431
432
Global Instance from_and_big_sepL_cons {A} (Φ : nat  A  uPred M) x l :
  FromAnd false ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
Proof. by rewrite /FromAnd big_sepL_cons. Qed.
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat  A  uPred M) x l :
433
  Persistent (Φ 0 x) 
434
  FromAnd true ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
435
Proof. intros. by rewrite /FromAnd big_opL_cons and_sep_l. Qed.
436

437
438
Global Instance from_and_big_sepL_app {A} (Φ : nat  A  uPred M) l1 l2 :
  FromAnd false ([ list] k  y  l1 ++ l2, Φ k y)
439
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
440
Proof. by rewrite /FromAnd big_opL_app. Qed.
441
Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat  A  uPred M) l1 l2 :
442
  ( k y, Persistent (Φ k y)) 
443
444
  FromAnd true ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
445
Proof. intros. by rewrite /FromAnd big_opL_app and_sep_l. Qed.
446

447
(* FromOp *)
448
449
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
450
Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
451
  IsOp a b1 b2  IsOp a' b1' b2'  IsOp' (a,a') (b1,b1') (b2,b2').
452
Proof. by constructor. Qed.
453
Global Instance is_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
454
455
  CoreId a  IsOp a' b1' b2'  IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
456
Global Instance is_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
457
458
  CoreId a'  IsOp a b1 b2  IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
459

460
461
Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
  IsOp a b1 b2  IsOp' (Some a) (Some b1) (Some b2).
462
Proof. by constructor. Qed.
463
464
465
466
(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
an [⋅]. *)
Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
467

468
(* IntoAnd *)
469
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
470
471
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
472
473
  IsOp a b1 b2  IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) ownM_op. Qed.
474

475
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
476
Proof. done. Qed.
477
Global Instance into_and_and_persistent_l P Q :
478
  Persistent P  IntoAnd false (P  Q) P Q.
479
Proof. intros; by rewrite /IntoAnd /= and_sep_l. Qed.
480
Global Instance into_and_and_persistent_r P Q :
481
  Persistent Q  IntoAnd false (P  Q) P Q.
482
Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
483

484
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
485
Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
486
487
488
Global Instance into_and_plainly p P Q1 Q2 :
  IntoAnd true P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?plainly_and and_sep_r. Qed.
489
Global Instance into_and_persistently p P Q1 Q2 :
490
491
  IntoAnd true P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
492
493
  rewrite /IntoAnd=>->.
  destruct p; by rewrite ?persistently_and persistently_and_sep_r.
494
Qed.
495
496
497
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.
498
499
500
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.
501
502
503
504
505
Global Instance into_and_except_0 p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd=>->. by destruct p; rewrite ?except_0_and ?except_0_sep.
Qed.
506

507
508
509
510
511
512
513
514
(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
[frame_big_sepL_app] cannot be applied repeatedly often when having
[ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
Global Instance into_and_big_sepL_cons {A} p (Φ : nat  A  uPred M) l x l' :
  IsCons l x l' 
  IntoAnd p ([ list] k  y  l, Φ k y)
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Proof. rewrite /IsCons=>->. apply mk_into_and_sep. by rewrite big_sepL_cons. Qed.
515
516
517
Global Instance into_and_big_sepL_app {A} p (Φ : nat  A  uPred M) l l1 l2 :
  IsApp l l1 l2 
  IntoAnd p ([ list] k  y  l, Φ k y)
518
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
519
Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
520
521

(* Frame *)
522
Global Instance frame_here p R : Frame p R R True.
523
Proof. by rewrite /Frame right_id persistently_if_elim. Qed.
524
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
525
Proof. rewrite /FromPure /Frame=> ->. by rewrite persistently_if_elim right_id. Qed.
526

527
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
528
529
530
531
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.
532
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
533
Proof. done. Qed.
534

535
536
Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
  Frame true R P1 Q1  MaybeFrame true R P2 Q2 progress  MakeSep Q1 Q2 Q' 
537
538
539
  Frame true R (P1  P2) Q' | 9.
Proof.
  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
540
  rewrite {1}(sep_dup ( R)). solve_sep_entails.
541
Qed.
542
Global Instance frame_sep_l R P1 P2 Q Q' :
543
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
544
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
545
546
547
Global Instance frame_sep_r p R P1 P2 Q Q' :
  Frame p R P2 Q  MakeSep P1 Q Q'  Frame p R (P1  P2) Q' | 10.
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc. Qed.
548

549
550
551
552
553
Global Instance frame_big_sepL_cons {A} p (Φ : nat  A  uPred M) R Q l x l' :
  IsCons l x l' 
  Frame p R (Φ 0 x  [ list] k  y  l', Φ (S k) y) Q 
  Frame p R ([ list] k  y  l, Φ k y) Q.
Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
554
555
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  uPred M) R Q l l1 l2 :
  IsApp l l1 l2 
556
  Frame p R (([ list] k  y  l1, Φ k y) 
557
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
558
  Frame p R ([ list] k  y  l, Φ k y) Q.
559
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
560

561
562
563
564
565
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.
566
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
567
Proof. done. Qed.
568
569
570
571
572
573
574
575

Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
  MaybeFrame p R P1 Q1 progress1 
  MaybeFrame p R P2 Q2 progress2 
  TCEq (progress1 || progress2) true 
  MakeAnd Q1 Q2 Q' 
  Frame p R (P1  P2) Q' | 9.
Proof. rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-; eauto 10 with I. Qed.
576
577
578
579
580
581
582
583

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.
584

585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
(* We could in principle write the instance [frame_or_spatial] by a bunch of
instances, i.e. (omitting the parameter [p = false]):

  Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
  Frame R P1 True → Frame R (P1 ∨ P2) P2
  Frame R P2 True → Frame R (P1 ∨ P2) P1

The problem here is that Coq will try to infer [Frame R P1 ?] and [Frame R P2 ?]
multiple times, whereas the current solution makes sure that said inference
appears at most once.

If Coq would memorize the results of type class resolution, the solution with
multiple instances would be preferred (and more Prolog-like). *)
Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
  MaybeFrame false R P1 Q1 progress1  MaybeFrame false R P2 Q2 progress2 
  TCOr (TCEq (progress1 && progress2) true) (TCOr
    (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
    (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) 
  MakeOr Q1 Q2 Q 
  Frame false R (P1  P2) Q | 9.
Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.

Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
  MaybeFrame true R P1 Q1 progress1  MaybeFrame true R P2 Q2 progress2 
  TCEq (progress1 || progress2) true 
  MakeOr Q1 Q2 Q  Frame true R (P1  P2) Q | 9.
Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
612

613
614
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
615
616
617
618
619
Proof.
  rewrite /Frame=> ?. apply wand_intro_l.
  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.

620
621
622
623
624
625
626
627
628
629
630
631
632
633
Global Instance frame_impl_persistent R P1 P2 Q2 :
  Frame true R P2 Q2  Frame true R (P1  P2) (P1  Q2).
Proof.
  rewrite /Frame /==> ?. apply impl_intro_l.
  by rewrite -and_sep_l assoc (comm _ P1) -assoc impl_elim_r and_sep_l.
Qed.
Global Instance frame_impl R P1 P2 Q2 :
  Persistent P1 
  Frame false R P2 Q2  Frame false R (P1  P2) (P1  Q2).
Proof.
  rewrite /Frame /==> ??. apply impl_intro_l.
  by rewrite and_sep_l assoc (comm _ P1) -assoc -(and_sep_l P1) impl_elim_r.
Qed.

634
635
636
637
638
639
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.

640
641
Global Instance frame_later p R R' P Q Q' :
  IntoLaterN 1 R' R  Frame p R P Q  MakeLater Q Q'  Frame p R' ( P) Q'.
642
Proof.
643
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
644
  by rewrite persistently_if_later later_sep.
645
646
647
648
649
650
651
652
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.

653
654
655
656
Global Instance frame_laterN p n R R' P Q Q' :
  IntoLaterN n R' R  Frame p R P Q  MakeLaterN n Q Q'  Frame p R' (^n P) Q'.
Proof.
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
657
  by rewrite persistently_if_laterN laterN_sep.
658
659
Qed.

660
661
662
663
Class MakePersistently (P Q : uPred M) := make_persistently :  P  Q.
Global Instance make_persistently_true : MakePersistently True True.
Proof. by rewrite /MakePersistently persistently_pure. Qed.
Global Instance make_persistently_default P : MakePersistently P ( P) | 100.
664
665
Proof. done. Qed.