coq_tactics.v 41.2 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.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import uPred.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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

10
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
13
14
15
16
17
18
19
20
21
22
  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
}.

23
Definition of_envs {M} (Δ : envs M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
24
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
25
26
Instance: Params (@of_envs) 1.

27
28
29
30
31
32
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.

33
34
35
36
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
37

38
Definition envs_dom {M} (Δ : envs M) : list ident :=
39
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
Definition envs_lookup {M} (i : ident) (Δ : envs M) : option (bool * uPred M) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
44
45
46
  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.

47
Definition envs_delete {M} (i : ident) (p : bool) (Δ : envs M) : envs M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
50
51
52
  let (Γp,Γs) := Δ in
  match p with
  | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
  end.

53
Definition envs_lookup_delete {M} (i : ident)
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
56
57
58
59
60
    (Δ : 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.

61
Fixpoint envs_lookup_delete_list {M} (js : list ident) (remove_persistent : bool)
62
63
64
65
66
67
68
69
70
71
    (Δ : 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.

72
Definition envs_snoc {M} (Δ : envs M)
73
    (p : bool) (j : ident) (P : uPred M) : envs M :=
74
75
76
  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
77
78
79
80
81
82
83
84
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.

85
Definition envs_simple_replace {M} (i : ident) (p : bool) (Γ : env (uPred M))
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
88
89
90
91
92
    (Δ : 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.

93
Definition envs_replace {M} (i : ident) (p q : bool) (Γ : env (uPred M))
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
97
    (Δ : envs M) : option (envs M) :=
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

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

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

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

107
Fixpoint envs_split_go {M}
108
    (js : list ident) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
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.
116
117
118
(* 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)
119
    (js : list ident) (Δ : envs M) : option (envs M * envs M) :=
120
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
121
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
122

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

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

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

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

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

189
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
190
191
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
192
193
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
194
  { by rewrite persistently_pure left_id. }
195
196
197
  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/=.
198
  rewrite persistently_if_sep -assoc. destruct q1; simpl.
199
  - destruct rp.
200
201
202
    + 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.
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
221
222
223
224
225
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.
226
      intros j; destruct (ident_beq_reflect j i); naive_solver.
227
    + by rewrite persistently_sep assoc.
228
229
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
230
      intros j; destruct (ident_beq_reflect j i); naive_solver.
231
232
233
    + solve_sep_entails.
Qed.

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

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

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

Lemma envs_replace_sound' Δ Δ' i p q Γ :
285
286
  envs_replace i p q Γ Δ = Some Δ' 
  of_envs (envs_delete i p Δ)  ?q [] Γ - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
289
290
291
292
293
294
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 Δ' 
295
  of_envs Δ  ?p P  (?q [] Γ - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
296
297
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

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

307
308
Lemma envs_clear_spatial_sound Δ :
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
309
Proof.
310
311
  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].
312
313
314
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

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

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

367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
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 *.
386
387
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
388
389
390
391
392
      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.
393
394
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
395
Qed.
396
397

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

401
402
403
404
405
406
407
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
408
(** * Adequacy *)
409
Lemma tac_adequate P : envs_entails (Envs Enil Enil) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
Proof.
411
  rewrite /envs_entails=> <-. rewrite /of_envs /= persistently_pure !right_id.
412
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
414
415
Qed.

(** * Basic rules *)
416
Lemma tac_assumption Δ i p P Q :
417
418
419
  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
420
421
422
423

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

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

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

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

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

(** * Later *)
457
458
459
460
461
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)
462
463
}.

464
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
465
Proof. constructor. Qed.
466
467
468
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
469
470
Proof. by constructor. Qed.

471
472
473
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
474
Proof. by split. Qed.
475

476
477
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
478
Proof.
479
480
  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
  repeat apply sep_mono; try apply persistently_mono.
481
  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
482
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
483
484
  - 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
485
486
Qed.

487
Lemma tac_next Δ Δ' n Q Q' :
488
489
490
491
492
493
  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
494
495

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

507
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
(** * 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 :
538
539
  IntoPersistentEnvs p Δ1 Δ2 
  of_envs Δ1  (if p then  of_envs Δ2 else  of_envs Δ2).
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
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 Δ Δ' 
556
  envs_entails Δ' Q  envs_entails Δ Q'.
557
Proof.
558
559
  rewrite /envs_entails=> ?? HQ.
  rewrite into_persistent_envs_sound -(from_always _ Q').
560
  destruct p; auto using persistently_mono, plainly_mono.
561
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
563

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

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

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

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

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

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

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

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

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

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

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

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

723
Class IntoIH (φ : Prop) (Δ : envs M) (Q : uPred M) :=
724
725
  into_ih : φ  of_envs Δ  Q.
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
726
727
728
729
730
731
732
733
734
735
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 
736
  env_spatial_is_nil Δ = true 
737
738
  envs_entails Δ ( P  Q) 
  envs_entails Δ Q.
739
Proof.
740
741
742
  rewrite /envs_entails /IntoIH=> HP ? HPQ.
  rewrite -(idemp uPred_and (of_envs Δ)) {1}(persistent (of_envs Δ)).
  by rewrite {1}HP // HPQ impl_elim_r.
743
744
Qed.

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