class_instances.v 32.3 KB
Newer Older
1
From iris.proofmode Require Export classes.
2
From iris.algebra Require Import gmap.
Ralf Jung's avatar
Ralf Jung committed
3
From stdpp Require Import gmultiset.
4
From iris.base_logic Require Import big_op 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 /= ?always_elim. Qed.
15
16
17
Global Instance from_assumption_False p P : FromAssumption p False P | 1.
Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.

18
19
20
Global Instance from_assumption_always_r P Q :
  FromAssumption true P Q  FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
21
22
23
24

Global Instance from_assumption_always_l p P Q :
  FromAssumption p P Q  FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
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
Global Instance from_assumption_bupd p P Q :
32
  FromAssumption p P Q  FromAssumption p P (|==> Q)%I.
33
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
34
35
36
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.
37
38

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

Ralf Jung's avatar
Ralf Jung committed
48
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
49
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
50
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
51
Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
52
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
53
Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
54
Global Instance into_pure_pure_or (φ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_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
57
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
58
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
59
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
60
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
61
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
62
63
64
65
Proof.
  rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
Qed.

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

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

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

Ralf Jung's avatar
Ralf Jung committed
114
Global Instance from_pure_exist {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
115
116
117
118
119
  ( 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
120
Global Instance from_pure_forall {X : Type} (Φ : X  uPred M) (φ : X  Prop) :
121
122
123
124
125
126
  ( 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.

127
128
129
130
131
132
133
134
135
136
137
(* IntoPersistentP *)
Global Instance into_persistentP_always_trans P Q :
  IntoPersistentP P Q  IntoPersistentP ( P) Q | 0.
Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
Global Instance into_persistentP_always P : IntoPersistentP ( P) P | 1.
Proof. done. Qed.
Global Instance into_persistentP_persistent P :
  PersistentP P  IntoPersistentP P P | 100.
Proof. done. Qed.

(* IntoLater *)
138
Global Instance into_laterN_later n P Q :
139
140
141
  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.
142
Proof. done. Qed.
143
Global Instance into_laterN_laterN_plus n m P Q :
144
145
  IntoLaterN m P Q  IntoLaterN' (n + m) (^n P) Q.
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
146

147
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
148
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
150
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
151
Global Instance into_laterN_and_r n P P2 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  IntoLaterN' n P2 Q2  IntoLaterN' n (P  P2) (P  Q2) | 11.
153
Proof.
154
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Qed.
156
157

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

Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
169
  IntoLaterN' n P1 Q1  IntoLaterN n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
  IntoLaterN' n (P1  P2) (Q1  Q2) | 10.
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
172
Global Instance into_laterN_sep_r n P P2 Q2 :
173
  IntoLaterN' n P2 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  IntoLaterN' n (P  P2) (P  Q2) | 11.
175
Proof.
176
  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
177
Qed.
178
179

Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat  A  uPred M) (l: list A) :
180
181
  ( x k, IntoLaterN' n (Φ k x) (Ψ k x)) 
  IntoLaterN' n ([ list] k  x  l, Φ k x) ([ list] k  x  l, Ψ k x).
182
Proof.
183
  rewrite /IntoLaterN' /IntoLaterN=> ?.
184
  rewrite big_opL_commute. by apply big_sepL_mono.
185
186
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
187
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
188
189
  ( x k, IntoLaterN' n (Φ k x) (Ψ k x)) 
  IntoLaterN' n ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
190
Proof.
191
  rewrite /IntoLaterN' /IntoLaterN=> ?.
192
  rewrite big_opM_commute; by apply big_sepM_mono.
193
Qed.
194
Global Instance into_laterN_big_sepS n `{Countable A}
195
    (Φ Ψ : A  uPred M) (X : gset A) :
196
197
  ( x, IntoLaterN' n (Φ x) (Ψ x)) 
  IntoLaterN' n ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
198
Proof.
199
  rewrite /IntoLaterN' /IntoLaterN=> ?.
200
  rewrite big_opS_commute; by apply big_sepS_mono.
201
202
203
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
    (Φ Ψ : A  uPred M) (X : gmultiset A) :
204
205
  ( x, IntoLaterN' n (Φ x) (Ψ x)) 
  IntoLaterN' n ([ mset] x  X, Φ x) ([ mset] x  X, Ψ x).
206
Proof.
207
  rewrite /IntoLaterN' /IntoLaterN=> ?.
208
  rewrite big_opMS_commute; by apply big_sepMS_mono.
209
210
211
Qed.

(* FromLater *)
212
Global Instance from_laterN_later P :FromLaterN 1 ( P) P | 0.
213
Proof. done. Qed.
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
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.
237

238
239
240
241
242
243
244
245
246
247
248
249
Global Instance from_later_always n P Q :
  FromLaterN n P Q  FromLaterN n ( P) ( Q).
Proof. by rewrite /FromLaterN -always_laterN=> ->. Qed.

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.

250
(* IntoWand *)
251
252
253
Global Instance wand_weaken_assumption P1 P2 Q :
  FromAssumption false P2 P1  WandWeaken P1 Q P2 Q | 0.
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
Global Instance wand_weaken_later P Q P' Q' :
  WandWeaken P Q P' Q'  WandWeaken' P Q ( P') ( Q').
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -later_wand -later_intro.
Qed.
Global Instance wand_weaken_laterN n P Q P' Q' :
  WandWeaken P Q P' Q'  WandWeaken' P Q (^n P') (^n Q').
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -laterN_wand -laterN_intro.
Qed.
Global Instance bupd_weaken_laterN P Q P' Q' :
  WandWeaken P Q P' Q'  WandWeaken' P Q (|==> P') (|==> Q').
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->.
  apply wand_intro_l. by rewrite bupd_wand_r.
Qed.

Global Instance into_wand_wand P P' Q Q' :
  WandWeaken P Q P' Q'  IntoWand (P - Q) P' Q'.
Proof. done. Qed.
Global Instance into_wand_impl P P' Q Q' :
  WandWeaken P Q P' Q'  IntoWand (P  Q) P' Q'.
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand. Qed.

Global Instance into_wand_iff_l P P' Q Q' :
  WandWeaken P Q P' Q'  IntoWand (P  Q) P' Q'.
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand. Qed.
Global Instance into_wand_iff_r P P' Q Q' :
  WandWeaken Q P Q' P'  IntoWand (P  Q) Q' P'.
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
284

285
286
287
Global Instance into_wand_forall {A} (Φ : A  uPred M) P Q x :
  IntoWand (Φ x) P Q  IntoWand ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
288
289
Global Instance into_wand_always R P Q : IntoWand R P Q  IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
290

Robbert Krebbers's avatar
Robbert Krebbers committed
291
292
293
294
295
296
Global Instance into_wand_later R P Q :
  IntoWand R P Q  IntoWand ( R) ( P) ( Q).
Proof. rewrite /IntoWand=> ->. by rewrite -later_wand. Qed.
Global Instance into_wand_laterN n R P Q :
  IntoWand R P Q  IntoWand (^n R) (^n P) (^n Q).
Proof. rewrite /IntoWand=> ->. by rewrite -laterN_wand. Qed.
297
Global Instance into_wand_bupd R P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
298
  IntoWand R P Q  IntoWand (|==> R) (|==> P) (|==> Q).
299
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
301
Qed.
302
303

(* FromAnd *)
304
305
306
307
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.
308
309
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
310
  PersistentP P1  FromAnd true (P1  P2) P1 P2 | 9.
311
312
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
313
  PersistentP P2  FromAnd true (P1  P2) P1 P2 | 10.
314
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330

Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
Global Instance from_and_always p P Q1 Q2 :
  FromAnd false P Q1 Q2  FromAnd p ( P) ( Q1) ( Q2).
Proof.
  intros. apply mk_from_and_and.
  by rewrite always_and_sep_l' -always_sep -(from_and _ P).
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.

331
332
Global Instance from_sep_ownM (a b1 b2 : M) :
  FromOp a b1 b2 
333
334
  FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromAnd -ownM_op from_op. Qed.
335
336
337
338
339
340
341
Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
  FromOp a b1 b2  Or (Persistent b1) (Persistent b2) 
  FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
  intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
  by rewrite -ownM_op from_op.
Qed.
342

343
Global Instance from_sep_bupd P Q1 Q2 :
344
345
346
  FromAnd false P Q1 Q2  FromAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.

347
348
349
350
351
352
353
354
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 :
  PersistentP (Φ 0 x) 
  FromAnd true ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.

355
356
Global Instance from_and_big_sepL_app {A} (Φ : nat  A  uPred M) l1 l2 :
  FromAnd false ([ list] k  y  l1 ++ l2, Φ k y)
357
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
358
Proof. by rewrite /FromAnd big_opL_app. Qed.
359
360
361
362
363
Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat  A  uPred M) l1 l2 :
  ( k y, PersistentP (Φ k y)) 
  FromAnd true ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
364

365
366
367
(* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a  b) a b.
Proof. by rewrite /FromOp. Qed.
368
369
370

(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
371
Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
372
  FromOp a b1 b2  FromOp a' b1' b2'  FromOp (a,a') (b1,b1') (b2,b2').
373
Proof. by constructor. Qed.
374
375
376
377
378
379
380
Global Instance from_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
  Persistent a  FromOp a' b1' b2'  FromOp (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
Global Instance from_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
  Persistent a'  FromOp a b1 b2  FromOp (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -persistent_dup. Qed.

381
382
383
384
Global Instance from_op_Some {A : cmraT} (a : A) b1 b2 :
  FromOp a b1 b2  FromOp (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.

385
386
387
(* IntoOp *)
Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a  b) a b.
Proof. by rewrite /IntoOp. Qed.
388

389
390
391
392
Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
  IntoOp a b1 b2  IntoOp a' b1' b2' 
  IntoOp (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
393
394
395
396
397
398
399
Global Instance into_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
  Persistent a  IntoOp a' b1' b2'  IntoOp (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
Global Instance into_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
  Persistent a'  IntoOp a b1 b2  IntoOp (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -persistent_dup. Qed.

400
401
402
403
Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
  IntoOp a b1 b2  IntoOp (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.

404
(* IntoAnd *)
405
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
406
407
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
408
  IntoOp a b1 b2 
409
410
  IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) ownM_op. Qed.
411

412
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
413
Proof. done. Qed.
414
415
416
417
418
419
420
Global Instance into_and_and_persistent_l P Q :
  PersistentP P  IntoAnd false (P  Q) P Q.
Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed.
Global Instance into_and_and_persistent_r P Q :
  PersistentP Q  IntoAnd false (P  Q) P Q.
Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.

421
422
423
424
425
426
427
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_into_and_sep. by rewrite pure_and always_and_sep_r. Qed.
Global Instance into_and_always p P Q1 Q2 :
  IntoAnd true P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd=>->. destruct p; by rewrite ?always_and always_and_sep_r.
Qed.
428
429
430
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.
431
432
433
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.
434

435
436
437
438
439
440
441
442
(* 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.
443
444
445
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)
446
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
447
Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
448
449

(* Frame *)
450
451
452
453
Global Instance frame_here p R : Frame p R R True.
Proof. by rewrite /Frame right_id always_if_elim. Qed.
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
Proof. rewrite /FromPure /Frame=> ->. by rewrite always_if_elim right_id. Qed.
454

455
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q ⊣⊢ PQ.
456
457
458
459
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.
460
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
461
Proof. done. Qed.
462
463
464
465
466
467
468
469

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 /= => <- <- <-.
  rewrite {1}(always_sep_dup ( R)). solve_sep_entails.
Qed.
470
Global Instance frame_sep_l R P1 P2 Q Q' :
471
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
472
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
473
474
475
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.
476

477
478
479
480
481
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.
482
483
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  uPred M) R Q l l1 l2 :
  IsApp l l1 l2 
484
  Frame p R (([ list] k  y  l1, Φ k y) 
485
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
486
  Frame p R ([ list] k  y  l, Φ k y) Q.
487
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
488

489
490
491
492
493
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.
494
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
495
Proof. done. Qed.
496
497
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.
498
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
499
500
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.
501
502
503
504
505
506
507
508
509
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.
510
511
512
513
514
515
516
517
518
519
520

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.
521
Global Instance frame_or R P1 P2 Q1 Q2 Q :
522
523
  Frame false R P1 Q1  Frame false R P2 Q2  MakeOr Q1 Q2 Q 
  Frame false R (P1  P2) Q.
524
525
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

526
527
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
528
529
530
531
532
533
534
535
536
537
538
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.

539
540
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'.
541
Proof.
542
543
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
  by rewrite always_if_later later_sep.
544
545
546
547
548
549
550
551
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.

552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
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=>-> <- <-.
  by rewrite always_if_laterN laterN_sep.
Qed.

Class MakeAlways (P Q : uPred M) := make_always :  P ⊣⊢ Q.
Global Instance make_always_true : MakeAlways True True.
Proof. by rewrite /MakeAlways always_pure. Qed.
Global Instance make_always_default P : MakeAlways P ( P) | 100.
Proof. done. Qed.

Global Instance frame_always R P Q Q' :
  Frame true R P Q  MakeAlways Q Q'  Frame true R ( P) Q'.
567
Proof.
568
569
  rewrite /Frame /MakeAlways=> <- <-.
  by rewrite always_sep /= always_always.
570
571
Qed.

572
573
574
575
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.
576
577
Proof. done. Qed.

578
579
Global Instance frame_except_0 p R P Q Q' :
  Frame p R P Q  MakeExcept0 Q Q'  Frame p R ( P) Q'.
580
Proof.
581
  rewrite /Frame /MakeExcept0=><- <-.
582
  by rewrite except_0_sep -(except_0_intro (?p R)).
583
584
Qed.

585
586
Global Instance frame_exist {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
587
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
588
589
Global Instance frame_forall {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
590
591
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

592
Global Instance frame_bupd p R P Q : Frame p R P Q  Frame p R (|==> P) (|==> Q).
593
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
594

595
596
597
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. done. Qed.
598
Global Instance from_or_bupd P Q1 Q2 :
599
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
600
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
601
602
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
603
604
605
Global Instance from_or_always P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
606
607
Global Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
608
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
609
610
611
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.
612
613
614
615

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
616
617
618
619
620
Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoOr pure_or. Qed.
Global Instance into_or_always P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
621
622
623
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
624
625
626
Global Instance into_or_laterN n P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr (^n P) (^n Q1) (^n Q2).
Proof. rewrite /IntoOr=>->. by rewrite laterN_or. Qed.
627
628

(* FromExist *)
629
Global Instance from_exist_exist {A} (Φ : A  uPred M): FromExist ( a, Φ a) Φ.
630
Proof. done. Qed.
631
Global Instance from_exist_bupd {A} P (Φ : A  uPred M) :
632
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
633
634
635
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
636
637
638
639
640
641
642
643
Global Instance from_exist_pure {A} (φ : A  Prop) :
  @FromExist M A ⌜∃ x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
Global Instance from_exist_always {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply always_mono, exist_intro.
Qed.
644
645
Global Instance from_exist_later {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
646
647
648
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
Qed.
649
650
651
652
653
Global Instance from_exist_laterN {A} n P (Φ : A  uPred M) :
  FromExist P Φ  FromExist (^n P) (λ a, ^n (Φ a))%I.
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply laterN_mono, exist_intro.
Qed.
654
655
656
657

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  uPred M) : IntoExist ( a, Φ a) Φ.
Proof. done. Qed.
658
659
660
Global Instance into_exist_pure {A} (φ : A  Prop) :
  @IntoExist M A ⌜∃ x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
661
662
663
Global Instance into_exist_always {A} P (Φ : A  uPred M) :
  IntoExist P Φ  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
664
665
666
667
668
669
Global Instance into_exist_later {A} P (Φ : A  uPred M) :
  IntoExist P Φ  Inhabited A  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
Global Instance into_exist_laterN {A} n P (Φ : A  uPred M) :
  IntoExist P Φ  Inhabited A  IntoExist (^n P) (λ a, ^n (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
670

671
672
673
674
675
676
677
(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A  uPred M) : IntoForall ( a, Φ a) Φ.
Proof. done. Qed.
Global Instance into_forall_always {A} P (Φ : A  uPred M) :
  IntoForall P Φ  IntoForall ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.

678
679
(* FromModal *)
Global Instance from_modal_later P : FromModal ( P) P.
680
Proof. apply later_intro. Qed.
681
Global Instance from_modal_bupd P : FromModal (|==> P) P.
682
Proof. apply bupd_intro. Qed.
683
Global Instance from_modal_except_0 P : FromModal ( P) P.
684
685
686
Proof. apply except_0_intro. Qed.

(* ElimModal *)
687
Global Instance elim_modal_wand P P' Q Q' R :
688
  ElimModal P P' Q Q'  ElimModal P P' (R - Q) (R - Q').
689
690
691
692
693
694
695
696
697
698
Proof.
  rewrite /ElimModal=> H. apply wand_intro_r.
  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
Qed.
Global Instance forall_modal_wand {A} P P' (Φ Ψ : A  uPred M) :
  ( x, ElimModal P P' (Φ x) (Ψ x))  ElimModal P P' ( x, Φ x) ( x, Ψ x).
Proof.
  rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
699
700
701
Global Instance elim_modal_always P Q : ElimModal ( P) P Q Q.
Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.

702
703
704
705
706
Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.

Global Instance elim_modal_except_0 P Q : IsExcept0 Q  ElimModal ( P) P Q Q.
Proof.
707
  intros. rewrite /ElimModal (except_0_intro (_ - _)).
708
709
710
711
712
  by rewrite -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_timeless_bupd P Q :
  TimelessP P  IsExcept0 Q  ElimModal ( P) P Q Q.
Proof.
713
  intros. rewrite /ElimModal (except_0_intro (_ - _)) (timelessP P).
714
715
  by rewrite -except_0_sep wand_elim_r.
Qed.
716
717
718
719
720
721
Global Instance elim_modal_timeless_bupd' p P Q :
  TimelessP P  IsExcept0 Q  ElimModal (?p P) P Q Q.
Proof.
  destruct p; simpl; auto using elim_modal_timeless_bupd.
  intros _ _. by rewrite /ElimModal wand_elim_r.
Qed.
722

723
724
725
726
727
Global Instance is_except_0_except_0 P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
Global Instance is_except_0_later P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_later. Qed.
Global Instance is_except_0_bupd P : IsExcept0 P  IsExcept0 (|==> P).
728
Proof.
729
730
  rewrite /IsExcept0=> HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
731
Qed.
732
End classes.