coq_tactics.v 39.9 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 environments classes.
Ralf Jung's avatar
Ralf Jung committed
4
From stdpp Require Import stringmap hlist.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Import bi.
7
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

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

Robbert Krebbers's avatar
Robbert Krebbers committed
11 12
Record envs (PROP : bi) :=
  Envs { env_persistent : env PROP; env_spatial : env PROP }.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15 16 17
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

Robbert Krebbers's avatar
Robbert Krebbers committed
18
Record envs_wf {PROP} (Δ : envs PROP) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21 22 23
  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
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
24 25
Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
26
Instance: Params (@of_envs) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Arguments of_envs : simpl never.
28

Robbert Krebbers's avatar
Robbert Krebbers committed
29
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
30 31 32
  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
33

Robbert Krebbers's avatar
Robbert Krebbers committed
34
Definition envs_dom {PROP} (Δ : envs PROP) : list string :=
35
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
36

Robbert Krebbers's avatar
Robbert Krebbers committed
37
Definition envs_lookup {PROP} (i : string) (Δ : envs PROP) : option (bool * PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39
  let (Γp,Γs) := Δ in
  match env_lookup i Γp with
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
  | Some P => Some (true, P)
  | None => P  env_lookup i Γs; Some (false, P)
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
  end.

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
Definition envs_snoc {PROP} (Δ : envs PROP)
    (p : bool) (j : string) (P : PROP) : envs PROP :=
72 73 74
  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
75 76
Definition envs_app {PROP : bi} (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81 82
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
Definition envs_simple_replace {PROP : bi} (i : string) (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87 88 89 90
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
91 92
Definition envs_replace {PROP : bi} (i : string) (p q : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

Robbert Krebbers's avatar
Robbert Krebbers committed
96
Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98
  if env_spatial Δ is Enil then true else false.

Robbert Krebbers's avatar
Robbert Krebbers committed
99
Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
100 101
  Envs (env_persistent Δ) Enil.

Robbert Krebbers's avatar
Robbert Krebbers committed
102
Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
103 104
  Envs Enil (env_spatial Δ).

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

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

Lemma of_envs_eq Δ :
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
130 131
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
132 133 134 135 136 137 138 139 140 141
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 :
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  envs_delete i p Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147 148
  - rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
    by rewrite (env_lookup_perm Γp) //= bare_persistently_sep -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151 152 153
    rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Lemma envs_lookup_persistent_sound Δ i P :
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  envs_lookup i Δ = Some (true,P)  Δ   P  Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
157 158 159
  intros. rewrite -persistently_and_bare_sep_l. apply and_intro; last done.
  rewrite envs_lookup_sound //; simpl.
  by rewrite -persistently_and_bare_sep_l and_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161 162
Qed.

Lemma envs_lookup_split Δ i p P :
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  (?p P - Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169
  - rewrite pure_True // left_id.
    rewrite (env_lookup_perm Γp) //= bare_persistently_sep.
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
171
    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173 174 175
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  ?p P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.

179
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ')  Δ  ?p [] Ps  Δ'.
181 182
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
  { by rewrite bare_persistently_emp left_id. }
184 185 186
  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/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  rewrite bare_persistently_if_sep -assoc. destruct q1; simpl.
188
  - destruct rp.
Robbert Krebbers's avatar
Robbert Krebbers committed
189 190 191 192 193
    + rewrite envs_lookup_sound //; simpl.
      by rewrite IH // (bare_persistently_bare_persistently_if q2).
    + rewrite envs_lookup_persistent_sound //.
      by rewrite IH // (bare_persistently_bare_persistently_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite bare_persistently_if_elim.
194 195
Qed.

196 197 198 199 200 201 202 203 204 205 206 207 208 209
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 :
Robbert Krebbers's avatar
Robbert Krebbers committed
210
  envs_lookup i Δ = None  Δ  ?p P - envs_snoc Δ p i P.
211
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
213 214
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
  - apply and_intro; [apply pure_intro|].
216
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
217
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
218 219
    + by rewrite bare_persistently_sep assoc.
  - apply and_intro; [apply pure_intro|].
220
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
221
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
222 223 224
    + solve_sep_entails.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
225
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229 230
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235
    + 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') //.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
      rewrite big_opL_app bare_persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
237 238
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241 242
    + 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.
243
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
244 245 246 247
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
248
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
252 253
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256 257 258
    + 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') //.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
      rewrite big_opL_app bare_persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
260 261
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
263 264 265
    + 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.
266
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
267 268 269 270
Qed.

Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
271
  Δ  ?p P  (?p [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
272 273 274
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
Robbert Krebbers's avatar
Robbert Krebbers committed
275
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
276 277 278 279 280 281 282 283
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 Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
284
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
285 286
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

287 288 289
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
  = '(p,P)  envs_lookup j Δ; if p then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
Proof.
291 292 293
  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
294 295
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
296 297
Lemma envs_clear_spatial_sound Δ :
  Δ  envs_clear_spatial Δ  [] env_spatial Δ.
298
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
299 300 301
  rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
302 303
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
304 305 306 307 308 309 310
Lemma env_spatial_is_nil_bare_persistently Δ :
  env_spatial_is_nil Δ = true  Δ   Δ.
Proof.
  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
  rewrite !right_id {1}bare_and_l persistently_and.
  by rewrite persistently_bare persistently_idemp persistently_pure.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
311

312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331
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) 
Robbert Krebbers's avatar
Robbert Krebbers committed
332 333
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
  Δ1  Δ2  Δ1'  Δ2'.
334 335 336
Proof.
  revert Δ1 Δ2 Δ1' Δ2'.
  induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
337 338
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite /of_envs !and_elim_l sep_elim_l. }
339 340 341 342 343 344 345 346 347 348 349
  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.
Lemma envs_split_sound Δ lr js Δ1 Δ2 :
350
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
351
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
352 353 354 355 356
  rewrite /envs_split=> ?. rewrite -(idemp bi_and Δ).
  rewrite {2}envs_clear_spatial_sound.
  rewrite (env_spatial_is_nil_bare_persistently (envs_clear_spatial _)) //.
  rewrite -persistently_and_bare_sep_l.
  rewrite (and_elim_l ( _)%I) persistently_and_bare_sep_r bare_persistently_elim.
357 358 359 360 361 362
  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=> ->. }
  destruct lr; simplify_eq; solve_sep_entails.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
363
Global Instance envs_Forall2_refl (R : relation PROP) :
364 365
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
Global Instance envs_Forall2_sym (R : relation PROP) :
367 368
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
369
Global Instance envs_Forall2_trans (R : relation PROP) :
370 371
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
373 374
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
375
Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
376 377 378
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
379
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
380
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
381 382
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
383 384 385
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
386 387
Global Instance of_envs_proper :
  Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
388
Proof.
389 390
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
391
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
392 393
Global Instance Envs_mono (R : relation PROP) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
394 395
Proof. by constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
396
(** * Adequacy *)
397
Lemma tac_adequate P : (Envs Enil Enil  P)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
398
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
399 400
  intros <-. rewrite /of_envs /= bare_persistently_emp left_id.
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
401 402 403
Qed.

(** * Basic rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
404 405 406 407 408 409 410
Lemma tac_emp_intro Δ :
  env_spatial_is_nil Δ = true 
  Δ  emp.
Proof.
  intros. by rewrite (env_spatial_is_nil_bare_persistently Δ) // (affine ( Δ)).
Qed.

411 412 413 414 415 416 417 418 419 420 421
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.

Instance affine_env_spatial Δ :
  TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ))  Affine ([] env_spatial Δ).
Proof. destruct 1 as [?|H]. apply _. induction H; simpl; apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
422 423 424
Lemma tac_assumption Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  FromAssumption p P Q 
425 426
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
427 428
  Δ  Q.
Proof.
429
  intros ?? H. rewrite envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
430 431
  destruct (env_spatial_is_nil Δ') eqn:?.
  - by rewrite (env_spatial_is_nil_bare_persistently Δ') // sep_elim_l.
432
  - rewrite from_assumption. destruct H as [?|?]=>//. by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
434 435 436 437

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
438
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
439 440 441 442
Proof.
  intros. rewrite envs_simple_replace_sound //.
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
443

Robbert Krebbers's avatar
Robbert Krebbers committed
444
Lemma tac_clear Δ Δ' i p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
445 446 447 448 449 450 451 452
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
  (Δ'  Q) 
  Δ  Q.
Proof.
  intros ? Hp HQ. rewrite envs_lookup_delete_sound //.
  destruct p; by rewrite /= HQ sep_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
453 454

(** * False *)
455
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
456 457
Proof. by rewrite -(False_elim Q). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
458 459 460 461 462 463 464 465 466
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
  Δ  Q.
Proof.
  intros ? ->. rewrite envs_lookup_sound //; simpl.
  by rewrite bare_persistently_if_elim sep_elim_l False_elim.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
467
(** * Pure *)
468
Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ  φ  Δ  Q.
469
Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
470

Robbert Krebbers's avatar
Robbert Krebbers committed
471
Lemma tac_pure Δ Δ' i p P φ Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
472 473 474
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  IntoPure P φ 
  (if p then TCTrue else Affine P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
475 476
  (φ  Δ'  Q)  Δ  Q.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
477 478 479 480 481
  intros ??? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
  - rewrite (into_pure P) -persistently_and_bare_sep_l persistently_pure.
    by apply pure_elim_l.
  - rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_l.
    by apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483
Qed.

Ralf Jung's avatar
Ralf Jung committed
484
Lemma tac_pure_revert Δ φ Q : (Δ  ⌜φ⌝  Q)  (φ  Δ  Q).
485
Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
486

Robbert Krebbers's avatar
Robbert Krebbers committed
487 488 489 490
(** * Persistently *)
Lemma tac_persistently_intro Δ Q Q' :
  FromPersistent Q' Q 
  (envs_clear_spatial Δ  Q)  Δ  Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
491
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
492 493 494
  intros ? HQ. rewrite -(from_persistent Q') -HQ envs_clear_spatial_sound.
  rewrite {1}(env_spatial_is_nil_bare_persistently (envs_clear_spatial Δ)) //.
  by rewrite -persistently_and_bare_sep_l and_elim_l.
495
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
496 497

Lemma tac_persistent Δ Δ' i p P P' Q :
498
  envs_lookup i Δ = Some (p, P) 
499
  IntoPersistent p P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
500
  (if p then TCTrue else Affine P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
501
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
502
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
504 505 506 507
  intros ???? <-. rewrite envs_replace_sound //; simpl.
  rewrite right_id. apply wand_elim_r', wand_mono=> //. destruct p; simpl.
  - by rewrite -(into_persistent _ P).
  - by rewrite -(into_persistent _ P) /= affine_bare.
Robbert Krebbers's avatar
Robbert Krebbers committed
508 509 510 511
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
512
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
513
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
514
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
516
  intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
Robbert Krebbers's avatar
Robbert Krebbers committed
517 518 519
  - rewrite (env_spatial_is_nil_bare_persistently Δ) // envs_app_sound //; simpl.
    rewrite right_id. apply impl_intro_l. rewrite bare_and_l persistently_and_sep_r_1.
    by rewrite bare_sep bare_persistently_elim bare_elim wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
521
    by rewrite persistent_and_sep_1 right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
522 523
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
524
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
525
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
526
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
527
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529 530
  intros ?? <-. rewrite envs_app_sound //; simpl. apply impl_intro_l.
  rewrite (_ : P = ?false P)%I // (into_persistent false P).
  by rewrite right_id persistently_and_bare_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
Qed.
532

Robbert Krebbers's avatar
Robbert Krebbers committed
533 534
Lemma tac_impl_intro_drop Δ P Q : (Δ  Q)  Δ  P  Q.
Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
535 536

Lemma tac_wand_intro Δ Δ' i P Q :
537
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
Proof.
539
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
540 541
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
542
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
543
  Affine P 
Robbert Krebbers's avatar
Robbert Krebbers committed
544
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
545
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
546
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
547 548 549
  intros ??? <-. rewrite envs_app_sound //; simpl.
  rewrite right_id. apply wand_mono=>//.
  by rewrite -(into_persistent _ P) /= affine_bare.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
551 552 553 554 555
Lemma tac_wand_intro_drop Δ P Q :
  TCOr (Affine P) (Absorbing Q) 
  (Δ  Q) 
  Δ  P - Q.
Proof. intros HPQ ->. apply wand_intro_l. by rewrite sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
556 557 558 559 560

(* 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, Δ') 
561
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
562
  IntoWand q p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
563 564 565 566 567
  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 Δ'' 
568
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
569 570 571
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
572 573 574
    rewrite -bare_persistently_if_idemp -bare_persistently_idemp into_wand /=.
    rewrite assoc (bare_persistently_bare_persistently_if q) -bare_persistently_if_sep wand_elim_r.
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
575 576
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
    by rewrite into_wand /= assoc wand_elim_r right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
578 579
Qed.

580
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
581
  envs_lookup_delete j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
582 583
  IntoWand q false R P1 P2 
  ElimModal P1' P1 Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
584
  ('(Δ1,Δ2)  envs_split lr js Δ';
585
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
586
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
587
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
588
Proof.
589
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
590 591 592 593
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
594 595
  rewrite HP1 into_wand /= -(elim_modal P1' P1 Q Q). cancel [P1'].
  apply wand_intro_l. by rewrite assoc right_id !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
596 597
Qed.

598 599 600 601 602
Lemma tac_unlock P Q : (P  Q)  P  locked Q.
Proof. by unlock. Qed.

Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
603
  IntoWand q false R P1 P2 
604 605 606 607 608 609 610
  ElimModal P1' P1 Q Q 
  (Δ'  P1'  locked Q') 
  Q' = (P2 - Q)%I 
  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
Robbert Krebbers's avatar
Robbert Krebbers committed
611 612
  rewrite into_wand -{2}(elim_modal P1' P1 Q Q). cancel [P1'].
  apply wand_intro_l. by rewrite assoc !wand_elim_r.
613 614
Qed.

615
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
616
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
617 618
  IntoWand q true R P1 P2 
  FromPure P1 φ 
619
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
620
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
Proof.
622
  intros. rewrite envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
623 624 625
  rewrite -bare_persistently_if_idemp into_wand /= -(from_pure P1).
  rewrite pure_True // persistently_pure bare_True_emp bare_emp.
  by rewrite emp_wand right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
626 627
Qed.

628
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
629
  envs_lookup_delete j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
630 631
  IntoWand q true R P1 P2 
  Persistent P1 
632
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
633 634 635 636
  (Δ'  P1)  (Δ''  Q)  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
  rewrite envs_lookup_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
  rewrite -(idemp bi_and (envs_delete _ _ _)).
638 639
  rewrite {2}envs_simple_replace_sound' //; rewrite /= right_id.
  rewrite {1}HP1 (persistent_persistently_2 P1) persistently_and_bare_sep_l assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
640 641
  rewrite -bare_persistently_if_idemp -bare_persistently_idemp.
  rewrite (bare_persistently_bare_persistently_if q) -bare_persistently_if_sep.
642
  by rewrite into_wand wand_elim_l wand_elim_r.
643 644
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
645
Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
646
  envs_lookup j Δ = Some (q,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
647 648 649 650 651
  (Δ  R) 
  IntoPersistent false R R' 
  (if q then TCTrue else Affine R) 
  envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' 
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
652
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
653 654 655 656 657 658 659
  intros ? HR ??? <-. rewrite -(idemp bi_and Δ) {1}HR.
  rewrite envs_replace_sound //; rewrite /= right_id. destruct q; simpl.
  - rewrite (_ : R = ?false R)%I // (into_persistent _ R).
    by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
  - rewrite -(affine_bare R) (_ : R = ?false R)%I // (into_persistent _ R).
    rewrite bare_and_r -bare_and_l bare_sep sep_elim_r bare_elim.
    by rewrite persistently_and_bare_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
660 661 662 663
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
664
  (Δ'  (if p then  P else P) - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
665
Proof.
666
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
667
  rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
668 669
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
670
Class IntoIH {PROP : bi} (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
671 672 673 674
  into_ih : φ  Δ  Q.
Global Instance into_ih_entails Δ Q : IntoIH (of_envs Δ  Q) Δ Q.
Proof. by rewrite /IntoIH. Qed.
Global Instance into_ih_forall {A} (φ : A  Prop) Δ Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
675
  ( x, IntoIH (φ x) Δ (Φ x))  IntoIH ( x, φ x) Δ ( x, Φ x)%I | 2.
676 677
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
678
  IntoIH φ Δ Q  IntoIH (ψ  φ) Δ (⌜ψ⌝  Q)%I | 1.
679 680 681 682
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.

Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P 
683 684 685 686
  env_spatial_is_nil Δ = true 
  (of_envs Δ   P  Q) 
  (of_envs Δ  Q).
Proof.
687
  rewrite /IntoIH. intros HP ? HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
688 689 690
  rewrite (env_spatial_is_nil_bare_persistently Δ) //.
  rewrite -(idemp bi_and ( Δ)%I) {1}HP // HPQ.
  by rewrite -{1}persistently_idemp !bare_persistently_elim impl_elim_r.
691 692
Qed.

693
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
694
  ElimModal P' P Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
695
  envs_split lr js Δ = Some (Δ1,Δ2) 
696
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
697
  (Δ1  P')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
698
Proof.
699
  intros ??? HP HQ. rewrite envs_split_sound //.
700
  rewrite (envs_app_sound Δ2) //; simpl.
701
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
702 703
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
704
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P P' Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
705
  envs_split lr js Δ = Some (Δ1,Δ2) 
706
  Persistent P 
Robbert Krebbers's avatar
Robbert Krebbers committed
707 708
  FromBare P' P 
  envs_app false (Esnoc Enil j P') Δ = Some Δ' 
709
  (Δ1  P)  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
710
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
711
  intros ???? HP <-. rewrite -(idemp bi_and Δ) {1}envs_split_sound //.
712 713
  rewrite HP. rewrite (persistent_persistently_2 P) sep_elim_l.
  rewrite persistently_and_bare_sep_l -bare_idemp bare_persistently_elim from_bare.
Robbert Krebbers's avatar
Robbert Krebbers committed
714
  rewrite envs_app_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
  by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
716 717
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
718
Lemma tac_assert_pure Δ Δ' j P P' φ Q :
719
  FromPure P φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
720 721
  FromBare P' P 
  envs_app false (Esnoc Enil j P') Δ = Some Δ' 
722 723
  φ  (Δ'  Q)  Δ  Q.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
724 725 726
  intros ???? <-. rewrite envs_app_sound //; simpl.
  rewrite right_id -(from_bare P') -(from_pure P) pure_True //.
  by rewrite bare_True_emp bare_emp emp_wand.
727 728
Qed.

729
Lemma tac_pose_proof Δ Δ' j P Q :
730
  P 
731
  envs_app true (Esnoc Enil j P) Δ = Some Δ'