coq_tactics.v 51 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
3
From iris.proofmode Require Export base environments classes.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import bi.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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

Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
Record envs (PROP : bi) :=
  Envs { env_persistent : env PROP; env_spatial : env PROP }.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15
16
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

Robbert Krebbers's avatar
Robbert Krebbers committed
17
Record envs_wf {PROP} (Δ : envs PROP) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20
21
22
  env_persistent_valid : env_wf (env_persistent Δ);
  env_spatial_valid : env_wf (env_spatial Δ);
  envs_disjoint i : env_persistent Δ !! i = None  env_spatial Δ !! i = None
}.

23
Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
24
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
25
Instance: Params (@of_envs) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Arguments of_envs : simpl never.
27

28
29
30
31
32
33
34
(* We seal [envs_entails], so that it does not get unfolded by the
   proofmode's own tactics, such as [iIntros (?)]. *)
Definition envs_entails_aux : seal (λ PROP (Δ : envs PROP) (Q : PROP), (of_envs Δ  Q)).
Proof. by eexists. Qed.
Definition envs_entails := unseal envs_entails_aux.
Definition envs_entails_eq : envs_entails = _ := seal_eq envs_entails_aux.
Arguments envs_entails {PROP} Δ Q%I : rename.
35
36
Instance: Params (@envs_entails) 1.

Robbert Krebbers's avatar
Robbert Krebbers committed
37
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
38
39
40
  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
41

42
Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
43
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
44

45
Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
  let (Γp,Γs) := Δ in
  match env_lookup i Γp with
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
  | Some P => Some (true, P)
  | None => P  env_lookup i Γs; Some (false, P)
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
  end.

52
Definition envs_delete {PROP} (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
  let (Γp,Γs) := Δ in
  match p with
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
  | true => Envs (env_delete i Γp) Γs
  | false => Envs Γp (env_delete i Γs)
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
  end.

59
Definition envs_lookup_delete {PROP} (i : ident)
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
61
62
63
  let (Γp,Γs) := Δ in
  match env_lookup_delete i Γp with
  | Some (P,Γp') => Some (true, P, Envs Γp' Γs)
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  | None => ''(P,Γs')  env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
  end.

67
Fixpoint envs_lookup_delete_list {PROP} (js : list ident) (remove_persistent : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
68
    (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
69
70
71
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
     ''(p,P,Δ')  envs_lookup_delete j Δ;
     let Δ' := if p : bool then (if remove_persistent then Δ' else Δ) else Δ' in
     ''(q,Hs,Δ'')  envs_lookup_delete_list js remove_persistent Δ';
75
76
77
     Some (p && q, P :: Hs, Δ'')
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
78
Definition envs_snoc {PROP} (Δ : envs PROP)
79
    (p : bool) (j : ident) (P : PROP) : envs PROP :=
80
81
82
  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
83
84
Definition envs_app {PROP : bi} (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
87
88
89
90
  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.

91
Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
92
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
  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.

99
Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
100
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
103
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

Robbert Krebbers's avatar
Robbert Krebbers committed
104
Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
  if env_spatial Δ is Enil then true else false.

Robbert Krebbers's avatar
Robbert Krebbers committed
107
Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
108
109
  Envs (env_persistent Δ) Enil.

Robbert Krebbers's avatar
Robbert Krebbers committed
110
Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
111
112
  Envs Enil (env_spatial Δ).

Robbert Krebbers's avatar
Robbert Krebbers committed
113
Fixpoint envs_split_go {PROP}
114
    (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
115
116
117
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
     ''(p,P,Δ1')  envs_lookup_delete j Δ1;
     if p : bool then envs_split_go js Δ1 Δ2 else
120
121
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
122
123
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
124
Definition envs_split {PROP} (d : direction)
125
    (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
126
  ''(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
127
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
128

Robbert Krebbers's avatar
Robbert Krebbers committed
129
(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
132
133
134
135
136
Section bi_tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Lemma of_envs_eq Δ :
137
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
138
139
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
142
143
144
145
146
147
148
149
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 :
150
151
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  ?p P  of_envs (envs_delete i p Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
  - rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
157
158
    rewrite (env_lookup_perm Γp) //= affinely_persistently_and.
    by rewrite and_sep_affinely_persistently -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
162
163
    rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Lemma envs_lookup_persistent_sound Δ i P :
165
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Proof.
167
  intros. rewrite -persistently_and_affinely_sep_l. apply and_intro; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  rewrite envs_lookup_sound //; simpl.
169
  by rewrite -persistently_and_affinely_sep_l and_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
Qed.

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

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

189
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
190
191
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
192
193
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
194
  { by rewrite affinely_persistently_emp left_id. }
195
196
197
  destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
  apply envs_lookup_delete_Some in Hj as [Hj ->].
  destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
198
  rewrite -affinely_persistently_if_sep_2 -assoc. destruct q1; simpl.
199
  - destruct rp.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
    + rewrite envs_lookup_sound //; simpl.
201
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
202
    + rewrite envs_lookup_persistent_sound //.
203
204
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite affinely_persistently_if_elim.
205
206
Qed.

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

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

260
Lemma envs_app_singleton_sound Δ Δ' p j Q :
261
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q - of_envs Δ'.
262
263
Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
264
265
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
266
  of_envs (envs_delete i p Δ)  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
268
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
271
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
273
274
275
276
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γp') //.
277
      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
278
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
280
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
284
    + 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.
285
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
Qed.

288
289
Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
290
  of_envs (envs_delete i p Δ)  ?p Q - of_envs Δ'.
291
292
Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
293
294
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
295
  of_envs Δ  ?p P  ((if p then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
296
297
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

298
299
300
Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
301
  of_envs Δ  ?p P  (?p Q - of_envs Δ').
302
303
304
305
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
306
Lemma envs_replace_sound' Δ Δ' i p q Γ :
307
  envs_replace i p q Γ Δ = Some Δ' 
308
  of_envs (envs_delete i p Δ)  (if q then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
310
311
312
313
314
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

315
316
Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
317
  of_envs (envs_delete i p Δ)  ?q Q - of_envs Δ'.
318
319
Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
322
  of_envs Δ  ?p P  ((if q then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
323
324
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

325
326
327
Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
328
  of_envs Δ  ?p P  (?q Q - of_envs Δ').
329
330
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.

331
332
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
Robbert Krebbers's avatar
Robbert Krebbers committed
333
  = ''(p,P)  envs_lookup j Δ; if p : bool then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Proof.
335
336
337
  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
338
339
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
340
Lemma envs_clear_spatial_sound Δ :
341
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
342
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
344
345
  rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
346
347
Qed.

348
Lemma env_spatial_is_nil_affinely_persistently Δ :
349
  env_spatial_is_nil Δ = true  of_envs Δ   of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
351
Proof.
  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
352
353
  rewrite !right_id {1}affinely_and_r persistently_and.
  by rewrite persistently_affinely persistently_idemp persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
354
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
355

356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
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) 
Robbert Krebbers's avatar
Robbert Krebbers committed
376
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
377
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
378
379
380
Proof.
  revert Δ1 Δ2 Δ1' Δ2'.
  induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
381
382
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite /of_envs !and_elim_l sep_elim_l. }
383
384
385
386
387
388
389
390
391
392
  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.
393
Lemma envs_split_sound Δ d js Δ1 Δ2 :
394
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
395
Proof.
396
  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
397
  rewrite {2}envs_clear_spatial_sound.
398
399
  rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
  rewrite -persistently_and_affinely_sep_l.
400
  rewrite (and_elim_l (bi_persistently _)%I)
401
          persistently_and_affinely_sep_r affinely_persistently_elim.
402
403
404
  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=> ->. }
405
  destruct d; simplify_eq/=; solve_sep_entails.
406
407
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
408
Global Instance envs_Forall2_refl (R : relation PROP) :
409
410
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
Global Instance envs_Forall2_sym (R : relation PROP) :
412
413
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
Global Instance envs_Forall2_trans (R : relation PROP) :
415
416
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
417
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
418
419
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
421
422
423
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
424
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
425
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
427
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
428
429
430
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
431
432
Global Instance of_envs_proper :
  Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
433
Proof.
434
435
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
436
Qed.
437
Global Instance Envs_proper (R : relation PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
438
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
439
440
Proof. by constructor. Qed.

441
Global Instance envs_entails_proper :
442
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails PROP).
443
Proof. rewrite envs_entails_eq. solve_proper. Qed.
444
Global Instance envs_entails_flip_mono :
445
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
446
Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
447

Robbert Krebbers's avatar
Robbert Krebbers committed
448
(** * Adequacy *)
449
Lemma tac_adequate P : envs_entails (Envs Enil Enil) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
450
Proof.
451
452
  rewrite envs_entails_eq /of_envs /= persistently_True_emp
          affinely_persistently_emp left_id=><-.
Robbert Krebbers's avatar
Robbert Krebbers committed
453
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
455
456
Qed.

(** * Basic rules *)
457
458
459
460
461
Lemma tac_eval Δ Q Q' :
  Q = Q' 
  envs_entails Δ Q'  envs_entails Δ Q.
Proof. by intros ->. Qed.

462
463
464
465
466
467
468
Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed.
Global Instance affine_env_snoc Γ i P :
  Affine P  AffineEnv Γ  AffineEnv (Esnoc Γ i P).
Proof. by constructor. Qed.

469
(* If the BI is affine, no need to walk on the whole environment. *)
470
Global Instance affine_env_bi `(BiAffine PROP) Γ : AffineEnv Γ | 0.
471
472
Proof. induction Γ; apply _. Qed.

473
Instance affine_env_spatial Δ :
474
475
476
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

477
478
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
479

Robbert Krebbers's avatar
Robbert Krebbers committed
480
481
482
Lemma tac_assumption Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  FromAssumption p P Q 
483
484
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
485
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
486
Proof.
487
  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
  destruct (env_spatial_is_nil Δ') eqn:?.
489
  - by rewrite (env_spatial_is_nil_affinely_persistently Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
490
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
491
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
493
494
495

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
496
497
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
Proof.
499
  rewrite envs_entails_eq=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
500
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
501
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
502

Robbert Krebbers's avatar
Robbert Krebbers committed
503
Lemma tac_clear Δ Δ' i p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
504
505
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
506
  envs_entails Δ' Q 
507
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
508
Proof.
509
  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
510
  by destruct p; rewrite /= HQ sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
511
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
513

(** * False *)
514
Lemma tac_ex_falso Δ Q : envs_entails Δ False  envs_entails Δ Q.
515
Proof. by rewrite envs_entails_eq -(False_elim Q). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
516

Robbert Krebbers's avatar
Robbert Krebbers committed
517
518
519
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
520
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
521
Proof.
522
  rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
523
  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
526
(** * Pure *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
527
528
(* This relies on the invariant that [FromPure false] implies
   [FromPure true] *)
529
530
531
532
533
534
535
536
Lemma tac_pure_intro Δ Q φ af :
  env_spatial_is_nil Δ = af  FromPure af Q φ  φ  envs_entails Δ Q.
Proof.
  intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af.
  - rewrite env_spatial_is_nil_affinely_persistently //=. f_equiv.
    by apply pure_intro.
  - by apply pure_intro.
Qed.
537

Robbert Krebbers's avatar
Robbert Krebbers committed
538
Lemma tac_pure Δ Δ' i p P φ Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
539
540
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  IntoPure P φ 
541
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
542
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
543
Proof.
544
  rewrite envs_entails_eq=> ?? HPQ HQ.
545
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
546
  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
547
    by apply pure_elim_l.
548
  - destruct HPQ.
549
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
550
      by apply pure_elim_l.
551
552
    + rewrite (into_pure P) (persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
554
Qed.

555
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝  Q)  (φ  envs_entails Δ Q).
556
Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
557

Robbert Krebbers's avatar
Robbert Krebbers committed
558
559
560
561
562
563
564
565
(** * Always modalities *)
Class FilterPersistentEnv
    (M : always_modality PROP) (C : PROP  Prop) (Γ1 Γ2 : env PROP) := {
  filter_persistent_env :
    ( P, C P   P  M ( P)) 
     ([] Γ1)  M ( ([] Γ2));
  filter_persistent_env_wf : env_wf Γ1  env_wf Γ2;
  filter_persistent_env_dom i : Γ1 !! i = None  Γ2 !! i = None;
566
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
Global Instance filter_persistent_env_nil M C : FilterPersistentEnv M C Enil Enil.
Proof.
  split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
  by rewrite affinely_emp -always_modality_emp.
Qed.
Global Instance filter_persistent_env_snoc M (C : PROP  Prop) Γ Γ' i P :
  C P 
  FilterPersistentEnv M C Γ Γ' 
  FilterPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
Proof.
  intros ? [HΓ Hwf Hdom]; split; simpl.
  - intros HC. rewrite affinely_persistently_and HC // HΓ //.
    by rewrite always_modality_and -affinely_persistently_and.
  - inversion 1; constructor; auto.
  - intros j. destruct (ident_beq _ _); naive_solver.
Qed.
Global Instance filter_persistent_env_snoc_not M (C : PROP  Prop) Γ Γ' i P :
  FilterPersistentEnv M C Γ Γ' 
  FilterPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
Proof.
  intros [HΓ Hwf Hdom]; split; simpl.
  - intros HC. by rewrite and_elim_r HΓ.
  - inversion 1; auto.
  - intros j. destruct (ident_beq _ _); naive_solver.
Qed.
592

Robbert Krebbers's avatar
Robbert Krebbers committed
593
594
595
596
597
598
599
Class FilterSpatialEnv
    (M : always_modality PROP) (C : PROP  Prop) (Γ1 Γ2 : env PROP) := {
  filter_spatial_env :
    ( P, C P  P  M P)  ( P, Absorbing (M P)) 
    ([] Γ1)  M ([] Γ2);
  filter_spatial_env_wf : env_wf Γ1  env_wf Γ2;
  filter_spatial_env_dom i : Γ1 !! i = None  Γ2 !! i = None;
600
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
Global Instance filter_spatial_env_nil M C : FilterSpatialEnv M C Enil Enil.
Proof. split=> // HC /=. by rewrite -always_modality_emp. Qed.
Global Instance filter_spatial_env_snoc M (C : PROP  Prop) Γ Γ' i P :
  C P 
  FilterSpatialEnv M C Γ Γ' 
  FilterSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
Proof.
  intros ? [HΓ Hwf Hdom]; split; simpl.
  - intros HC ?. by rewrite {1}(HC P) // HΓ // always_modality_sep.
  - inversion 1; constructor; auto.
  - intros j. destruct (ident_beq _ _); naive_solver.
Qed.

Global Instance filter_spatial_env_snoc_not M (C : PROP  Prop) Γ Γ' i P :
  FilterSpatialEnv M C Γ Γ' 
  FilterSpatialEnv M C (Esnoc Γ i P) Γ' | 100.
Proof.
  intros [HΓ Hwf Hdom]; split; simpl.
  - intros HC ?. by rewrite HΓ // sep_elim_r.
  - inversion 1; auto.
  - intros j. destruct (ident_beq _ _); naive_solver.
Qed.
623

Robbert Krebbers's avatar
Robbert Krebbers committed
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
Ltac tac_always_cases :=
  simplify_eq/=;
  repeat match goal with
  | H : TCAnd _ _ |- _ => destruct H
  | H : TCEq ?x _ |- _ => inversion H; subst x; clear H
  | H : TCForall _ _ |- _ => apply TCForall_Forall in H
  | H : FilterPersistentEnv _ _ _ _ |- _ => destruct H
  | H : FilterSpatialEnv _ _ _ _ |- _ => destruct H
  end; simpl; auto using Enil_wf.

Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
  FromAlways M Q' Q 
  match always_modality_persistent_spec M with
  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
  | AIEnvFilter C => FilterPersistentEnv M C Γp Γp'
  | AIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
  | AIEnvClear => TCEq Γp' Enil
  | AIEnvId => TCEq Γp Γp'
  end 
  match always_modality_spatial_spec M with
  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
  | AIEnvFilter C => FilterSpatialEnv M C Γs Γs'
  | AIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
  | AIEnvClear => TCEq Γs' Enil
  | AIEnvId => TCEq Γs Γs'
  end 
  envs_entails (Envs Γp' Γs') Q  envs_entails (Envs Γp Γs) Q'.
Proof.
652
  rewrite envs_entails_eq /FromAlways /of_envs /= => <- HΓp HΓs <-.
Robbert Krebbers's avatar
Robbert Krebbers committed
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')).
  { split; simpl in *.
    - destruct (always_modality_persistent_spec M); tac_always_cases.
    - destruct (always_modality_spatial_spec M); tac_always_cases.
    - destruct (always_modality_persistent_spec M),
        (always_modality_spatial_spec M); tac_always_cases; naive_solver. }
  rewrite pure_True // left_id. rewrite -always_modality_sep. apply sep_mono.
  - destruct (always_modality_persistent_spec M) eqn:?; tac_always_cases.
    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
        persistently_True_emp affinely_persistently_emp.
    + eauto using always_modality_persistent_forall_big_and.
    + eauto using always_modality_persistent_filter.
    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
        persistently_True_emp affinely_persistently_emp.
    + eauto using always_modality_persistent_id.
  - destruct (always_modality_spatial_spec M) eqn:?; tac_always_cases.
    + by rewrite -always_modality_emp.
    + eauto using always_modality_spatial_forall_big_sep.
    + eauto using always_modality_spatial_filter,
        always_modality_spatial_filter_absorbing.
    + rewrite -(always_modality_spatial_clear M) // -always_modality_emp.
      by rewrite -absorbingly_True_emp absorbingly_pure -True_intro.
    + by destruct (always_modality_spatial_id M).
676
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
677
678

Lemma tac_persistent Δ Δ' i p P P' Q :
679
  envs_lookup i Δ = Some (p, P) 
680
  IntoPersistent p P P' 
681
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
682
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
683
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
684
Proof.
685
  rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
686
687
688
  destruct p; simpl.
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
689
    + rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
690
691
              (into_persistent _ P) wand_elim_r //.
    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
692
693
      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
                 absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
694
695
696
Qed.

(** * Implication and wand *)
697
Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
698
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q  of_envs Δ'.
699
700
Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.

701
702
Lemma tac_impl_intro Δ Δ' i P P' Q R :
  FromImpl R P Q 
703
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
704
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
705
  FromAffinely P' P 
706
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
707
Proof.
708
  rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
709
  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
710
    rewrite envs_app_singleton_sound //; simpl.
711
712
    rewrite -(from_affinely P') -affinely_and_lr.
    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
713
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
714
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
Qed.
716
717
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
  FromImpl R P Q 
718
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
719
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
720
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
721
Proof.
722
  rewrite /FromImpl envs_entails_eq => <- ?? <-.
723
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
724
  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
725
  by rewrite persistently_and_affinely_sep_l wand_elim_r.
726
Qed.
727
728
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q  envs_entails Δ Q  envs_entails Δ R.
729
730
731
Proof.
  rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
732

733
734
Lemma tac_wand_intro Δ Δ' i P Q R :
  FromWand R P Q 
735
  envs_app false (Esnoc Enil i P) Δ = Some Δ'