class_instances.v 17.3 KB
Newer Older
1
From iris.proofmode Require Export classes.
2 3
From iris.algebra Require Import gmap.
From iris.base_logic Require Import big_op.
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Import uPred.

Section classes.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.

(* FromAssumption *)
Global Instance from_assumption_exact p P : FromAssumption p P P.
Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
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.
Global Instance from_assumption_always_r P Q :
  FromAssumption true P Q  FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
19
Global Instance from_assumption_bupd p P Q :
20
  FromAssumption p P Q  FromAssumption p P (|==> Q)%I.
21
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
22 23 24 25 26 27 28

(* IntoPure *)
Global Instance into_pure_pure φ : @IntoPure M ( φ) φ.
Proof. done. Qed.
Global Instance into_pure_eq {A : cofeT} (a b : A) :
  Timeless a  @IntoPure M (a  b) (a  b).
Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
29 30
Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
  @IntoPure M ( a) ( a).
31 32 33 34
Proof. by rewrite /IntoPure discrete_valid. Qed.

(* FromPure *)
Global Instance from_pure_pure φ : @FromPure M ( φ) φ.
35
Proof. done. Qed.
36 37 38 39 40
Global Instance from_pure_internal_eq {A : cofeT} (a b : A) :
  @FromPure M (a  b) (a  b).
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply internal_eq_refl'.
Qed.
41 42
Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
  @FromPure M ( a) ( a).
43 44
Proof.
  rewrite /FromPure. eapply pure_elim; [done|]=> ?.
45
  rewrite -cmra_valid_intro //. auto with I.
46
Qed.
47
Global Instance from_pure_bupd P φ : FromPure P φ  FromPure (|==> P) φ.
48
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71

(* 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 *)
Global Instance into_later_default P : IntoLater P P | 1000.
Proof. apply later_intro. Qed.
Global Instance into_later_later P : IntoLater ( P) P.
Proof. done. Qed.
Global Instance into_later_and P1 P2 Q1 Q2 :
  IntoLater P1 Q1  IntoLater P2 Q2  IntoLater (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
Global Instance into_later_or P1 P2 Q1 Q2 :
  IntoLater P1 Q1  IntoLater P2 Q2  IntoLater (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
Global Instance into_later_sep P1 P2 Q1 Q2 :
72
  IntoLater P1 Q1  IntoLater P2 Q2  IntoLater (P1  P2) (Q1  Q2).
73 74 75 76 77
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.

Global Instance into_later_big_sepM `{Countable K} {A}
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
  ( x k, IntoLater (Φ k x) (Ψ k x)) 
78
  IntoLater ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
79 80 81 82 83 84
Proof.
  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
Qed.
Global Instance into_later_big_sepS `{Countable A}
    (Φ Ψ : A  uPred M) (X : gset A) :
  ( x, IntoLater (Φ x) (Ψ x)) 
85
  IntoLater ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
86 87 88 89 90 91 92 93 94 95 96 97 98 99
Proof.
  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
Qed.

(* FromLater *)
Global Instance from_later_later P : FromLater ( P) P.
Proof. done. Qed.
Global Instance from_later_and P1 P2 Q1 Q2 :
  FromLater P1 Q1  FromLater P2 Q2  FromLater (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
Global Instance from_later_or P1 P2 Q1 Q2 :
  FromLater P1 Q1  FromLater P2 Q2  FromLater (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
Global Instance from_later_sep P1 P2 Q1 Q2 :
100
  FromLater P1 Q1  FromLater P2 Q2  FromLater (P1  P2) (Q1  Q2).
101 102 103
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.

(* IntoWand *)
104
Global Instance into_wand_wand P Q Q' :
105
  FromAssumption false Q Q'  IntoWand (P - Q) P Q'.
106 107 108 109
Proof. by rewrite /FromAssumption /IntoWand /= => ->. Qed.
Global Instance into_wand_impl P Q Q' :
  FromAssumption false Q Q'  IntoWand (P  Q) P Q'.
Proof. rewrite /FromAssumption /IntoWand /= => ->. by rewrite impl_wand. Qed.
110 111 112 113 114 115
Global Instance into_wand_iff_l P Q : IntoWand (P  Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance into_wand_iff_r P Q : IntoWand (P  Q) Q P.
Proof. apply and_elim_r', impl_wand. Qed.
Global Instance into_wand_always R P Q : IntoWand R P Q  IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
116
Global Instance into_wand_bupd R P Q :
117
  IntoWand R P Q  IntoWand R (|==> P) (|==> Q) | 100.
118
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_wand_r. Qed.
119 120 121 122 123

(* FromAnd *)
Global Instance from_and_and P1 P2 : FromAnd (P1  P2) P1 P2.
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
124
  PersistentP P1  FromAnd (P1  P2) P1 P2 | 9.
125 126
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
127
  PersistentP P2  FromAnd (P1  P2) P1 P2 | 10.
128 129 130 131 132 133 134 135 136
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
Global Instance from_and_always P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
Global Instance from_and_later P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.

(* FromSep *)
137
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
138
Proof. done. Qed.
139 140 141 142
Global Instance from_sep_ownM (a b1 b2 : M) :
  FromOp a b1 b2 
  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromSep -ownM_op from_op. Qed.
143 144 145 146 147 148
Global Instance from_sep_always P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
Global Instance from_sep_later P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
149
Global Instance from_sep_bupd P Q1 Q2 :
150
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
151
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
152 153 154 155

Global Instance from_sep_big_sepM
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) m :
  ( k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
156 157
  FromSep ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
158 159 160 161 162
Proof.
  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
Qed.
Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) X :
  ( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) 
163
  FromSep ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
164 165 166 167
Proof.
  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
Qed.

168 169 170 171 172 173 174 175 176 177 178 179 180 181
(* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a  b) a b.
Proof. by rewrite /FromOp. Qed.
Global Instance from_op_persistent {A : cmraT} (a : A) :
  Persistent a  FromOp a a a.
Proof. intros. by rewrite /FromOp -(persistent_dup a). Qed.
Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
  FromOp a b1 b2  FromOp a' b1' b2' 
  FromOp (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
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.

182 183 184 185 186 187 188 189 190 191 192 193 194 195
(* IntoOp *)
Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a  b) a b.
Proof. by rewrite /IntoOp. Qed.
Global Instance into_op_persistent {A : cmraT} (a : A) :
  Persistent a  IntoOp a a a.
Proof. intros; apply (persistent_dup a). Qed.
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.
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.

196
(* IntoAnd *)
197
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
198 199
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
200
  IntoOp a b1 b2 
201 202
  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.
203

204
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
205
Proof. done. Qed.
206 207 208 209 210 211 212 213 214 215 216 217
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.

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.

Global Instance into_and_big_sepM
218
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) p m :
219
  ( k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
220 221
  IntoAnd p ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
222
Proof.
223
  rewrite /IntoAnd=> HΦ. destruct p.
224 225 226 227
  - apply and_intro; apply big_sepM_mono; auto.
    + intros k x ?. by rewrite HΦ and_elim_l.
    + intros k x ?. by rewrite HΦ and_elim_r.
  - rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
228
Qed.
229 230
Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) p X :
  ( x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) 
231
  IntoAnd p ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
232
Proof.
233
  rewrite /IntoAnd=> HΦ. destruct p.
234 235 236 237
  - apply and_intro; apply big_sepS_mono; auto.
    + intros x ?. by rewrite HΦ and_elim_l.
    + intros x ?. by rewrite HΦ and_elim_r.
  - rewrite -big_sepS_sepS. apply big_sepS_mono; auto.
238 239 240 241 242
Qed.

(* Frame *)
Global Instance frame_here R : Frame R R True.
Proof. by rewrite /Frame right_id. Qed.
243 244
Global Instance frame_here_pure φ Q : FromPure Q φ  Frame ( φ) Q True.
Proof. rewrite /FromPure /Frame=> ->. by rewrite right_id. Qed.
245

246
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
247 248 249 250
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.
251
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
252 253
Proof. done. Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
254
  Frame R P1 Q  MakeSep Q P2 Q'  Frame R (P1  P2) Q' | 9.
255 256
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
Global Instance frame_sep_r R P1 P2 Q Q' :
257
  Frame R P2 Q  MakeSep P1 Q Q'  Frame R (P1  P2) Q' | 10.
258
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
259 260 261 262 263 264

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.
265
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285
Proof. done. Qed.
Global Instance frame_and_l R P1 P2 Q Q' :
  Frame R P1 Q  MakeAnd Q P2 Q'  Frame R (P1  P2) Q' | 9.
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
Global Instance frame_and_r R P1 P2 Q Q' :
  Frame R P2 Q  MakeAnd P1 Q Q'  Frame R (P1  P2) Q' | 10.
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.
Global Instance frame_or R P1 P2 Q1 Q2 Q :
  Frame R P1 Q1  Frame R P2 Q2  MakeOr Q1 Q2 Q  Frame R (P1  P2) Q.
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

Global Instance frame_wand R P1 P2 Q2 :
286
  Frame R P2 Q2  Frame R (P1 - P2) (P1 - Q2).
287 288 289 290 291 292 293 294 295 296 297
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.

298
Global Instance frame_later R R' P Q Q' :
299
  IntoLater R' R  Frame R P Q  MakeLater Q Q'  Frame R' ( P) Q'.
300
Proof.
301
  rewrite /Frame /MakeLater /IntoLater=>-> <- <-. by rewrite later_sep.
302 303
Qed.

304 305 306 307
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.
308 309
Proof. done. Qed.

310 311
Global Instance frame_except_0 R P Q Q' :
  Frame R P Q  MakeExcept0 Q Q'  Frame R ( P) Q'.
312
Proof.
313 314
  rewrite /Frame /MakeExcept0=><- <-.
  by rewrite except_0_sep -(except_0_intro R).
315 316
Qed.

317 318 319 320 321 322 323
Global Instance frame_exist {A} R (Φ Ψ : A  uPred M) :
  ( a, Frame R (Φ a) (Ψ a))  Frame R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
Global Instance frame_forall {A} R (Φ Ψ : A  uPred M) :
  ( a, Frame R (Φ a) (Ψ a))  Frame R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

324
Global Instance frame_bupd R P Q : Frame R P Q  Frame R (|==> P) (|==> Q).
325
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
326

327 328 329
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. done. Qed.
330
Global Instance from_or_bupd P Q1 Q2 :
331
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
332
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
333 334 335 336 337 338 339 340 341

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.

(* FromExist *)
342
Global Instance from_exist_exist {A} (Φ : A  uPred M): FromExist ( a, Φ a) Φ.
343
Proof. done. Qed.
344
Global Instance from_exist_bupd {A} P (Φ : A  uPred M) :
345
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
346 347 348
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
349 350 351
Global Instance from_exist_later {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro. Qed.
352 353 354 355 356 357 358 359 360 361

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  uPred M) : IntoExist ( a, Φ a) Φ.
Proof. done. Qed.
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_always {A} P (Φ : A  uPred M) :
  IntoExist P Φ  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
362

363 364 365 366 367 368 369 370 371
(* IntoModal *)
Global Instance into_modal_later P : IntoModal P ( P).
Proof. apply later_intro. Qed.
Global Instance into_modal_bupd P : IntoModal P (|==> P).
Proof. apply bupd_intro. Qed.
Global Instance into_modal_except_0 P : IntoModal P ( P).
Proof. apply except_0_intro. Qed.

(* ElimModal *)
372
Global Instance elim_modal_wand P P' Q Q' R :
373
  ElimModal P P' Q Q'  ElimModal P P' (R - Q) (R - Q').
374 375 376 377 378 379 380 381 382 383
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.

384 385 386
Global Instance elim_modal_always P Q : ElimModal ( P) P Q Q.
Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.

387 388 389 390 391
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.
392
  intros. rewrite /ElimModal (except_0_intro (_ - _)).
393 394 395 396 397
  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.
398
  intros. rewrite /ElimModal (except_0_intro (_ - _)) (timelessP P).
399 400
  by rewrite -except_0_sep wand_elim_r.
Qed.
401

402 403 404 405 406
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).
407
Proof.
408 409
  rewrite /IsExcept0=> HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
410
Qed.
411
End classes.