class_instances.v 44.9 KB
Newer Older
1
From stdpp Require Import nat_cancel.
2 3 4
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import base modality_instances classes.
From iris.proofmode Require Import ltac_tactics.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7
Import bi.

Robbert Krebbers's avatar
Robbert Krebbers committed
8
(* FIXME(Coq #6294): needs new unification *)
9 10 11 12 13 14
(** The lemma [from_assumption_exact is not an instance, but defined using
[notypeclasses refine] through [Hint Extern] to enable the better unification
algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
by [refine], which otherwise causes TC search to fail. Such unshelved goals are
created for example when solving [FromAssumption p ?P ?Q] where both [?P] and
[?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example. *)
15 16 17
Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Hint Extern 0 (FromAssumption _ _ _) =>
18
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
19

Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22 23 24 25 26 27 28
(* FIXME(Coq #6294): needs new unification *)
(** Similarly, the lemma [from_exist_exist] is defined using a [Hint Extern] to
enable the better unification algorithm.
See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
Lemma from_exist_exist {PROP : bi} {A} (Φ : A  PROP) : FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Hint Extern 0 (FromExist _ _) =>
  notypeclasses refine (from_exist_exist _) : typeclass_instances.

29
Section class_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31
Context {PROP : bi}.
Implicit Types P Q R : PROP.
32
Implicit Types mP : option PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
33

34
(** AsEmpValid *)
35
Global Instance as_emp_valid_emp_valid P : AsEmpValid0 ( P) P | 0.
36
Proof. by rewrite /AsEmpValid. Qed.
37
Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P  Q) (P - Q).
38
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
39
Global Instance as_emp_valid_equiv P Q : AsEmpValid0 (P  Q) (P - Q).
40 41 42 43 44 45 46 47 48
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.

Global Instance as_emp_valid_forall {A : Type} (φ : A  Prop) (P : A  PROP) :
  ( x, AsEmpValid (φ x) (P x))  AsEmpValid ( x, φ x) ( x, P x).
Proof.
  rewrite /AsEmpValid=>H1. split=>H2.
  - apply bi.forall_intro=>?. apply H1, H2.
  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
Qed.
49 50 51 52 53 54
Global Instance as_emp_valid_tforall {TT : tele} (φ : TT  Prop) (P : TT  PROP) :
  ( x, AsEmpValid (φ x) (P x))  AsEmpValid (.. x, φ x) (.. x, P x).
Proof.
  rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
  apply as_emp_valid_forall.
Qed.
55

56
(** FromAffinely *)
57 58
Global Instance from_affinely_affine P : Affine P  FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
59
Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
60
Proof. by rewrite /FromAffinely. Qed.
61 62 63
Global Instance from_affinely_intuitionistically P :
  FromAffinely ( P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.
64

65
(** IntoAbsorbingly *)
66 67 68 69
Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
Global Instance into_absorbingly_absorbing P : Absorbing P  IntoAbsorbingly P P | 1.
Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
70
Global Instance into_absorbingly_intuitionistically P :
71
  IntoAbsorbingly (<pers> P) ( P) | 2.
72 73 74
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
75
Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
76
Proof. by rewrite /IntoAbsorbingly. Qed.
77

78
(** FromAssumption *)
79
Global Instance from_assumption_persistently_r P Q :
80
  FromAssumption true P Q  KnownRFromAssumption true P (<pers> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof.
82
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
83
  apply intuitionistically_persistent.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Qed.
85
Global Instance from_assumption_affinely_r P Q :
86
  FromAssumption true P Q  KnownRFromAssumption true P (<affine> Q).
87 88 89 90
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_idemp.
Qed.
91 92 93 94 95 96
Global Instance from_assumption_intuitionistically_r P Q :
  FromAssumption true P Q  KnownRFromAssumption true P ( Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_idemp.
Qed.
97
Global Instance from_assumption_absorbingly_r p P Q :
98
  FromAssumption p P Q  KnownRFromAssumption p P (<absorb> Q).
99 100 101 102
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply absorbingly_intro.
Qed.
103

104
Global Instance from_assumption_intuitionistically_l p P Q :
105 106 107
  FromAssumption true P Q  KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
108
  by rewrite intuitionistically_if_elim.
109
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Global Instance from_assumption_persistently_l_true P Q :
111
  FromAssumption true P Q  KnownLFromAssumption true (<pers> P) Q.
112 113
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
114
  rewrite intuitionistically_persistently_elim //.
115
Qed.
116
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
117
  FromAssumption true P Q  KnownLFromAssumption false (<pers> P) Q.
118 119
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
120
  by rewrite intuitionistically_into_persistently.
121
Qed.
122
Global Instance from_assumption_affinely_l_true p P Q :
123
  FromAssumption p P Q  KnownLFromAssumption p (<affine> P) Q.
124 125 126 127
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_elim.
Qed.
128 129 130 131 132 133
Global Instance from_assumption_intuitionistically_l_true p P Q :
  FromAssumption p P Q  KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_elim.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
136 137 138 139 140
  FromAssumption p (Φ x) Q  KnownLFromAssumption p ( x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite forall_elim.
Qed.
141 142 143 144 145 146
Global Instance from_assumption_tforall {TT : tele} p (Φ : TT  PROP) Q x :
  FromAssumption p (Φ x) Q  KnownLFromAssumption p (.. x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite bi_tforall_forall forall_elim.
Qed.
147

148
(** IntoPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
149 150 151
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Ralf Jung's avatar
Ralf Jung committed
152
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
153
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
154
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
155
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
156
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
157
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
158
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
159 160
  FromPure false P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163 164

Global Instance into_pure_exist {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
165 166 167
Global Instance into_pure_texist {TT : tele} (Φ : TT  PROP) (φ : TT  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure (.. x, Φ x) (.. x, φ x).
Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170
Global Instance into_pure_forall {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
171 172 173 174 175
Global Instance into_pure_tforall {TT : tele} (Φ : TT  PROP) (φ : TT  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure (.. x, Φ x) (.. x, φ x).
Proof.
  rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177 178 179

Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.
180 181
Global Instance into_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
182
Proof.
183 184 185
  rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
  apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //.
  by rewrite -affinely_affinely_if affinely_True_emp affinely_emp left_id.
186
Qed.
187

188
Global Instance into_pure_affinely P φ : IntoPure P φ  IntoPure (<affine> P) φ.
189
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
190 191 192
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.
193
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (<absorb> P) φ.
194 195
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
196
  IntoPure P φ  IntoPure (<pers> P) φ.
197
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
198

199
(** FromPure *)
200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
Global Instance from_pure_emp : @FromPure PROP true emp True.
Proof. rewrite /FromPure /=. apply (affine _). Qed.
Global Instance from_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
Proof. by rewrite /FromPure /=. Qed.
Global Instance from_pure_pure_and a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1  FromPure a2 P2 φ2 
  FromPure (if a1 then true else a2) (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure pure_and=> <- <- /=. rewrite affinely_if_and.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
Global Instance from_pure_pure_or a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1  FromPure a2 P2 φ2 
  FromPure (if a1 then true else a2) (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure pure_or=> <- <- /=. rewrite affinely_if_or.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
218 219 220 221 222 223 224 225 226 227 228 229 230
Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  FromPure a P2 φ2  FromPure a (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure /IntoPure pure_impl=> -> <-. destruct a=>//=.
  apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
Qed.

Global Instance from_pure_exist {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
  by setoid_rewrite Hx.
Qed.
231 232 233
Global Instance from_pure_texist {TT : tele} a (Φ : TT  PROP) (φ : TT  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a (.. x, Φ x) (.. x, φ x).
Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
234 235 236 237 238 239
Global Instance from_pure_forall {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
  destruct a=>//=. apply affinely_forall.
Qed.
240 241 242 243 244
Global Instance from_pure_tforall {TT : tele} a (Φ : TT  PROP) (φ : TT  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a (.. x, Φ x) (.. x, φ x).
Proof.
  rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
Qed.
245

246 247 248
Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1  FromPure a2 P2 φ2 
  FromPure (if a1 then a2 else false) (P1  P2) (φ1  φ2).
249
Proof.
250 251 252
  rewrite /FromPure=> <- <-. destruct a1; simpl.
  - by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
253
Qed.
254 255 256 257
Global Instance from_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  FromPure a P2 φ2 
  TCOr (TCEq a false) (Affine P1) 
  FromPure a (P1 - P2) (φ1  φ2).
258
Proof.
259 260 261 262 263 264
  rewrite /FromPure /IntoPure=> HP1 <- Ha /=. apply wand_intro_l.
  destruct a; simpl.
  - destruct Ha as [Ha|?]; first inversion Ha.
    rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
    by rewrite affinely_and_l pure_impl impl_elim_r.
  - by rewrite HP1 sep_and pure_impl impl_elim_r.
265 266
Qed.

267
Global Instance from_pure_persistently P a φ :
268
  FromPure true P φ  FromPure a (<pers> P) φ.
269 270
Proof.
  rewrite /FromPure=> <- /=.
Ralf Jung's avatar
Ralf Jung committed
271
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
272
Qed.
273 274 275 276 277
Global Instance from_pure_affinely_true a P φ :
  FromPure a P φ  FromPure true (<affine> P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite -affinely_affinely_if affinely_idemp. Qed.
Global Instance from_pure_intuitionistically_true a P φ :
  FromPure a P φ  FromPure true ( P) φ.
278
Proof.
279 280 281
  rewrite /FromPure=><- /=.
  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
  by rewrite intuitionistic_intuitionistically.
282
Qed.
283 284
Global Instance from_pure_absorbingly a P φ :
  FromPure a P φ  FromPure false (<absorb> P) φ.
285
Proof.
286 287
  rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
  by rewrite -persistent_absorbingly_affinely_2.
288
Qed.
289

290
(** IntoPersistent *)
291
Global Instance into_persistent_persistently p P Q :
292
  IntoPersistent true P Q  IntoPersistent p (<pers> P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294 295 296
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
297
Global Instance into_persistent_affinely p P Q :
298
  IntoPersistent p P Q  IntoPersistent p (<affine> P) Q | 0.
299
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
300
Global Instance into_persistent_intuitionistically p P Q :
301 302 303 304 305
  IntoPersistent true P Q  IntoPersistent p ( P) Q | 0.
Proof.
  rewrite /IntoPersistent /= =><-.
  destruct p; simpl;
    eauto using persistently_mono, intuitionistically_elim,
Ralf Jung's avatar
Ralf Jung committed
306
    intuitionistically_into_persistently_1.
307
Qed.
308
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof. by rewrite /IntoPersistent. Qed.
310 311
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
312
Proof. intros. by rewrite /IntoPersistent. Qed.
313

314
(** FromModal *)
315
Global Instance from_modal_affinely P :
316
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
317 318 319
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
320
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
321
Proof. by rewrite /FromModal. Qed.
322 323
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
324
Proof. by rewrite /FromModal. Qed.
325
Global Instance from_modal_intuitionistically_affine_bi P :
326
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
327 328 329
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
330

331
Global Instance from_modal_absorbingly P :
332
  FromModal modality_id (<absorb> P) (<absorb> P) P.
333 334
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

335
(** IntoWand *)
336 337 338 339 340 341 342 343 344 345
Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P - Q) P' Q'  IntoWand p q (P - Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_impl' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P  Q) P' Q'  IntoWand p q (P  Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_wandM' p q mP (Q P' Q' : PROP) :
  IntoWand' p q (mP -? Q) P' Q'  IntoWand p q (mP -? Q) P' Q' | 100.
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
346 347
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
348
Proof.
349
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
Qed.
351 352
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
353 354
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
355
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
356 357 358
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
359
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
360
  IntoWand false true (P'  Q) P Q.
361
Proof.
362
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
363 364
  rewrite -(intuitionistically_idemp P) HP.
  by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
365
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
Global Instance into_wand_impl_true_false P Q P' :
367
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
368
  IntoWand true false (P'  Q) P Q.
369
Proof.
370
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
371
  rewrite HP sep_and intuitionistically_elim impl_elim_l //.
372
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
373 374
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
375
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
377
  rewrite sep_and [( (_  _))%I]intuitionistically_elim impl_elim_r //.
378
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
379

380
Global Instance into_wand_wandM p q mP' P Q :
381
  FromAssumption q P (default emp%I mP')  IntoWand p q (mP' -? Q) P Q.
382 383
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
384 385 386 387 388 389 390
Global Instance into_wand_and_l p q R1 R2 P' Q' :
  IntoWand p q R1 P' Q'  IntoWand p q (R1  R2) P' Q'.
Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_l. Qed.
Global Instance into_wand_and_r p q R1 R2 P' Q' :
  IntoWand p q R2 Q' P'  IntoWand p q (R1  R2) Q' P'.
Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_r. Qed.

391 392 393
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
394 395
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
396 397 398 399 400 401
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
402
  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
403
Qed.
404

Robbert Krebbers's avatar
Robbert Krebbers committed
405 406 407
Global Instance into_wand_forall {A} p q (Φ : A  PROP) P Q x :
  IntoWand p q (Φ x) P Q  IntoWand p q ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
408
Global Instance into_wand_tforall {TT : tele} p q (Φ : TT  PROP) P Q x :
409 410 411
  IntoWand p q (Φ x) P Q  IntoWand p q (.. x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.

412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
Global Instance into_wand_affine p q R P Q :
  IntoWand p q R P Q  IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand /= => HR. apply wand_intro_r. destruct p; simpl in *.
  - rewrite (affinely_elim R) -(affine_affinely ( R)%I) HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
  - rewrite HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
Qed.
(* In case the argument is affine, but the wand resides in the spatial context,
we can only eliminate the affine modality in the argument. This would lead to
the following instance:

  IntoWand false q R P Q → IntoWand' false q R (<affine> P) Q.

This instance is redundant, however, since the elimination of the affine
modality is already covered by the [IntoAssumption] instances that are used at
the leaves of the instance search for [IntoWand]. *)
Global Instance into_wand_affine_args q R P Q :
  IntoWand true q R P Q  IntoWand' true q R (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR. apply wand_intro_r.
  rewrite -(affine_affinely ( R)%I) HR. destruct q; simpl.
  - rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
    by rewrite affinely_sep_2 wand_elim_l.
  - by rewrite affinely_sep_2 wand_elim_l.
Qed.

444
Global Instance into_wand_intuitionistically p q R P Q :
445 446
  IntoWand true q R P Q  IntoWand p q ( R) P Q.
Proof. rewrite /IntoWand /= => ->. by rewrite {1}intuitionistically_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
447
Global Instance into_wand_persistently_true q R P Q :
448
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
449
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
450 451 452
Global Instance into_wand_persistently_false q R P Q :
  Absorbing R  IntoWand false q R P Q  IntoWand false q (<pers> R) P Q.
Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
453

454
(** FromWand *)
455 456
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
457
Global Instance from_wand_wandM mP1 P2 :
458
  FromWand (mP1 -? P2) (default emp mP1)%I P2.
459
Proof. by rewrite /FromWand wandM_sound. Qed.
460

461
(** FromImpl *)
462 463 464
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.

465
(** FromAnd *)
Robbert Krebbers's avatar
Robbert Krebbers committed
466 467 468
Global Instance from_and_and P1 P2 : FromAnd (P1  P2) P1 P2 | 100.
Proof. by rewrite /FromAnd. Qed.
Global Instance from_and_sep_persistent_l P1 P1' P2 :
469
  Persistent P1  IntoAbsorbingly P1' P1  FromAnd (P1  P2) P1' P2 | 9.
470
Proof.
471 472 473
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
474
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
Global Instance from_and_sep_persistent_r P1 P2 P2' :
476
  Persistent P2  IntoAbsorbingly P2' P2  FromAnd (P1  P2) P1 P2' | 10.
477
Proof.
478 479 480
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
481 482
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
483 484
Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.
485

Robbert Krebbers's avatar
Robbert Krebbers committed
486
Global Instance from_and_persistently P Q1 Q2 :
487
  FromAnd P Q1 Q2 
488
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
489 490
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
491
  FromSep P Q1 Q2 
492
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
493
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
494

495 496
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat  A  PROP) l x l' :
  IsCons l x l' 
Robbert Krebbers's avatar
Robbert Krebbers committed
497
  Persistent (Φ 0 x) 
498 499 500 501
  FromAnd ([ list] k  y  l, Φ k y) (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Proof. rewrite /IsCons=> -> ?. by rewrite /FromAnd big_sepL_cons persistent_and_sep_1. Qed.
Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat  A  PROP) l l1 l2 :
  IsApp l l1 l2 
Robbert Krebbers's avatar
Robbert Krebbers committed
502
  ( k y, Persistent (Φ k y)) 
503
  FromAnd ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
504
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
505
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
506

507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528
Global Instance from_and_big_sepL2_cons_persistent {A B}
    (Φ : nat  A  B  PROP) l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1'  IsCons l2 x2 l2' 
  Persistent (Φ 0 x1 x2) 
  FromAnd ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([ list] k  y1;y2  l1';l2', Φ (S k) y1 y2).
Proof.
  rewrite /IsCons=> -> -> ?.
  by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
Qed.
Global Instance from_and_big_sepL2_app_persistent {A B}
    (Φ : nat  A  B  PROP) l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1''  IsApp l2 l2' l2'' 
  ( k y1 y2, Persistent (Φ k y1 y2)) 
  FromAnd ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    ([ list] k  y1;y2  l1';l2', Φ k y1 y2)
    ([ list] k  y1;y2  l1'';l2'', Φ (length l1' + k) y1 y2).
Proof.
  rewrite /IsApp=> -> -> ?. rewrite /FromAnd persistent_and_sep_1.
  apply wand_elim_l', big_sepL2_app.
Qed.

529 530
Global Instance from_and_big_sepMS_disj_union_persistent
    `{Countable A} (Φ : A  PROP) X1 X2 :
531
  ( y, Persistent (Φ y)) 
532 533
  FromAnd ([ mset] y  X1  X2, Φ y) ([ mset] y  X1, Φ y) ([ mset] y  X2, Φ y).
Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qed.
534

535
(** FromSep *)
Robbert Krebbers's avatar
Robbert Krebbers committed
536 537 538
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.
Global Instance from_sep_and P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
539
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
540 541 542 543 544 545
  FromSep (P1  P2) P1 P2 | 101.
Proof. intros. by rewrite /FromSep sep_and. Qed.

Global Instance from_sep_pure φ ψ : @FromSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.

546
Global Instance from_sep_affinely P Q1 Q2 :
547
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
548
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
549 550 551
Global Instance from_sep_intuitionistically P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite intuitionistically_sep_2. Qed.
552
Global Instance from_sep_absorbingly P Q1 Q2 :
553
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
554
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
Global Instance from_sep_persistently P Q1 Q2 :
556
  FromSep P Q1 Q2 
557
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
558
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
559

560 561 562 563 564 565 566
Global Instance from_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
  IsCons l x l' 
  FromSep ([ list] k  y  l, Φ k y) (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Proof. rewrite /IsCons=> ->. by rewrite /FromSep big_sepL_cons. Qed.
Global Instance from_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
  IsApp l l1 l2 
  FromSep ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
567
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
568
Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.
569

570 571 572 573 574 575 576 577 578 579 580 581 582 583
Global Instance from_sep_big_sepL2_cons {A B} (Φ : nat  A  B  PROP)
    l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1'  IsCons l2 x2 l2' 
  FromSep ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([ list] k  y1;y2  l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=> -> ->. by rewrite /FromSep big_sepL2_cons. Qed.
Global Instance from_sep_big_sepL2_app {A B} (Φ : nat  A  B  PROP)
    l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1''  IsApp l2 l2' l2'' 
  FromSep ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    ([ list] k  y1;y2  l1';l2', Φ k y1 y2)
    ([ list] k  y1;y2  l1'';l2'', Φ (length l1' + k) y1 y2).
Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.

584 585 586
Global Instance from_sep_big_sepMS_disj_union `{Countable A} (Φ : A  PROP) X1 X2 :
  FromSep ([ mset] y  X1  X2, Φ y) ([ mset] y  X1, Φ y) ([ mset] y  X2, Φ y).
Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.
587

588
(** IntoAnd *)
589
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
590
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
591
Global Instance into_and_and_affine_l P Q Q' :
592
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
593 594
Proof.
  intros. rewrite /IntoAnd /=.
595
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
596 597
Qed.
Global Instance into_and_and_affine_r P P' Q :
598
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
599 600
Proof.
  intros. rewrite /IntoAnd /=.
601
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
602 603
Qed.

604
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
605
Proof.
606 607
  rewrite /IntoAnd /= intuitionistically_sep
    -and_sep_intuitionistically intuitionistically_and //.
608
Qed.
609
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
610
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
611 612
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
613 614

Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
615
Proof. by rewrite /IntoAnd pure_and intuitionistically_if_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
616

617
Global Instance into_and_affinely p P Q1 Q2 :
618
  IntoAnd p P Q1 Q2  IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
  rewrite /IntoAnd. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
621
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
622
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Qed.
624 625 626 627 628 629 630
Global Instance into_and_intuitionistically p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd. destruct p; simpl.
  - rewrite -intuitionistically_and !intuitionistically_idemp //.
  - intros ->. by rewrite intuitionistically_and.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
631
Global Instance into_and_persistently p P Q1 Q2 :
632
  IntoAnd p P Q1 Q2 
633
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
634
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
  rewrite /IntoAnd /=. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
636
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
638 639
Qed.

640
(** IntoSep *)
641 642
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
643

644
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
645
  | and_into_sep_affine P Q Q' : Affine P  FromAffinely Q' Q  AndIntoSep P P Q Q'
646
  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
647 648 649 650 651 652
Existing Class AndIntoSep.
Global Existing Instance and_into_sep_affine | 0.
Global Existing Instance and_into_sep | 2.

Global Instance into_sep_and_persistent_l P P' Q Q' :
  Persistent P  AndIntoSep P P' Q Q'  IntoSep (P  Q) P' Q'.
653
Proof.
654
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
655
  - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
656 657
    by rewrite persistent_and_affinely_sep_l_1.
  - by rewrite persistent_and_affinely_sep_l_1.
658
Qed.
659 660
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
661
Proof.
662
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
663
  - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
664 665
    by rewrite persistent_and_affinely_sep_r_1.
  - by rewrite persistent_and_affinely_sep_r_1.
666
Qed.
667

668 669 670
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

671
Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
672
  IntoSep P Q1 Q2  IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
673
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
674 675 676
Global Instance into_sep_intuitionistically `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) ( Q1) ( Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite intuitionistically_sep. Qed.
677 678 679 680
(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely.
Also, it overlaps with `into_sep_affinely_later`, and hence has lower
precedence. *)
Global Instance into_sep_affinely_trim P Q1 Q2 :
681
  IntoSep P Q1 Q2  IntoSep (<affine> P) Q1 Q2 | 20.
682
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
683

684
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
685
  IntoSep P Q1 Q2 
686
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
687
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
688 689
Global Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
690
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
691
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar