coq_tactics.v 44.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
3
From iris.proofmode Require Export environments classes.
Ralf Jung's avatar
Ralf Jung committed
4
From stdpp Require Import stringmap hlist.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Import bi.
7
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
18
Record envs_wf {PROP} (Δ : envs PROP) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
21
22
23
  env_persistent_valid : env_wf (env_persistent Δ);
  env_spatial_valid : env_wf (env_spatial Δ);
  envs_disjoint i : env_persistent Δ !! i = None  env_spatial Δ !! i = None
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
24
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
114
115
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
     '(p,P,Δ1')  envs_lookup_delete j Δ1;
     if p then envs_split_go js Δ1 Δ2 else
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
(* if [lr = true] then [result = (remaining hyps, hyps named js)] and
   if [lr = false] then [result = (hyps named js, remaining hyps)] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
Definition envs_split {PROP} (lr : bool)
    (js : list string) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
118
119
120
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
  if lr then Some (Δ1,Δ2) else Some (Δ2,Δ1).

Robbert Krebbers's avatar
Robbert Krebbers committed
121
(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
124
125
126
127
128
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 (strings.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 (strings.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
383
  destruct (envs_lookup_delete j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq; auto.
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
  rewrite -(IH _ _ _ _ _ HΔ); last first.
  { intros j' P'; destruct (decide (j = j')) as [->|].
    - by rewrite (envs_lookup_envs_delete _ _ _ P).
    - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
Lemma envs_split_sound Δ lr js Δ1 Δ2 :
384
  envs_split lr 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
395
396
397
  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
  apply envs_split_go_sound in HΔ as ->; last first.
  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
  destruct lr; simplify_eq; solve_sep_entails.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
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
446
447
448
449
Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed.
Global Instance affine_env_snoc Γ i P :
  Affine P  AffineEnv Γ  AffineEnv (Esnoc Γ i P).
Proof. by constructor. Qed.

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

450
451
452
453
454
455
Lemma tac_emp_intro Δ :
  (* Establishing [AffineEnv (env_spatial Δ)] is rather expensive (linear in the
  size of the context), so first check whether the whole BI is affine (which
  takes constant time). *)
  TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) 
  Δ  emp.
456
Proof. intros. by rewrite (affine Δ). Qed.
457

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
526
(** * Persistently *)
527
528
529
530
Lemma tac_persistently_intro Δ a p Q Q' :
  FromPersistent a p Q' Q 
  (if a then TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) else TCTrue) 
  ((if p then envs_clear_spatial Δ else Δ)  Q)  Δ  Q'.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
Proof.
532
533
  intros ? Haffine HQ. rewrite -(from_persistent a p Q') -HQ. destruct p=> /=.
  - rewrite envs_clear_spatial_sound.
534
535
    rewrite {1}(env_spatial_is_nil_affinely_persistently (envs_clear_spatial Δ)) //.
    destruct a=> /=. by rewrite sep_elim_l. by rewrite affinely_elim sep_elim_l.
536
  - destruct a=> //=. apply and_intro; auto using tac_emp_intro.
537
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
539

Lemma tac_persistent Δ Δ' i p P P' Q :
540
  envs_lookup i Δ = Some (p, P) 
541
  IntoPersistent p P P' 
542
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
543
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
544
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
Proof.
546
547
548
549
  intros ?? HPQ ? HQ. rewrite envs_replace_singleton_sound //; simpl.
  destruct p; simpl.
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
550
    + rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
551
552
              (into_persistent _ P) wand_elim_r //.
    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
553
554
      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
                 absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
556
557
Qed.

(** * Implication and wand *)
558
Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
559
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  Δ  ?p Q  Δ'.
560
561
Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.

562
Lemma tac_impl_intro Δ Δ' i P P' Q :
563
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
564
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
565
  FromAffinely P' P 
566
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
567
Proof.
568
  intros ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
569
  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
570
    rewrite envs_app_singleton_sound //; simpl.
571
572
    rewrite -(from_affinely P') -affinely_and_lr.
    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
573
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
574
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
576
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
577
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
578
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
579
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
580
Proof.
581
  intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
582
  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
583
  by rewrite persistently_and_affinely_sep_l wand_elim_r.
584
585
586
587
588
589
590
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
591
Qed.
592

Robbert Krebbers's avatar
Robbert Krebbers committed
593
594
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
595
596

Lemma tac_wand_intro Δ Δ' i P Q :
597
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
598
Proof.
599
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
600
601
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
602
  IntoPersistent false P P' 
603
  TCOr (Affine P) (Absorbing Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
604
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
605
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
606
Proof.
607
608
  intros ? HPQ ? HQ. rewrite envs_app_singleton_sound //; simpl.
  apply wand_intro_l. destruct HPQ.
609
  - rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
610
            (into_persistent _ P) wand_elim_r //.
611
  - rewrite (_ : P = ?false P)%I // (into_persistent _ P).
612
613
    by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
               absorbingly_sep_l wand_elim_r HQ.
614
615
616
Qed.
Lemma tac_wand_intro_pure Δ P φ Q :
  IntoPure P φ 
617
  TCOr (Affine P) (Absorbing Q) 
618
619
  (φ  Δ  Q)  Δ  P - Q.
Proof.
620
  intros ? HPQ HQ. apply wand_intro_l. destruct HPQ.
621
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
622
    by apply pure_elim_l.
623
624
  - 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
625
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
626
627
628
629
630
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
631
632
633
634
635

(* 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, Δ') 
636
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
637
  IntoWand q p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
638
639
640
641
642
  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 Δ'' 
643
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
644
645
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
646
647
  - rewrite envs_lookup_persistent_sound //.
    rewrite envs_simple_replace_singleton_sound //; simpl.
648
649
650
    rewrite -affinely_persistently_if_idemp -affinely_persistently_idemp into_wand /=.
    rewrite assoc (affinely_persistently_affinely_persistently_if q).
    by rewrite affinely_persistently_if_sep_2 wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
651
  - rewrite envs_lookup_sound //; simpl.
652
653
    rewrite envs_lookup_sound // (envs_replace_singleton_sound' _ Δ'') //; simpl.
    by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
655
Qed.

656
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
657
  envs_lookup_delete j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
658
659
  IntoWand q false R P1 P2 
  ElimModal P1' P1 Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
660
  ('(Δ1,Δ2)  envs_split lr js Δ';
661
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
662
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
663
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
664
Proof.
665
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
666
667
668
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
669
  rewrite (envs_app_singleton_sound Δ2) //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
670
  rewrite HP1 into_wand /= -(elim_modal P1' P1 Q Q). cancel [P1'].
671
  apply wand_intro_l. by rewrite assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
672
673
Qed.

674
675
676
677
678
Lemma tac_unlock P Q : (P  Q)  P  locked Q.
Proof. by unlock. Qed.

Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
679
  IntoWand q false R P1 P2 
680
681
682
683
684
685
686
  ElimModal P1' P1 Q Q 
  (Δ'  P1'  locked Q') 
  Q' = (P2 - Q)%I 
  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
Robbert Krebbers's avatar
Robbert Krebbers committed
687
688
  rewrite into_wand -{2}(elim_modal P1' P1 Q Q). cancel [P1'].
  apply wand_intro_l. by rewrite assoc !wand_elim_r.
689
690
Qed.

691
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
692
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
693
694
  IntoWand q true R P1 P2 
  FromPure P1 φ 
695
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
696
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
Proof.
698
  intros. rewrite envs_simple_replace_singleton_sound //; simpl.
699
700
  rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure P1).
  rewrite pure_True // persistently_pure affinely_True_emp affinely_emp.
701
  by rewrite emp_wand wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
702
703
Qed.

704
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P1' P2 R Q :
705
  envs_lookup_delete j Δ = Some (q, R, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
706
707
  IntoWand q true R P1 P2 
  Persistent P1 
708
  IntoAbsorbingly P1' P1 
709
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
710
  (Δ'  P1')  (Δ''  Q)  Δ  Q.