coq_tactics.v 46.6 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
3
From iris.proofmode Require Export base environments classes.
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
Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
25
  (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
  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.
114 115
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
116
Definition envs_split {PROP} (d : direction)
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    (js : list string) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
118
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
119
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
120

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
Section bi_tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Lemma of_envs_eq Δ :
129
  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 :
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
  - rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
148 149
    rewrite (env_lookup_perm Γp) //= affinely_persistently_and.
    by rewrite and_sep_affinely_persistently -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154
    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
155
Lemma envs_lookup_persistent_sound Δ i P :
156
  envs_lookup i Δ = Some (true,P)  Δ   P  Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Proof.
158
  intros. rewrite -persistently_and_affinely_sep_l. apply and_intro; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  rewrite envs_lookup_sound //; simpl.
160
  by rewrite -persistently_and_affinely_sep_l and_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163
Qed.

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

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

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

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

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

250
Lemma envs_app_singleton_sound Δ Δ' p j Q :
251
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  Δ  ?p Q - Δ'.
252 253
Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
254 255
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
256
  envs_delete i p Δ  (if p then  [] Γ else [] Γ) - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
260 261
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] 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 266
    + 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') //.
267
      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
268
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
269 270
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
272 273 274
    + 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.
275
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
276 277
Qed.

278 279
Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
280
  envs_delete i p Δ  ?p Q - Δ'.
281 282
Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
283 284
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
285
  Δ  ?p P  ((if p then  [] Γ else [] Γ) - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

288 289 290
Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
291
  Δ  ?p P  (?p Q - Δ').
292 293 294 295
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
296
Lemma envs_replace_sound' Δ Δ' i p q Γ :
297
  envs_replace i p q Γ Δ = Some Δ' 
298
  envs_delete i p Δ  (if q then  [] Γ else [] Γ) - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
299 300 301 302 303 304
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

305 306
Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
307
  envs_delete i p Δ  ?q Q - Δ'.
308 309
Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
310 311
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
312
  Δ  ?p P  ((if q then  [] Γ else [] Γ) - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

315 316 317
Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
318
  Δ  ?p P  (?q Q - Δ').
319 320
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.

321 322 323
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
324
Proof.
325 326 327
  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
328 329
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
330 331
Lemma envs_clear_spatial_sound Δ :
  Δ  envs_clear_spatial Δ  [] env_spatial Δ.
332
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
333 334 335
  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.
336 337
Qed.

338
Lemma env_spatial_is_nil_affinely_persistently Δ :
339
  env_spatial_is_nil Δ = true  Δ   Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341
Proof.
  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
342 343
  rewrite !right_id {1}affinely_and_r persistently_and.
  by rewrite persistently_affinely persistently_idemp persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
345

346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365
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
366 367
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
  Δ1  Δ2  Δ1'  Δ2'.
368 369 370
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
371 372
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite /of_envs !and_elim_l sep_elim_l. }
373 374 375 376 377 378 379 380 381 382
  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.
383 384
Lemma envs_split_sound Δ d js Δ1 Δ2 :
  envs_split d js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
385
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
386 387
  rewrite /envs_split=> ?. rewrite -(idemp bi_and Δ).
  rewrite {2}envs_clear_spatial_sound.
388 389
  rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
  rewrite -persistently_and_affinely_sep_l.
390
  rewrite (and_elim_l (bi_persistently _)%I)
391
          persistently_and_affinely_sep_r affinely_persistently_elim.
392 393 394
  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=> ->. }
395
  destruct d; simplify_eq; solve_sep_entails.
396 397
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
398
Global Instance envs_Forall2_refl (R : relation PROP) :
399 400
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
Global Instance envs_Forall2_sym (R : relation PROP) :
402 403
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Global Instance envs_Forall2_trans (R : relation PROP) :
405 406
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
408 409
  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
410
Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
411 412 413
  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
414
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
415
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
416 417
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
418 419 420
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421 422
Global Instance of_envs_proper :
  Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
423
Proof.
424 425
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
426
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
427 428
Global Instance Envs_mono (R : relation PROP) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
429 430
Proof. by constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
431
(** * Adequacy *)
432
Lemma tac_adequate P : (Envs Enil Enil  P)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
Proof.
434
  intros <-. rewrite /of_envs /= persistently_True_emp affinely_persistently_emp left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
435
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
436 437 438
Qed.

(** * Basic rules *)
439 440 441 442 443 444 445
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.

446 447 448 449
(* If the BI is affine, no need to walk on the whole environment. *)
Global Instance affine_env_bi `(AffineBI PROP) Γ : AffineEnv Γ | 0.
Proof. induction Γ; apply _. Qed.

450
Instance affine_env_spatial Δ :
451 452 453 454
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  Δ  emp.
455
Proof. intros. by rewrite (affine Δ). Qed.
456

Robbert Krebbers's avatar
Robbert Krebbers committed
457 458 459
Lemma tac_assumption Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  FromAssumption p P Q 
460 461
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
462 463
  Δ  Q.
Proof.
464
  intros ?? H. rewrite envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
465
  destruct (env_spatial_is_nil Δ') eqn:?.
466
  - by rewrite (env_spatial_is_nil_affinely_persistently Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
469 470 471 472

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
473
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
474
Proof.
475 476
  intros. rewrite envs_simple_replace_singleton_sound //.
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
478

Robbert Krebbers's avatar
Robbert Krebbers committed
479
Lemma tac_clear Δ Δ' i p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
480 481 482 483 484 485 486 487
  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
488 489

(** * False *)
490
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
491 492
Proof. by rewrite -(False_elim Q). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
493 494 495 496 497 498
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.
499
  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
500 501
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
502
(** * Pure *)
503
Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ  φ  Δ  Q.
504
Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
505

Robbert Krebbers's avatar
Robbert Krebbers committed
506
Lemma tac_pure Δ Δ' i p P φ Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
507 508
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  IntoPure P φ 
509
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
510 511
  (φ  Δ'  Q)  Δ  Q.
Proof.
512
  intros ?? HPQ HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
513
  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
514
    by apply pure_elim_l.
515
  - destruct HPQ.
516
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
517
      by apply pure_elim_l.
518 519
    + rewrite (into_pure P) (persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
520 521
Qed.

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

525 526
(** * Persistence and plainness modalities *)
Class IntoPlainEnv (Γ1 Γ2 : env PROP) := {
527
  into_plain_env_subenv : env_subenv Γ2 Γ1;
528
  into_plain_env_plain : Plain ([] Γ2);
529 530 531 532 533 534 535 536 537 538 539 540
}.

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.

541 542 543 544 545 546 547 548 549 550
Lemma into_plain_env_sound Γ1 Γ2 :
  IntoPlainEnv Γ1 Γ2  (Envs Γ1 Enil)  bi_plainly (Envs Γ2 Enil).
Proof .
  intros [Hsub ?]. rewrite !of_envs_eq plainly_and plainly_pure /=. f_equiv.
  { f_equiv=>-[/= ???]. split; auto. by eapply env_subenv_wf. }
  rewrite !(right_id emp%I). trans ( [] Γ2)%I.
  - do 2 f_equiv. clear -Hsub.
    induction Hsub as [|????? IH|????? IH]=>//=; rewrite IH //. apply and_elim_r.
  - by rewrite {1}(plain ([] Γ2)) affinely_elim plainly_affinely
               plainly_persistently persistently_plainly.
551 552
Qed.

553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572
Class IntoAlwaysEnvs (pe : bool) (pl : bool) (Δ1 Δ2 : envs PROP) := {
  into_persistent_envs_persistent :
    if pl then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
    else env_persistent Δ1 = env_persistent Δ2;
  into_persistent_envs_spatial :
    if pe || pl then env_spatial Δ2 = Enil else env_spatial Δ1 = env_spatial Δ2
}.

Global Instance into_always_false_false Δ : IntoAlwaysEnvs false false Δ Δ.
Proof. by split. Qed.
Global Instance into_always_envs_true_false Γp Γs :
  IntoAlwaysEnvs true false (Envs Γp Γs) (Envs Γp Enil).
Proof. by split. Qed.
Global Instance into_always_envs_x_true Γp1 Γp2 Γs1 pe :
  IntoPlainEnv Γp1 Γp2 
  IntoAlwaysEnvs pe true (Envs Γp1 Γs1) (Envs Γp2 Enil).
Proof. destruct pe; by split. Qed.

Lemma tac_always_intro Δ Δ' a pe pl Q Q' :
  FromAlways a pe pl Q' Q 
573
  (if a then AffineEnv (env_spatial Δ') else TCTrue) 
574 575
  IntoAlwaysEnvs pe pl Δ' Δ 
  (Δ  Q)  Δ'  Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
576
Proof.
577 578 579 580 581 582 583 584 585 586 587 588
  intros ? Haffine [Hep Hes] HQ. rewrite -(from_always a pe pl Q') -HQ.
  trans (bi_affinely_if a Δ'); [destruct a=>//; by apply: affinely_intro|f_equiv].
  destruct pl; [|destruct pe].
  - rewrite (envs_clear_spatial_sound Δ') into_plain_env_sound sep_elim_l.
    destruct Δ as [Δ ?]. rewrite orb_true_r /= in Hes. rewrite Hes /=.
    destruct pe=>/= //. by rewrite persistently_plainly.
  - rewrite (envs_clear_spatial_sound Δ') /= /envs_clear_spatial Hep.
    destruct Δ as [Δ ?]. simpl in Hes. subst. simpl.
    rewrite -(sep_elim_l (bi_persistently _)). f_equiv.
    rewrite {1}(env_spatial_is_nil_affinely_persistently (Envs Δ Enil)) //.
    by rewrite affinely_elim.
  - destruct Δ, Δ'; simpl in *. by subst.
589
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
590 591

Lemma tac_persistent Δ Δ' i p P P' Q :
592
  envs_lookup i Δ = Some (p, P) 
593
  IntoPersistent p P P' 
594
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
595
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
596
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
597
Proof.
598 599 600 601
  intros ?? HPQ ? HQ. rewrite envs_replace_singleton_sound //; simpl.
  destruct p; simpl.
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
602
    + rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
603 604
              (into_persistent _ P) wand_elim_r //.
    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
605 606
      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
                 absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
607 608 609
Qed.

(** * Implication and wand *)
610
Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
611
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  Δ  ?p Q  Δ'.
612 613
Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.

614
Lemma tac_impl_intro Δ Δ' i P P' Q :
615
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
616
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
617
  FromAffinely P' P 
618
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Proof.
620
  intros ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
621
  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
622
    rewrite envs_app_singleton_sound //; simpl.
623 624
    rewrite -(from_affinely P') -affinely_and_lr.
    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
625
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
626
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
627 628
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
629
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
630
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
631
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
632
Proof.
633
  intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
634
  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
635
  by rewrite persistently_and_affinely_sep_l wand_elim_r.
636 637 638 639 640 641 642
Qed.
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
  (φ  Δ  ⌜ψ⌝)  Δ  ⌜φ  ψ⌝.
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Proof.
  intros. apply impl_intro_l. rewrite (into_pure P). by apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
643
Qed.
644

Robbert Krebbers's avatar
Robbert Krebbers committed
645 646
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
647 648

Lemma tac_wand_intro Δ Δ' i P Q :
649
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
650
Proof.
651
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
652 653
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
654
  IntoPersistent false P P' 
655
  TCOr (Affine P) (Absorbing Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
656
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
657
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
658
Proof.
659 660
  intros ? HPQ ? HQ. rewrite envs_app_singleton_sound //; simpl.
  apply wand_intro_l. destruct HPQ.
661
  - rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
662
            (into_persistent _ P) wand_elim_r //.
663
  - rewrite (_ : P = ?false P)%I // (into_persistent _ P).
664 665
    by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
               absorbingly_sep_l wand_elim_r HQ.
666 667 668
Qed.
Lemma tac_wand_intro_pure Δ P φ Q :
  IntoPure P φ 
669
  TCOr (Affine P) (Absorbing Q) 
670 671
  (φ  Δ  Q)  Δ  P - Q.
Proof.
672
  intros ? HPQ HQ. apply wand_intro_l. destruct HPQ.
673
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
674
    by apply pure_elim_l.
675 676
  - rewrite (into_pure P) (persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
    rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
677
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
678 679 680 681 682
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
683 684 685 686 687

(* 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, Δ') 
688
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
689
  IntoWand q p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
690 691 692 693 694
  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 Δ'' 
695
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
696 697
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
698 699
  - rewrite envs_lookup_persistent_sound //.
    rewrite envs_simple_replace_singleton_sound //; simpl.
Jacques-Henri Jourdan's avatar