class_instances.v 44 KB
Newer Older
1
From iris.proofmode Require Export classes.
2
From iris.algebra Require Import gmap.
3
From stdpp Require Import gmultiset nat_cancel.
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
171
172
173
Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ^n P  lP.
Global Instance make_laterN_true n : MakeLaterN n True True | 0.
Proof. by rewrite /MakeLaterN laterN_True. Qed.
Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
174
Proof. done. Qed.
175
176
177
178
179
Global Instance make_laterN_1 P : MakeLaterN 1 P ( P) | 2.
Proof. done. Qed.
Global Instance make_laterN_default P : MakeLaterN n P (^n P) | 100.
Proof. done. Qed.

180
Global Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
181
Proof. done. Qed.
182
Global Instance into_laterN_later only_head n n' m' P Q lQ :
183
184
185
186
187
188
  NatCancel n 1 n' m' 
  (** If canceling has failed (i.e. [1 = m']), we should make progress deeper
  into [P], as such, we continue with the [IntoLaterN] class, which is required
  to make progress. If canceling has succeeded, we do not need to make further
  progress, but there may still be a left-over (i.e. [n']) to cancel more deeply
  into [P], as such, we continue with [MaybeIntoLaterN]. *)
189
  TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) 
190
  MakeLaterN m' Q lQ 
191
  IntoLaterN only_head n ( P) lQ | 2.
192
193
194
195
196
Proof.
  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
  move=> Hn [_ ->|->] <-;
    by rewrite -later_laterN -laterN_plus -Hn Nat.add_comm.
Qed.
197
Global Instance into_laterN_laterN only_head n m n' m' P Q lQ :
198
  NatCancel n m n' m' 
199
  TCIf (TCEq m m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) 
200
  MakeLaterN m' Q lQ 
201
  IntoLaterN only_head n (^m P) lQ | 1.
202
203
204
Proof.
  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
  move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Qed.
206

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

Robbert Krebbers's avatar
Robbert Krebbers committed
217
Global Instance into_later_forall {A} n (Φ Ψ : A  uPred M) :
218
219
  ( x, IntoLaterN false n (Φ x) (Ψ x)) 
  IntoLaterN false n ( x, Φ x) ( x, Ψ x).
220
Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
Global Instance into_later_exist {A} n (Φ Ψ : A  uPred M) :
222
223
  ( x, IntoLaterN false n (Φ x) (Ψ x)) 
  IntoLaterN false n ( x, Φ x) ( x, Ψ x).
224
Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
225

226
Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
227
228
  IntoLaterN false n P1 Q1  MaybeIntoLaterN false n P2 Q2 
  IntoLaterN false n (P1  P2) (Q1  Q2) | 10.
229
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_or. Qed.
230
Global Instance into_laterN_or_r n P P2 Q2 :
231
232
  IntoLaterN false n P2 Q2 
  IntoLaterN false n (P  P2) (P  Q2) | 11.
233
Proof.
234
  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
235
236
237
Qed.

Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
238
239
  IntoLaterN false n P1 Q1  MaybeIntoLaterN false n P2 Q2 
  IntoLaterN false n (P1  P2) (Q1  Q2) | 10.
240
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
241
Global Instance into_laterN_sep_r n P P2 Q2 :
242
243
  IntoLaterN false n P2 Q2 
  IntoLaterN false n (P  P2) (P  Q2) | 11.
244
Proof.
245
  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
246
Qed.
247
248

Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat  A  uPred M) (l: list A) :
249
250
  ( x k, IntoLaterN false n (Φ k x) (Ψ k x)) 
  IntoLaterN false n ([ list] k  x  l, Φ k x) ([ list] k  x  l, Ψ k x).
251
Proof.
252
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
253
  rewrite big_opL_commute. by apply big_sepL_mono.
254
255
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
256
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
257
258
  ( x k, IntoLaterN false n (Φ k x) (Ψ k x)) 
  IntoLaterN false n ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
259
Proof.
260
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
261
  rewrite big_opM_commute; by apply big_sepM_mono.
262
Qed.
263
Global Instance into_laterN_big_sepS n `{Countable A}
264
    (Φ Ψ : A  uPred M) (X : gset A) :
265
266
  ( x, IntoLaterN false n (Φ x) (Ψ x)) 
  IntoLaterN false n ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
267
Proof.
268
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
269
  rewrite big_opS_commute; by apply big_sepS_mono.
270
271
272
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
    (Φ Ψ : A  uPred M) (X : gmultiset A) :
273
274
  ( x, IntoLaterN false n (Φ x) (Ψ x)) 
  IntoLaterN false n ([ mset] x  X, Φ x) ([ mset] x  X, Ψ x).
275
Proof.
276
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
277
  rewrite big_opMS_commute; by apply big_sepMS_mono.
278
279
280
Qed.

(* FromLater *)
281
Global Instance from_laterN_later P : FromLaterN 1 ( P) P | 0.
282
Proof. done. Qed.
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
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.
306

307
308
309
Global Instance from_later_plainly n P Q :
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
Proof. by rewrite /FromLaterN -plainly_laterN=> ->. Qed.
310
Global Instance from_later_persistently n P Q :
311
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
312
Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
313
314
315
316
317
318
319
320
321

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.

322
(* IntoWand *)
323
324
Global Instance wand_weaken_assumption p P1 P2 Q :
  FromAssumption p P2 P1  WandWeaken p P1 Q P2 Q | 0.
325
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
326
327
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
328
Proof.
329
  rewrite /WandWeaken' /WandWeaken=> ->.
330
  by rewrite persistently_if_later -later_wand -later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
Qed.
332
333
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
334
Proof.
335
  rewrite /WandWeaken' /WandWeaken=> ->.
336
  by rewrite persistently_if_laterN -laterN_wand -laterN_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
Qed.
338
339
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
340
341
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->.
342
  apply wand_intro_l. by rewrite persistently_if_elim bupd_wand_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
344
Qed.

345
346
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
347
Proof. done. Qed.
348
349
Global Instance into_wand_impl p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
350
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
351

352
353
Global Instance into_wand_iff_l p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
354
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand_1. Qed.
355
356
Global Instance into_wand_iff_r p P P' Q Q' :
  WandWeaken p Q P Q' P'  IntoWand p (P  Q) Q' P'.
357
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
358

Robbert Krebbers's avatar
Robbert Krebbers committed
359
360
361
362
363
364
365
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.

366
367
Global Instance into_wand_forall {A} p (Φ : A  uPred M) P Q x :
  IntoWand p (Φ x) P Q  IntoWand p ( x, Φ x) P Q.
368
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
369
370
371
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.
372
Global Instance into_wand_persistently p R P Q :
373
  IntoWand p R P Q  IntoWand p ( R) P Q.
374
Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
375

376
377
Global Instance into_wand_later p R P Q :
  IntoWand p R P Q  IntoWand p ( R) ( P) ( Q).
378
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_later -later_wand. Qed.
379
380
Global Instance into_wand_laterN p n R P Q :
  IntoWand p R P Q  IntoWand p (^n R) (^n P) (^n Q).
381
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_laterN -laterN_wand. Qed.
382

383
Global Instance into_wand_bupd R P Q :
384
  IntoWand false R P Q  IntoWand false (|==> R) (|==> P) (|==> Q).
385
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
387
Qed.
388
389
390
391
392
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.
393
394

(* FromAnd *)
395
396
397
398
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.
399
400
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
401
  Persistent P1  FromAnd true (P1  P2) P1 P2 | 9.
402
Proof. intros. by rewrite /FromAnd and_sep_l. Qed.
403
Global Instance from_and_sep_persistent_r P1 P2 :
404
  Persistent P2  FromAnd true (P1  P2) P1 P2 | 10.
405
Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
406
407
408

Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
409
410
411
412
413
414
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.
415
Global Instance from_and_persistently p P Q1 Q2 :
416
417
418
  FromAnd false P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof.
  intros. apply mk_from_and_and.
419
  by rewrite persistently_and_sep_l -persistently_sep -(from_and _ P).
420
421
422
423
424
425
426
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.
427
428
429
430
431
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.
432

433
Global Instance from_sep_ownM (a b1 b2 : M) :
434
  IsOp a b1 b2 
435
  FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
436
Proof. intros. by rewrite /FromAnd -ownM_op -is_op. Qed.
437
Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
438
  IsOp a b1 b2  Or (CoreId b1) (CoreId b2) 
439
440
441
  FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
  intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
442
  by rewrite -ownM_op -is_op.
443
Qed.
444

445
Global Instance from_sep_bupd P Q1 Q2 :
446
447
448
  FromAnd false P Q1 Q2  FromAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.

449
450
451
452
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 :
453
  Persistent (Φ 0 x) 
454
  FromAnd true ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
455
Proof. intros. by rewrite /FromAnd big_opL_cons and_sep_l. Qed.
456

457
458
Global Instance from_and_big_sepL_app {A} (Φ : nat  A  uPred M) l1 l2 :
  FromAnd false ([ list] k  y  l1 ++ l2, Φ k y)
459
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
460
Proof. by rewrite /FromAnd big_opL_app. Qed.
461
Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat  A  uPred M) l1 l2 :
462
  ( k y, Persistent (Φ k y)) 
463
464
  FromAnd true ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
465
Proof. intros. by rewrite /FromAnd big_opL_app and_sep_l. Qed.
466

467
(* FromOp *)
468
469
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
470
Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
471
  IsOp a b1 b2  IsOp a' b1' b2'  IsOp' (a,a') (b1,b1') (b2,b2').
472
Proof. by constructor. Qed.
473
Global Instance is_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
474
475
  CoreId a  IsOp a' b1' b2'  IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
476
Global Instance is_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
477
478
  CoreId a'  IsOp a b1 b2  IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
479

480
481
Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
  IsOp a b1 b2  IsOp' (Some a) (Some b1) (Some b2).
482
Proof. by constructor. Qed.
483
484
485
486
(* 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.
487

488
(* IntoAnd *)
489
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
490
491
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
492
493
  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.
494

495
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
496
Proof. done. Qed.
497
Global Instance into_and_and_persistent_l P Q :
498
  Persistent P  IntoAnd false (P  Q) P Q.
499
Proof. intros; by rewrite /IntoAnd /= and_sep_l. Qed.
500
Global Instance into_and_and_persistent_r P Q :
501
  Persistent Q  IntoAnd false (P  Q) P Q.
502
Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
503

504
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
505
Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
506
507
508
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.
509
Global Instance into_and_persistently p P Q1 Q2 :
510
511
  IntoAnd true P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
512
513
  rewrite /IntoAnd=>->.
  destruct p; by rewrite ?persistently_and persistently_and_sep_r.
514
Qed.
515
516
517
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.
518
519
520
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.
521
522
523
524
525
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.
526

527
528
529
530
531
532
533
534
(* 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.
535
536
537
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)
538
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
539
Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
540
541

(* Frame *)
542
Global Instance frame_here p R : Frame p R R True.
543
Proof. by rewrite /Frame right_id persistently_if_elim. Qed.
544
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
545
Proof. rewrite /FromPure /Frame=> ->. by rewrite persistently_if_elim right_id. Qed.
546

547
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
548
549
550
551
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.
552
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
553
Proof. done. Qed.
554

555
556
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' 
557
558
559
  Frame true R (P1  P2) Q' | 9.
Proof.
  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
560
  rewrite {1}(sep_dup ( R)). solve_sep_entails.
561
Qed.
562
Global Instance frame_sep_l R P1 P2 Q Q' :
563
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
564
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
565
566
567
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.
568

569
570
571
572
573
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.
574
575
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  uPred M) R Q l l1 l2 :
  IsApp l l1 l2 
576
  Frame p R (([ list] k  y  l1, Φ k y) 
577
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
578
  Frame p R ([ list] k  y  l, Φ k y) Q.
579
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
580

581
582
583
584
585
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.
586
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
587
Proof. done. Qed.
588
589
590
591
592
593
594
595

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.
596
597
598
599
600
601
602
603

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

605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
(* 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.
632

633
634
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
635
636
637
638
639
Proof.
  rewrite /Frame=> ?. apply wand_intro_l.
  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.

640
641
642
643
644
645
646
647
648
649
650
651
652
653
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.

654
Global Instance frame_later p R R' P Q Q' :
655
  NoBackTrack (MaybeIntoLaterN true 1 R' R) 
656
  Frame p R P Q  MakeLaterN 1 Q Q'  Frame p R' ( P) Q'.
657
Proof.
658
  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
659
  by rewrite persistently_if_later later_sep.