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) 
Robbert Krebbers's avatar
Robbert Krebbers committed
679
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
680
  envs_entails Δ' Q  envs_entails Δ (P - Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
681
Proof.
682
  rewrite /envs_entails => ? HPQ ? HQ. rewrite envs_app_singleton_sound //=.
683
  apply wand_intro_l. destruct HPQ.
684
  - rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
685
            (into_persistent _ P) wand_elim_r //.
686
  - rewrite (_ : P = ?false P)%I // (into_persistent _ P).
687
688
    by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
               absorbingly_sep_l wand_elim_r HQ.
689
690
691
Qed.
Lemma tac_wand_intro_pure Δ P φ Q :
  IntoPure P φ 
692
  TCOr (Affine P) (Absorbing Q) 
693
  (φ  envs_entails Δ Q)  envs_entails Δ (P - Q).
694
Proof.
695
  intros ? HPQ HQ. apply wand_intro_l. destruct HPQ.
696
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
697
    by apply pure_elim_l.
698
699
  - 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
700
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
701
702