coq_tactics.v 43.9 KB
Newer Older
1
From iris.bi Require Export bi telescopes.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
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 9
Local Open Scope lazy_bool_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
10
(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15 16
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
17
(** * Starting and stopping the proof mode *)
18
Lemma tac_start P : envs_entails (Envs Enil Enil 1) P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
19
Proof.
20 21
  rewrite envs_entails_eq !of_envs_eq /=.
  rewrite intuitionistically_True_emp left_id=><-.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27 28 29 30 31 32 33 34 35 36 37 38
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
39
(** * Basic rules *)
40
Lemma tac_eval Δ Q Q' :
41 42 43
  ( (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]. *)
44
  envs_entails Δ Q'  envs_entails Δ Q.
45
Proof. by intros <-. Qed.
46

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

62 63 64 65 66 67 68
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.

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
80 81
Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  FromAssumption p P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
  (let Δ' := envs_delete true i p Δ in
   if env_spatial_is_nil Δ' then TCTrue
85
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
86
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
88 89 90
  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
91
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93

94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
Lemma tac_assumption_coq Δ P Q :
  ( P) 
  FromAssumption true P Q 
  (if env_spatial_is_nil Δ then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ))) 
  envs_entails Δ Q.
Proof.
  rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
  rewrite envs_entails_eq -(left_id emp%I bi_sep (of_envs Δ)).
  rewrite -bi.intuitionistically_emp HP HPQ.
  destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
  - destruct H; by rewrite sep_elim_l.
Qed.

109
Lemma tac_rename Δ i j p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  envs_lookup i Δ = Some (p,P) 
111 112 113 114
  match envs_simple_replace i p (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
115
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Proof.
117 118
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
119
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
121

122 123
Lemma tac_clear Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
125
  envs_entails (envs_delete true i p Δ) Q 
126
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
128 129
  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
130
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132

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

Robbert Krebbers's avatar
Robbert Krebbers committed
136 137 138
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
139
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Proof.
141
  rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
142
  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
145
(** * Pure *)
146 147 148 149 150
Lemma tac_pure_intro Δ Q φ a :
  FromPure a Q φ 
  (if a then AffineEnv (env_spatial Δ) else TCTrue) 
  φ 
  envs_entails Δ Q.
151
Proof.
152 153
  intros ???. rewrite envs_entails_eq -(from_pure a Q). destruct a; simpl.
  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp.
154 155
  - by apply pure_intro.
Qed.
156

157 158
Lemma tac_pure Δ i p P φ Q :
  envs_lookup i Δ = Some (p, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  IntoPure P φ 
160
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
161
  (φ  envs_entails (envs_delete true i p Δ) Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Proof.
163
  rewrite envs_entails_eq=> ?? HPQ HQ.
164
  rewrite envs_lookup_sound //; simpl. destruct p; simpl.
165
  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
    by apply pure_elim_l.
167
  - destruct HPQ.
168
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
169
      by apply pure_elim_l.
170
    + rewrite (into_pure P) -(persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
171
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173
Qed.

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

177
(** * Intuitionistic *)
178
Lemma tac_intuitionistic Δ i p P P' Q :
179
  envs_lookup i Δ = Some (p, P) 
180
  IntoPersistent p P P' 
181
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
182 183 184 185 186
  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
187
Proof.
188 189
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
190
  destruct p; simpl; rewrite /bi_intuitionistically.
191
  - by rewrite -(into_persistent true P) /= wand_elim_r.
192
  - destruct HPQ.
193
    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
194
              (into_persistent _ P) wand_elim_r //.
195
    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
196
      by rewrite -{1}absorbingly_intuitionistically_into_persistently
197
        absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
198 199
Qed.

200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215
Lemma tac_spatial Δ i p P P' Q :
  envs_lookup i Δ = Some (p, P) 
  (if p then FromAffinely P' P else TCEq P' P) 
  match envs_replace i p false (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Proof.
  intros ? HP. destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq=> <-. rewrite envs_replace_singleton_sound //; simpl.
  destruct p; simpl; last destruct HP.
  - by rewrite intuitionistically_affinely (from_affinely P' P) wand_elim_r.
  - by rewrite wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
216
(** * Implication and wand *)
217
Lemma tac_impl_intro Δ i P P' Q R :
218
  FromImpl R P Q 
219
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
220
  FromAffinely P' P 
221 222 223 224 225
  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
226
Proof.
227 228
  destruct (envs_app _ _ _) eqn:?; last done.
  rewrite /FromImpl envs_entails_eq => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
229
  - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
230
    rewrite envs_app_singleton_sound //; simpl.
231
    rewrite -(from_affinely P' P) -affinely_and_lr.
232
    by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
233
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
234
    by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
Qed.
236
Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
237
  FromImpl R P Q 
238
  IntoPersistent false P P' 
239 240 241 242 243
  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
244
Proof.
245 246
  destruct (envs_app _ _ _) eqn:?; last done.
  rewrite /FromImpl envs_entails_eq => <- ??.
247
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
248
  rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
249
  by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
250
Qed.
251 252
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q  envs_entails Δ Q  envs_entails Δ R.
253 254 255
Proof.
  rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256

257
Lemma tac_wand_intro Δ i P Q R :
258
  FromWand R P Q 
259 260 261 262 263
  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
264
Proof.
265 266
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite /FromWand envs_entails_eq => <- HQ.
267
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Qed.
269 270

Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
271
  FromWand R P Q 
272
  IntoPersistent false P P' 
273
  TCOr (Affine P) (Absorbing Q) 
274 275 276 277 278
  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
279
Proof.
280 281
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite /FromWand envs_entails_eq => <- ? HPQ HQ.
282
  rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
283
  - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
284
            (into_persistent _ P) wand_elim_r //.
285
  - rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
286
    by rewrite -{1}absorbingly_intuitionistically_into_persistently
287
      absorbingly_sep_l wand_elim_r HQ.
288
Qed.
289 290
Lemma tac_wand_intro_drop Δ P Q R :
  FromWand R P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  TCOr (Affine P) (Absorbing Q) 
292
  envs_entails Δ Q 
293
  envs_entails Δ R.
294
Proof.
295
  rewrite envs_entails_eq /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
296 297 298 299
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
300 301 302
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
303
  envs_lookup j Δ' = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
304
  IntoWand q p R P1 P2 
305
  match envs_replace j q (p &&& q) (Esnoc Enil j P2) Δ' with
306 307 308
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
  rewrite envs_entails_eq /IntoWand. intros ?? HR ?.
311
  destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
312 313 314 315 316 317
  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
318 319
Qed.

320
Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
321
  envs_lookup j Δ = Some (q, R) 
322 323
  IntoWand q false R P1 P2 
  (if am then AddModal P1' P1 Q else TCEq P1' P1) 
324 325
  match
    ''(Δ1,Δ2)  envs_split (if neg is true then Right else Left)
326 327
                           js (envs_delete true j q Δ);
    Δ2'  envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2;
328 329 330 331 332 333 334
    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
335
Proof.
336
  rewrite envs_entails_eq. intros ?? Hmod HQ.
337 338
  destruct (_ = _) as [[Δ1 Δ2']|] eqn:?; last done.
  destruct HQ as [HP1 HQ].
Robbert Krebbers's avatar
Robbert Krebbers committed
339 340 341
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
342
  rewrite (envs_app_singleton_sound Δ2) //; simpl.
343 344 345 346 347 348 349 350
  rewrite -intuitionistically_if_idemp (into_wand q false) /=.
  destruct (negb am &&& q &&& env_spatial_is_nil Δ1) eqn:Hp; simpl.
  - move: Hp. rewrite !lazy_andb_true negb_true. intros [[-> ->] ?]; simpl.
    destruct Hmod. rewrite env_spatial_is_nil_intuitionistically // HP1.
    by rewrite assoc intuitionistically_sep_2 wand_elim_l wand_elim_r HQ.
  - rewrite intuitionistically_if_elim HP1. destruct am; last destruct Hmod.
    + by rewrite assoc -(comm _ P1') -assoc wand_trans HQ.
    + by rewrite assoc wand_elim_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
351 352
Qed.

353 354 355 356
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.
357
Lemma tac_unlock Δ Q : envs_entails Δ Q  envs_entails Δ (locked Q).
358 359
Proof. by unlock. Qed.

360
Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
361
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
362
  IntoWand q false R P1 P2 
363
  (if am then AddModal P1' P1 Q else TCEq P1' P1) 
364
  envs_entails (envs_delete true j q Δ) (P1'  locked Q') 
365
  Q' = (P2 - Q)%I 
366
  envs_entails Δ Q.
367
Proof.
368
  rewrite envs_entails_eq. intros ?? Hmod HPQ ->.
369
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
370 371
  rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
  destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
372 373
Qed.

374
Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
375
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
376
  IntoWand q true R P1 P2 
377
  FromPure a P1 φ 
378 379 380 381 382 383
  φ 
  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
384
Proof.
385 386
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
387
  rewrite -intuitionistically_if_idemp (into_wand q true) /=.
388 389 390
  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
391 392
Qed.

393 394
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
395 396
  IntoWand q true R P1 P2 
  Persistent P1 
397
  IntoAbsorbingly P1' P1 
398
  envs_entails (envs_delete true j q Δ) P1' 
399 400 401 402
  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
403
Proof.
404
  rewrite envs_entails_eq => ???? HP1 HQ.
405 406
  destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
  rewrite -HQ envs_lookup_sound //.
407
  rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
408
  rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
409
  rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
Ralf Jung's avatar
Ralf Jung committed
410
  rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
411 412
  rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
  rewrite (intuitionistically_intuitionistically_if q).
413
  by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
414 415
Qed.

416
Lemma tac_specialize_intuitionistic_helper Δ j q P R R' Q :
417
  envs_lookup j Δ = Some (q,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
418
  (if q then TCTrue else BiAffine PROP) 
419
  envs_entails Δ (<absorb> R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
420
  IntoPersistent false R R' 
421 422 423 424
  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
425
Proof.
426 427 428
  rewrite envs_entails_eq => ?? HR ??.
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
429
  rewrite envs_replace_singleton_sound //; destruct q; simpl.
430
  - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
Robbert Krebbers's avatar
Robbert Krebbers committed
431 432
      absorbingly_elim_persistently sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
433
  - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
Robbert Krebbers's avatar
Robbert Krebbers committed
434 435
      (into_persistent _ R) sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
436 437
Qed.

438 439
(* A special version of [tac_assumption] that does not do any of the
[FromAssumption] magic. *)
440
Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
441
  envs_lookup i Δ = Some (q,P) 
442
  envs_entails Δ (<absorb> P).
443 444
Proof.
  rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
Ralf Jung's avatar
Ralf Jung committed
445
  rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
446 447
Qed.

448 449 450 451 452
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 
453
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
Proof.
455 456 457
  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
458
  rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
459 460
Qed.

461
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
462 463
  into_ih : φ  of_envs Δ  Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
464
Proof. by rewrite envs_entails_eq /IntoIH. Qed.
465
Global Instance into_ih_forall {A} (φ : A  Prop) Δ Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
466
  ( x, IntoIH (φ x) Δ (Φ x))  IntoIH ( x, φ x) Δ ( x, Φ x)%I | 2.
467 468
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
469
  IntoIH φ Δ Q  IntoIH (ψ  φ) Δ (⌜ψ⌝  Q)%I | 1.
470
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
471 472 473

Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P 
474
  env_spatial_is_nil Δ = true 
475
  envs_entails Δ (<pers> P  Q) 
476
  envs_entails Δ Q.
477
Proof.
478
  rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
479
  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
480
  rewrite -(idemp bi_and ( (of_envs Δ))%I) {1}HP // HPQ.
Ralf Jung's avatar
Ralf Jung committed
481
  rewrite {1}intuitionistically_into_persistently_1 intuitionistically_elim impl_elim_r //.
482 483
Qed.

484 485 486 487 488
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.
489
Proof.
490 491
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
  rewrite envs_entails_eq=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
492
  by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
493 494
Qed.

495
Definition IntoEmpValid (φ : Type) (P : PROP) := φ   P.
496 497 498
(** These lemmas are [Defined] because the guardedness checker must see
through them. See https://gitlab.mpi-sws.org/iris/iris/issues/274. For the
same reason, their bodies use as little automation as possible. *)
499
Lemma into_emp_valid_here φ P : AsEmpValid φ P  IntoEmpValid φ P.
500
Proof. by intros [??]. Defined.
501 502
Lemma into_emp_valid_impl (φ ψ : Type) P :
  φ  IntoEmpValid ψ P  IntoEmpValid (φ  ψ) P.
503
Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
504 505
Lemma into_emp_valid_forall {A} (φ : A  Type) P x :
  IntoEmpValid (φ x) P  IntoEmpValid ( x : A, φ x) P.
506
Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
507 508 509
Lemma into_emp_valid_tforall {TT : tele} (φ : TT  Prop) P x :
  IntoEmpValid (φ x) P  IntoEmpValid (.. x : TT, φ x) P.
Proof. rewrite /IntoEmpValid tforall_forall=> Hi1 Hi2. apply Hi1, Hi2. Defined.
510
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P  φ   P.
511 512 513 514 515 516 517
Proof. intros HP. apply HP. Defined.

(** When called by the proof mode, the proof of [P] is produced by calling
[into_emp_valid_proj]. That call must be transparent to the guardedness
checker, per https://gitlab.mpi-sws.org/iris/iris/issues/274; hence, it must
be done _outside_ [tac_pose_proof], so the latter can remain opaque. *)
Lemma tac_pose_proof Δ j P Q :
Gregory Malecha's avatar
Gregory Malecha committed
518
  ( P) 
519 520 521 522 523
  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
524
Proof.
525
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
526 527
  rewrite envs_entails_eq => HP <-. rewrite envs_app_singleton_sound //=.
  by rewrite -HP /= intuitionistically_emp emp_wand.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529
Qed.

530 531 532 533 534 535 536 537 538 539
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.
540
Proof.
541 542 543 544
  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 [? ->] <-.
545 546
  rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
  by rewrite wand_elim_r.
547 548
Qed.

549 550
Lemma tac_apply Δ i p R P1 P2 :
  envs_lookup i Δ = Some (p, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
551
  IntoWand p false R P1 P2 
552
  envs_entails (envs_delete true i p Δ) P1  envs_entails Δ P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
Proof.
554
  rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_sound //.
555
  by rewrite (into_wand p false) /= HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
556 557 558
Qed.

(** * Conjunction splitting *)
559
Lemma tac_and_split Δ P Q1 Q2 :
560
  FromAnd P Q1 Q2  envs_entails Δ Q1  envs_entails Δ Q2  envs_entails Δ P.
561
Proof. rewrite envs_entails_eq. intros. rewrite -(from_and P). by apply and_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
562 563

(** * Separating conjunction splitting *)
564
Lemma tac_sep_split Δ d js P Q1 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
565
  FromSep P Q1 Q2 
566 567 568 569
  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
570
Proof.
571 572
  destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
  rewrite envs_entails_eq=>? [HQ1 HQ2].
573
  rewrite envs_split_sound //. by rewrite HQ1 HQ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
574 575 576
Qed.

(** * Combining *)
Robbert Krebbers's avatar
Robbert Krebbers committed
577
Class FromSeps {PROP : bi} (P : PROP) (Qs : list PROP) :=
578
  from_seps : [] Qs  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
579 580
Arguments FromSeps {_} _%I _%I.
Arguments from_seps {_} _%I _%I {_}.
581

Robbert Krebbers's avatar
Robbert Krebbers committed
582 583
Global Instance from_seps_nil : @FromSeps PROP emp [].
Proof. by rewrite /FromSeps. Qed.
584 585 586
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
587 588
  FromSeps P' Qs  FromSep P Q P'  FromSeps P (Q :: Qs) | 2.
Proof. by rewrite /FromSeps /FromSep /= => ->. Qed.
589 590

Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
591
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) 
592 593
  FromSeps P Ps 
  envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 
594
  envs_entails Δ3 Q  envs_entails Δ1 Q.
595
Proof.
596
  rewrite envs_entails_eq => ??? <-. rewrite envs_lookup_delete_list_sound //.
597
  rewrite from_seps. rewrite envs_app_singleton_sound //=.
598
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
599 600 601
Qed.

(** * Conjunction/separating conjunction elimination *)
602
Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
603 604
  envs_lookup i Δ = Some (p, P) 
  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) 
605 606 607 608 609
  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
610
Proof.
611
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
612
  rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
613
  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
614
  - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
615 616
Qed.

617 618 619
(* 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. *)
620
Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
621
  envs_lookup i Δ = Some (p, P) 
622 623
  (if p then IntoAnd p P P1 P2 : Type else
    TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
624
      (if d is Left then TCOr (Affine P2) (Absorbing Q)
625
       else TCOr (Affine P1) (Absorbing Q)))) 
626 627 628 629
  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.
630
Proof.
631 632
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_eq => ? HP HQ.
633
  rewrite envs_simple_replace_singleton_sound //=. destruct p.
634
  { rewrite (into_and _ P) HQ. destruct d; simpl.
635 636
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
Robbert Krebbers's avatar
Robbert Krebbers committed
637
  destruct HP as [?|[??]].
638
  { rewrite (into_and _ P) HQ. destruct d; simpl.
639 640
    - by rewrite and_elim_l wand_elim_r.
    - by rewrite and_elim_r wand_elim_r. }
641
  rewrite (into_sep P) HQ. destruct d; simpl.
642 643
  - by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
  - by rewrite -assoc wand_elim_r sep_elim_r.
644 645
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
646
(** * Framing *)
647
Lemma tac_frame_pure Δ (φ : Prop) P Q :
648
  φ  Frame true ⌜φ⌝ P Q  envs_entails Δ Q  envs_entails Δ P.
649
Proof.
650
  rewrite envs_entails_eq => ? Hframe ->. rewrite -Hframe /=.
651
  rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
652
  auto using and_intro, pure_intro.
653
Qed.
654

655 656
Lemma tac_frame Δ i p R P Q :
  envs_lookup i Δ = Some (p, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
657
  Frame p R P Q 
658
  envs_entails (envs_delete false i p Δ) Q  envs_entails Δ P.
Robbert Krebbers's avatar
Robbert Krebbers committed
659
Proof.
660
  rewrite envs_entails_eq. intros ? Hframe HQ.
661
  rewrite (envs_lookup_sound' _ false) //. by