class_instances.v 32.8 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
Global Instance from_pure_later P φ : FromPure P φ  FromPure ( P)%I φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed.

130 131 132 133 134 135 136 137 138 139 140
(* 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 *)
141
Global Instance into_laterN_later n P Q :
142 143 144
  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.
145
Proof. done. Qed.
146
Global Instance into_laterN_laterN_plus n m P Q :
147 148
  IntoLaterN m P Q  IntoLaterN' (n + m) (^n P) Q.
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
149

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

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

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

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

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

241 242 243 244 245 246 247 248 249 250 251 252
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.

253
(* IntoWand *)
254 255
Global Instance wand_weaken_assumption p P1 P2 Q :
  FromAssumption p P2 P1  WandWeaken p P1 Q P2 Q | 0.
256
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
257 258
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
259
Proof.
260 261
  rewrite /WandWeaken' /WandWeaken=> ->.
  by rewrite always_if_later -later_wand -later_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
Qed.
263 264
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
265
Proof.
266 267
  rewrite /WandWeaken' /WandWeaken=> ->.
  by rewrite always_if_laterN -laterN_wand -laterN_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Qed.
269 270
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
271 272
Proof.
  rewrite /WandWeaken' /WandWeaken=> ->.
273
  apply wand_intro_l. by rewrite always_if_elim bupd_wand_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
274 275
Qed.

276 277
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
278
Proof. done. Qed.
279 280
Global Instance into_wand_impl p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
281 282
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand. Qed.

283 284
Global Instance into_wand_iff_l p P P' Q Q' :
  WandWeaken p P Q P' Q'  IntoWand p (P  Q) P' Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand. Qed.
286 287
Global Instance into_wand_iff_r p P P' Q Q' :
  WandWeaken p Q P Q' P'  IntoWand p (P  Q) Q' P'.
Robbert Krebbers's avatar
Robbert Krebbers committed
288
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
289

290 291
Global Instance into_wand_forall {A} p (Φ : A  uPred M) P Q x :
  IntoWand p (Φ x) P Q  IntoWand p ( x, Φ x) P Q.
292
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
293 294
Global Instance into_wand_always p R P Q :
  IntoWand p R P Q  IntoWand p ( R) P Q.
295
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
296

297 298 299 300 301 302 303
Global Instance into_wand_later p R P Q :
  IntoWand p R P Q  IntoWand p ( R) ( P) ( Q).
Proof. rewrite /IntoWand=> ->. by rewrite always_if_later -later_wand. Qed.
Global Instance into_wand_laterN p n R P Q :
  IntoWand p R P Q  IntoWand p (^n R) (^n P) (^n Q).
Proof. rewrite /IntoWand=> ->. by rewrite always_if_laterN -laterN_wand. Qed.

304
Global Instance into_wand_bupd R P Q :
305
  IntoWand false R P Q  IntoWand false (|==> R) (|==> P) (|==> Q).
306
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
308
Qed.
309 310 311 312 313
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.
314 315

(* FromAnd *)
316 317 318 319
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.
320 321
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
322
  PersistentP P1  FromAnd true (P1  P2) P1 P2 | 9.
323 324
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
325
  PersistentP P2  FromAnd true (P1  P2) P1 P2 | 10.
326
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342

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.

343 344
Global Instance from_sep_ownM (a b1 b2 : M) :
  FromOp a b1 b2 
345 346
  FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromAnd -ownM_op from_op. Qed.
347 348 349 350 351 352 353
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.
354

355
Global Instance from_sep_bupd P Q1 Q2 :
356 357 358
  FromAnd false P Q1 Q2  FromAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.

359 360 361 362 363 364 365 366
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.

367 368
Global Instance from_and_big_sepL_app {A} (Φ : nat  A  uPred M) l1 l2 :
  FromAnd false ([ list] k  y  l1 ++ l2, Φ k y)
369
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
370
Proof. by rewrite /FromAnd big_opL_app. Qed.
371 372 373 374 375
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.
376

377 378 379
(* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a  b) a b.
Proof. by rewrite /FromOp. Qed.
380 381 382

(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
383
Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
384
  FromOp a b1 b2  FromOp a' b1' b2'  FromOp (a,a') (b1,b1') (b2,b2').
385
Proof. by constructor. Qed.
386 387 388 389 390 391 392
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.

393 394 395 396
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.

397 398 399
(* IntoOp *)
Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a  b) a b.
Proof. by rewrite /IntoOp. Qed.
400

401 402 403 404
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.
405 406 407 408 409 410 411
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.

412 413 414 415
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.

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

424
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
425
Proof. done. Qed.
426 427 428 429 430 431 432
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.

433 434 435 436 437 438 439
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.
440 441 442
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.
443 444 445
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.
446

447 448 449 450 451 452 453 454
(* 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.
455 456 457
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)
458
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
459
Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
460 461

(* Frame *)
462 463 464 465
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.
466

467
Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q  PQ.
468 469 470 471
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.
472
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
473
Proof. done. Qed.
474 475 476 477 478 479 480 481

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.
482
Global Instance frame_sep_l R P1 P2 Q Q' :
483
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
484
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
485 486 487
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.
488

489 490 491 492 493
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.
494 495
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  uPred M) R Q l l1 l2 :
  IsApp l l1 l2 
496
  Frame p R (([ list] k  y  l1, Φ k y) 
497
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
498
  Frame p R ([ list] k  y  l, Φ k y) Q.
499
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
500

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

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.
533
Global Instance frame_or R P1 P2 Q1 Q2 Q :
534 535
  Frame false R P1 Q1  Frame false R P2 Q2  MakeOr Q1 Q2 Q 
  Frame false R (P1  P2) Q.
536 537
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

538 539
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
540 541 542 543 544 545 546 547 548 549 550
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.

551 552
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'.
553
Proof.
554 555
  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
  by rewrite always_if_later later_sep.
556 557 558 559 560 561 562 563
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.

564 565 566 567 568 569 570 571 572 573 574 575 576 577 578
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'.
579
Proof.
580 581
  rewrite /Frame /MakeAlways=> <- <-.
  by rewrite always_sep /= always_always.
582 583
Qed.

584 585 586 587
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.
588 589
Proof. done. Qed.

590 591
Global Instance frame_except_0 p R P Q Q' :
  Frame p R P Q  MakeExcept0 Q Q'  Frame p R ( P) Q'.
592
Proof.
593
  rewrite /Frame /MakeExcept0=><- <-.
594
  by rewrite except_0_sep -(except_0_intro (?p R)).
595 596
Qed.

597 598
Global Instance frame_exist {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
599
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
600 601
Global Instance frame_forall {A} p R (Φ Ψ : A  uPred M) :
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
602 603
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

604
Global Instance frame_bupd p R P Q : Frame p R P Q  Frame p R (|==> P) (|==> Q).
605
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
606

607 608 609
(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. done. Qed.
610
Global Instance from_or_bupd P Q1 Q2 :
611
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
612
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
613 614
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
615 616 617
Global Instance from_or_always P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
618 619
Global Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
620
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
621 622 623
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.
624 625 626 627

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
628 629 630 631 632
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.
633 634 635
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
636 637 638
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.
639 640

(* FromExist *)
641
Global Instance from_exist_exist {A} (Φ : A  uPred M): FromExist ( a, Φ a) Φ.
642
Proof. done. Qed.
643
Global Instance from_exist_bupd {A} P (Φ : A  uPred M) :
644
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
645 646 647
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
648 649 650 651 652 653 654 655
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.
656 657
Global Instance from_exist_later {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.