class_instances.v 40.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
172
173
  IntoLaterN n P Q  IntoLaterN' (S n) ( P) Q.
Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
Global Instance into_laterN_laterN n P : IntoLaterN' n (^n P) P.
174
Proof. done. Qed.
175
Global Instance into_laterN_laterN_plus n m P Q :
176
177
  IntoLaterN m P Q  IntoLaterN' (n + m) (^n P) Q.
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
178

179
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
180
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
181
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
182
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
183
Global Instance into_laterN_and_r n P P2 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  IntoLaterN' n P2 Q2  IntoLaterN' n (P  P2) (P  Q2) | 11.
185
Proof.
186
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
187
Qed.
188

Robbert Krebbers's avatar
Robbert Krebbers committed
189
190
191
192
193
194
195
196
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.

197
Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
198
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
200
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_or. Qed.
201
Global Instance into_laterN_or_r n P P2 Q2 :
202
  IntoLaterN' n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  IntoLaterN' n (P  P2) (P  Q2) | 11.
204
Proof.
205
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
206
207
208
Qed.

Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
209
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
212
Global Instance into_laterN_sep_r n P P2 Q2 :
213
  IntoLaterN' n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
214
  IntoLaterN' n (P  P2) (P  Q2) | 11.
215
Proof.
216
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
217
Qed.
218
219

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

(* FromLater *)
252
Global Instance from_laterN_later P : FromLaterN 1 ( P) P | 0.
253
Proof. done. Qed.
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
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.
277

278
279
280
Global Instance from_later_plainly n P Q :
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
Proof. by rewrite /FromLaterN -plainly_laterN=> ->. Qed.
281
Global Instance from_later_persistently n P Q :
282
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
283
Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
284
285
286
287
288
289
290
291
292

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.

293
(* IntoWand *)
294
295
Global Instance wand_weaken_assumption p P1 P2 Q :
  FromAssumption p P2 P1  WandWeaken p P1 Q P2 Q | 0.
296
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
297
298
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
299
Proof.
300
  rewrite /WandWeaken' /WandWeaken=> ->.
301
  by rewrite persistently_if_later -later_wand -later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
Qed.
303
304
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
305
Proof.
306
  rewrite /WandWeaken' /WandWeaken=> ->.
307
  by rewrite persistently_if_laterN -laterN_wand -laterN_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Qed.
309
310
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
311
312
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->.
313
  apply wand_intro_l. by rewrite persistently_if_elim bupd_wand_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
314
315
Qed.

316
317
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
318
Proof. done. Qed.
319
320
Global Instance into_wand_impl p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
321
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
322

323
324
Global Instance into_wand_iff_l p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
325
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand_1. Qed.
326
327
Global Instance into_wand_iff_r p P P' Q Q' :
  WandWeaken p Q P Q' P'  IntoWand p (P  Q) Q' P'.
328
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
329

Robbert Krebbers's avatar
Robbert Krebbers committed
330
331
332
333
334
335
336
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.

337
338
Global Instance into_wand_forall {A} p (Φ : A  uPred M) P Q x :
  IntoWand p (Φ x) P Q  IntoWand p ( x, Φ x) P Q.
339
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
340
341
342
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.
343
Global Instance into_wand_persistently p R P Q :
344
  IntoWand p R P Q  IntoWand p ( R) P Q.
345
Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
346

347
348
Global Instance into_wand_later p R P Q :
  IntoWand p R P Q  IntoWand p ( R) ( P) ( Q).
349
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_later -later_wand. Qed.
350
351
Global Instance into_wand_laterN p n R P Q :
  IntoWand p R P Q  IntoWand p (^n R) (^n P) (^n Q).
352
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_laterN -laterN_wand. Qed.
353

354
Global Instance into_wand_bupd R P Q :
355
  IntoWand false R P Q  IntoWand false (|==> R) (|==> P) (|==> Q).
356
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
357
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
358
Qed.
359
360
361
362
363
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.
364
365

(* FromAnd *)
366
367
368
369
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.
370
371
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
372
  Persistent P1  FromAnd true (P1  P2) P1 P2 | 9.
373
Proof. intros. by rewrite /FromAnd and_sep_l. Qed.
374
Global Instance from_and_sep_persistent_r P1 P2 :
375
  Persistent P2  FromAnd true (P1  P2) P1 P2 | 10.
376
Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
377
378
379

Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
380
381
382
383
384
385
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.
386
Global Instance from_and_persistently p P Q1 Q2 :
387
388
389
  FromAnd false P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof.
  intros. apply mk_from_and_and.
390
  by rewrite persistently_and_sep_l -persistently_sep -(from_and _ P).
391
392
393
394
395
396
397
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.
398
399
400
401
402
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.
403

404
Global Instance from_sep_ownM (a b1 b2 : M) :
405
  IsOp a b1 b2 
406
  FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
407
Proof. intros. by rewrite /FromAnd -ownM_op -is_op. Qed.
408
Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
409
  IsOp a b1 b2  Or (CoreId b1) (CoreId b2) 
410
411
412
  FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
  intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
413
  by rewrite -ownM_op -is_op.
414
Qed.
415

416
Global Instance from_sep_bupd P Q1 Q2 :
417
418
419
  FromAnd false P Q1 Q2  FromAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.

420
421
422
423
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 :
424
  Persistent (Φ 0 x) 
425
  FromAnd true ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
426
Proof. intros. by rewrite /FromAnd big_opL_cons and_sep_l. Qed.
427

428
429
Global Instance from_and_big_sepL_app {A} (Φ : nat  A  uPred M) l1 l2 :
  FromAnd false ([ list] k  y  l1 ++ l2, Φ k y)
430
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
431
Proof. by rewrite /FromAnd big_opL_app. Qed.
432
Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat  A  uPred M) l1 l2 :
433
  ( k y, Persistent (Φ k y)) 
434
435
  FromAnd true ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
436
Proof. intros. by rewrite /FromAnd big_opL_app and_sep_l. Qed.
437

438
(* FromOp *)
439
440
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
441
Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
442
  IsOp a b1 b2  IsOp a' b1' b2'  IsOp' (a,a') (b1,b1') (b2,b2').
443
Proof. by constructor. Qed.
444
Global Instance is_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
445
446
  CoreId a  IsOp a' b1' b2'  IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
447
Global Instance is_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
448
449
  CoreId a'  IsOp a b1 b2  IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
450

451
452
Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
  IsOp a b1 b2  IsOp' (Some a) (Some b1) (Some b2).
453
Proof. by constructor. Qed.
454
455
456
457
(* 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.
458

459
(* IntoAnd *)
460
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
461
462
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
463
464
  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.
465

466
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
467
Proof. done. Qed.
468
Global Instance into_and_and_persistent_l P Q :
469
  Persistent P  IntoAnd false (P  Q) P Q.
470
Proof. intros; by rewrite /IntoAnd /= and_sep_l. Qed.
471
Global Instance into_and_and_persistent_r P Q :
472
  Persistent Q  IntoAnd false (P  Q) P Q.
473
Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
474

475
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
476
Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
477
478
479
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.
480
Global Instance into_and_persistently p P Q1 Q2 :
481
482
  IntoAnd true P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
483
484
  rewrite /IntoAnd=>->.
  destruct p; by rewrite ?persistently_and persistently_and_sep_r.
485
Qed.
486
487
488
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.
489
490
491
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.
492
493
494
495
496
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.
497

498
499
500
501
502
503
504
505
(* 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.
506
507
508
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)
509
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
510
Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
511
512

(* Frame *)
513
Global Instance frame_here p R : Frame p R R True.
514
Proof. by rewrite /Frame right_id persistently_if_elim. Qed.
515
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
516
Proof. rewrite /FromPure /Frame=> ->. by rewrite persistently_if_elim right_id. Qed.
517

518
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
519
520
521
522
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.
523
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
524
Proof. done. Qed.
525
526
527
528
529
530

Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
  Frame true R P1 Q1  MaybeFrame true R P2 Q2  MakeSep Q1 Q2 Q' 
  Frame true R (P1  P2) Q' | 9.
Proof.
  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
531
  rewrite {1}(sep_dup ( R)). solve_sep_entails.
532
Qed.
533
Global Instance frame_sep_l R P1 P2 Q Q' :
534
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
535
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
536
537
538
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.
539

540
541
542
543
544
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.
545
546
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  uPred M) R Q l l1 l2 :
  IsApp l l1 l2 
547
  Frame p R (([ list] k  y  l1, Φ k y) 
548
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
549
  Frame p R ([ list] k  y  l, Φ k y) Q.
550
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
551

552
553
554
555
556
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.
557
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
558
Proof. done. Qed.
559
560
Global Instance frame_and_l p R P1 P2 Q Q' :
  Frame p R P1 Q  MakeAnd Q P2 Q'  Frame p R (P1  P2) Q' | 9.
561
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
562
563
Global Instance frame_and_r p R P1 P2 Q Q' :
  Frame p R P2 Q  MakeAnd P1 Q Q'  Frame p R (P1  P2) Q' | 10.
564
565
566
567
568
569
570
571
572
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.
573
574
575
576
577
578
579
580
581
582
583

Global Instance frame_or_persistent_l R P1 P2 Q1 Q2 Q :
  Frame true R P1 Q1  MaybeFrame true R P2 Q2  MakeOr Q1 Q2 Q 
  Frame true R (P1  P2) Q | 9.
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
Global Instance frame_or_persistent_r R P1 P2 Q1 Q2 Q :
  MaybeFrame true R P2 Q2  MakeOr P1 Q2 Q 
  Frame true R (P1  P2) Q | 10.
Proof.
  rewrite /Frame /MaybeFrame /MakeOr => <- <-. by rewrite sep_or_l sep_elim_r.
Qed.
584
Global Instance frame_or R P1 P2 Q1 Q2 Q :
585
586
  Frame false R P1 Q1  Frame false R P2 Q2  MakeOr Q1 Q2 Q 
  Frame false R (P1  P2) Q.
587
588
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

589
590
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
591
592
593
594
595
596
597
598
599
600
601
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.

602
603
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'.
604
Proof.
605
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
606
  by rewrite persistently_if_later later_sep.
607
608
609
610
611
612
613
614
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.

615
616
617
618
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=>-> <- <-.
619
  by rewrite persistently_if_laterN laterN_sep.
620
621
Qed.

622
623
624
625
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.
626
627
Proof. done. Qed.

628
629
Global Instance frame_persistently R P Q Q' :
  Frame true R P Q  MakePersistently Q Q'  Frame true R ( P) Q'.
630
Proof.
631
  rewrite /Frame /MakePersistently=> <- <-.
632
  by rewrite persistently_sep /= persistent_persistently.
633
634
Qed.

635
636
637
638
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.
639
640
Proof. done. Qed.

641
642
Global Instance frame_except_0 p R P Q Q' :
  Frame p R P Q  MakeExcept0 Q Q'  Frame p R ( P) Q'.
643
Proof.
644
  rewrite /Frame /MakeExcept0=><- <-.
645
  by rewrite except_0_sep -(except_0_intro (?p R)).
646
647
Qed.

648
649
Global Instance frame_exist {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
650
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
651
652
Global Instance frame_forall {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
653
654
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

655
Global Instance frame_bupd p R P Q : Frame p R P Q  Frame p R (|==> P) (|==> Q).