coq_tactics.v 34.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 environments classes.
4
From iris.prelude 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
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
10
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
}.

Coercion of_envs {M} (Δ : envs M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
23
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
24
25
26
27
28
29
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
30

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

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.

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

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

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

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

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

113
Lemma of_envs_def Δ :
Ralf Jung's avatar
Ralf Jung committed
114
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
115
116
Proof. done. Qed.

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

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

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

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

199
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
Proof.
201
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
204
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
205
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
208
209
    + 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') //.
210
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
213
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
216
217
218
219
220
221
    + 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 Δ' 
222
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
225
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
228
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
232
    + 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') //.
233
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
235
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
236
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
239
240
241
242
243
244
    + 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 Δ' 
245
  Δ  ?p P  (?p [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
246
247
248
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

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

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

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

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

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

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

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

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

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

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

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

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

(** * Later *)
405
406
407
408
409
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)
410
411
}.

412
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
Proof. constructor. Qed.
414
415
416
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
417
418
Proof. by constructor. Qed.

419
420
421
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
422
Proof. by split. Qed.
423

424
Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2  Δ1  ^n Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
425
Proof.
426
  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -always_laterN.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
  repeat apply sep_mono; try apply always_mono.
428
  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
429
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
430
431
  - 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
432
433
Qed.

434
435
436
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
437
438

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

(** * Always *)
450
Lemma tac_always_intro Δ Q : env_spatial_is_nil Δ = true  (Δ  Q)  Δ   Q.
451
Proof. intros. by apply (always_intro _ _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
453

Lemma tac_persistent Δ Δ' i p P P' Q :
454
  envs_lookup i Δ = Some (p, P)  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
455
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
456
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
Proof.
458
  intros ??? <-. rewrite envs_replace_sound //; simpl.
459
  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
460
461
462
463
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
464
  env_spatial_is_nil Δ = true 
Robbert Krebbers's avatar
Robbert Krebbers committed
465
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
466
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
469
470
471
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 :
472
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
473
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
474
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
476
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
477
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
Qed.
479
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
Ralf Jung's avatar
Ralf Jung committed
480
  (φ  Δ  ⌜ψ⌝)  Δ  ⌜φ  ψ⌝.
481
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
482
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
Proof.
484
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
487
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
488
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
Proof.
490
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
491
492
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
493
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
494
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
495
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
496
497
498
499
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
500
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
501
Proof.
502
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
504
505
506
507
508
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, Δ') 
509
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
510
  IntoWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
511
512
513
514
515
  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 Δ'' 
516
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
517
518
519
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
520
    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
521
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
524
    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
526
Qed.

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

545
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
546
  envs_lookup j Δ = Some (q, R) 
547
  IntoWand R P1 P2  FromPure P1 φ 
548
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
549
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Proof.
551
  intros. rewrite envs_simple_replace_sound //; simpl.
552
  rewrite right_id (into_wand R) -(from_pure P1) pure_True //.
553
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
Qed.

556
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
557
  envs_lookup_delete j Δ = Some (q, R, Δ') 
558
  IntoWand R P1 P2  PersistentP P1 
559
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
  (Δ'  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
576
Proof.
577
578
579
580
  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
581
582
583
584
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
585
  (Δ'  (if p then  P else P) - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
586
Proof.
587
588
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
  by rewrite HQ /uPred_always_if wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
589
590
Qed.

591
592
593
594
595
596
597
598
599
600
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.

601
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
602
  ElimModal P' P Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
603
  envs_split lr js Δ = Some (Δ1,Δ2) 
604
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
605
  (Δ1  P')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
606
Proof.
607
  intros ??? HP HQ. rewrite envs_split_sound //.
608
  rewrite (envs_app_sound Δ2) //; simpl.
609
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
610
611
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
612
613
614
615
616
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 Δ' 
  (Δ1  P)  PersistentP P 
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
617
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
618
619
620
  intros ?? HP ? <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
  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
621
622
Qed.

623
Lemma tac_pose_proof Δ Δ' j P Q :
624
  P 
625
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
626
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
627
Proof.
628
629
  intros HP ? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -HP always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
630
631
Qed.

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

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
655
   {A : ofeT} (x y : A) (Φ : A  uPred M),
656
657
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
658
    ( n, Proper (dist n ==> dist n) Φ) 
659
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
660
Proof.
661
  intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
662
  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
663
  destruct lr; auto using internal_eq_sym.
Robbert Krebbers's avatar
Robbert Krebbers committed
664
665
666
667
Qed.

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

(** * Conjunction splitting *)
689
690
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
691
692
693

(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
694
  FromSep P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
695
  envs_split lr js Δ = Some (Δ1,Δ2) 
696
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
Proof.
698
  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
699
700
701
702
703
704
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) 
705
  FromSep P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
706
707
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
708
  (Δ4  Q)  Δ1  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
709
710
711
712
713
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.
714
      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
716
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
717
718
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
719
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
720
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
721
      by rewrite right_id assoc (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
722
723
724
Qed.

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

734
735
736
737
738
739
740
741
742
743
744
745
746
747
(* 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
748
(** * Framing *)
749
Lemma tac_frame_pure Δ (φ : Prop) P Q :
Ralf Jung's avatar
Ralf Jung committed
750
751
  φ  Frame ⌜φ⌝ P Q  (Δ  Q)  Δ  P.
Proof. intros ?? ->. by rewrite -(frame ⌜φ⌝ P) pure_True // left_id. Qed.
752

753
754
755
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
756
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
757
  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
758
759
  - 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
760
761
762
Qed.

(** * Disjunction *)
763
764
765
766
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
767
768

Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
769
  envs_lookup i Δ = Some (p, P)  IntoOr P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
770
771
  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 
  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 
772
  (Δ1  Q)  (Δ2  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
773
Proof.
774
  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
775
  rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
776
777
778
779
  - rewrite