coq_tactics.v 41.3 KB
Newer Older
1
2
From iris.base_logic Require Export base_logic.
From iris.base_logic Require Import big_op 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 uPred.
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.

11
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15
16
17
18
19
20
21
22
23
  Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

Record envs_wf {M} (Δ : envs M) := {
  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 {M} (Δ : envs M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
25
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
26
27
Instance: Params (@of_envs) 1.

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

34
35
36
37
Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
  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
38

39
40
Definition envs_dom {M} (Δ : envs M) : list string :=
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
  let (Γp,Γs) := Δ in
  match env_lookup i Γp with
  | Some P => Some (true, P) | None => P  env_lookup i Γs; Some (false, P)
  end.

Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
  let (Γp,Γs) := Δ in
  match p with
  | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
  end.

Definition envs_lookup_delete {M} (i : string)
    (Δ : envs M) : option (bool * uPred M * envs M) :=
  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.

62
63
64
65
66
67
68
69
70
71
72
Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : bool)
    (Δ : envs M) : option (bool * list (uPred M) * envs M) :=
  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.

73
74
75
76
77
Definition envs_snoc {M} (Δ : envs M)
    (p : bool) (j : string) (P : uPred M) : envs M :=
  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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
Definition envs_app {M} (p : bool)
    (Γ : env (uPred M)) (Δ : envs M) : option (envs M) :=
  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.

Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  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.

Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

99
Definition env_spatial_is_nil {M} (Δ : envs M) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
  if env_spatial Δ is Enil then true else false.

102
103
104
Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
  Envs (env_persistent Δ) Enil.

105
106
107
Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
  Envs Enil (env_spatial Δ).

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

Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
(* Coq versions of the tactics *)
Section tactics.
126
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
130
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

131
Lemma of_envs_def Δ :
Ralf Jung's avatar
Ralf Jung committed
132
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
133
134
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
140
141
142
143
144
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 :
145
146
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  ?p P  of_envs (envs_delete i p Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Proof.
148
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
150
  - rewrite (env_lookup_perm Γp) //= persistently_sep.
151
    ecancel [ [] _;  P; [] Γs]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
154
155
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
156
    ecancel [ [] _; P; [] (env_delete _ _)]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
159
160
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
161
162
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  P  of_envs (envs_delete i p Δ).
163
Proof. intros. rewrite envs_lookup_sound //. by rewrite persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Lemma envs_lookup_persistent_sound Δ i P :
165
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Proof.
167
  intros. apply (persistently_entails_l _ _). by rewrite envs_lookup_sound // sep_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.
173
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
175
  - rewrite (env_lookup_perm Γp) //= persistently_sep.
176
    rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - 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.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
187
  envs_lookup_delete i Δ = Some (p,P,Δ')  of_envs Δ  P  of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

190
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
191
192
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
193
194
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
195
  { by rewrite persistently_pure left_id. }
196
197
198
  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/=.
199
  rewrite persistently_if_sep -assoc. destruct q1; simpl.
200
  - destruct rp.
201
202
203
    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (persistently_elim_if q2).
    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (persistently_elim_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite persistently_if_elim.
204
205
Qed.

206
207
208
209
210
211
212
213
214
215
216
217
218
219
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 :
220
  envs_lookup i Δ = None  of_envs Δ  ?p P - of_envs (envs_snoc Δ p i P).
221
222
223
224
225
226
Proof.
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
227
      intros j; destruct (string_beq_reflect j i); naive_solver.
228
    + by rewrite persistently_sep assoc.
229
230
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
231
      intros j; destruct (string_beq_reflect j i); naive_solver.
232
233
234
    + solve_sep_entails.
Qed.

235
236
Lemma envs_app_sound Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ'  of_envs Δ  ?p [] Γ - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Proof.
238
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_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/=.
242
    apply wand_intro_l, sep_intro_True_l; [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 persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
250
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
251
252
253
    + 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.
254
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
256
257
258
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
259
  of_envs (envs_delete i p Δ)  ?p [] Γ - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
261
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
262
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
264
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
265
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
269
    + 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') //.
270
      rewrite big_opL_app persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
273
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
274
275
276
    + 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.
277
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
279
280
281
Qed.

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

Lemma envs_replace_sound' Δ Δ' i p q Γ :
286
287
  envs_replace i p q Γ Δ = Some Δ' 
  of_envs (envs_delete i p Δ)  ?q [] Γ - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
288
289
290
291
292
293
294
295
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
296
  of_envs Δ  ?p P  (?q [] Γ - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
297
298
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

299
300
301
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
302
Proof.
303
304
305
  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
306
307
Qed.

308
309
Lemma envs_clear_spatial_sound Δ :
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
310
Proof.
311
312
  rewrite /of_envs /envs_clear_spatial /=; apply pure_elim_sep_l=> Hwf.
  rewrite right_id -assoc; apply sep_intro_True_l; [apply pure_intro|done].
313
314
315
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

316
Lemma env_spatial_is_nil_persistent Δ :
317
  env_spatial_is_nil Δ = true  Persistent (of_envs Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
318
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
319
Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
320

321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
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) 
341
342
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
343
344
345
346
347
348
349
350
351
352
353
354
355
356
Proof.
  revert Δ1 Δ2 Δ1' Δ2'.
  induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
  apply pure_elim with (envs_wf Δ1); [unfold of_envs; solve_sep_entails|]=> Hwf.
  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.
357
Lemma envs_split_sound Δ d js Δ1 Δ2 :
358
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
359
Proof.
360
  rewrite /envs_split=> ?. rewrite -(idemp uPred_and (of_envs Δ)).
361
  rewrite {2}envs_clear_spatial_sound sep_elim_l and_sep_r.
362
363
364
  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=> ->. }
365
  destruct d; simplify_eq; solve_sep_entails.
366
367
Qed.

368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
Global Instance envs_Forall2_refl (R : relation (uPred M)) :
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Global Instance envs_Forall2_sym (R : relation (uPred M)) :
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Global Instance envs_Forall2_trans (R : relation (uPred M)) :
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Lemma envs_Forall2_impl (R R' : relation (uPred M)) Δ1 Δ2 :
  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.

Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in *.
387
388
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
389
390
391
392
393
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Global Instance of_envs_proper : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
394
395
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
396
Qed.
397
398

Global Instance Envs_proper (R : relation (uPred M)) :
399
400
401
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
Proof. by constructor. Qed.

402
403
404
405
406
407
408
Global Instance envs_entails_proper :
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails M).
Proof. solve_proper. Qed.
Global Instance envs_entails_flip_mono :
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails M).
Proof. rewrite /envs_entails=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
409
(** * Adequacy *)
410
Lemma tac_adequate P : envs_entails (Envs Enil Enil) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
Proof.
412
  rewrite /envs_entails=> <-. rewrite /of_envs /= persistently_pure !right_id.
413
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
416
Qed.

(** * Basic rules *)
417
Lemma tac_assumption Δ i p P Q :
418
419
420
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q 
  envs_entails Δ Q.
Proof. intros. by rewrite /envs_entails envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
423
424

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
425
426
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
Proof.
428
  rewrite /envs_entails=> ?? <-. rewrite envs_simple_replace_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
429
430
431
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.
Lemma tac_clear Δ Δ' i p P Q :
432
433
434
435
436
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  envs_entails Δ' Q  envs_entails Δ Q.
Proof.
  rewrite /envs_entails=> ? <-. by rewrite envs_lookup_delete_sound // sep_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
437
438

(** * False *)
439
440
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
441
442

(** * Pure *)
443
444
Lemma tac_pure_intro Δ Q φ : FromPure Q φ  φ  envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
445

Robbert Krebbers's avatar
Robbert Krebbers committed
446
Lemma tac_pure Δ Δ' i p P φ Q :
447
  envs_lookup_delete i Δ = Some (p, P, Δ')  IntoPure P φ 
448
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
Proof.
450
  rewrite /envs_entails=> ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
451
  rewrite (into_pure P); by apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
453
Qed.

454
455
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
456
457

(** * Later *)
458
459
460
461
462
Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
  into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
  into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
  into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
463
464
}.

465
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
466
Proof. constructor. Qed.
467
468
469
Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
  IntoLaterNEnv n Γ1 Γ2  IntoLaterN n P Q 
  IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
470
471
Proof. by constructor. Qed.

472
473
474
Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
  IntoLaterNEnv n Γp1 Γp2  IntoLaterNEnv n Γs1 Γs2 
  IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
475
Proof. by split. Qed.
476

477
478
Lemma into_laterN_env_sound n Δ1 Δ2 :
  IntoLaterNEnvs n Δ1 Δ2  of_envs Δ1  ^n (of_envs Δ2).
Robbert Krebbers's avatar
Robbert Krebbers committed
479
Proof.
480
481
  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
  repeat apply sep_mono; try apply persistently_mono.
482
  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
483
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
484
485
  - induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
  - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
486
487
Qed.

488
Lemma tac_next Δ Δ' n Q Q' :
489
490
491
492
493
494
  FromLaterN n Q Q'  IntoLaterNEnvs n Δ Δ' 
  envs_entails Δ' Q'  envs_entails Δ Q.
Proof.
  rewrite /envs_entails=> ?? HQ.
  by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
495
496

Lemma tac_löb Δ Δ' i Q :
497
  env_spatial_is_nil Δ = true 
498
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
499
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
Proof.
501
502
  rewrite /envs_entails=> ?? HQ.
  rewrite -(persistently_elim Q) -(löb ( Q)) -persistently_later.
503
  apply impl_intro_l, (persistently_intro _ _).
504
  rewrite envs_app_sound //; simpl.
505
  by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
506
507
Qed.

508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
(** * Persistence and plainness modality *)
Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
  into_plain_env_subenv : env_subenv Γ2 Γ1;
  into_plain_env_plain : Plain ([] Γ2);
}.
Class IntoPersistentEnvs (p : bool) (Δ1 Δ2 : envs M) := {
  into_persistent_envs_persistent :
    if p then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
    else env_persistent Δ1 = env_persistent Δ2;
  into_persistent_envs_spatial : env_spatial Δ2 = Enil
}.

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.

Global Instance into_persistent_envs_false Γp Γs :
  IntoPersistentEnvs false (Envs Γp Γs) (Envs Γp Enil).
Proof. by split. Qed.
Global Instance into_persistent_envs_true Γp1 Γp2 Γs1 :
  IntoPlainEnv Γp1 Γp2 
  IntoPersistentEnvs true (Envs Γp1 Γs1) (Envs Γp2 Enil).
Proof. by split. Qed.

Lemma into_persistent_envs_sound (p : bool) Δ1 Δ2 :
539
540
  IntoPersistentEnvs p Δ1 Δ2 
  of_envs Δ1  (if p then  of_envs Δ2 else  of_envs Δ2).
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
Proof.
  rewrite /of_envs. destruct Δ1 as [Γp1 Γs1], Δ2 as [Γp2 Γs2]=> -[/= Hp ->].
  apply pure_elim_sep_l=> Hwf. rewrite sep_elim_l. destruct p; simplify_eq/=.
  - destruct Hp. rewrite right_id plainly_sep plainly_pure.
    apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; eauto using Enil_wf, env_subenv_wf.
    + rewrite persistently_elim plainly_persistently plainly_plainly.
      by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
  - rewrite right_id persistently_sep persistently_pure.
    apply sep_intro_True_l; [apply pure_intro|by rewrite persistent_persistently].
    destruct Hwf; constructor; simpl; eauto using Enil_wf.
Qed.

Lemma tac_always_intro Δ Δ' p Q Q' :
  FromAlways p Q' Q 
  IntoPersistentEnvs p Δ Δ' 
557
  envs_entails Δ' Q  envs_entails Δ Q'.
558
Proof.
559
560
  rewrite /envs_entails=> ?? HQ.
  rewrite into_persistent_envs_sound -(from_always _ Q').
561
  destruct p; auto using persistently_mono, plainly_mono.
562
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
564

Lemma tac_persistent Δ Δ' i p P P' Q :
565
  envs_lookup i Δ = Some (p, P) 
566
  IntoPersistent p P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
567
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
568
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
569
Proof.
570
  rewrite /envs_entails=> ? HP ? <-. rewrite envs_replace_sound //; simpl.
571
  by rewrite right_id (into_persistent _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
572
573
574
575
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
576
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
577
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
578
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
579
Proof.
580
581
  rewrite /envs_entails=> ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
  - rewrite (persistent (of_envs Δ)) envs_app_sound //; simpl.
582
    by rewrite right_id -persistently_impl_wand persistently_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
583
  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
584
    by rewrite and_sep_l right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
586
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
587
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
588
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
589
  envs_entails Δ' Q  envs_entails Δ (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
590
Proof.
591
592
  rewrite /envs_entails=> ?? HQ.
  rewrite envs_app_sound //=; simpl. apply impl_intro_l.
593
  rewrite (_ : P = ?false P) // (into_persistent false P).
594
  by rewrite right_id persistently_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
Qed.
596

597
598
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
599
600

Lemma tac_wand_intro Δ Δ' i P Q :
601
602
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
  envs_entails Δ' Q  envs_entails Δ (P - Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
603
Proof.
604
605
  rewrite /envs_entails=> ? HQ.
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
606
607
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
608
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
609
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
610
  envs_entails Δ' Q  envs_entails Δ (P - Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
611
Proof.
612
  rewrite /envs_entails => ?? <-. rewrite envs_app_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
614
  rewrite right_id. by apply wand_mono.
Qed.
615
616
Lemma tac_wand_intro_drop Δ P Q : envs_entails Δ Q  envs_entails Δ (P - Q).
Proof. rewrite /envs_entails=> <-. apply wand_intro_l. by rewrite sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
617
618
619
620
621

(* 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, Δ') 
622
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
623
  IntoWand p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
624
625
626
627
628
  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 Δ'' 
629
  envs_entails Δ'' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
630
Proof.
631
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
Robbert Krebbers's avatar
Robbert Krebbers committed
632
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
633
    rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
634
    + by rewrite persistently_wand persistent_persistently !wand_elim_r.
635
    + by rewrite !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
636
637
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
638
    by rewrite right_id assoc (into_wand _ R) persistently_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
639
640
Qed.

641
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
642
  envs_lookup_delete j Δ = Some (q, R, Δ') 
643
  IntoWand false R P1 P2  ElimModal P1' P1 Q Q 
644
  ('(Δ1,Δ2)  envs_split (if neg is true then Right else Left) js Δ';
645
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
646
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
647
  envs_entails Δ1 P1'  envs_entails Δ2' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
648
Proof.
649
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
650
651
652
653
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
  rewrite (envs_app_sound Δ2) //; simpl.
654
  rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
655
  rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
656
  by rewrite persistently_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
657
658
Qed.

659
Lemma tac_unlock Δ Q : envs_entails Δ Q  envs_entails Δ (locked Q).
660
661
662
663
Proof. by unlock. Qed.

Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
664
  IntoWand false R P1 P2 
665
  ElimModal P1' P1 Q Q 
666
  envs_entails Δ' (P1'  locked Q') 
667
  Q' = (P2 - Q)%I 
668
  envs_entails Δ Q.
669
Proof.
670
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
671
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
672
  rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
673
674
675
676
  rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
  by rewrite assoc !wand_elim_r.
Qed.

677
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
678
  envs_lookup j Δ = Some (q, R) 
679
  IntoWand false R P1 P2  FromPure P1 φ 
680
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
681
  φ  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
682
Proof.
683
  rewrite /envs_entails=> ????? <-. rewrite envs_simple_replace_sound //; simpl.
684
  rewrite right_id (into_wand _ R) -(from_pure P1) pure_True //.
685
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
686
687
Qed.

688
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
689
  envs_lookup_delete j Δ = Some (q, R, Δ') 
690
  IntoWand false R P1 P2  Persistent P1 
691
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
692
  envs_entails Δ' P1  envs_entails Δ'' Q  envs_entails Δ Q.
693
Proof.
694
  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
695
  rewrite envs_lookup_sound //.
696
  rewrite -(idemp uPred_and (of_envs (envs_delete _ _ _))).
697
  rewrite {1}HP1 (persistent P1) persistently_and_sep_l assoc.
698
  rewrite envs_simple_replace_sound' //; simpl.
699
  rewrite right_id (into_wand _ R) (persistently_elim_if q) -persistently_if_sep wand_elim_l.
700
701
702
703
704
  by rewrite wand_elim_r.
Qed.

Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
  envs_lookup j Δ = Some (q,P) 
705
  envs_entails Δ R  Persistent R 
706
  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' 
707
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
708
Proof.
709
710
  rewrite /envs_entails. intros ? HR ?? <-.
  rewrite -(idemp uPred_and (of_envs Δ)) {1}HR and_sep_l.
711
  rewrite envs_replace_sound //; simpl.
712
  by rewrite right_id assoc (sep_elim_l R) persistent_persistently wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
713
714
715
716
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
717
718
  envs_entails Δ' ((if p then  P else P)%I - Q) 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
719
Proof.
720
  rewrite /envs_entails=> ? HQ. rewrite envs_lookup_delete_sound //; simpl.
721
  by rewrite HQ /uPred_persistently_if wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
722
723
Qed.

724
Class IntoIH (φ : Prop) (Δ : envs M) (Q : uPred M) :=
725
726
  into_ih : φ  of_envs Δ  Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
727
728
729
730
731
732
733
734
735
736
Proof. by rewrite /IntoIH. Qed.
Global Instance into_ih_forall {A} (φ : A  Prop) Δ Φ :
  ( x, IntoIH (φ x) Δ (Φ x))  IntoIH ( x, φ x) Δ ( x, Φ x) | 2.
Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
  IntoIH φ Δ Q  IntoIH (ψ  φ) Δ (⌜ψ⌝  Q) | 1.
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.

Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P 
737
  env_spatial_is_nil Δ = true 
738
739
  envs_entails Δ ( P  Q) 
  envs_entails Δ Q.
740
Proof.
741
742
743
  rewrite /envs_entails /IntoIH=> HP ? HPQ.
  rewrite -(idemp uPred_and (of_envs Δ)) {1}(persistent (of_envs Δ)).
  by rewrite {1}HP // HPQ impl_elim_r.
744
745
Qed.

746
Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
747
  ElimModal P' P Q Q 
748
  envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2) 
749
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
750
  envs_entails Δ1 P'  envs_entails Δ2' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
751
Proof.
752
  rewrite /envs_entails=> ??? HP HQ. rewrite envs_split_sound //.
753
  rewrite (envs_app_sound Δ2) //; simpl.
754
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
755
756
Qed.

757
758
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' neg js j P Q :
  envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
759
  envs_app false (Esnoc Enil j P) Δ = Some Δ' 
760
  Persistent P 
761
  envs_entails Δ1 P  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
762
Proof.
763
764
  rewrite /envs_entails=> ??? HP <-.
  rewrite -(idemp uPred_and (of_envs Δ)) {1}envs_split_sound //.
765
  rewrite HP sep_elim_l (and_sep_l P) envs_app_sound //; simpl.