coq_tactics.v 40.1 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
(** * Adequacy *)
16
Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P  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 23
Qed.

(** * Basic rules *)
24
Lemma tac_eval Δ Q Q' :
25 26 27
  ( (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]. *)
28
  envs_entails Δ Q'  envs_entails Δ Q.
29
Proof. by intros <-. Qed.
30

31
Lemma tac_eval_in Δ i p P P' Q :
32
  envs_lookup i Δ = Some (p, P) 
33
  ( (P'':=P'), P  P') 
34 35 36 37 38
  match envs_simple_replace i p (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
39
Proof.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
40
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
41
  rewrite envs_entails_eq /=. intros ? HP ?.
42 43
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
44
Qed.
45

46 47 48 49 50 51 52
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.

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

57
Instance affine_env_spatial Δ :
58 59 60
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

61 62
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
63

64
(* TODO: convert to not take Δ' *)
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Lemma tac_assumption Δ Δ' i p P Q :
66
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  FromAssumption p P Q 
68 69
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
70
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Proof.
72
  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  destruct (env_spatial_is_nil Δ') eqn:?.
74
  - by rewrite (env_spatial_is_nil_intuitionistically Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
77

78
Lemma tac_rename Δ i j p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  envs_lookup i Δ = Some (p,P) 
80 81 82 83
  match envs_simple_replace i p (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
84
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof.
86 87 88
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90

91
(* TODO: convert to not take Δ' *)
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Lemma tac_clear Δ Δ' i p P Q :
93
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
95
  envs_entails Δ' Q 
96
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Proof.
98
  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
99
  by destruct p; rewrite /= HQ sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102

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

Robbert Krebbers's avatar
Robbert Krebbers committed
106 107 108
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
109
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Proof.
111
  rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
112
  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
115
(** * Pure *)
116 117 118 119 120
Lemma tac_pure_intro Δ Q φ a :
  FromPure a Q φ 
  (if a then AffineEnv (env_spatial Δ) else TCTrue) 
  φ 
  envs_entails Δ Q.
121
Proof.
122 123
  intros ???. rewrite envs_entails_eq -(from_pure a Q). destruct a; simpl.
  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp.
124 125
  - by apply pure_intro.
Qed.
126

127
(* TODO: convert to not take Δ' *)
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Lemma tac_pure Δ Δ' i p P φ Q :
129
  envs_lookup_delete true i Δ = Some (p, P, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  IntoPure P φ 
131
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
132
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Proof.
134
  rewrite envs_entails_eq=> ?? HPQ HQ.
135
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
136
  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    by apply pure_elim_l.
138
  - destruct HPQ.
139
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
140
      by apply pure_elim_l.
141
    + rewrite (into_pure P) -(persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
142
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144
Qed.

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

148
(** * Intuitionistic *)
149
Lemma tac_intuitionistic Δ i p P P' Q :
150
  envs_lookup i Δ = Some (p, P) 
151
  IntoPersistent p P P' 
152
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
153 154 155 156 157
  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
158
Proof.
159
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
160
  rewrite envs_entails_eq=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
161
  destruct p; simpl; rewrite /bi_intuitionistically.
162
  - by rewrite -(into_persistent true P) /= wand_elim_r.
163
  - destruct HPQ.
164
    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
165
              (into_persistent _ P) wand_elim_r //.
166
    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
167
      by rewrite -{1}absorbingly_intuitionistically_into_persistently
168
        absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171
Qed.

(** * Implication and wand *)
172
Lemma tac_impl_intro Δ i P P' Q R :
173
  FromImpl R P Q 
174
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
175
  FromAffinely P' P 
176 177 178 179 180
  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
181
Proof.
182
  destruct (envs_app _ _ _) eqn:?; last done.
183
  rewrite /FromImpl envs_entails_eq => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
184
  - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
185
    rewrite envs_app_singleton_sound //; simpl.
186
    rewrite -(from_affinely P' P) -affinely_and_lr.
187
    by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
188
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
189
    by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Qed.
191
Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
192
  FromImpl R P Q 
193
  IntoPersistent false P P' 
194 195 196 197 198
  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
199
Proof.
200
  destruct (envs_app _ _ _) eqn:?; last done.
201
  rewrite /FromImpl envs_entails_eq => <- ??.
202
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
203
  rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
204
  by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
205
Qed.
206 207
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q  envs_entails Δ Q  envs_entails Δ R.
208 209 210
Proof.
  rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
211

212
Lemma tac_wand_intro Δ i P Q R :
213
  FromWand R P Q 
214
  match envs_app false (Esnoc Enil i P) Δ with
215
  | None => False
216 217
  | Some Δ' => envs_entails Δ' Q
  end 
218
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
Proof.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
220 221 222
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite /FromWand envs_entails_eq => <- HQ.
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
Qed.
224 225

Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
226
  FromWand R P Q 
227
  IntoPersistent false P P' 
228
  TCOr (Affine P) (Absorbing Q) 
229 230 231 232 233
  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
234
Proof.
235
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
236
  rewrite /FromWand envs_entails_eq => <- ? HPQ HQ.
237
  rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
238
  - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
239
            (into_persistent _ P) wand_elim_r //.
240
  - rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
241
    by rewrite -{1}absorbingly_intuitionistically_into_persistently
242
      absorbingly_sep_l wand_elim_r HQ.
243
Qed.
244 245
Lemma tac_wand_intro_drop Δ P Q R :
  FromWand R P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
246
  TCOr (Affine P) (Absorbing Q) 
247
  envs_entails Δ Q 
248
  envs_entails Δ R.
249
Proof.
250
  rewrite envs_entails_eq /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
251 252 253 254
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. *)
255
(* TODO: convert to not take Δ' or Δ'' *)
256 257
Lemma tac_specialize remove_intuitionistic Δ Δ' Δ'' i p j q P1 P2 R Q :
  envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') 
258
  envs_lookup j Δ' = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
259
  IntoWand q p R P1 P2 
260
  envs_replace j q (p && q) (Esnoc Enil j P2) Δ' = Some Δ'' 
261
  envs_entails Δ'' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
Proof.
263 264 265 266 267 268 269 270
  rewrite envs_entails_eq /IntoWand.
  intros [? ->]%envs_lookup_delete_Some ? HR ? <-.
  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
271 272
Qed.

273
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
274
  envs_lookup_delete true j Δ = Some (q, R, Δ') 
275
  IntoWand q false R P1 P2  AddModal P1' P1 Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
276
  (''(Δ1,Δ2)  envs_split (if neg is true then Right else Left) js Δ';
277
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
278
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
279
  envs_entails Δ1 P1'  envs_entails Δ2' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
Proof.
281
  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283 284
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
285
  rewrite (envs_app_singleton_sound Δ2) //; simpl.
286
  rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
287
  apply wand_intro_l. by rewrite assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
288 289
Qed.

290 291 292 293
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.
294
Lemma tac_unlock Δ Q : envs_entails Δ Q  envs_entails Δ (locked Q).
295 296 297
Proof. by unlock. Qed.

Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
298
  envs_lookup_delete true j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
299
  IntoWand q false R P1 P2 
300
  AddModal P1' P1 Q 
301
  envs_entails Δ' (P1'  locked Q') 
302
  Q' = (P2 - Q)%I 
303
  envs_entails Δ Q.
304
Proof.
305
  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
306
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
307
  rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  apply wand_intro_l. by rewrite assoc !wand_elim_r.
309 310
Qed.

311
Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
312
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  IntoWand q true R P1 P2 
314
  FromPure a P1 φ 
315 316 317 318 319 320
  φ 
  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
321
Proof.
322
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
323
  rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
324
  rewrite -intuitionistically_if_idemp (into_wand q true) /=.
325 326 327
  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
328 329
Qed.

330
Lemma tac_specialize_assert_intuitionistic Δ Δ' Δ'' j q P1 P1' P2 R Q :
331
  envs_lookup_delete true j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
332 333
  IntoWand q true R P1 P2 
  Persistent P1 
334
  IntoAbsorbingly P1' P1 
335
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
336
  envs_entails Δ' P1'  envs_entails Δ'' Q  envs_entails Δ Q.
337
Proof.
338
  rewrite envs_entails_eq => /envs_lookup_delete_Some [? ->] ???? HP1 <-.
339
  rewrite envs_lookup_sound //.
340
  rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
341
  rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
342
  rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
Ralf Jung's avatar
Ralf Jung committed
343
  rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
344 345
  rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
  rewrite (intuitionistically_intuitionistically_if q).
346
  by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
347 348
Qed.

349
Lemma tac_specialize_intuitionistic_helper Δ Δ'' j q P R R' Q :
350
  envs_lookup j Δ = Some (q,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
351
  (if q then TCTrue else BiAffine PROP) 
352
  envs_entails Δ (<absorb> R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
353 354
  IntoPersistent false R R' 
  envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' 
355
  envs_entails Δ'' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
357
  rewrite envs_entails_eq => ?? HR ?? <-. rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
358
  rewrite envs_replace_singleton_sound //; destruct q; simpl.
359
  - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
Robbert Krebbers's avatar
Robbert Krebbers committed
360 361
      absorbingly_elim_persistently sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
362
  - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
Robbert Krebbers's avatar
Robbert Krebbers committed
363 364
      (into_persistent _ R) sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
365 366
Qed.

367 368
(* A special version of [tac_assumption] that does not do any of the
[FromAssumption] magic. *)
369
Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
370
  envs_lookup i Δ = Some (q,P) 
371
  envs_entails Δ (<absorb> P).
372 373
Proof.
  rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
Ralf Jung's avatar
Ralf Jung committed
374
  rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
375 376
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
377
Lemma tac_revert Δ Δ' i p P Q :
378
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
379 380
  envs_entails Δ' ((if p then  P else P)%I - Q) 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
381
Proof.
382
  rewrite envs_entails_eq => ? HQ. rewrite envs_lookup_delete_sound //=.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
  rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
384 385
Qed.

386
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
387 388
  into_ih : φ  of_envs Δ  Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
389
Proof. by rewrite envs_entails_eq /IntoIH. Qed.
390
Global Instance into_ih_forall {A} (φ : A  Prop) Δ Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
391
  ( x, IntoIH (φ x) Δ (Φ x))  IntoIH ( x, φ x) Δ ( x, Φ x)%I | 2.
392 393
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
394
  IntoIH φ Δ Q  IntoIH (ψ  φ) Δ (⌜ψ⌝  Q)%I | 1.
395
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
396 397 398

Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P 
399
  env_spatial_is_nil Δ = true 
400
  envs_entails Δ (<pers> P  Q) 
401
  envs_entails Δ Q.
402
Proof.
403
  rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
404
  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
405
  rewrite -(idemp bi_and ( (of_envs Δ))%I) {1}HP // HPQ.
Ralf Jung's avatar
Ralf Jung committed
406
  rewrite {1}intuitionistically_into_persistently_1 intuitionistically_elim impl_elim_r //.
407 408
Qed.

409 410 411 412 413
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.
414
Proof.
415
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
416
  rewrite envs_entails_eq=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
417
  by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
418 419
Qed.

420
Lemma tac_pose_proof Δ j P Q :
421
  P 
422 423 424 425 426
  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
427
Proof.
428
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
429
  rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=.
430
  by rewrite -HP /= intuitionistically_emp emp_wand.
Robbert Krebbers's avatar
Robbert Krebbers committed
431 432
Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
433 434
Lemma tac_pose_proof_hyp Δ i j Q :
  match envs_lookup_delete false i Δ with
435
  | None => False
Joseph Tassarotti's avatar
Joseph Tassarotti committed
436 437 438 439 440
  | Some (p, P, Δ') =>
    match envs_app p (Esnoc Enil j P) Δ' with
    | None => False
    | Some Δ'' => envs_entails Δ'' Q
    end
441 442
  end 
  envs_entails Δ Q.
443
Proof.
444 445
  destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
  destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
446
  rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *.
447
  intros [? ->] <-.
448 449
  rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
  by rewrite wand_elim_r.
450 451
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
452
Lemma tac_apply Δ Δ' i p R P1 P2 :
453
  envs_lookup_delete true i Δ = Some (p, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
454
  IntoWand p false R P1 P2 
455
  envs_entails Δ' P1  envs_entails Δ P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
456
Proof.
457
  rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_delete_sound //.
458
  by rewrite (into_wand p false) /= HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
459 460 461
Qed.

(** * Conjunction splitting *)
462
Lemma tac_and_split Δ P Q1 Q2 :
463
  FromAnd P Q1 Q2  envs_entails Δ Q1  envs_entails Δ Q2  envs_entails Δ P.
464
Proof. rewrite envs_entails_eq. intros. rewrite -(from_and P). by apply and_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
465 466

(** * Separating conjunction splitting *)
467
Lemma tac_sep_split Δ d js P Q1 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
468
  FromSep P Q1 Q2 
469 470 471 472
  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
473
Proof.
474
  destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
475
  rewrite envs_entails_eq=>? [HQ1 HQ2].
476
  rewrite envs_split_sound //. by rewrite HQ1 HQ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
477 478 479
Qed.

(** * Combining *)
Robbert Krebbers's avatar
Robbert Krebbers committed
480
Class FromSeps {PROP : bi} (P : PROP) (Qs : list PROP) :=
481
  from_seps : [] Qs  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483
Arguments FromSeps {_} _%I _%I.
Arguments from_seps {_} _%I _%I {_}.
484

Robbert Krebbers's avatar
Robbert Krebbers committed
485 486
Global Instance from_seps_nil : @FromSeps PROP emp [].
Proof. by rewrite /FromSeps. Qed.
487 488 489
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
490 491
  FromSeps P' Qs  FromSep P Q P'  FromSeps P (Q :: Qs) | 2.
Proof. by rewrite /FromSeps /FromSep /= => ->. Qed.
492 493

Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
494
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) 
495 496
  FromSeps P Ps 
  envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 
497
  envs_entails Δ3 Q  envs_entails Δ1 Q.
498
Proof.
499
  rewrite envs_entails_eq => ??? <-. rewrite envs_lookup_delete_list_sound //.
500
  rewrite from_seps. rewrite envs_app_singleton_sound //=.
501
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
502 503 504
Qed.

(** * Conjunction/separating conjunction elimination *)
505
Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
506 507
  envs_lookup i Δ = Some (p, P) 
  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) 
508 509 510 511 512
  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
513
Proof.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
514 515 516 517
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
  - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
518 519
Qed.

520 521 522
(* 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. *)
523
Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
524
  envs_lookup i Δ = Some (p, P) 
525 526
  (if p then IntoAnd p P P1 P2 : Type else
    TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
527
      (if d is Left then TCOr (Affine P2) (Absorbing Q)
528
       else TCOr (Affine P1) (Absorbing Q)))) 
529 530 531 532
  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.
533
Proof.
534
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
535
  rewrite envs_entails_eq => ? HP HQ.
536
  rewrite envs_simple_replace_singleton_sound //=. destruct p.
537
  { rewrite (into_and _ P) HQ. destruct d; simpl.
538 539
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
Robbert Krebbers's avatar
Robbert Krebbers committed
540
  destruct HP as [?|[??]].
541
  { rewrite (into_and _ P) HQ. destruct d; simpl.
542 543
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
544
  rewrite (into_sep P) HQ. destruct d; simpl.
545 546
  - by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
  - by rewrite -assoc wand_elim_r sep_elim_r.
547 548
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
549
(** * Framing *)
550
Lemma tac_frame_pure Δ (φ : Prop) P Q :
551
  φ  Frame true ⌜φ⌝ P Q  envs_entails Δ Q  envs_entails Δ P.
552
Proof.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
553
  rewrite envs_entails_eq => ? Hframe ->. rewrite -Hframe /=.
554
  rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
555
  auto using and_intro, pure_intro.
556
Qed.
557

558
Lemma tac_frame Δ Δ' i p R P Q :
559
  envs_lookup_delete false i Δ = Some (p, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
560
  Frame p R P Q 
561
  envs_entails Δ' Q  envs_entails Δ P.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
Proof.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
563 564
  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hframe HQ.
  rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
565 566 567
Qed.

(** * Disjunction *)
568 569 570
Lemma tac_or_l Δ P Q1 Q2 :
  FromOr P Q1 Q2  envs_entails Δ Q1  envs_entails Δ P.
Proof.
571
  rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_l'.
572 573 574 575
Qed.
Lemma tac_or_r Δ P Q1 Q2 :
  FromOr P Q1 Q2  envs_entails Δ Q2  envs_entails Δ P.
Proof.
576
  rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
577
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
578

579
Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
580
  envs_lookup i Δ = Some (p, P)  IntoOr P P1 P2 
581 582 583 584 585 586
  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
587
Proof.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
588 589
  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.
590
  rewrite envs_entails_eq. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
591
  rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
592 593 594 595
  - 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
596 597 598
Qed.

(** * Forall *)
Robbert Krebbers's avatar
Robbert Krebbers committed
599
Lemma tac_forall_intro {A} Δ (Φ : A  PROP) Q :
600
  FromForall Q Φ 
601 602
  ( a, envs_entails Δ (Φ a)) 
  envs_entails Δ Q.
603
Proof. rewrite envs_entails_eq /FromForall=> <-. apply forall_intro. Qed.
604

605
Lemma tac_forall_specialize {A} Δ i p P (Φ : A  PROP) Q :
606
  envs_lookup i Δ = Some (p, P)  IntoForall P Φ 
607
  ( x : A,
608 609 610 611
      match envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ with
      | None => False
      | Some Δ' => envs_entails Δ' Q
      end) 
612
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
Proof.
614
  rewrite envs_entails_eq. intros ?? (x&?).
Joseph Tassarotti's avatar
Joseph Tassarotti committed
615
  destruct (envs_simple_replace) as [Δ'|] eqn:?; last done.
616
  rewrite envs_simple_replace_singleton_sound //; simpl.
617
  by rewrite (into_forall P) (forall_elim x) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
618 619
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
620
Lemma tac_forall_revert {A} Δ (Φ : A  PROP) :
621
  envs_entails Δ ( a, Φ a)   a, envs_entails Δ (Φ a).
622
Proof. rewrite envs_entails_eq => HΔ a. by rewrite HΔ (forall_elim a). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
623 624

(** * Existential *)
Robbert Krebbers's avatar
Robbert Krebbers committed
625
Lemma tac_exist {A} Δ P (Φ : A  PROP) :
626 627
  FromExist P Φ  ( a, envs_entails Δ (Φ a))  envs_entails Δ P.
Proof.
628
  rewrite envs_entails_eq => ? [a ?].
629 630
  rewrite -(from_exist P). eauto using exist_intro'.
Qed.
631

Robbert Krebbers's avatar
Robbert Krebbers committed
632
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A  PROP) Q :
633
  envs_lookup i Δ = Some (p, P)  IntoExist P Φ 
634 635 636 637 638
  ( a,
    match envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ with
    | Some Δ' => envs_entails Δ' Q
    | None => False
    end) 
639
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
Proof.
641
  rewrite envs_entails_eq => ?? HΦ. rewrite envs_lookup_sound //.
642
  rewrite (into_exist P) intuitionistically_if_exist sep_exist_r.
643 644
  apply exist_elim=> a; specialize (HΦ a) as Hmatch.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
645
  rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
646
Qed.
647

648
(** * Modalities *)
Joseph Tassarotti's avatar