class_instances.v 32.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 /= ?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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
251 252 253 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
Global Instance wand_weaken_exact P Q : WandWeaken P Q P Q.
Proof. done. Qed.
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.
283

284 285 286
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.
287 288
Global Instance into_wand_always R P Q : IntoWand R P Q  IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
289

Robbert Krebbers's avatar
Robbert Krebbers committed
290 291 292 293 294 295
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.
296
Global Instance into_wand_bupd R P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  IntoWand R P Q  IntoWand (|==> R) (|==> P) (|==> Q).
298
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
300
Qed.
301 302

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

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.

330 331
Global Instance from_sep_ownM (a b1 b2 : M) :
  FromOp a b1 b2 
332 333
  FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromAnd -ownM_op from_op. Qed.
334 335 336 337 338 339 340
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.
341

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

346 347 348 349 350 351 352 353
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.

354 355
Global Instance from_and_big_sepL_app {A} (Φ : nat  A  uPred M) l1 l2 :
  FromAnd false ([ list] k  y  l1 ++ l2, Φ k y)
356
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
357
Proof. by rewrite /FromAnd big_opL_app. Qed.
358 359 360 361 362
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.
363

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

(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
370
Global Instance from_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
371
  FromOp a b1 b2  FromOp a' b1' b2'  FromOp (a,a') (b1,b1') (b2,b2').
372
Proof. by constructor. Qed.
373 374 375 376 377 378 379
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.

380 381 382 383
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.

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

388 389 390 391
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.
392 393 394 395 396 397 398
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.

399 400 401 402
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.

403
(* IntoAnd *)
404
Global Instance into_and_sep p P Q : IntoAnd p (P  Q) P Q.
405 406
Proof. by apply mk_into_and_sep. Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
407
  IntoOp a b1 b2 
408 409
  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.
410

411
Global Instance into_and_and P Q : IntoAnd true (P  Q) P Q.
412
Proof. done. Qed.
413 414 415 416 417 418 419
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.

420 421 422 423 424 425 426
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.
427 428 429
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.
430 431 432
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.
433

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

(* Frame *)
449 450 451 452
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.
453

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

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

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

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

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

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

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

551 552 553 554 555 556 557 558 559 560 561 562 563 564 565
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'.
566
Proof.
567 568
  rewrite /Frame /MakeAlways=> <- <-.
  by rewrite always_sep /= always_always.
569 570
Qed.

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

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

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

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

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

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. done. Qed.
615 616 617 618 619
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.
620 621 622
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
623 624 625
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.
626 627

(* FromExist *)
628
Global Instance from_exist_exist {A} (Φ : A  uPred M): FromExist ( a, Φ a) Φ.
629
Proof. done. Qed.
630
Global Instance from_exist_bupd {A} P (Φ : A  uPred M) :
631
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
632 633 634
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
635 636 637 638 639 640 641 642
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.
643 644
Global Instance from_exist_later {A} P (Φ : A  uPred M) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
645 646 647
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
Qed.
648 649 650 651 652
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.
653 654 655 656

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  uPred M) : IntoExist ( a, Φ a) Φ.
Proof. done. Qed.
657 658 659
Global Instance into_exist_pure {A} (φ : A  Prop) :
  @IntoExist M A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
660 661 662
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.
663 664 665 666 667 668
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.
669

670 671 672 673 674 675 676
(* 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.

677 678
(* FromModal *)
Global Instance from_modal_later P : FromModal ( P) P.
679
Proof. apply later_intro. Qed.
680
Global Instance from_modal_bupd P :