coq_tactics.v 51.5 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
Definition envs_entails {PROP} (Δ : envs PROP) (Q : PROP) : Prop :=
29
  of_envs Δ  Q.
30
Arguments envs_entails {_} _ _%I : simpl never.
31
32
33
Typeclasses Opaque envs_entails.
Instance: Params (@envs_entails) 1.

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

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

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

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

56
Definition envs_lookup_delete {PROP} (i : ident)
Robbert Krebbers's avatar
Robbert Krebbers committed
57
    (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
  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
61
  | None => ''(P,Γs')  env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
  end.

64
Fixpoint envs_lookup_delete_list {PROP} (js : list ident) (remove_persistent : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
65
    (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
66
67
68
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
Robbert Krebbers's avatar
Robbert Krebbers committed
69
70
71
     ''(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 Δ';
72
73
74
     Some (p && q, P :: Hs, Δ'')
  end.

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

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

96
Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
97
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
100
  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
101
Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
  if env_spatial Δ is Enil then true else false.

Robbert Krebbers's avatar
Robbert Krebbers committed
104
Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
105
106
  Envs (env_persistent Δ) Enil.

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

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

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

Lemma of_envs_eq Δ :
134
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
135
136
Proof. done. Qed.

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

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

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

186
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
187
188
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
189
190
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
191
  { by rewrite affinely_persistently_emp left_id. }
192
193
194
  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/=.
195
  rewrite -affinely_persistently_if_sep_2 -assoc. destruct q1; simpl.
196
  - destruct rp.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    + rewrite envs_lookup_sound //; simpl.
198
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
199
    + rewrite envs_lookup_persistent_sound //.
200
201
      by rewrite IH // (affinely_persistently_affinely_persistently_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite affinely_persistently_if_elim.
202
203
Qed.

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

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

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

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

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

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

295
296
297
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 Δ' 
298
  of_envs Δ  ?p P  (?p Q - of_envs Δ').
299
300
301
302
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

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

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

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

322
323
324
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 Δ' 
325
  of_envs Δ  ?p P  (?q Q - of_envs Δ').
326
327
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
337
Lemma envs_clear_spatial_sound Δ :
338
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
339
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
  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.
343
344
Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
405
Global Instance envs_Forall2_refl (R : relation PROP) :
406
407
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
Global Instance envs_Forall2_sym (R : relation PROP) :
409
410
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
Global Instance envs_Forall2_trans (R : relation PROP) :
412
413
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
415
416
  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
417
Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
418
419
420
  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
421
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
422
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
424
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
425
426
427
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
428
429
Global Instance of_envs_proper :
  Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
430
Proof.
431
432
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
433
Qed.
434
Global Instance Envs_proper (R : relation PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
435
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
436
437
Proof. by constructor. Qed.

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

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

(** * Basic rules *)
453
454
455
456
457
Lemma tac_eval Δ Q Q' :
  Q = Q' 
  envs_entails Δ Q'  envs_entails Δ Q.
Proof. by intros ->. Qed.

458
459
460
461
462
463
464
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.

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

469
Instance affine_env_spatial Δ :
470
471
472
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

473
474
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  of_envs Δ  emp.
Proof. intros. by rewrite (affine (of_envs Δ)). Qed.
475

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

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

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

(** * False *)
510
511
Lemma tac_ex_falso Δ Q : envs_entails Δ False  envs_entails Δ Q.
Proof. by rewrite /envs_entails -(False_elim Q). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
512

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

Robbert Krebbers's avatar
Robbert Krebbers committed
522
(** * Pure *)
523
524
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ  φ  envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
525

Robbert Krebbers's avatar
Robbert Krebbers committed
526
Lemma tac_pure Δ Δ' i p P φ Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
527
528
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  IntoPure P φ 
529
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
530
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
Proof.
532
533
  rewrite /envs_entails=> ?? HPQ HQ.
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
534
  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
    by apply pure_elim_l.
536
  - destruct HPQ.
537
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
538
      by apply pure_elim_l.
539
540
    + 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
541
542
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
546
547
548
549
550
551
552
553
(** * 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;
554
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
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.
580

Robbert Krebbers's avatar
Robbert Krebbers committed
581
582
583
584
585
586
587
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;
588
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
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.
611

Robbert Krebbers's avatar
Robbert Krebbers committed
612
613
614
615
616
617
618
619
620
621
622
623
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
652
653
654
655
656
657
658
659
660
661
662
663
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.
  rewrite /envs_entails /FromAlways /of_envs /= => <- HΓp HΓs <-.
  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).
664
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
665
666

Lemma tac_persistent Δ Δ' i p P P' Q :
667
  envs_lookup i Δ = Some (p, P) 
668
  IntoPersistent p P P' 
669
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
670
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
671
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
672
Proof.
673
  rewrite /envs_entails=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
674
675
676
  destruct p; simpl.
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
677
    + rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
678
679
              (into_persistent _ P) wand_elim_r //.
    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
680
681
      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
                 absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
682
683
684
Qed.

(** * Implication and wand *)
685
Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
686
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q  of_envs Δ'.
687
688
Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.

689
690
Lemma tac_impl_intro Δ Δ' i P P' Q R :
  FromImpl R P Q 
691
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
692
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
693
  FromAffinely P' P 
694
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
695
Proof.
696
  rewrite /FromImpl /envs_entails => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
697
  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
698
    rewrite envs_app_singleton_sound //; simpl.
699
700
    rewrite -(from_affinely P') -affinely_and_lr.
    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
701
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
702
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
703
Qed.
704
705
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
  FromImpl R P Q 
706
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
707
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
708
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
709
Proof.
710
  rewrite /FromImpl /envs_entails => <- ?? <-.
711
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
712
  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
713
  by rewrite persistently_and_affinely_sep_l wand_elim_r.
714
Qed.
715
716
717
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q  envs_entails Δ Q  envs_entails Δ R.
Proof. rewrite /FromImpl /envs_entails=> <- ?. apply impl_intro_l. by rewrite and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
718

719
720
Lemma tac_wand_intro Δ Δ' i P Q R :
  FromWand R P Q 
721
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
722
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
723
Proof.
724
  rewrite /FromWand /envs_entails=> <- ? HQ.
725
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
726
Qed.
727
728
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q R :
  FromWand R P Q 
729
  IntoPersistent false P P' 
730
  TCOr (Affine P) (Absorbing Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
731
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
732
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
733
Proof.
Jacques-Henri Jourdan's avatar