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

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

51
52
Global Instance into_pure_persistently P φ : IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite persistently_pure. Qed.
53

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

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

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

98
99
Global Instance from_pure_persistently P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
100
101
102
103
104
105
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.
106
Global Instance from_pure_bupd P φ : FromPure P φ  FromPure (|==> P) φ.
107
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
108

Ralf Jung's avatar
Ralf Jung committed
109
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
110
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
111
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
112
Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
113
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
114
Proof. rewrite /FromPure pure_and and_sep_l. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
115
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
116
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
117
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
118
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
119
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
120
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
121
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
122
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1 - P2) (φ1  φ2).
123
Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
124

Ralf Jung's avatar
Ralf Jung committed
125
Global Instance from_pure_exist {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
126
127
128
129
130
  ( 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
131
Global Instance from_pure_forall {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
132
133
134
135
136
137
  ( 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.

138
(* IntoPersistent *)
139
Global Instance into_persistent_persistently_trans p P Q :
140
  IntoPersistent true P Q  IntoPersistent p ( P) Q | 0.
141
Proof. rewrite /IntoPersistent /==> ->. by rewrite persistent_persistently_if. Qed.
142
Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
143
Proof. done. Qed.
144
145
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
146
147
148
Proof. done. Qed.

(* IntoLater *)
149
Global Instance into_laterN_later n P Q :
150
151
152
  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.
153
Proof. done. Qed.
154
Global Instance into_laterN_laterN_plus n m P Q :
155
156
  IntoLaterN m P Q  IntoLaterN' (n + m) (^n P) Q.
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
157

158
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
159
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
161
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
162
Global Instance into_laterN_and_r n P P2 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  IntoLaterN' n P2 Q2  IntoLaterN' n (P  P2) (P  Q2) | 11.
164
Proof.
165
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Qed.
167

Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
170
171
172
173
174
175
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.

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

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

Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat  A  uPred M) (l: list A) :
199
200
  ( x k, IntoLaterN' n (Φ k x) (Ψ k x)) 
  IntoLaterN' n ([ list] k  x  l, Φ k x) ([ list] k  x  l, Ψ k x).
201
Proof.
202
  rewrite /IntoLaterN' /IntoLaterN=> ?.
203
  rewrite big_opL_commute. by apply big_sepL_mono.
204
205
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
206
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
207
208
  ( x k, IntoLaterN' n (Φ k x) (Ψ k x)) 
  IntoLaterN' n ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
209
Proof.
210
  rewrite /IntoLaterN' /IntoLaterN=> ?.
211
  rewrite big_opM_commute; by apply big_sepM_mono.
212
Qed.
213
Global Instance into_laterN_big_sepS n `{Countable A}
214
    (Φ Ψ : A  uPred M) (X : gset A) :
215
216
  ( x, IntoLaterN' n (Φ x) (Ψ x)) 
  IntoLaterN' n ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
217
Proof.
218
  rewrite /IntoLaterN' /IntoLaterN=> ?.
219
  rewrite big_opS_commute; by apply big_sepS_mono.
220
221
222
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
    (Φ Ψ : A  uPred M) (X : gmultiset A) :
223
224
  ( x, IntoLaterN' n (Φ x) (Ψ x)) 
  IntoLaterN' n ([ mset] x  X, Φ x) ([ mset] x  X, Ψ x).
225
Proof.
226
  rewrite /IntoLaterN' /IntoLaterN=> ?.
227
  rewrite big_opMS_commute; by apply big_sepMS_mono.
228
229
230
Qed.

(* FromLater *)
231
Global Instance from_laterN_later P : FromLaterN 1 ( P) P | 0.
232
Proof. done. Qed.
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
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.
256

257
Global Instance from_later_persistently n P Q :
258
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
259
Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
260
261
262
263
264
265
266
267
268

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.

269
(* IntoWand *)
270
271
Global Instance wand_weaken_assumption p P1 P2 Q :
  FromAssumption p P2 P1  WandWeaken p P1 Q P2 Q | 0.
272
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
273
274
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
275
Proof.
276
  rewrite /WandWeaken' /WandWeaken=> ->.
277
  by rewrite persistently_if_later -later_wand -later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
Qed.
279
280
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
281
Proof.
282
  rewrite /WandWeaken' /WandWeaken=> ->.
283
  by rewrite persistently_if_laterN -laterN_wand -laterN_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Qed.
285
286
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
287
288
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->.
289
  apply wand_intro_l. by rewrite persistently_if_elim bupd_wand_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
291
Qed.

292
293
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
294
Proof. done. Qed.
295
296
Global Instance into_wand_impl p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
297
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298

299
300
Global Instance into_wand_iff_l p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
301
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand_1. Qed.
302
303
Global Instance into_wand_iff_r p P P' Q Q' :
  WandWeaken p Q P Q' P'  IntoWand p (P  Q) Q' P'.
304
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
305

306
307
Global Instance into_wand_forall {A} p (Φ : A  uPred M) P Q x :
  IntoWand p (Φ x) P Q  IntoWand p ( x, Φ x) P Q.
308
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
309
Global Instance into_wand_persistently p R P Q :
310
  IntoWand p R P Q  IntoWand p ( R) P Q.
311
Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
312

313
314
Global Instance into_wand_later p R P Q :
  IntoWand p R P Q  IntoWand p ( R) ( P) ( Q).
315
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_later -later_wand. Qed.
316
317
Global Instance into_wand_laterN p n R P Q :
  IntoWand p R P Q  IntoWand p (^n R) (^n P) (^n Q).
318
Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_laterN -laterN_wand. Qed.
319

320
Global Instance into_wand_bupd R P Q :
321
  IntoWand false R P Q  IntoWand false (|==> R) (|==> P) (|==> Q).
322
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
324
Qed.
325
326
327
328
329
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.
330
331

(* FromAnd *)
332
333
334
335
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.
336
337
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
338
  Persistent P1  FromAnd true (P1  P2) P1 P2 | 9.
339
Proof. intros. by rewrite /FromAnd and_sep_l. Qed.
340
Global Instance from_and_sep_persistent_r P1 P2 :
341
  Persistent P2  FromAnd true (P1  P2) P1 P2 | 10.
342
Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
343
344
345

Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
346
Global Instance from_and_persistently p P Q1 Q2 :
347
348
349
  FromAnd false P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof.
  intros. apply mk_from_and_and.
350
  by rewrite persistently_and_sep_l -persistently_sep -(from_and _ P).
351
352
353
354
355
356
357
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.
358
359
360
361
362
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.
363

364
Global Instance from_sep_ownM (a b1 b2 : M) :
365
  IsOp a b1 b2 
366
  FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
367
Proof. intros. by rewrite /FromAnd -ownM_op -is_op. Qed.
368
Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
369
  IsOp a b1 b2  Or (CoreId b1) (CoreId b2) 
370
371
372
  FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
  intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
373
  by rewrite -ownM_op -is_op.
374
Qed.
375

376
Global Instance from_sep_bupd P Q1 Q2 :
377
378
379
  FromAnd false P Q1 Q2  FromAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.

380
381
382
383
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 :
384
  Persistent (Φ 0 x) 
385
  FromAnd true ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
386
Proof. intros. by rewrite /FromAnd big_opL_cons and_sep_l. Qed.
387

388
389
Global Instance from_and_big_sepL_app {A} (Φ : nat  A  uPred M) l1 l2 :
  FromAnd false ([ list] k  y  l1 ++ l2, Φ k y)
390
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
391
Proof. by rewrite /FromAnd big_opL_app. Qed.
392
Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat  A  uPred M) l1 l2 :
393
  ( k y, Persistent (Φ k y)) 
394
395
  FromAnd true ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
396
Proof. intros. by rewrite /FromAnd big_opL_app and_sep_l. Qed.
397

398
(* FromOp *)
399
400
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
401
Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  IsOp a b1 b2  IsOp a' b1' b2'  IsOp' (a,a') (b1,b1') (b2,b2').
403
Proof. by constructor. Qed.
404
Global Instance is_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
405
406
  CoreId a  IsOp a' b1' b2'  IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
407
Global Instance is_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
408
409
  CoreId a'  IsOp a b1 b2  IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
410

411
412
Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
  IsOp a b1 b2  IsOp' (Some a) (Some b1) (Some b2).
413
Proof. by constructor. Qed.
414
415
416
417
(* 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.
418

419
(* IntoAnd *)
420
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
421
422
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
423
424
  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.
425

426
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
427
Proof. done. Qed.
428
Global Instance into_and_and_persistent_l P Q :
429
  Persistent P  IntoAnd false (P  Q) P Q.
430
Proof. intros; by rewrite /IntoAnd /= and_sep_l. Qed.
431
Global Instance into_and_and_persistent_r P Q :
432
  Persistent Q  IntoAnd false (P  Q) P Q.
433
Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
434

435
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
436
Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
437
Global Instance into_and_persistently p P Q1 Q2 :
438
439
  IntoAnd true P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
440
  rewrite /IntoAnd=>->. destruct p; by rewrite ?persistently_and persistently_and_sep_r.
441
Qed.
442
443
444
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.
445
446
447
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.
448
449
450
451
452
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.
453

454
455
456
457
458
459
460
461
(* 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.
462
463
464
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)
465
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
466
Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
467
468

(* Frame *)
469
Global Instance frame_here p R : Frame p R R True.
470
Proof. by rewrite /Frame right_id persistently_if_elim. Qed.
471
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
472
Proof. rewrite /FromPure /Frame=> ->. by rewrite persistently_if_elim right_id. Qed.
473

474
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
475
476
477
478
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.
479
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
480
Proof. done. Qed.
481
482
483
484
485
486

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 /= => <- <- <-.
487
  rewrite {1}(sep_dup ( R)). solve_sep_entails.
488
Qed.
489
Global Instance frame_sep_l R P1 P2 Q Q' :
490
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
491
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
492
493
494
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.
495

496
497
498
499
500
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.
501
502
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  uPred M) R Q l l1 l2 :
  IsApp l l1 l2 
503
  Frame p R (([ list] k  y  l1, Φ k y) 
504
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
505
  Frame p R ([ list] k  y  l, Φ k y) Q.
506
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
507

508
509
510
511
512
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.
513
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
514
Proof. done. Qed.
515
516
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.
517
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
518
519
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.
520
521
522
523
524
525
526
527
528
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.
529
530
531
532
533
534
535
536
537
538
539

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.
540
Global Instance frame_or R P1 P2 Q1 Q2 Q :
541
542
  Frame false R P1 Q1  Frame false R P2 Q2  MakeOr Q1 Q2 Q 
  Frame false R (P1  P2) Q.
543
544
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

545
546
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
547
548
549
550
551
552
553
554
555
556
557
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.

558
559
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'.
560
Proof.
561
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
562
  by rewrite persistently_if_later later_sep.
563
564
565
566
567
568
569
570
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.

571
572
573
574
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=>-> <- <-.
575
  by rewrite persistently_if_laterN laterN_sep.
576
577
Qed.

578
579
580
581
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.
582
583
Proof. done. Qed.

584
585
Global Instance frame_persistently R P Q Q' :
  Frame true R P Q  MakePersistently Q Q'  Frame true R ( P) Q'.
586
Proof.
587
  rewrite /Frame /MakePersistently=> <- <-.
588
  by rewrite persistently_sep /= persistent_persistently.
589
590
Qed.

591
592
593
594
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.
595
596
Proof. done. Qed.

597
598
Global Instance frame_except_0 p R P Q Q' :
  Frame p R P Q  MakeExcept0 Q Q'  Frame p R ( P) Q'.
599
Proof.
600
  rewrite /Frame /MakeExcept0=><- <-.
601
  by rewrite except_0_sep -(except_0_intro (?p R)).
602
603
Qed.

604
605
Global Instance frame_exist {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
606
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
607
608
Global Instance frame_forall {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
609
610
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

611
Global Instance frame_bupd p R P Q : Frame p R P Q  Frame p R (|==> P) (|==> Q).
612
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
613

614
615
616
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. done. Qed.
617
Global Instance from_or_bupd P Q1 Q2 :
618
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
619
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
620
621
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
622
Global Instance from_or_persistently P Q1 Q2 :
623
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
624
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
625
626
Global Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
627
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
628
629
630
Global Instance from_or_laterN n P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromOr=><-. by rewrite laterN_or. Qed.
631
632
633
Global Instance from_or_except_0 P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=><-. by rewrite except_0_or. Qed.
634
635
636
637

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
638