coq_tactics.v 33.8 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Export upred.
2
From iris.algebra Require Import upred_big_op upred_tactics.
3
From iris.proofmode Require Export environments classes.
4
From iris.prelude Require Import stringmap hlist.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import uPred.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
11
12
13
14
15
16
17
18
19
20
21
  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 :=
22
  ( envs_wf Δ   [] env_persistent Δ  [] env_spatial Δ)%I.
23
24
25
26
27
28
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
29

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

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.

53
54
55
56
57
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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
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 Δ).

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

82
83
84
Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
  Envs (env_persistent Δ) Enil.

85
86
87
Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
  Envs Enil (env_spatial Δ).

88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
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
105
106
(* Coq versions of the tactics *)
Section tactics.
107
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
110
111
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

112
Lemma of_envs_def Δ :
113
  of_envs Δ = ( envs_wf Δ   [] env_persistent Δ  [] env_spatial Δ)%I.
114
115
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
118
119
120
121
122
123
124
125
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 :
126
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  envs_delete i p Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
128
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
130
131
  - rewrite (env_lookup_perm Γp) //= always_sep.
    ecancel [ [] _;  P; [] Γs]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
134
135
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
136
    ecancel [ [] _; P; [] (env_delete _ _)]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
139
140
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
141
  envs_lookup i Δ = Some (p,P)  Δ  P  envs_delete i p Δ.
142
Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Lemma envs_lookup_persistent_sound Δ i P :
144
  envs_lookup i Δ = Some (true,P)  Δ   P  Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof.
146
  intros. apply (always_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
149
Qed.

Lemma envs_lookup_split Δ i p P :
150
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  (?p P - Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
152
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
154
  - rewrite (env_lookup_perm Γp) //= always_sep.
155
    rewrite pure_equiv // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
158
    rewrite (env_lookup_perm Γs) //=. rewrite pure_equiv // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
162
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
163
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  ?p P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
166
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
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 :
  envs_lookup i Δ = None  Δ  ?p P - envs_snoc Δ p i P.
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.
      intros j; case_decide; naive_solver.
191
    + by rewrite always_sep assoc.
192
193
194
195
196
197
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
      intros j; case_decide; naive_solver.
    + solve_sep_entails.
Qed.

198
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Proof.
200
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
203
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
204
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
207
208
    + 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') //.
209
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
212
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
216
217
218
219
220
    + 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 _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
221
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
224
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
226
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
227
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
230
231
    + 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') //.
232
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
235
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
239
240
241
242
243
    + 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 _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

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

Lemma envs_replace_sound' Δ Δ' i p q Γ :
248
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
250
251
252
253
254
255
256
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 Δ' 
257
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
258
259
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

260
261
262
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
263
Proof.
264
265
266
  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
267
268
Qed.

269
Lemma envs_clear_spatial_sound Δ : Δ  envs_clear_spatial Δ  [] env_spatial Δ.
270
Proof.
271
272
  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].
273
274
275
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

276
277
Lemma env_spatial_is_nil_persistent Δ :
  env_spatial_is_nil Δ = true  PersistentP Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
279
Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
280

281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
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) 
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2')  Δ1  Δ2  Δ1'  Δ2'.
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 :
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
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.

327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
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 *.
346
347
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
348
349
350
351
352
      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.
353
354
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
355
356
357
358
359
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
360
(** * Adequacy *)
361
Lemma tac_adequate P : (Envs Enil Enil  P)  True  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Proof.
363
364
  intros <-. rewrite /of_envs /= always_pure !right_id.
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
365
366
367
Qed.

(** * Basic rules *)
368
Lemma tac_assumption Δ i p P Q :
369
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q  Δ  Q.
370
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
371
372
373
374

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
375
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
377
378
379
380
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 :
381
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
384
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.

(** * False *)
385
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
387
388
Proof. by rewrite -(False_elim Q). Qed.

(** * Pure *)
389
Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ  φ  Δ  Q.
390
Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
391

Robbert Krebbers's avatar
Robbert Krebbers committed
392
Lemma tac_pure Δ Δ' i p P φ Q :
393
  envs_lookup_delete i Δ = Some (p, P, Δ')  IntoPure P φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
394
395
396
  (φ  Δ'  Q)  Δ  Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
397
  rewrite (into_pure P); by apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
398
399
Qed.

400
Lemma tac_pure_revert Δ φ Q : (Δ   φ  Q)  (φ  Δ  Q).
401
Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
403

(** * Later *)
404
405
406
407
408
Class IntoLaterEnv (Γ1 Γ2 : env (uPred M)) :=
  into_later_env : env_Forall2 IntoLater Γ1 Γ2.
Class IntoLaterEnvs (Δ1 Δ2 : envs M) := {
  into_later_persistent: IntoLaterEnv (env_persistent Δ1) (env_persistent Δ2);
  into_later_spatial: IntoLaterEnv (env_spatial Δ1) (env_spatial Δ2)
409
410
}.

411
Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
Proof. constructor. Qed.
413
414
415
Global Instance into_later_env_snoc Γ1 Γ2 i P Q :
  IntoLaterEnv Γ1 Γ2  IntoLater P Q 
  IntoLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
416
417
Proof. by constructor. Qed.

418
419
420
Global Instance into_later_envs Γp1 Γp2 Γs1 Γs2 :
  IntoLaterEnv Γp1 Γp2  IntoLaterEnv Γs1 Γs2 
  IntoLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Proof. by split. Qed.
422

423
Lemma into_later_env_sound Δ1 Δ2 : IntoLaterEnvs Δ1 Δ2  Δ1   Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
424
425
426
Proof.
  intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
  repeat apply sep_mono; try apply always_mono.
427
  - rewrite -later_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
428
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
429
430
  - induction Hp; rewrite /= ?later_sep. apply later_intro. by apply sep_mono.
  - induction Hs; rewrite /= ?later_sep. apply later_intro. by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
431
432
433
Qed.

Lemma tac_next Δ Δ' Q Q' :
434
435
  IntoLaterEnvs Δ Δ'  FromLater Q Q'  (Δ'  Q')  Δ  Q.
Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
436
437

Lemma tac_löb Δ Δ' i Q :
438
  env_spatial_is_nil Δ = true 
439
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
440
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
Proof.
442
443
444
445
  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
446
447
Qed.

448
Lemma tac_timeless Δ Δ' i p P P' Q :
449
450
  IsExceptLast Q 
  envs_lookup i Δ = Some (p, P)  IntoExceptLast P P' 
451
  envs_simple_replace i p (Esnoc Enil i P') Δ = Some Δ' 
452
453
454
  (Δ'  Q)  Δ  Q.
Proof.
  intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
455
456
  rewrite right_id HQ -{2}(is_except_last Q).
  by rewrite (into_except_last P) -except_last_always_if except_last_frame_r wand_elim_r.
457
458
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
459
(** * Always *)
460
Lemma tac_always_intro Δ Q : env_spatial_is_nil Δ = true  (Δ  Q)  Δ   Q.
461
Proof. intros. by apply (always_intro _ _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
463

Lemma tac_persistent Δ Δ' i p P P' Q :
464
  envs_lookup i Δ = Some (p, P)  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
465
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
466
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
Proof.
468
  intros ??? <-. rewrite envs_replace_sound //; simpl.
469
  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
470
471
472
473
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
474
  env_spatial_is_nil Δ = true 
Robbert Krebbers's avatar
Robbert Krebbers committed
475
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
476
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
478
479
480
481
Proof.
  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
  by rewrite right_id always_wand_impl always_elim HQ.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
482
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
483
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
484
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
487
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
Qed.
489
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
490
Proof.
491
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
493
494
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
495
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
496
Proof.
497
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
500
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
501
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
502
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
504
505
506
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
507
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
508
Proof.
509
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
511
512
513
514
515
Qed.

(* 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, Δ') 
516
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
517
  IntoWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
518
519
520
521
522
  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 Δ'' 
523
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
526
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
527
    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
528
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
529
530
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
531
    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
Qed.

534
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
535
  envs_lookup_delete j Δ = Some (q, R, Δ') 
536
  IntoWand R P1 P2  ElimVs P1' P1 Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
537
  ('(Δ1,Δ2)  envs_split lr js Δ';
538
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
539
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
540
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
541
Proof.
542
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
543
544
545
546
  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.
547
  rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
548
  rewrite -(elim_vs P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
549
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
551
Qed.

552
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
553
  envs_lookup j Δ = Some (q, R) 
554
  IntoWand R P1 P2  FromPure P1 φ 
555
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
556
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Proof.
558
  intros. rewrite envs_simple_replace_sound //; simpl.
559
560
  rewrite right_id (into_wand R) -(from_pure P1) pure_equiv //.
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
562
Qed.

563
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
564
  envs_lookup_delete j Δ = Some (q, R, Δ') 
565
  IntoWand R P1 P2  PersistentP P1 
566
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
  (Δ'  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.
  rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
  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
583
Proof.
584
585
586
587
  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
588
589
590
591
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
592
  (Δ'  if p then  P  Q else P - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
593
594
595
596
597
598
Proof.
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
  - by rewrite HQ -always_and_sep_l impl_elim_r.
  - by rewrite HQ wand_elim_r.
Qed.

599
600
601
602
603
604
605
606
607
608
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.

609
610
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
  ElimVs P' P Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
611
  envs_split lr js Δ = Some (Δ1,Δ2) 
612
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
613
  (Δ1  P')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Proof.
615
  intros ??? HP HQ. rewrite envs_split_sound //.
616
  rewrite (envs_app_sound Δ2) //; simpl.
617
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
618
619
620
621
Qed.

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
622
  (Δ  P)  PersistentP P  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Proof.
624
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
626
627
628
  rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
  by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
Qed.

629
630
631
Lemma tac_pose_proof Δ Δ' j P Q :
  (True  P) 
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
632
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
633
Proof.
634
635
  intros HP ? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -HP always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
636
637
Qed.

638
639
640
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 Δ'' 
641
  (Δ''  Q)  Δ  Q.
642
643
644
645
646
647
648
649
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
650
Lemma tac_apply Δ Δ' i p R P1 P2 :
651
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand R P1 P2 
652
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
653
654
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
655
  by rewrite (into_wand R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
656
657
658
659
660
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
Ralf Jung's avatar
Ralf Jung committed
661
   {A : cofeT} (x y : A) (Φ : A  uPred M),
662
663
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
664
    ( n, Proper (dist n ==> dist n) Φ) 
665
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
666
667
668
669
670
671
672
673
Proof.
  intros ? A x y ? HPxy -> ?; apply eq_rewrite; auto.
  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
  destruct lr; auto using eq_sym.
Qed.

Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
674
  envs_lookup j Δ = Some (q, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
675
   {A : cofeT} Δ' x y (Φ : A  uPred M),
676
677
    (Pxy  x  y) 
    (P  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
678
679
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
680
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
681
682
683
684
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.
685
686
687
688
689
  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
  rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
  - apply (eq_rewrite x y (λ y, ?q Φ y - Δ')%I); eauto with I. solve_proper.
  - apply (eq_rewrite y x (λ y, ?q Φ y - Δ')%I); eauto using eq_sym with I.
    solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
690
691
692
Qed.

(** * Conjunction splitting *)
693
694
Lemma tac_and_split Δ P Q1 Q2 : FromAnd P Q1 Q2  (Δ  Q1)  (Δ  Q2)  Δ  P.
Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
695
696
697

(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
698
  FromSep P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
699
  envs_split lr js Δ = Some (Δ1,Δ2) 
700
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
701
Proof.
702
  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
703
704
705
706
707
708
Qed.

(** * Combining *)
Lemma tac_combine Δ1 Δ2 Δ3 Δ4 i1 p P1 i2 q P2 j P Q :
  envs_lookup_delete i1 Δ1 = Some (p,P1,Δ2) 
  envs_lookup_delete i2 (if p then Δ1 else Δ2) = Some (q,P2,Δ3) 
709
  FromSep P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
710
711
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
712
  (Δ4  Q)  Δ1  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
713
714
715
716
717
Proof.
  intros [? ->]%envs_lookup_delete_Some [? ->]%envs_lookup_delete_Some ?? <-.
  destruct p.
  - rewrite envs_lookup_persistent_sound //. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
718
      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
719
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
720
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
721
722
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
723
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
724
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
725
      by rewrite right_id assoc (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
726
727
728
Qed.

(** * Conjunction/separating conjunction elimination *)
729
730
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
731
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
732
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
733
Proof.
734
  intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
735
  by destruct p; rewrite /= ?right_id (comm _ P1) ?always_and_sep wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
736
737
Qed.

738
739
740
741
742
743
744
745
746
747
748
749
750
751
(* Using this tactic, one can destruct a (non-separating) conjunction in the
spatial context as long as one of the conjuncts is thrown away. It corresponds
to the principle of "external choice" in linear logic. *)
Lemma tac_and_destruct_choice Δ Δ' i p (lr : bool) j P P1 P2 Q :
  envs_lookup i Δ = Some (p, P)  IntoAnd true P P1 P2 
  envs_simple_replace i p (Esnoc Enil j (if lr then P1 else P2)) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Proof.
  intros. rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id (into_and true P). destruct lr.
  - by rewrite and_elim_l wand_elim_r.
  - by rewrite and_elim_r wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
752
(** * Framing *)
753
754
755
756
Lemma tac_frame_pure Δ (φ : Prop) P Q :
  φ  Frame ( φ) P Q  (Δ  Q)  Δ  P.
Proof. intros ?? ->. by rewrite -(frame ( φ) P) pure_equiv // left_id. Qed.

757
758
759
Lemma tac_frame Δ Δ' i p R P Q :
  envs_lookup_delete i Δ = Some (p, R, Δ')  Frame R P Q 
  ((if p then Δ else Δ')  Q)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
760
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
761
  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
762
763
  - by rewrite envs_lookup_persistent_sound // always_elim -(frame R P) HQ.
  - rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
764
765
766
Qed.

(** * Disjunction *)
767
768
769
770
Lemma tac_or_l Δ P Q1 Q2 : FromOr P Q1 Q2  (Δ  Q1)  Δ  P.
Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
Lemma tac_or_r Δ P Q1 Q2 : FromOr P Q1 Q2  (Δ  Q2)  Δ  P.
Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
771
772

Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
773
  envs_lookup i Δ = Some (p, P)  IntoOr P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
774
775
  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 
  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 
776
  (Δ1  Q)  (Δ2  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
777
Proof.
778
  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
779
  rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
780
781
782
783
  - rewrite (envs_simple_replace_sound' _ Δ1) //.
    by rewrite /= right_id wand_elim_r.
  - rewrite (envs_simple_replace_sound' _ Δ2) //.
    by rewrite /= right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
784
785
786
Qed.

(** * Forall *)
787
Lemma tac_forall_intro {A} Δ (Φ : A  uPred M) : ( a, Δ  Φ a)  Δ   a, Φ a.
Robbert Krebbers's avatar
Robbert Krebbers committed
788
789
Proof. apply forall_intro. Qed.

790
Class ForallSpecialize {As} (xs : hlist As)
791
  (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P  Φ xs.
792
793
794
795
796
797
798
799
800
801
802
Arguments forall_specialize {_} _ _ _ {_}.

Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
Proof. done. Qed.
Global Instance forall_specialize_cons A As x xs Φ (Ψ : A  himpl As (uPred M)) :
  ( x, ForallSpecialize xs (Φ x) (Ψ x)) 
  ForallSpecialize (hcons x xs) ( x : A, Φ x) Ψ.
Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.

Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
  envs_lookup i Δ = Some (p, P)  ForallSpecialize xs P Φ 
803
  envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ' 
804
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
805
Proof.
806
807
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id (forall_specialize _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
808
809
810
Qed.

Lemma tac_forall_revert {A} Δ (Φ : A  uPred M) :