coq_tactics.v 49.4 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
}.

24
Definition 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

29
Definition envs_entails {PROP} (Δ : envs PROP) (Q : PROP) : Prop :=
30
  of_envs Δ  Q.
31
Arguments envs_entails {_} _ _%I : simpl never.
32 33 34
Typeclasses Opaque envs_entails.
Instance: Params (@envs_entails) 1.

Robbert Krebbers's avatar
Robbert Krebbers committed
35
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
36 37 38
  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
39

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
50
Definition envs_delete {PROP} (i : string) (p : bool) (Δ : envs PROP) : envs PROP :=
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
  let (Γp,Γs) := Δ in
  match p with
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54
  | true => Envs (env_delete i Γp) Γs
  | false => Envs Γp (env_delete i Γs)
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
57 58
Definition envs_lookup_delete {PROP} (i : string)
    (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61 62 63 64
  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
65 66
Fixpoint envs_lookup_delete_list {PROP} (js : list string) (remove_persistent : bool)
    (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
67 68 69 70 71 72 73 74 75
  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
76 77
Definition envs_snoc {PROP} (Δ : envs PROP)
    (p : bool) (j : string) (P : PROP) : envs PROP :=
78 79 80
  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
81 82
Definition envs_app {PROP : bi} (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87 88
  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
89 90
Definition envs_simple_replace {PROP : bi} (i : string) (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93 94 95 96
  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
97 98
Definition envs_replace {PROP : bi} (i : string) (p q : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
99 100 101
  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
102
Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104
  if env_spatial Δ is Enil then true else false.

Robbert Krebbers's avatar
Robbert Krebbers committed
105
Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
106 107
  Envs (env_persistent Δ) Enil.

Robbert Krebbers's avatar
Robbert Krebbers committed
108
Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
109 110
  Envs Enil (env_spatial Δ).

Robbert Krebbers's avatar
Robbert Krebbers committed
111 112
Fixpoint envs_split_go {PROP}
    (js : list string) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
113 114 115 116 117 118 119
  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.
120 121
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
122
Definition envs_split {PROP} (d : direction)
Robbert Krebbers's avatar
Robbert Krebbers committed
123
    (js : list string) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
124
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
125
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
126

Robbert Krebbers's avatar
Robbert Krebbers committed
127
(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129 130 131 132 133 134
Section bi_tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

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

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

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

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

187
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
188 189
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
190 191
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
192
  { by rewrite affinely_persistently_emp left_id. }
193 194 195
  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/=.
196
  rewrite -affinely_persistently_if_sep_2 -assoc. destruct q1; simpl.
197
  - destruct rp.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
    + rewrite envs_lookup_sound //; simpl.
199
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
200
    + rewrite envs_lookup_persistent_sound //.
201 202
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite affinely_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
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
222 223
  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
224
  - apply and_intro; [apply pure_intro|].
225
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
226
      intros j; destruct (string_beq_reflect j i); naive_solver.
227
    + by rewrite affinely_persistently_and and_sep_affinely_persistently assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
228
  - apply and_intro; [apply pure_intro|].
229
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
230
      intros j; destruct (string_beq_reflect j i); naive_solver.
231 232 233
    + solve_sep_entails.
Qed.

234
Lemma envs_app_sound Δ Δ' p Γ :
235 236
  envs_app p Γ Δ = Some Δ' 
  of_envs Δ  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
  rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
239 240 241
  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
242
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
243 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.
    + rewrite (env_app_perm _ _ Γp') //.
247
      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
248
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
252 253 254
    + 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.
255
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
256 257
Qed.

258
Lemma envs_app_singleton_sound Δ Δ' p j Q :
259
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q - of_envs Δ'.
260 261
Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
262 263
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
264
  of_envs (envs_delete i p Δ)  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
265 266
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
268 269
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
271 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.
    + rewrite (env_replace_perm _ _ Γp') //.
275
      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
276
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
280 281 282
    + 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.
283
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
284 285
Qed.

286 287
Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
288
  of_envs (envs_delete i p Δ)  ?p Q - of_envs Δ'.
289 290
Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
291 292
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
293
  of_envs Δ  ?p P  ((if p then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

296 297 298
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 Δ' 
299
  of_envs Δ  ?p P  (?p Q - of_envs Δ').
300 301 302 303
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
304
Lemma envs_replace_sound' Δ Δ' i p q Γ :
305
  envs_replace i p q Γ Δ = Some Δ' 
306
  of_envs (envs_delete i p Δ)  (if q then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
307 308 309 310 311 312
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

313 314
Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
315
  of_envs (envs_delete i p Δ)  ?q Q - of_envs Δ'.
316 317
Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
318 319
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
320
  of_envs Δ  ?p P  ((if q then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

323 324 325
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 Δ' 
326
  of_envs Δ  ?p P  (?q Q - of_envs Δ').
327 328
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.

329 330 331
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
332
Proof.
333 334 335
  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
336 337
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
338
Lemma envs_clear_spatial_sound Δ :
339
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
340
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
341 342 343
  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.
344 345
Qed.

346
Lemma env_spatial_is_nil_affinely_persistently Δ :
347
  env_spatial_is_nil Δ = true  of_envs Δ   of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
348 349
Proof.
  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
350 351
  rewrite !right_id {1}affinely_and_r persistently_and.
  by rewrite persistently_affinely persistently_idemp persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
353

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

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

439
Global Instance envs_entails_proper :
440
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails PROP).
441 442
Proof. solve_proper. Qed.
Global Instance envs_entails_flip_mono :
443
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
444 445
Proof. rewrite /envs_entails=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
446
(** * Adequacy *)
447
Lemma tac_adequate P : envs_entails (Envs Enil Enil) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
Proof.
449
  intros <-. rewrite /of_envs /= persistently_True_emp affinely_persistently_emp left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
450
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
451 452 453
Qed.

(** * Basic rules *)
454 455 456 457 458 459 460
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.

461 462 463 464
(* 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.

465
Instance affine_env_spatial Δ :
466 467 468
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

469 470
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  of_envs Δ  emp.
Proof. intros. by rewrite (affine (of_envs Δ)). Qed.
471

Robbert Krebbers's avatar
Robbert Krebbers committed
472 473 474
Lemma tac_assumption Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  FromAssumption p P Q 
475 476
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
477
  of_envs Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
Proof.
479
  intros ?? H. rewrite envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
  destruct (env_spatial_is_nil Δ') eqn:?.
481
  - by rewrite (env_spatial_is_nil_affinely_persistently Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
484 485 486 487

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
488 489
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
490
Proof.
491
  rewrite /envs_entails=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
492
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
493
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
494

Robbert Krebbers's avatar
Robbert Krebbers committed
495
Lemma tac_clear Δ Δ' i p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
496 497
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
498 499
  (envs_entails Δ' Q) 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
Proof.
501 502
  rewrite /envs_entails=> ?? HQ. rewrite envs_lookup_delete_sound //.
  by destruct p; rewrite /= HQ sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
504 505

(** * False *)
506 507
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
508

Robbert Krebbers's avatar
Robbert Krebbers committed
509 510 511
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
512
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
513
Proof.
514
  rewrite /envs_entails => ??. subst. rewrite envs_lookup_sound //; simpl.
515
  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
516 517
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
518
(** * Pure *)
519 520
Lemma tac_pure_intro Δ Q φ : FromPure Q φ  φ  envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
521

Robbert Krebbers's avatar
Robbert Krebbers committed
522
Lemma tac_pure Δ Δ' i p P φ Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
523 524
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  IntoPure P φ 
525
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
526
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
527
Proof.
528 529
  rewrite /envs_entails=> ?? HPQ HQ.
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
530
  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
    by apply pure_elim_l.
532
  - destruct HPQ.
533
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
534
      by apply pure_elim_l.
535 536
    + 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
537 538
Qed.

539 540
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
541

542 543
(** * Persistence and plainness modalities *)
Class IntoPlainEnv (Γ1 Γ2 : env PROP) := {
544
  into_plain_env_subenv : env_subenv Γ2 Γ1;
545
  into_plain_env_plain : Plain ([] Γ2);
546 547 548 549 550 551 552 553 554 555 556 557
}.

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.

558
Lemma into_plain_env_sound Γ1 Γ2 :
559
  IntoPlainEnv Γ1 Γ2  of_envs (Envs Γ1 Enil)  bi_plainly $ of_envs $ Envs Γ2 Enil.
560
Proof.
561 562 563 564 565 566 567
  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.
568 569
Qed.

570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589
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 
590
  (if a then AffineEnv (env_spatial Δ') else TCTrue) 
591
  IntoAlwaysEnvs pe pl Δ' Δ 
592
  (envs_entails Δ Q)  envs_entails Δ' Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
593
Proof.
594 595 596 597
  rewrite /envs_entails => ? Haffine [Hep Hes] HQ.
  rewrite -(from_always a pe pl Q') -HQ.
  trans (bi_affinely_if a (of_envs Δ'));
    [destruct a=>//; by apply: affinely_intro|f_equiv].
598 599 600 601 602 603 604 605 606 607
  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.
608
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
609 610

Lemma tac_persistent Δ Δ' i p P P' Q :
611
  envs_lookup i Δ = Some (p, P) 
612
  IntoPersistent p P P' 
613
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
614
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
615
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
Proof.
617
  rewrite /envs_entails=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
618 619 620
  destruct p; simpl.
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
621
    + rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
622 623
              (into_persistent _ P) wand_elim_r //.
    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
624 625
      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
                 absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
626 627 628
Qed.

(** * Implication and wand *)
629
Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
630
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q  of_envs Δ'.
631 632
Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.

633
Lemma tac_impl_intro Δ Δ' i P P' Q :
634
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
635
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
636
  FromAffinely P' P 
637
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
638
Proof.
639
  rewrite /envs_entails => ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
640
  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
641
    rewrite envs_app_singleton_sound //; simpl.
642 643
    rewrite -(from_affinely P') -affinely_and_lr.
    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
644
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
645
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
646 647
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
648
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
649
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
650
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
651
Proof.
652 653
  rewrite /envs_entails => ?? <-.
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
654
  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
655
  by rewrite persistently_and_affinely_sep_l wand_elim_r.
656 657
Qed.
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
658
  (φ  envs_entails Δ ⌜ψ⌝)  envs_entails Δ ⌜φ  ψ⌝.
659
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
660 661
Lemma tac_impl_intro_pure Δ P φ Q :
  IntoPure P φ  (φ  envs_entails Δ Q)  envs_entails Δ (P  Q).
662 663
Proof.
  intros. apply impl_intro_l. rewrite (into_pure P). by apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
664
Qed.
665

666 667
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
668 669

Lemma tac_wand_intro Δ Δ' i P Q :
670 671
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
  envs_entails Δ' Q  envs_entails Δ (P - Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
672
Proof.
673 674
  rewrite /envs_entails=> ? HQ.
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
675 676
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
677
  IntoPersistent false P P' 
678
  TCOr (Affine P) (Absorbing Q)