coq_tactics.v 41.4 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
3
From iris.proofmode Require Export base environments classes modality_instances.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import bi.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8

(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11 12 13 14
Section bi_tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Robbert Krebbers's avatar
Robbert Krebbers committed
15 16
(** * Starting and stopping the proof mode *)
Lemma tac_start P : envs_entails (Envs Enil Enil 1) P  bi_emp_valid P.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Proof.
18 19
  rewrite envs_entails_eq !of_envs_eq /=.
  rewrite intuitionistically_True_emp left_id=><-.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36
Lemma tac_stop Δ P :
  (match env_intuitionistic Δ, env_spatial Δ with
   | Enil, Γs => env_to_prop Γs
   | Γp, Enil =>  env_to_prop_and Γp
   | Γp, Γs =>  env_to_prop_and Γp  env_to_prop Γs
   end%I  P) 
  envs_entails Δ P.
Proof.
  rewrite envs_entails_eq !of_envs_eq. intros <-.
  rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
  destruct (env_intuitionistic Δ), (env_spatial Δ);
    by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
37
(** * Basic rules *)
38
Lemma tac_eval Δ Q Q' :
39 40 41
  ( (Q'':=Q'), Q''  Q)  (* We introduce [Q''] as a let binding so that
    tactics like `reflexivity` as called by [rewrite //] do not eagerly unify
    it with [Q]. See [test_iEval] in [tests/proofmode]. *)
42
  envs_entails Δ Q'  envs_entails Δ Q.
43
Proof. by intros <-. Qed.
44

45
Lemma tac_eval_in Δ i p P P' Q :
46
  envs_lookup i Δ = Some (p, P) 
47
  ( (P'':=P'), P  P') 
48 49 50 51 52
  match envs_simple_replace i p (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
53
Proof.
54 55
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq /=. intros ? HP ?.
56 57
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
58
Qed.
59

60 61 62 63 64 65 66
Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed.
Global Instance affine_env_snoc Γ i P :
  Affine P  AffineEnv Γ  AffineEnv (Esnoc Γ i P).
Proof. by constructor. Qed.

67
(* If the BI is affine, no need to walk on the whole environment. *)
68
Global Instance affine_env_bi `(BiAffine PROP) Γ : AffineEnv Γ | 0.
69 70
Proof. induction Γ; apply _. Qed.

71
Instance affine_env_spatial Δ :
72 73 74
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

75 76
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
77

Robbert Krebbers's avatar
Robbert Krebbers committed
78 79
Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  FromAssumption p P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
  (let Δ' := envs_delete true i p Δ in
   if env_spatial_is_nil Δ' then TCTrue
83
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
84
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87 88
  intros ?? H. rewrite envs_entails_eq envs_lookup_sound //.
  simpl in *. destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
91

92
Lemma tac_rename Δ i j p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  envs_lookup i Δ = Some (p,P) 
94 95 96 97
  match envs_simple_replace i p (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
98
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Proof.
100 101
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
102
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
104

105 106
Lemma tac_clear Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
108
  envs_entails (envs_delete true i p Δ) Q 
109
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Proof.
111 112
  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
  by destruct p; rewrite /= sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115

(** * False *)
116
Lemma tac_ex_falso Δ Q : envs_entails Δ False  envs_entails Δ Q.
117
Proof. by rewrite envs_entails_eq -(False_elim Q). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
118

Robbert Krebbers's avatar
Robbert Krebbers committed
119 120 121
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
122
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Proof.
124
  rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
125
  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
126 127
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
128
(** * Pure *)
129 130 131 132 133
Lemma tac_pure_intro Δ Q φ a :
  FromPure a Q φ 
  (if a then AffineEnv (env_spatial Δ) else TCTrue) 
  φ 
  envs_entails Δ Q.
134
Proof.
135 136
  intros ???. rewrite envs_entails_eq -(from_pure a Q). destruct a; simpl.
  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp.
137 138
  - by apply pure_intro.
Qed.
139

140 141
Lemma tac_pure Δ i p P φ Q :
  envs_lookup i Δ = Some (p, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  IntoPure P φ 
143
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
144
  (φ  envs_entails (envs_delete true i p Δ) Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof.
146
  rewrite envs_entails_eq=> ?? HPQ HQ.
147
  rewrite envs_lookup_sound //; simpl. destruct p; simpl.
148
  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
    by apply pure_elim_l.
150
  - destruct HPQ.
151
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
152
      by apply pure_elim_l.
153
    + rewrite (into_pure P) -(persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
154
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156
Qed.

157
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝  Q)  (φ  envs_entails Δ Q).
158
Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
159

160
(** * Intuitionistic *)
161
Lemma tac_intuitionistic Δ i p P P' Q :
162
  envs_lookup i Δ = Some (p, P) 
163
  IntoPersistent p P P' 
164
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
165 166 167 168 169
  match envs_replace i p true (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Proof.
171 172
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
173
  destruct p; simpl; rewrite /bi_intuitionistically.
174
  - by rewrite -(into_persistent true P) /= wand_elim_r.
175
  - destruct HPQ.
176
    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
177
              (into_persistent _ P) wand_elim_r //.
178
    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
179
      by rewrite -{1}absorbingly_intuitionistically_into_persistently
180
        absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
181 182 183
Qed.

(** * Implication and wand *)
184
Lemma tac_impl_intro Δ i P P' Q R :
185
  FromImpl R P Q 
186
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
187
  FromAffinely P' P 
188 189 190 191 192
  match envs_app false (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Proof.
194 195
  destruct (envs_app _ _ _) eqn:?; last done.
  rewrite /FromImpl envs_entails_eq => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
196
  - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
197
    rewrite envs_app_singleton_sound //; simpl.
198
    rewrite -(from_affinely P' P) -affinely_and_lr.
199
    by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
200
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
201
    by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
Qed.
203
Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
204
  FromImpl R P Q 
205
  IntoPersistent false P P' 
206 207 208 209 210
  match envs_app true (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
Proof.
212 213
  destruct (envs_app _ _ _) eqn:?; last done.
  rewrite /FromImpl envs_entails_eq => <- ??.
214
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
215
  rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
216
  by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
217
Qed.
218 219
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q  envs_entails Δ Q  envs_entails Δ R.
220 221 222
Proof.
  rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
223

224
Lemma tac_wand_intro Δ i P Q R :
225
  FromWand R P Q 
226 227 228 229 230
  match envs_app false (Esnoc Enil i P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
Proof.
232 233
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite /FromWand envs_entails_eq => <- HQ.
234
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
Qed.
236 237

Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
238
  FromWand R P Q 
239
  IntoPersistent false P P' 
240
  TCOr (Affine P) (Absorbing Q) 
241 242 243 244 245
  match envs_app true (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
Proof.
247 248
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite /FromWand envs_entails_eq => <- ? HPQ HQ.
249
  rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
250
  - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
251
            (into_persistent _ P) wand_elim_r //.
252
  - rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
253
    by rewrite -{1}absorbingly_intuitionistically_into_persistently
254
      absorbingly_sep_l wand_elim_r HQ.
255
Qed.
256 257
Lemma tac_wand_intro_drop Δ P Q R :
  FromWand R P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  TCOr (Affine P) (Absorbing Q) 
259
  envs_entails Δ Q 
260
  envs_entails Δ R.
261
Proof.
262
  rewrite envs_entails_eq /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264 265 266
Qed.

(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
but it is doing some work to keep the order of hypotheses preserved. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
267 268 269
Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
  envs_lookup i Δ = Some (p, P1) 
  let Δ' := envs_delete remove_intuitionistic i p Δ in
270
  envs_lookup j Δ' = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
271
  IntoWand q p R P1 P2 
272 273 274 275
  match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
276
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
  rewrite envs_entails_eq /IntoWand. intros ?? HR ?.
278
  destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
279 280 281 282 283 284
  rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
  rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
  - rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp.
    rewrite {1}(intuitionistically_intuitionistically_if q).
    by rewrite HR assoc intuitionistically_if_sep_2 !wand_elim_r.
  - by rewrite HR assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
285 286
Qed.

287
Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
288
  envs_lookup j Δ = Some (q, R) 
289
  IntoWand q false R P1 P2  AddModal P1' P1 Q 
290 291 292
  match
    ''(Δ1,Δ2)  envs_split (if neg is true then Right else Left)
    js (envs_delete true j q Δ);
293
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
294 295 296 297 298 299 300
    Some (Δ1,Δ2') (* does not preserve position of [j] *)
  with
  | Some (Δ1,Δ2') =>
     (* The constructor [conj] of [∧] still stores the contexts [Δ1] and [Δ2'] *)
     envs_entails Δ1 P1'  envs_entails Δ2' Q
  | None => False
  end  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Proof.
302 303 304
  rewrite envs_entails_eq. intros ??? HQ.
  destruct (_ = _) as [[Δ1 Δ2']|] eqn:?; last done.
  destruct HQ as [HP1 HQ].
Robbert Krebbers's avatar
Robbert Krebbers committed
305 306 307
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
308
  rewrite (envs_app_singleton_sound Δ2) //; simpl.
309
  rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
310
  apply wand_intro_l. by rewrite assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
311 312
Qed.

313 314 315 316
Lemma tac_unlock_emp Δ Q : envs_entails Δ Q  envs_entails Δ (emp  locked Q).
Proof. rewrite envs_entails_eq=> ->. by rewrite -lock left_id. Qed.
Lemma tac_unlock_True Δ Q : envs_entails Δ Q  envs_entails Δ (True  locked Q).
Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
317
Lemma tac_unlock Δ Q : envs_entails Δ Q  envs_entails Δ (locked Q).
318 319
Proof. by unlock. Qed.

320 321
Lemma tac_specialize_frame Δ j q R P1 P2 P1' Q Q' :
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
322
  IntoWand q false R P1 P2 
323
  AddModal P1' P1 Q 
324
  envs_entails (envs_delete true j q Δ) (P1'  locked Q') 
325
  Q' = (P2 - Q)%I 
326
  envs_entails Δ Q.
327
Proof.
328
  rewrite envs_entails_eq. intros ??? HPQ ->.
329
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
330
  rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
Robbert Krebbers's avatar
Robbert Krebbers committed
331
  apply wand_intro_l. by rewrite assoc !wand_elim_r.
332 333
Qed.

334
Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
335
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
336
  IntoWand q true R P1 P2 
337
  FromPure a P1 φ 
338 339 340 341 342 343
  φ 
  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Proof.
345 346
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
347
  rewrite -intuitionistically_if_idemp (into_wand q true) /=.
348 349 350
  rewrite -(from_pure a P1) pure_True //.
  rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
  by rewrite intuitionistically_emp left_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
351 352
Qed.

353 354
Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
355 356
  IntoWand q true R P1 P2 
  Persistent P1 
357
  IntoAbsorbingly P1' P1 
358
  envs_entails (envs_delete true j q Δ) P1' 
359 360 361 362
  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
363
Proof.
364
  rewrite envs_entails_eq => ???? HP1 HQ.
365 366
  destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
  rewrite -HQ envs_lookup_sound //.
367
  rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
368
  rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
369
  rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
Ralf Jung's avatar
Ralf Jung committed
370
  rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
371 372
  rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
  rewrite (intuitionistically_intuitionistically_if q).
373
  by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
374 375
Qed.

376
Lemma tac_specialize_intuitionistic_helper Δ j q P R R' Q :
377
  envs_lookup j Δ = Some (q,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
378
  (if q then TCTrue else BiAffine PROP) 
379
  envs_entails Δ (<absorb> R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
380
  IntoPersistent false R R' 
381 382 383 384
  match envs_replace j q true (Esnoc Enil j R') Δ with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
385
Proof.
386 387 388
  rewrite envs_entails_eq => ?? HR ??.
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
389
  rewrite envs_replace_singleton_sound //; destruct q; simpl.
390
  - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
Robbert Krebbers's avatar
Robbert Krebbers committed
391 392
      absorbingly_elim_persistently sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
393
  - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
Robbert Krebbers's avatar
Robbert Krebbers committed
394 395
      (into_persistent _ R) sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
396 397
Qed.

398 399
(* A special version of [tac_assumption] that does not do any of the
[FromAssumption] magic. *)
400
Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
401
  envs_lookup i Δ = Some (q,P) 
402
  envs_entails Δ (<absorb> P).
403 404
Proof.
  rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
Ralf Jung's avatar
Ralf Jung committed
405
  rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
406 407
Qed.

408 409 410 411 412
Lemma tac_revert Δ i Q :
  match envs_lookup_delete true i Δ with
  | Some (p,P,Δ') => envs_entails Δ' ((if p then  P else P)%I - Q)
  | None => False
  end 
413
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
Proof.
415 416 417
  rewrite envs_entails_eq => HQ.
  destruct (envs_lookup_delete _ _ _) as [[[p P] Δ']|] eqn:?; last done.
  rewrite envs_lookup_delete_sound //=.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
  rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
419 420
Qed.

421
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
422 423
  into_ih : φ  of_envs Δ  Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
424
Proof. by rewrite envs_entails_eq /IntoIH. Qed.
425
Global Instance into_ih_forall {A} (φ : A  Prop) Δ Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
426
  ( x, IntoIH (φ x) Δ (Φ x))  IntoIH ( x, φ x) Δ ( x, Φ x)%I | 2.
427 428
Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
429
  IntoIH φ Δ Q  IntoIH (ψ  φ) Δ (⌜ψ⌝  Q)%I | 1.
430
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
431 432 433

Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P 
434
  env_spatial_is_nil Δ = true 
435
  envs_entails Δ (<pers> P  Q) 
436
  envs_entails Δ Q.
437
Proof.
438
  rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
439
  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
440
  rewrite -(idemp bi_and ( (of_envs Δ))%I) {1}HP // HPQ.
Ralf Jung's avatar
Ralf Jung committed
441
  rewrite {1}intuitionistically_into_persistently_1 intuitionistically_elim impl_elim_r //.
442 443
Qed.

444 445 446 447 448
Lemma tac_assert Δ j P Q :
  match envs_app true (Esnoc Enil j (P - P)%I) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end  envs_entails Δ Q.
449
Proof.
450 451
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_eq=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
452
  by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
453 454
Qed.

455 456 457 458 459 460 461 462 463 464 465 466 467
Definition IntoEmpValid (φ : Type) (P : PROP) := φ  bi_emp_valid P.
Lemma into_emp_valid_here φ P : AsEmpValid φ P  IntoEmpValid φ P.
Proof. by intros [??]. Qed.
Lemma into_emp_valid_impl (φ ψ : Type) P :
  φ  IntoEmpValid ψ P  IntoEmpValid (φ  ψ) P.
Proof. rewrite /IntoEmpValid; auto. Qed.
Lemma into_emp_valid_forall {A} (φ : A  Type) P x :
  IntoEmpValid (φ x) P  IntoEmpValid ( x : A, φ x) P.
Proof. rewrite /IntoEmpValid; auto. Qed.

Lemma tac_pose_proof Δ j (φ : Prop) P Q :
  φ 
  IntoEmpValid φ P 
468 469 470 471 472
  match envs_app true (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
473
Proof.
474
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
475 476
  rewrite envs_entails_eq => ? HP <-. rewrite envs_app_singleton_sound //=.
  by rewrite -HP //= intuitionistically_emp emp_wand.
Robbert Krebbers's avatar
Robbert Krebbers committed
477 478
Qed.

479 480 481 482 483 484 485 486 487 488
Lemma tac_pose_proof_hyp Δ i j Q :
  match envs_lookup_delete false i Δ with
  | None => False
  | Some (p, P, Δ') =>
    match envs_app p (Esnoc Enil j P) Δ' with
    | None => False
    | Some Δ'' => envs_entails Δ'' Q
    end
  end 
  envs_entails Δ Q.
489
Proof.
490 491 492 493
  destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
  destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
  rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *.
  intros [? ->] <-.
494 495
  rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
  by rewrite wand_elim_r.
496 497
Qed.

498 499
Lemma tac_apply Δ i p R P1 P2 :
  envs_lookup i Δ = Some (p, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
500
  IntoWand p false R P1 P2 
501
  envs_entails (envs_delete true i p Δ) P1  envs_entails Δ P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
Proof.
503
  rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_sound //.
504
  by rewrite (into_wand p false) /= HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
505 506 507
Qed.

(** * Conjunction splitting *)
508
Lemma tac_and_split Δ P Q1 Q2 :
509
  FromAnd P Q1 Q2  envs_entails Δ Q1  envs_entails Δ Q2  envs_entails Δ P.
510
Proof. rewrite envs_entails_eq. intros. rewrite -(from_and P). by apply and_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
511 512

(** * Separating conjunction splitting *)
513
Lemma tac_sep_split Δ d js P Q1 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
514
  FromSep P Q1 Q2 
515 516 517 518
  match envs_split d js Δ with
  | None => False
  | Some (Δ1,Δ2) => envs_entails Δ1 Q1  envs_entails Δ2 Q2
  end  envs_entails Δ P.
Robbert Krebbers's avatar
Robbert Krebbers committed
519
Proof.
520 521
  destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
  rewrite envs_entails_eq=>? [HQ1 HQ2].
522
  rewrite envs_split_sound //. by rewrite HQ1 HQ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
523 524 525
Qed.

(** * Combining *)
Robbert Krebbers's avatar
Robbert Krebbers committed
526
Class FromSeps {PROP : bi} (P : PROP) (Qs : list PROP) :=
527
  from_seps : [] Qs  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529
Arguments FromSeps {_} _%I _%I.
Arguments from_seps {_} _%I _%I {_}.
530

Robbert Krebbers's avatar
Robbert Krebbers committed
531 532
Global Instance from_seps_nil : @FromSeps PROP emp [].
Proof. by rewrite /FromSeps. Qed.
533 534 535
Global Instance from_seps_singleton P : FromSeps P [P] | 1.
Proof. by rewrite /FromSeps /= right_id. Qed.
Global Instance from_seps_cons P P' Q Qs :
Robbert Krebbers's avatar
Robbert Krebbers committed
536 537
  FromSeps P' Qs  FromSep P Q P'  FromSeps P (Q :: Qs) | 2.
Proof. by rewrite /FromSeps /FromSep /= => ->. Qed.
538 539

Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
540
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) 
541 542
  FromSeps P Ps 
  envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 
543
  envs_entails Δ3 Q  envs_entails Δ1 Q.
544
Proof.
545
  rewrite envs_entails_eq => ??? <-. rewrite envs_lookup_delete_list_sound //.
546
  rewrite from_seps. rewrite envs_app_singleton_sound //=.
547
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
548 549 550
Qed.

(** * Conjunction/separating conjunction elimination *)
551
Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
552 553
  envs_lookup i Δ = Some (p, P) 
  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) 
554 555 556 557 558
  match envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Proof.
560
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
561
  rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
562
  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
563
  - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
564 565
Qed.

566 567 568
(* Using this tactic, one can destruct a (non-separating) conjunction in the
spatial context as long as one of the conjuncts is thrown away. It corresponds
to the principle of "external choice" in linear logic. *)
569
Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
570
  envs_lookup i Δ = Some (p, P) 
571 572
  (if p then IntoAnd p P P1 P2 : Type else
    TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
573
      (if d is Left then TCOr (Affine P2) (Absorbing Q)
574
       else TCOr (Affine P1) (Absorbing Q)))) 
575 576 577 578
  match envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end  envs_entails Δ Q.
579
Proof.
580 581
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq => ? HP HQ.
582
  rewrite envs_simple_replace_singleton_sound //=. destruct p.
583
  { rewrite (into_and _ P) HQ. destruct d; simpl.
584 585
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
Robbert Krebbers's avatar
Robbert Krebbers committed
586
  destruct HP as [?|[??]].
587
  { rewrite (into_and _ P) HQ. destruct d; simpl.
588 589
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
590
  rewrite (into_sep P) HQ. destruct d; simpl.
591 592
  - by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
  - by rewrite -assoc wand_elim_r sep_elim_r.
593 594
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
595
(** * Framing *)
596
Lemma tac_frame_pure Δ (φ : Prop) P Q :
597
  φ  Frame true ⌜φ⌝ P Q  envs_entails Δ Q  envs_entails Δ P.
598
Proof.
599
  rewrite envs_entails_eq => ? Hframe ->. rewrite -Hframe /=.
600
  rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
601
  auto using and_intro, pure_intro.
602
Qed.
603

604 605
Lemma tac_frame Δ i p R P Q :
  envs_lookup i Δ = Some (p, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
606
  Frame p R P Q 
607
  envs_entails (envs_delete false i p Δ) Q  envs_entails Δ P.
Robbert Krebbers's avatar
Robbert Krebbers committed
608
Proof.
609
  rewrite envs_entails_eq. intros ? Hframe HQ.
610
  rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
611 612 613
Qed.

(** * Disjunction *)
614 615 616
Lemma tac_or_l Δ P Q1 Q2 :
  FromOr P Q1 Q2  envs_entails Δ Q1  envs_entails Δ P.
Proof.
617
  rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_l'.
618 619 620 621
Qed.
Lemma tac_or_r Δ P Q1 Q2 :
  FromOr P Q1 Q2  envs_entails Δ Q2  envs_entails Δ P.
Proof.
622
  rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
623
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
624

625
Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
626
  envs_lookup i Δ = Some (p, P)  IntoOr P P1 P2 
627 628 629 630 631 632
  match envs_simple_replace i p (Esnoc Enil j1 P1) Δ,
        envs_simple_replace i p (Esnoc Enil j2 P2) Δ with
  | Some Δ1, Some Δ2 => envs_entails Δ1 Q  envs_entails Δ2 Q
  | _, _ => False
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
633
Proof.
634 635 636
  destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; last done.
  destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; last done.
  rewrite envs_entails_eq. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
637
  rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
638 639 640 641
  - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
    by rewrite wand_elim_r.
  - rewrite (envs_simple_replace_singleton_sound' _ Δ2) //.
    by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
642 643 644
Qed.

(** * Forall *)
Robbert Krebbers's avatar
Robbert Krebbers committed
645
Lemma tac_forall_intro {A} Δ (Φ : A  PROP) Q :
646
  FromForall Q Φ 
647 648
  ( a, envs_entails Δ (Φ a)) 
  envs_entails Δ Q.
649
Proof. rewrite envs_entails_eq /FromForall=> <-. apply forall_intro. Qed.
650

651
Lemma tac_forall_specialize {A} Δ i p P (Φ : A  PROP) Q :
652
  envs_lookup i Δ = Some (p, P)  IntoForall P Φ 
653
  ( x : A,
654 655 656 657
      match envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ with
      | None => False
      | Some Δ' => envs_entails Δ' Q
      end) 
658
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
659
Proof.
660 661
  rewrite envs_entails_eq. intros ?? (x&?).
  destruct (envs_simple_replace) as [Δ'|] eqn:?; last done.
662
  rewrite envs_simple_replace_singleton_sound //; simpl.
663
  by rewrite (into_forall P) (forall_elim x) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
664 665
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
666
Lemma tac_forall_revert {A} Δ (Φ : A  PROP) :
667
  envs_entails Δ ( a, Φ a)   a, envs_entails Δ (Φ a).
668
Proof. rewrite envs_entails_eq => HΔ a. by rewrite HΔ (forall_elim a). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
669 670

(** * Existential *)
Robbert Krebbers's avatar
Robbert Krebbers committed
671
Lemma tac_exist {A} Δ P (Φ : A  PROP) :
672 673
  FromExist P Φ  ( a, envs_entails Δ (Φ a))  envs_entails Δ P.
Proof.
674
  rewrite envs_entails_eq => ? [a ?].
675 676
  rewrite -(from_exist P). eauto using exist_intro'.
Qed.
677

Robbert Krebbers's avatar
Robbert Krebbers committed
678
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A  PROP) Q :
679
  envs_lookup i Δ = Some (p, P)  IntoExist P Φ 
680 681 682 683 684
  ( a,
    match envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ with
    | Some Δ' => envs_entails Δ' Q
    | None => False
    end) 
685
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
686
Proof.
687
  rewrite envs_entails_eq => ?? HΦ. rewrite envs_lookup_sound //.
688
  rewrite (into_exist P) intuitionistically_if_exist sep_exist_r.
689 690
  apply exist_elim=> a; specialize (HΦ a) as Hmatch.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
691
  rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
692
Qed.
693

694
(** * Modalities *)
695
Lemma tac_modal_elim Δ i p p' φ P' P Q Q' :
696
  envs_lookup i Δ = Some (p, P) 
697
  ElimModal φ p p' P P' Q Q' 
698
  φ 
699 700 701 702 703
  match envs_replace i p p' (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q'
  end 
  envs_entails Δ Q.
704
Proof.
705 706
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_eq => ??? HΔ. rewrite envs_replace_singleton_sound //=.
707
  rewrite HΔ. by eapply elim_modal.
Robbert Krebbers's avatar
Robbert Krebbers committed
708
Qed.