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

8 9
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.

10
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15 16 17 18 19 20 21 22
  Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

Record envs_wf {M} (Δ : envs M) := {
  env_persistent_valid : env_wf (env_persistent Δ);
  env_spatial_valid : env_wf (env_spatial Δ);
  envs_disjoint i : env_persistent Δ !! i = None  env_spatial Δ !! i = None
}.

23
Definition of_envs {M} (Δ : envs M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
24
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
25 26
Instance: Params (@of_envs) 1.

27 28 29 30 31 32
Definition envs_entails {M} (Δ : envs M) (Q : uPred M) : Prop :=
  of_envs Δ  Q.
Arguments envs_entails {_} _ _%I.
Typeclasses Opaque envs_entails.
Instance: Params (@envs_entails) 1.

33 34 35 36
Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
  env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
37

38
Definition envs_dom {M} (Δ : envs M) : list ident :=
39
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
Definition envs_lookup {M} (i : ident) (Δ : envs M) : option (bool * uPred M) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44 45 46
  let (Γp,Γs) := Δ in
  match env_lookup i Γp with
  | Some P => Some (true, P) | None => P  env_lookup i Γs; Some (false, P)
  end.

47
Definition envs_delete {M} (i : ident) (p : bool) (Δ : envs M) : envs M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50 51 52
  let (Γp,Γs) := Δ in
  match p with
  | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
  end.

53
Definition envs_lookup_delete {M} (i : ident)
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56 57
    (Δ : envs M) : option (bool * uPred M * envs M) :=
  let (Γp,Γs) := Δ in
  match env_lookup_delete i Γp with
  | Some (P,Γp') => Some (true, P, Envs Γp' Γs)
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  | None => ''(P,Γs')  env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60
  end.

61
Fixpoint envs_lookup_delete_list {M} (js : list ident) (remove_persistent : bool)
62 63 64 65
    (Δ : envs M) : option (bool * list (uPred M) * envs M) :=
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68
     ''(p,P,Δ')  envs_lookup_delete j Δ;
     let Δ' := if p : bool then (if remove_persistent then Δ' else Δ) else Δ' in
     ''(q,Hs,Δ'')  envs_lookup_delete_list js remove_persistent Δ';
69 70 71
     Some (p && q, P :: Hs, Δ'')
  end.

72
Definition envs_snoc {M} (Δ : envs M)
73
    (p : bool) (j : ident) (P : uPred M) : envs M :=
74 75 76
  let (Γp,Γs) := Δ in
  if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).

Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81 82 83 84
Definition envs_app {M} (p : bool)
    (Γ : env (uPred M)) (Δ : envs M) : option (envs M) :=
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_app Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_app Γ Γs; Some (Envs Γp Γs')
  end.

85
Definition envs_simple_replace {M} (i : ident) (p : bool) (Γ : env (uPred M))
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87 88 89 90 91 92
    (Δ : envs M) : option (envs M) :=
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_replace i Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_replace i Γ Γs; Some (Envs Γp Γs')
  end.

93
Definition envs_replace {M} (i : ident) (p q : bool) (Γ : env (uPred M))
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96 97
    (Δ : envs M) : option (envs M) :=
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

98
Definition env_spatial_is_nil {M} (Δ : envs M) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100
  if env_spatial Δ is Enil then true else false.

101 102 103
Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
  Envs (env_persistent Δ) Enil.

104 105 106
Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
  Envs Enil (env_spatial Δ).

107
Fixpoint envs_split_go {M}
108
    (js : list ident) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
109 110 111
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113
     ''(p,P,Δ1')  envs_lookup_delete j Δ1;
     if p : bool then envs_split_go js Δ1 Δ2 else
114 115
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
116 117 118
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {M} (d : direction)
119
    (js : list ident) (Δ : envs M) : option (envs M * envs M) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  ''(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
121
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
122

Robbert Krebbers's avatar
Robbert Krebbers committed
123 124
(* Coq versions of the tactics *)
Section tactics.
125
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
126 127 128 129
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

130
Lemma of_envs_def Δ :
Ralf Jung's avatar
Ralf Jung committed
131
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
132 133
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
134 135 136 137 138 139 140 141 142 143
Lemma envs_lookup_delete_Some Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ')
   envs_lookup i Δ = Some (p,P)  Δ' = envs_delete i p Δ.
Proof.
  rewrite /envs_lookup /envs_delete /envs_lookup_delete.
  destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct.
  destruct (Γp !! i), (Γs !! i); naive_solver.
Qed.

Lemma envs_lookup_sound Δ i p P :
144 145
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  ?p P  of_envs (envs_delete i p Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
146
Proof.
147
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
149
  - rewrite (env_lookup_perm Γp) //= persistently_sep.
150
    ecancel [ [] _;  P; [] Γs]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
155
    ecancel [ [] _; P; [] (env_delete _ _)]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157 158 159
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
160 161
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  P  of_envs (envs_delete i p Δ).
162
Proof. intros. rewrite envs_lookup_sound //. by rewrite persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Lemma envs_lookup_persistent_sound Δ i P :
164
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Proof.
166
  intros. apply (persistently_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169
Qed.

Lemma envs_lookup_split Δ i p P :
170
  envs_lookup i Δ = Some (p,P)  of_envs Δ  ?p P  (?p P - of_envs Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
171
Proof.
172
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
174
  - rewrite (env_lookup_perm Γp) //= persistently_sep.
175
    rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
178
    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181 182
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
183
  envs_lookup_delete i Δ = Some (p,P,Δ')  of_envs Δ  ?p P  of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
186
  envs_lookup_delete i Δ = Some (p,P,Δ')  of_envs Δ  P  of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
187 188
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

189
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
190 191
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
192 193
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
194
  { by rewrite persistently_pure left_id. }
195 196 197
  destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
  apply envs_lookup_delete_Some in Hj as [Hj ->].
  destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
198
  rewrite persistently_if_sep -assoc. destruct q1; simpl.
199
  - destruct rp.
200 201 202
    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (persistently_elim_if q2).
    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (persistently_elim_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite persistently_if_elim.
203 204
Qed.

205 206 207 208 209 210 211 212 213 214 215 216 217 218
Lemma envs_lookup_snoc Δ i p P :
  envs_lookup i Δ = None  envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc.
Qed.
Lemma envs_lookup_snoc_ne Δ i j p P :
  i  j  envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne.
Qed.

Lemma envs_snoc_sound Δ p i P :
219
  envs_lookup i Δ = None  of_envs Δ  ?p P - of_envs (envs_snoc Δ p i P).
220 221 222 223 224 225
Proof.
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
226
      intros j; destruct (ident_beq_reflect j i); naive_solver.
227
    + by rewrite persistently_sep assoc.
228 229
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
230
      intros j; destruct (ident_beq_reflect j i); naive_solver.
231 232 233
    + solve_sep_entails.
Qed.

234 235
Lemma envs_app_sound Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ'  of_envs Δ  ?p [] Γ - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
Proof.
237
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
238 239 240
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
241
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
242 243 244 245
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γp') //.
246
      rewrite big_opL_app persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
247 248
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
249
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251 252
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
253
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
254 255 256 257
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
258
  of_envs (envs_delete i p Δ)  ?p [] Γ - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
261
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
262 263
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
264
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
265 266 267 268
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γp') //.
269
      rewrite big_opL_app persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
270 271
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
272
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
273 274 275
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
276
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278 279 280
Qed.

Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
281
  of_envs Δ  ?p P  (?p [] Γ - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283 284
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
285 286
  envs_replace i p q Γ Δ = Some Δ' 
  of_envs (envs_delete i p Δ)  ?q [] Γ - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288 289 290 291 292 293 294
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
295
  of_envs Δ  ?p P  (?q [] Γ - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
296 297
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

298 299
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
Robbert Krebbers's avatar
Robbert Krebbers committed
300
  = ''(p,P)  envs_lookup j Δ; if p : bool then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Proof.
302 303 304
  rewrite /envs_lookup /envs_clear_spatial.
  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
  by destruct (Γs !! j).
Robbert Krebbers's avatar
Robbert Krebbers committed
305 306
Qed.

307 308
Lemma envs_clear_spatial_sound Δ :
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
309
Proof.
310 311
  rewrite /of_envs /envs_clear_spatial /=; apply pure_elim_sep_l=> Hwf.
  rewrite right_id -assoc; apply sep_intro_True_l; [apply pure_intro|done].
312 313 314
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

315
Lemma env_spatial_is_nil_persistent Δ :
316
  env_spatial_is_nil Δ = true  Persistent (of_envs Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
317
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
318
Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
319

320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339
Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ 
  envs_lookup i Δ = Some (p,P)  envs_lookup i (envs_delete i p Δ) = None.
Proof.
  rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - rewrite env_lookup_env_delete //. revert Hlookup.
    destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _).
  - rewrite env_lookup_env_delete //. by destruct (Γp !! _).
Qed.
Lemma envs_lookup_envs_delete_ne Δ i j p :
  i  j  envs_lookup i (envs_delete j p Δ) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
  - by rewrite env_lookup_env_delete_ne.
  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
Qed.

Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
  ( j P, envs_lookup j Δ1 = Some (false, P)  envs_lookup j Δ2 = None) 
340 341
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
342 343 344 345 346 347 348 349 350 351 352 353 354 355
Proof.
  revert Δ1 Δ2 Δ1' Δ2'.
  induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
  apply pure_elim with (envs_wf Δ1); [unfold of_envs; solve_sep_entails|]=> Hwf.
  destruct (envs_lookup_delete j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq; auto.
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
  rewrite -(IH _ _ _ _ _ HΔ); last first.
  { intros j' P'; destruct (decide (j = j')) as [->|].
    - by rewrite (envs_lookup_envs_delete _ _ _ P).
    - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
356
Lemma envs_split_sound Δ d js Δ1 Δ2 :
357
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
358
Proof.
359
  rewrite /envs_split=> ?. rewrite -(idemp uPred_and (of_envs Δ)).
360
  rewrite {2}envs_clear_spatial_sound sep_elim_l and_sep_r.
361 362 363
  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
  apply envs_split_go_sound in HΔ as ->; last first.
  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
364
  destruct d; simplify_eq/=; solve_sep_entails.
365 366
Qed.

367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
Global Instance envs_Forall2_refl (R : relation (uPred M)) :
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Global Instance envs_Forall2_sym (R : relation (uPred M)) :
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Global Instance envs_Forall2_trans (R : relation (uPred M)) :
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Lemma envs_Forall2_impl (R R' : relation (uPred M)) Δ1 Δ2 :
  envs_Forall2 R Δ1 Δ2  ( P Q, R P Q  R' P Q)  envs_Forall2 R' Δ1 Δ2.
Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.

Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in *.
386 387
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
388 389 390 391 392
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Global Instance of_envs_proper : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
393 394
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
395
Qed.
396 397

Global Instance Envs_proper (R : relation (uPred M)) :
398 399 400
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
Proof. by constructor. Qed.

401 402 403 404 405 406 407
Global Instance envs_entails_proper :
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails M).
Proof. solve_proper. Qed.
Global Instance envs_entails_flip_mono :
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails M).
Proof. rewrite /envs_entails=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
408
(** * Adequacy *)
409
Lemma tac_adequate P : envs_entails (Envs Enil Enil) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
Proof.
411
  rewrite /envs_entails=> <-. rewrite /of_envs /= persistently_pure !right_id.
412
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
413 414 415
Qed.

(** * Basic rules *)
416 417 418 419 420
Lemma tac_eval Δ Q Q' :
  Q = Q' 
  envs_entails Δ Q'  envs_entails Δ Q.
Proof. by intros ->. Qed.

421
Lemma tac_assumption Δ i p P Q :
422 423 424
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q 
  envs_entails Δ Q.
Proof. intros. by rewrite /envs_entails envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
425 426 427 428

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
429 430
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
431
Proof.
432
  rewrite /envs_entails=> ?? <-. rewrite envs_simple_replace_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
433 434 435
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.
Lemma tac_clear Δ Δ' i p P Q :
436 437 438 439 440
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  envs_entails Δ' Q  envs_entails Δ Q.
Proof.
  rewrite /envs_entails=> ? <-. by rewrite envs_lookup_delete_sound // sep_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
441 442

(** * False *)
443 444
Lemma tac_ex_falso Δ Q : envs_entails Δ False  envs_entails Δ Q.
Proof. by rewrite /envs_entails -(False_elim Q). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
445 446

(** * Pure *)
447 448
Lemma tac_pure_intro Δ Q φ : FromPure Q φ  φ  envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
449

Robbert Krebbers's avatar
Robbert Krebbers committed
450
Lemma tac_pure Δ Δ' i p P φ Q :
451
  envs_lookup_delete i Δ = Some (p, P, Δ')  IntoPure P φ 
452
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
453
Proof.
454
  rewrite /envs_entails=> ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
455
  rewrite (into_pure P); by apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
456 457
Qed.

458 459
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝  Q)  (φ  envs_entails Δ Q).
Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
460 461

(** * Later *)
462 463 464 465 466
Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
  into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
  into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
  into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
467 468
}.

469
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
470
Proof. constructor. Qed.
471 472 473
Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
  IntoLaterNEnv n Γ1 Γ2  IntoLaterN n P Q 
  IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
474 475
Proof. by constructor. Qed.

476 477 478
Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
  IntoLaterNEnv n Γp1 Γp2  IntoLaterNEnv n Γs1 Γs2 
  IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
479
Proof. by split. Qed.
480

481 482
Lemma into_laterN_env_sound n Δ1 Δ2 :
  IntoLaterNEnvs n Δ1 Δ2  of_envs Δ1  ^n (of_envs Δ2).
Robbert Krebbers's avatar
Robbert Krebbers committed
483
Proof.
484 485
  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
  repeat apply sep_mono; try apply persistently_mono.
486
  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
487
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
488 489
  - induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
  - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
490 491
Qed.

492
Lemma tac_next Δ Δ' n Q Q' :
493 494 495 496 497 498
  FromLaterN n Q Q'  IntoLaterNEnvs n Δ Δ' 
  envs_entails Δ' Q'  envs_entails Δ Q.
Proof.
  rewrite /envs_entails=> ?? HQ.
  by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
499 500

Lemma tac_löb Δ Δ' i Q :
501
  env_spatial_is_nil Δ = true 
502
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
503
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
504
Proof.
505 506
  rewrite /envs_entails=> ?? HQ.
  rewrite -(persistently_elim Q) -(löb ( Q)) -persistently_later.
507
  apply impl_intro_l, (persistently_intro _ _).
508
  rewrite envs_app_sound //; simpl.
509
  by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
510 511
Qed.

512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542
(** * Persistence and plainness modality *)
Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
  into_plain_env_subenv : env_subenv Γ2 Γ1;
  into_plain_env_plain : Plain ([] Γ2);
}.
Class IntoPersistentEnvs (p : bool) (Δ1 Δ2 : envs M) := {
  into_persistent_envs_persistent :
    if p then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
    else env_persistent Δ1 = env_persistent Δ2;
  into_persistent_envs_spatial : env_spatial Δ2 = Enil
}.

Global Instance into_plain_env_nil : IntoPlainEnv Enil Enil.
Proof. constructor. constructor. simpl; apply _. Qed.
Global Instance into_plain_env_snoc_plain Γ1 Γ2 i P :
  Plain P  IntoPlainEnv Γ1 Γ2 
  IntoPlainEnv (Esnoc Γ1 i P) (Esnoc Γ2 i P) | 1.
Proof. intros ? [??]; constructor. by constructor. simpl; apply _. Qed.
Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P :
  IntoPlainEnv Γ1 Γ2  IntoPlainEnv (Esnoc Γ1 i P) Γ2 | 2.
Proof. intros [??]; constructor. by constructor. done. Qed.

Global Instance into_persistent_envs_false Γp Γs :
  IntoPersistentEnvs false (Envs Γp Γs) (Envs Γp Enil).
Proof. by split. Qed.
Global Instance into_persistent_envs_true Γp1 Γp2 Γs1 :
  IntoPlainEnv Γp1 Γp2 
  IntoPersistentEnvs true (Envs Γp1 Γs1) (Envs Γp2 Enil).
Proof. by split. Qed.

Lemma into_persistent_envs_sound (p : bool) Δ1 Δ2 :
543 544
  IntoPersistentEnvs p Δ1 Δ2 
  of_envs Δ1  (if p then  of_envs Δ2 else  of_envs Δ2).
545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560
Proof.
  rewrite /of_envs. destruct Δ1 as [Γp1 Γs1], Δ2 as [Γp2 Γs2]=> -[/= Hp ->].
  apply pure_elim_sep_l=> Hwf. rewrite sep_elim_l. destruct p; simplify_eq/=.
  - destruct Hp. rewrite right_id plainly_sep plainly_pure.
    apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; eauto using Enil_wf, env_subenv_wf.
    + rewrite persistently_elim plainly_persistently plainly_plainly.
      by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
  - rewrite right_id persistently_sep persistently_pure.
    apply sep_intro_True_l; [apply pure_intro|by rewrite persistent_persistently].
    destruct Hwf; constructor; simpl; eauto using Enil_wf.
Qed.

Lemma tac_always_intro Δ Δ' p Q Q' :
  FromAlways p Q' Q 
  IntoPersistentEnvs p Δ Δ' 
561
  envs_entails Δ' Q  envs_entails Δ Q'.
562
Proof.
563 564
  rewrite /envs_entails=> ?? HQ.
  rewrite into_persistent_envs_sound -(from_always _ Q').
565
  destruct p; auto using persistently_mono, plainly_mono.
566
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
567 568

Lemma tac_persistent Δ Δ' i p P P' Q :
569
  envs_lookup i Δ = Some (p, P) 
570
  IntoPersistent p P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
571
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
572
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
Proof.
574
  rewrite /envs_entails=> ? HP ? <-. rewrite envs_replace_sound //; simpl.
575
  by rewrite right_id (into_persistent _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
576 577 578 579
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
580
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
581
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
582
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
583
Proof.
584 585
  rewrite /envs_entails=> ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
  - rewrite (persistent (of_envs Δ)) envs_app_sound //; simpl.
586
    by rewrite right_id -persistently_impl_wand persistently_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
587
  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
588
    by rewrite and_sep_l right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
589 590
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
591
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
592
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
593
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
594
Proof.
595 596
  rewrite /envs_entails=> ?? HQ.
  rewrite envs_app_sound //=; simpl. apply impl_intro_l.
597
  rewrite (_ : P = ?false P) // (into_persistent false P).
598
  by rewrite right_id persistently_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
Qed.
600

601 602
Lemma tac_impl_intro_drop Δ P Q : envs_entails Δ Q  envs_entails Δ (P  Q).
Proof. rewrite /envs_entails=> ?. apply impl_intro_l. by rewrite and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
603 604

Lemma tac_wand_intro Δ Δ' i P Q :
605 606
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
  envs_entails Δ' Q  envs_entails Δ (P - Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
607
Proof.
608 609
  rewrite /envs_entails=> ? HQ.
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
610 611
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
612
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
613
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
614
  envs_entails Δ' Q  envs_entails Δ (P - Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
615
Proof.
616
  rewrite /envs_entails => ?? <-. rewrite envs_app_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
617 618
  rewrite right_id. by apply wand_mono.
Qed.
619 620
Lemma tac_wand_intro_drop Δ P Q : envs_entails Δ Q  envs_entails Δ (P - Q).
Proof. rewrite /envs_entails=> <-. apply wand_intro_l. by rewrite sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
621 622 623 624 625

(* 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. *)
Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
  envs_lookup_delete i Δ = Some (p, P1, Δ') 
626
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
627
  IntoWand p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
628 629 630 631 632
  match p with
  | true  => envs_simple_replace j q (Esnoc Enil j P2) Δ
  | false => envs_replace j q false (Esnoc Enil j P2) Δ'
             (* remove [i] and make [j] spatial *)
  end = Some Δ'' 
633
  envs_entails Δ'' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
634
Proof.
635
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
Robbert Krebbers's avatar
Robbert Krebbers committed
636
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
637
    rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
638
    + by rewrite persistently_wand persistent_persistently !wand_elim_r.
639
    + by rewrite !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
640 641
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
642
    by rewrite right_id assoc (into_wand _ R) persistently_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
643 644
Qed.

645
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
646
  envs_lookup_delete j Δ = Some (q, R, Δ') 
647
  IntoWand false R P1 P2  AddModal P1' P1 Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
648
  (''(Δ1,Δ2)  envs_split (if neg is true then Right else Left) js Δ';
649
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
650
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
651
  envs_entails Δ1 P1'  envs_entails Δ2' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
652
Proof.
653
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
654 655 656 657
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
  rewrite (envs_app_sound Δ2) //; simpl.
658
  rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
659
  rewrite -(add_modal P1' P1 Q). apply sep_mono_r, wand_intro_l.
660
  by rewrite persistently_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
661 662
Qed.

663
Lemma tac_unlock Δ Q : envs_entails Δ Q  envs_entails Δ (locked Q).
664 665 666 667
Proof. by unlock. Qed.

Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
668
  IntoWand false R P1 P2 
669
  AddModal P1' P1 Q 
670
  envs_entails Δ' (P1'  locked Q') 
671
  Q' = (P2 - Q)%I 
672
  envs_entails Δ Q.
673
Proof.
674
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
675
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
676
  rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
677
  rewrite -{2}(add_modal P1' P1 Q). apply sep_mono_r, wand_intro_l.
678 679 680
  by rewrite assoc !wand_elim_r.
Qed.

681
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
682
  envs_lookup j Δ = Some (q, R) 
683
  IntoWand false R P1 P2  FromPure P1 φ 
684
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
685
  φ  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
686
Proof.
687
  rewrite /envs_entails=> ????? <-. rewrite envs_simple_replace_sound //; simpl.
688
  rewrite right_id (into_wand _ R) -(from_pure P1) pure_True //.
689
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
690 691
Qed.

692
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
693
  envs_lookup_delete j Δ = Some (q, R, Δ') 
694
  IntoWand false R P1 P2  Persistent P1 
695
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
696
  envs_entails Δ' P1  envs_entails Δ'' Q  envs_entails Δ Q.
697
Proof.
698
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
699
  rewrite envs_lookup_sound //.
700
  rewrite -(idemp uPred_and (of_envs (envs_delete _ _ _))).
701
  rewrite {1}HP1 (persistent P1) persistently_and_sep_l assoc.
702
  rewrite envs_simple_replace_sound' //; simpl.
703
  rewrite right_id (into_wand _ R) (persistently_elim_if q) -persistently_if_sep wand_elim_l.
704 705 706 707 708
  by rewrite wand_elim_r.
Qed.

Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
  envs_lookup j Δ = Some (q,P) 
709
  envs_entails Δ R  Persistent R 
710
  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' 
711
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
712
Proof.
713