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

Coercion of_envs {M} (Δ : envs M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
25
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
26
27
28
29
30
31
Instance: Params (@of_envs) 1.

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
32

33
34
Definition envs_dom {M} (Δ : envs M) : list string :=
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

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.

56
57
58
59
60
61
62
63
64
65
66
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.

67
68
69
70
71
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
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 Δ).

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

96
97
98
Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
  Envs (env_persistent Δ) Enil.

99
100
101
Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
  Envs Enil (env_spatial Δ).

102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
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.
(* if [lr = true] then [result = (remaining hyps, hyps named js)] and
   if [lr = false] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {M} (lr : bool)
    (js : list string) (Δ : envs M) : option (envs M * envs M) :=
  '(Δ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
118
119
(* Coq versions of the tactics *)
Section tactics.
120
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
122
123
124
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

125
Lemma of_envs_def Δ :
Ralf Jung's avatar
Ralf Jung committed
126
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
127
128
Proof. done. Qed.

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

Lemma envs_lookup_split Δ i p P :
163
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  (?p P - Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
165
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
167
  - rewrite (env_lookup_perm Γp) //= always_sep.
168
    rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
171
    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
175
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
176
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  ?p P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
179
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ')  Δ  ?p [] Ps  Δ'.
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
  { by rewrite always_pure left_id. }
  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/=.
  rewrite always_if_sep -assoc. destruct q1; simpl.
  - destruct rp.
    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (always_elim_if q2).
    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (always_elim_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite always_if_elim.
Qed.

197
198
199
200
201
202
203
204
205
206
207
208
209
210
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 :
211
  envs_lookup i Δ = None  Δ  ?p P - envs_snoc Δ p i P.
212
213
214
215
216
217
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.
218
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
219
    + by rewrite always_sep assoc.
220
221
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
222
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
223
224
225
    + solve_sep_entails.
Qed.

226
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
Proof.
228
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
232
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
235
236
    + 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') //.
237
      rewrite big_opL_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
239
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
240
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
243
    + 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.
244
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
246
247
248
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
249
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
250
251
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
252
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
254
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
255
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
256
257
258
259
    + 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') //.
260
      rewrite big_opL_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
262
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
263
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
267
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
269
270
271
Qed.

Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
272
  Δ  ?p P  (?p [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
273
274
275
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
276
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
278
279
280
281
282
283
284
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 Δ' 
285
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

288
289
290
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
291
Proof.
292
293
294
  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
295
296
Qed.

297
Lemma envs_clear_spatial_sound Δ : Δ  envs_clear_spatial Δ  [] env_spatial Δ.
298
Proof.
299
300
  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].
301
302
303
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

304
305
Lemma env_spatial_is_nil_persistent Δ :
  env_spatial_is_nil Δ = true  PersistentP Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
307
Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
308

309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
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) 
329
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2')  Δ1  Δ2  Δ1'  Δ2'.
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
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.
Lemma envs_split_sound Δ lr js Δ1 Δ2 :
345
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
346
347
348
349
350
351
352
353
354
Proof.
  rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
  rewrite {2}envs_clear_spatial_sound sep_elim_l always_and_sep_r.
  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.

355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
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 *.
374
375
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
376
377
378
379
380
      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.
381
382
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
383
384
385
386
387
Qed.
Global Instance Envs_mono (R : relation (uPred M)) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
Proof. by constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
388
(** * Adequacy *)
389
Lemma tac_adequate P : (Envs Enil Enil  P)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
390
Proof.
391
392
  intros <-. rewrite /of_envs /= always_pure !right_id.
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
393
394
395
Qed.

(** * Basic rules *)
396
Lemma tac_assumption Δ i p P Q :
397
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q  Δ  Q.
398
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
399
400
401
402

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
403
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
405
406
407
408
Proof.
  intros. rewrite envs_simple_replace_sound //.
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.
Lemma tac_clear Δ Δ' i p P Q :
409
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
411
412
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.

(** * False *)
413
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
416
Proof. by rewrite -(False_elim Q). Qed.

(** * Pure *)
417
Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ  φ  Δ  Q.
418
Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
419

Robbert Krebbers's avatar
Robbert Krebbers committed
420
Lemma tac_pure Δ Δ' i p P φ Q :
421
  envs_lookup_delete i Δ = Some (p, P, Δ')  IntoPure P φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
422
423
424
  (φ  Δ'  Q)  Δ  Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
425
  rewrite (into_pure P); by apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
427
Qed.

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

(** * Later *)
432
433
434
435
436
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)
437
438
}.

439
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
Proof. constructor. Qed.
441
442
443
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
444
445
Proof. by constructor. Qed.

446
447
448
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
449
Proof. by split. Qed.
450

451
Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2  Δ1  ^n Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
Proof.
453
  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -always_laterN.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
  repeat apply sep_mono; try apply always_mono.
455
  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
456
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
457
458
  - 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
459
460
Qed.

461
462
463
Lemma tac_next Δ Δ' n Q Q' :
  FromLaterN n Q Q'  IntoLaterNEnvs n Δ Δ'  (Δ'  Q')  Δ  Q.
Proof. intros ?? HQ. by rewrite -(from_laterN n Q) into_laterN_env_sound HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
464
465

Lemma tac_löb Δ Δ' i Q :
466
  env_spatial_is_nil Δ = true 
467
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
468
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
Proof.
470
471
472
473
  intros ?? HQ. rewrite -(always_elim Q) -(löb ( Q)) -always_later.
  apply impl_intro_l, (always_intro _ _).
  rewrite envs_app_sound //; simpl.
  by rewrite right_id always_and_sep_l' wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
476
Qed.

(** * Always *)
477
478
479
480
481
482
Lemma tac_always_intro Δ Q :
  (envs_clear_spatial Δ  Q)  Δ   Q.
Proof.
  intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
  by apply (always_intro _ _).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
484

Lemma tac_persistent Δ Δ' i p P P' Q :
485
  envs_lookup i Δ = Some (p, P)  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
486
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
487
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
Proof.
489
  intros ??? <-. rewrite envs_replace_sound //; simpl.
490
  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
491
492
493
494
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
495
  (if env_spatial_is_nil Δ then Unit else PersistentP P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
496
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
497
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
499
500
501
502
503
  intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
  - rewrite (persistentP Δ) envs_app_sound //; simpl.
    by rewrite right_id always_wand_impl always_elim.
  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
    by rewrite always_and_sep_l right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
504
505
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
506
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
507
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
508
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
509
510
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
511
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
Qed.
513
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
Ralf Jung's avatar
Ralf Jung committed
514
  (φ  Δ  ⌜ψ⌝)  Δ  ⌜φ  ψ⌝.
515
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
516
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
517
Proof.
518
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
519
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
521
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
522
523

Lemma tac_wand_intro Δ Δ' i P Q :
524
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
Proof.
526
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
527
528
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
529
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
530
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
531
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
534
535
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
536
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Proof.
538
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
539
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
Lemma tac_wand_intro_drop Δ P Q : (Δ  Q)  Δ  P - Q.
Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
542
543
544
545
546

(* 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, Δ') 
547
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
548
  IntoWand p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
549
550
551
552
553
  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 Δ'' 
554
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
556
557
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
558
559
560
    rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
    + by rewrite always_wand always_always !wand_elim_r.
    + by rewrite !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
562
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
563
    by rewrite right_id assoc (into_wand _ R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
564
565
Qed.

566
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
567
  envs_lookup_delete j Δ = Some (q, R, Δ') 
568
  IntoWand false R P1 P2  ElimModal P1' P1 Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
569
  ('(Δ1,Δ2)  envs_split lr js Δ';
570
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
571
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
572
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
Proof.
574
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
576
577
578
  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.
579
  rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
580
  rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
581
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
582
583
Qed.

584
585
586
587
588
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, Δ') 
589
  IntoWand false R P1 P2 
590
591
592
593
594
595
596
  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.
597
  rewrite (into_wand _ R) assoc -(comm _ P1') -assoc always_if_elim.
598
599
600
601
  rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
  by rewrite assoc !wand_elim_r.
Qed.

602
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
603
  envs_lookup j Δ = Some (q, R) 
604
  IntoWand false R P1 P2  FromPure P1 φ 
605
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
606
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
607
Proof.
608
  intros. rewrite envs_simple_replace_sound //; simpl.
609
  rewrite right_id (into_wand _ R) -(from_pure P1) pure_True //.
610
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
611
612
Qed.

613
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
614
  envs_lookup_delete j Δ = Some (q, R, Δ') 
615
  IntoWand false R P1 P2  PersistentP P1 
616
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
617
618
619
620
621
622
623
  (Δ'  P1)  (Δ''  Q)  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
  rewrite envs_lookup_sound //.
  rewrite -(idemp uPred_and (envs_delete _ _ _)).
  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
  rewrite envs_simple_replace_sound' //; simpl.
624
  rewrite right_id (into_wand _ R) (always_elim_if q) -always_if_sep wand_elim_l.
625
626
627
628
629
630
631
632
  by rewrite wand_elim_r.
Qed.

Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
  envs_lookup j Δ = Some (q,P) 
  (Δ  R)  PersistentP R 
  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
633
Proof.
634
635
636
637
  intros ? HR ?? <-.
  rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
  rewrite envs_replace_sound //; simpl.
  by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
638
639
640
641
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
642
  (Δ'  (if p then  P else P) - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
643
Proof.
644
645
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
  by rewrite HQ /uPred_always_if wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
646
647
Qed.

648
649
650
651
652
653
654
655
656
657
Lemma tac_revert_ih Δ P Q :
  env_spatial_is_nil Δ = true 
  (of_envs Δ  P) 
  (of_envs Δ   P  Q) 
  (of_envs Δ  Q).
Proof.
  intros ? HP HPQ.
  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
Qed.

658
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
659
  ElimModal P' P Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
660
  envs_split lr js Δ = Some (Δ1,Δ2) 
661
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
662
  (Δ1  P')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
663
Proof.
664
  intros ??? HP HQ. rewrite envs_split_sound //.
665
  rewrite (envs_app_sound Δ2) //; simpl.
666
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
667
668
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
669
670
671
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
  envs_split lr js Δ = Some (Δ1,Δ2) 
  envs_app false (Esnoc Enil j P) Δ = Some Δ' 
672
673
  PersistentP P 
  (Δ1  P)  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
674
Proof.
675
  intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
676
677
  rewrite HP sep_elim_l (always_and_sep_l P) envs_app_sound //; simpl.
  by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
678
679
Qed.

680
681
682
683
684
685
686
687
688
Lemma tac_assert_pure Δ Δ' j P φ Q :
  envs_app false (Esnoc Enil j P) Δ = Some Δ' 
  FromPure P φ 
  φ  (Δ'  Q)  Δ  Q.
Proof.
  intros ??? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -(from_pure P) pure_True // -always_impl_wand True_impl.
Qed.

689
Lemma tac_pose_proof Δ Δ' j P Q :
690
  P 
691
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
692
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
693
Proof.
694
695
  intros HP ? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -HP always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
696
697
Qed.

698
699
700
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' 
701
  (Δ''  Q)  Δ  Q.
702
703
704
705
706
707
708
709
Proof.
  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
710
Lemma tac_apply Δ Δ' i p R P1 P2 :
711
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand false R P1 P2 
712
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
713
714
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
715
  by rewrite (into_wand _ R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
716
717
718
719
720
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
721
   {A : ofeT} (x y : A) (Φ : A  uPred M),
722
723
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x)) 
724
    (NonExpansive Φ) 
725
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
726
Proof.
727
  intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
728
  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
729
  destruct lr; auto using internal_eq_sym.
Robbert Krebbers's avatar
Robbert Krebbers committed
730
731
732
733
Qed.

Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
734
  envs_lookup j Δ = Some (q, P) 
735
   {A : ofeT} Δ' x y (Φ : A  uPred M),
736
737
    (Pxy  x  y) 
    (P  Φ (if lr then y else x)) 
738
    (NonExpansive Φ) 
Robbert Krebbers's avatar
Robbert Krebbers committed
739
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
740
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
741
742
743
744
Proof.
  intros ?? A Δ' x y Φ HPxy HP ?? <-.
  rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
  rewrite sep_elim_l HPxy always_and_sep_r.
745
746
  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
  rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
747
  - apply (internal_eq_rewrite x y (λ y, ?q Φ y - Δ')%I);
748
      eauto with I. solve_proper.
749
  - apply (internal_eq_rewrite y x (λ y, ?q Φ y - Δ')%I);
750
      eauto using internal_eq_sym with I.
751
    solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
752
753
754
Qed.

(** * Conjunction splitting *)
755
756
757
Lemma tac_and_split Δ P Q1 Q2 :
  FromAnd true P Q1 Q2  (Δ  Q1)  (Δ  Q2)  Δ  P.
Proof. intros. rewrite -(from_and true P). by apply and_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
758
759
760

(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
761
  FromAnd false P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
762
  envs_split lr js Δ = Some (Δ1,Δ2) 
763
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
764
Proof.
765
  intros. rewrite envs_split_sound // -(from_and false P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
766
767
768
Qed.

(** * Combining *)
769
770
771
772
773
774
775
776
777
Class FromSeps {M} (P : uPred M) (Qs : list (uPred M)) :=
  from_seps : [] Qs  P.
Arguments from_seps {_} _ _ {_}.

Global Instance from_seps_nil : @FromSeps M True [].
Proof. done. Qed.
Global Instance from_seps_singleton P : FromSeps P [P] | 1.
Proof. by rewrite /FromSeps /= right_id. Qed.
Global Instance from_seps_cons P P' Q Qs :
778
779
  FromSeps P' Qs  FromAnd false P Q P'  FromSeps P (Q :: Qs) | 2.
Proof. by rewrite /FromSeps /FromAnd /= => ->. Qed.
780
781
782
783
784
785
786
787
788
789

Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
  envs_lookup_delete_list js false Δ1 = Some (p, Ps, Δ2) 
  FromSeps P Ps 
  envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 
  (Δ3  Q)  Δ1  Q.
Proof.
  intros ??? <-. rewrite envs_lookup_delete_list_sound //.
  rewrite from_seps. rewrite envs_app_sound //; simpl.
  by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
790
791
792
Qed.

(** * Conjunction/separating conjunction elimination *)
793
794
Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
  envs_lookup i Δ = Some (p, P)  IntoAnd p P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
795
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
796
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
797
Proof.
798
  intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
799
  by destruct p; rewrite /= ?right_id (comm _ P1) ?always_and_sep wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
800
801
Qed.

802
803
804
805
806
807
808