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

Inductive env (A : Type) : Type :=
  | Enil : env A
10
  | Esnoc : env A  ident  A  env A.
Robbert Krebbers's avatar
Robbert Krebbers committed
11
Arguments Enil {_}.
12
Arguments Esnoc {_} _ _ _.
13
14
Instance: Params (@Enil) 1 := {}.
Instance: Params (@Esnoc) 1 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

16
Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
  match Γ with
  | Enil => None
19
  | Esnoc Γ j x => if ident_beq i j then Some x else env_lookup i Γ
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  end.
21
22

Module env_notations.
23
  Notation "y ≫= f" := (pm_option_bind f y).
24
  Notation "x ← y ; z" := (y = λ x, z).
25
  Notation "' x1 ← y ; z" := (y = (λ x1, z)).
26
27
28
  Notation "Γ !! j" := (env_lookup j Γ).
End env_notations.
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

30
31
Local Open Scope lazy_bool_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
32
33
34
35
36
37
38
Inductive env_wf {A} : env A  Prop :=
  | Enil_wf : env_wf Enil
  | Esnoc_wf Γ i x : Γ !! i = None  env_wf Γ  env_wf (Esnoc Γ i x).

Fixpoint env_to_list {A} (E : env A) : list A :=
  match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end.
Coercion env_to_list : env >-> list.
39
Instance: Params (@env_to_list) 1 := {}.
40

41
Fixpoint env_dom {A} (Γ : env A) : list ident :=
42
  match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
43

Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47
Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
  match Γapp with
  | Enil => Some Γ
  | Esnoc Γapp i x =>
48
     Γ'  env_app Γapp Γ;
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
     match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
  end.
51

52
Fixpoint env_replace {A} (i: ident) (Γi: env A) (Γ: env A) : option (env A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
55
  match Γ with
  | Enil => None
  | Esnoc Γ j x =>
56
     if ident_beq i j then env_app Γi Γ else
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
61
     match Γi !! j with
     | None => Γ'  env_replace i Γi Γ; Some (Esnoc Γ' j x)
     | Some _ => None
     end
  end.
62

63
Fixpoint env_delete {A} (i : ident) (Γ : env A) : env A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
  match Γ with
  | Enil => Enil
66
  | Esnoc Γ j x => if ident_beq i j then Γ else Esnoc (env_delete i Γ) j x
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  end.
68

69
Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
  match Γ with
  | Enil => None
  | Esnoc Γ j x =>
73
     if ident_beq i j then Some (x,Γ)
74
     else '(y,Γ')  env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
76

Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
79
80
81
Inductive env_Forall2 {A B} (P : A  B  Prop) : env A  env B  Prop :=
  | env_Forall2_nil : env_Forall2 P Enil Enil
  | env_Forall2_snoc Γ1 Γ2 i x y :
     env_Forall2 P Γ1 Γ2  P x y  env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y).

82
83
84
85
86
87
88
Inductive env_subenv {A} : relation (env A) :=
  | env_subenv_nil : env_subenv Enil Enil
  | env_subenv_snoc Γ1 Γ2 i x :
     env_subenv Γ1 Γ2  env_subenv (Esnoc Γ1 i x) (Esnoc Γ2 i x)
  | env_subenv_skip Γ1 Γ2 i y :
     env_subenv Γ1 Γ2  env_subenv Γ1 (Esnoc Γ2 i y).

Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
91
Section env.
Context {A : Type}.
Implicit Types Γ : env A.
92
Implicit Types i : ident.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Implicit Types x : A.
Tej Chajed's avatar
Tej Chajed committed
94
Hint Resolve Esnoc_wf Enil_wf : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
95

96
97
98
Ltac simplify :=
  repeat match goal with
  | _ => progress simplify_eq/=
99
100
  | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
  | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
101
102
  | H : context [pm_option_bind _ ?x] |- _ => destruct x eqn:?
  | |- context [pm_option_bind _ ?x] => destruct x eqn:?
103
104
  | _ => case_match
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
108
109
110

Lemma env_lookup_perm Γ i x : Γ !! i = Some x  Γ  x :: env_delete i Γ.
Proof.
  induction Γ; intros; simplify; rewrite 1?Permutation_swap; f_equiv; eauto.
Qed.

111
112
113
114
115
116
Lemma env_lookup_snoc Γ i P : env_lookup i (Esnoc Γ i P) = Some P.
Proof. induction Γ; simplify; auto. Qed.
Lemma env_lookup_snoc_ne Γ i j P :
  i  j  env_lookup i (Esnoc Γ j P) = env_lookup i Γ.
Proof. induction Γ=> ?; simplify; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
Lemma env_app_perm Γ Γapp Γ' :
  env_app Γapp Γ = Some Γ'  env_to_list Γ'  Γapp ++ Γ.
Proof. revert Γ'; induction Γapp; intros; simplify; f_equal; auto. Qed.
Lemma env_app_fresh Γ Γapp Γ' i :
  env_app Γapp Γ = Some Γ'  Γapp !! i = None  Γ !! i = None  Γ' !! i = None.
Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
Lemma env_app_fresh_1 Γ Γapp Γ' i x :
  env_app Γapp Γ = Some Γ'  Γ' !! i = None  Γ !! i = None.
Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.
Lemma env_app_disjoint Γ Γapp Γ' i :
  env_app Γapp Γ = Some Γ'  Γapp !! i = None  Γ !! i = None.
Proof.
  revert Γ'.
  induction Γapp; intros; simplify; naive_solver eauto using env_app_fresh_1.
Qed.
Lemma env_app_wf Γ Γapp Γ' : env_app Γapp Γ = Some Γ'  env_wf Γ  env_wf Γ'.
Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed.

Lemma env_replace_fresh Γ Γj Γ' i j :
  env_replace j Γj Γ = Some Γ' 
  Γj !! i = None  env_delete j Γ !! i = None  Γ' !! i = None.
Proof. revert Γ'. induction Γ; intros; simplify; eauto using env_app_fresh. Qed.
Lemma env_replace_wf Γ Γi Γ' i :
  env_replace i Γi Γ = Some Γ'  env_wf (env_delete i Γ)  env_wf Γ'.
Proof.
  revert Γ'. induction Γ; intros ??; simplify; [|inversion_clear 1];
    eauto using env_app_wf, env_replace_fresh.
Qed.
Lemma env_replace_lookup Γ Γi Γ' i :
  env_replace i Γi Γ = Some Γ'  is_Some (Γ !! i).
Proof. revert Γ'. induction Γ; intros; simplify; eauto. Qed.
Lemma env_replace_perm Γ Γi Γ' i :
  env_replace i Γi Γ = Some Γ'  Γ'  Γi ++ env_delete i Γ.
Proof.
151
152
  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify; auto using env_app_perm.
  rewrite -Permutation_middle -IH //.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
Qed.

Lemma env_lookup_delete_correct Γ i :
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  env_lookup_delete i Γ = (x  Γ !! i; Some (x,env_delete i Γ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
159
160
Proof. induction Γ; intros; simplify; eauto. Qed.
Lemma env_lookup_delete_Some Γ Γ' i x :
  env_lookup_delete i Γ = Some (x,Γ')  Γ !! i = Some x  Γ' = env_delete i Γ.
Proof. rewrite env_lookup_delete_correct; simplify; naive_solver. Qed.
161
162

Lemma env_lookup_env_delete Γ j : env_wf Γ  env_delete j Γ !! j = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Proof. induction 1; intros; simplify; eauto. Qed.
164
165
Lemma env_lookup_env_delete_ne Γ i j : i  j  env_delete j Γ !! i = Γ !! i.
Proof. induction Γ; intros; simplify; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
Lemma env_delete_fresh Γ i j : Γ !! i = None  env_delete j Γ !! i = None.
Proof. induction Γ; intros; simplify; eauto. Qed.
168

Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
Lemma env_delete_wf Γ j : env_wf Γ  env_wf (env_delete j Γ).
Proof. induction 1; simplify; eauto using env_delete_fresh. Qed.

172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
Global Instance env_Forall2_refl (P : relation A) :
  Reflexive P  Reflexive (env_Forall2 P).
Proof. intros ? Γ. induction Γ; constructor; auto. Qed.
Global Instance env_Forall2_sym (P : relation A) :
  Symmetric P  Symmetric (env_Forall2 P).
Proof. induction 2; constructor; auto. Qed.
Global Instance env_Forall2_trans (P : relation A) :
  Transitive P  Transitive (env_Forall2 P).
Proof.
  intros ? Γ1 Γ2 Γ3 HΓ; revert Γ3.
  induction HΓ; inversion_clear 1; constructor; eauto.
Qed.
Global Instance env_Forall2_antisymm (P Q : relation A) :
  AntiSymm P Q  AntiSymm (env_Forall2 P) (env_Forall2 Q).
Proof. induction 2; inversion_clear 1; constructor; auto. Qed.
Lemma env_Forall2_impl {B} (P Q : A  B  Prop) Γ Σ :
  env_Forall2 P Γ Σ  ( x y, P x y  Q x y)  env_Forall2 Q Γ Σ.
Proof. induction 1; constructor; eauto. Qed.

Global Instance Esnoc_proper (P : relation A) :
  Proper (env_Forall2 P ==> (=) ==> P ==> env_Forall2 P) Esnoc.
Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed.
Global Instance env_to_list_proper (P : relation A) :
  Proper (env_Forall2 P ==> Forall2 P) env_to_list.
Proof. induction 1; constructor; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
201
202
203
Lemma env_Forall2_fresh {B} (P : A  B  Prop) Γ Σ i :
  env_Forall2 P Γ Σ  Γ !! i = None  Σ !! i = None.
Proof. by induction 1; simplify. Qed.
Lemma env_Forall2_wf {B} (P : A  B  Prop) Γ Σ :
  env_Forall2 P Γ Σ  env_wf Γ  env_wf Σ.
Proof. induction 1; inversion_clear 1; eauto using env_Forall2_fresh. Qed.
204
205
206
207
208
209
210
211

Lemma env_subenv_fresh Γ Σ i : env_subenv Γ Σ  Σ !! i = None  Γ !! i = None.
Proof. by induction 1; simplify. Qed.
Lemma env_subenv_wf Γ Σ : env_subenv Γ Σ  env_wf Σ  env_wf Γ.
Proof. induction 1; inversion_clear 1; eauto using env_subenv_fresh. Qed.
Global Instance env_to_list_subenv_proper :
  Proper (env_subenv ==> sublist) (@env_to_list A).
Proof. induction 1; simpl; constructor; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
End env.
213

214
215
216
217
218
Record envs (PROP : bi) := Envs {
  env_intuitionistic : env PROP;
  env_spatial : env PROP;
  env_counter : positive (** A counter to generate fresh hypothesis names *)
}.
219
220
221
222
223
224
Add Printing Constructor envs.
Arguments Envs {_} _ _ _.
Arguments env_intuitionistic {_} _.
Arguments env_spatial {_} _.
Arguments env_counter {_} _.

225
226
227
228
229
230
231
232
233
234
235
236
(** We now define the judgment [envs_entails Δ Q] for proof mode entailments.
This judgment expresses that [Q] can be proved under the proof mode environment
[Δ]. To improve performance and to encapsulate the internals of the proof mode
(i.e. to ensure that tactics like [intro] cannot accidentally unfold the
entailment), we seal off [envs_entails].

The way the the definitions below are setup involves some trickery so we can
implement the [iFresh] tactic, which increases the counter [env_counter], in
an efficient way. Concretely, we made sure that [envs_entails (Envs Γp Γs c) Q]
and [envs_entails (Envs Γp Γs c') Q] are convertible for any [c] and [c']. This
way, [iFresh] can simply be implemented by changing the goal from
[envs_entails (Envs Γp Γs c) Q] into [envs_entails (Envs Γp Γs (Pos_succ c)) Q]
Ralf Jung's avatar
Ralf Jung committed
237
using the tactic [change_no_check]. This way, the generated proof term
238
239
240
241
242
243
244
245
246
247
contains no additional steps for changing the counter.

For all definitions below, we first define a version that take the two contexts
[env_intuitionistic] and [env_spatial] as its arguments, and then lift these
definitions that take the whole proof mode context [Δ : envs PROP]. This is
crucial to make sure that the counter [env_counter] is not part of the seal. *)
Record envs_wf' {PROP : bi} (Γp Γs : env PROP) := {
  env_intuitionistic_valid : env_wf Γp;
  env_spatial_valid : env_wf Γs;
  envs_disjoint i : Γp !! i = None  Γs !! i = None
248
}.
249
250
251
252
253
254
255
256
Definition envs_wf {PROP : bi} (Δ : envs PROP) :=
  envs_wf' (env_intuitionistic Δ) (env_spatial Δ).

Definition of_envs' {PROP : bi} (Γp Γs : env PROP) : PROP :=
  (envs_wf' Γp Γs   [] Γp  [] Γs)%I.
Instance: Params (@of_envs') 1 := {}.
Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
  of_envs' (env_intuitionistic Δ) (env_spatial Δ).
257
Instance: Params (@of_envs) 1 := {}.
258
259
Arguments of_envs : simpl never.

260
Definition envs_entails_aux :
261
  seal (λ (PROP : bi) (Γp Γs : env PROP) (Q : PROP), of_envs' Γp Γs  Q).
262
Proof. by eexists. Qed.
263
264
265
Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
  envs_entails_aux.(unseal) PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
Definition envs_entails_eq :
266
  @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ  Q).
267
Proof. by rewrite /envs_entails envs_entails_aux.(seal_eq). Qed.
268
Arguments envs_entails {PROP} Δ Q%I : rename.
269
Instance: Params (@envs_entails) 1 := {}.
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285

Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
  env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.

Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
  env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).

Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
  let (Γp,Γs,n) := Δ in
  match env_lookup i Γp with
  | Some P => Some (true, P)
  | None => P  env_lookup i Γs; Some (false, P)
  end.

286
Definition envs_delete {PROP} (remove_intuitionistic : bool)
287
288
289
    (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
  let (Γp,Γs,n) := Δ in
  match p with
290
  | true => Envs (if remove_intuitionistic then env_delete i Γp else Γp) Γs n
291
292
293
  | false => Envs Γp (env_delete i Γs) n
  end.

294
Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool)
295
296
297
    (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
  let (Γp,Γs,n) := Δ in
  match env_lookup_delete i Γp with
298
  | Some (P,Γp') => Some (true, P, Envs (if remove_intuitionistic then Γp' else Γp) Γs n)
299
  | None => '(P,Γs')  env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
300
301
  end.

302
Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
303
304
305
306
    (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
307
308
     '(p,P,Δ')  envs_lookup_delete remove_intuitionistic j Δ;
     '(q,Ps,Δ'')  envs_lookup_delete_list remove_intuitionistic js Δ';
309
     Some ((p:bool) &&& q, P :: Ps, Δ'')
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
  end.

Definition envs_snoc {PROP} (Δ : envs PROP)
    (p : bool) (j : ident) (P : PROP) : envs PROP :=
  let (Γp,Γs,n) := Δ in
  if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.

Definition envs_app {PROP : bi} (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
  let (Γp,Γs,n) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_app Γ Γp; Some (Envs Γp' Γs n)
  | false => _  env_app Γ Γp; Γs'  env_app Γ Γs; Some (Envs Γp Γs' n)
  end.

Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
  let (Γp,Γs,n) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_replace i Γ Γp; Some (Envs Γp' Γs n)
  | false => _  env_app Γ Γp; Γs'  env_replace i Γ Γs; Some (Envs Γp Γs' n)
  end.

Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
  if beq p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete true i p Δ).

Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
  if env_spatial Δ is Enil then true else false.

Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
  Envs (env_intuitionistic Δ) Enil (env_counter Δ).

344
Definition envs_clear_intuitionistic {PROP} (Δ : envs PROP) : envs PROP :=
345
346
347
  Envs Enil (env_spatial Δ) (env_counter Δ).

Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
348
  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
349
350
351
352
353
354

Fixpoint envs_split_go {PROP}
    (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
355
     '(p,P,Δ1')  envs_lookup_delete true j Δ1;
356
357
358
359
360
361
362
     if p : bool then envs_split_go js Δ1 Δ2 else
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {PROP} (d : direction)
    (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
363
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
364
365
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).

Robbert Krebbers's avatar
Robbert Krebbers committed
366
367
Fixpoint env_to_prop_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_go (P  acc)%I Γ end.
368
Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
Robbert Krebbers's avatar
Robbert Krebbers committed
369
370
371
372
373
374
  match Γ with Enil => emp%I | Esnoc Γ _ P => env_to_prop_go P Γ end.

Fixpoint env_to_prop_and_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_and_go (P  acc)%I Γ end.
Definition env_to_prop_and {PROP : bi} (Γ : env PROP) : PROP :=
  match Γ with Enil => True%I | Esnoc Γ _ P => env_to_prop_and_go P Γ end.
375
376
377

Section envs.
Context {PROP : bi}.
378
Implicit Types Γ Γp Γs : env PROP.
379
380
381
382
383
384
385
386
387
388
389
390
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Lemma of_envs_eq Δ :
  of_envs Δ = (envs_wf Δ⌝   [] env_intuitionistic Δ  [] env_spatial Δ)%I.
Proof. done. Qed.
(** An environment is a ∗ of something intuitionistic and the spatial environment.
TODO: Can we define it as such? *)
Lemma of_envs_eq' Δ :
  of_envs Δ  (envs_wf Δ⌝   [] env_intuitionistic Δ)  [] env_spatial Δ.
Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed.

391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
Global Instance envs_Forall2_refl (R : relation PROP) :
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Global Instance envs_Forall2_sym (R : relation PROP) :
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Global Instance envs_Forall2_trans (R : relation PROP) :
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
  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 PROP) Δ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.

407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
Global Instance env_intuitionistic_mono :
  Proper (envs_Forall2 () ==> env_Forall2 ()) (@env_intuitionistic PROP).
Proof. solve_proper. Qed.
Global Instance env_intuitionistic_flip_mono :
  Proper (flip (envs_Forall2 ()) ==> flip (env_Forall2 ())) (@env_intuitionistic PROP).
Proof. solve_proper. Qed.
Global Instance env_intuitionistic_proper :
  Proper (envs_Forall2 () ==> env_Forall2 ()) (@env_intuitionistic PROP).
Proof. solve_proper. Qed.

Global Instance env_spatial_mono :
  Proper (envs_Forall2 () ==> env_Forall2 ()) (@env_spatial PROP).
Proof. solve_proper. Qed.
Global Instance env_spatial_flip_mono :
  Proper (flip (envs_Forall2 ()) ==> flip (env_Forall2 ())) (@env_spatial PROP).
Proof. solve_proper. Qed.
Global Instance env_spatial_proper :
  Proper (envs_Forall2 () ==> env_Forall2 ()) (@env_spatial PROP).
Proof. solve_proper. Qed.

Global Instance of_envs_mono' :
  Proper (env_Forall2 () ==> env_Forall2 () ==> ()) (@of_envs' PROP).
429
Proof.
430
  intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply and_mono; simpl in *.
431
432
433
434
  - apply pure_mono=> -[???]. constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
435
436
Global Instance of_envs_proper' :
  Proper (env_Forall2 () ==> env_Forall2 () ==> ()) (@of_envs' PROP).
437
Proof.
438
439
  intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply (anti_symm ()); apply of_envs_mono';
    eapply (env_Forall2_impl ()); by eauto using equiv_entails.
440
Qed.
441
442
443
444
445
446

Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
Proof. solve_proper. Qed.
Global Instance of_envs_proper : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
Proof. solve_proper. Qed.

447
448
449
450
451
452
453
Global Instance Envs_proper (R : relation PROP) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP).
Proof. by constructor. Qed.

Global Instance envs_entails_proper :
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails PROP).
Proof. rewrite envs_entails_eq. solve_proper. Qed.
454
455
456
Global Instance envs_entails_mono :
  Proper (flip (envs_Forall2 ()) ==> () ==> impl) (@envs_entails PROP).
Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
457
458
459
460
Global Instance envs_entails_flip_mono :
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.

461
Lemma envs_delete_intuitionistic Δ i : envs_delete false i true Δ = Δ.
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
Proof. by destruct Δ. Qed.
Lemma envs_delete_spatial Δ i :
  envs_delete false i false Δ = envs_delete true i false Δ.
Proof. by destruct Δ. Qed.

Lemma envs_lookup_delete_Some Δ Δ' rp i p P :
  envs_lookup_delete rp i Δ = Some (p,P,Δ')
   envs_lookup i Δ = Some (p,P)  Δ' = envs_delete rp 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' Δ rp i p P :
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  ?p P  of_envs (envs_delete rp i p Δ).
Proof.
480
481
  rewrite /envs_lookup /envs_delete !of_envs_eq=>?.
  apply pure_elim_l=> Hwf.
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
    destruct rp.
    + rewrite (env_lookup_perm Γp) //= intuitionistically_and.
      by rewrite and_sep_intuitionistically -assoc.
    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
      by rewrite intuitionistically_and and_elim_l -assoc.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    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.
Lemma envs_lookup_sound Δ i p P :
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  ?p P  of_envs (envs_delete true i p Δ).
Proof. apply envs_lookup_sound'. Qed.
499
Lemma envs_lookup_intuitionistic_sound Δ i P :
500
501
502
503
504
505
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
Lemma envs_lookup_sound_2 Δ i p P :
  envs_wf Δ  envs_lookup i Δ = Some (p,P) 
  ?p P  of_envs (envs_delete true i p Δ)  of_envs Δ.
Proof.
506
507
  rewrite /envs_lookup !of_envs_eq=>Hwf ?.
  rewrite [envs_wf Δ⌝%I]pure_True // left_id.
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //= intuitionistically_and
      and_sep_intuitionistically and_elim_r.
    cancel [ P]%I. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //= and_elim_r.
    cancel [P]. solve_sep_entails.
Qed.

Lemma envs_lookup_split Δ i p P :
  envs_lookup i Δ = Some (p,P)  of_envs Δ  ?p P  (?p P - of_envs Δ).
Proof.
  intros. apply pure_elim with (envs_wf Δ).
  { rewrite of_envs_eq. apply and_elim_l. }
  intros. rewrite {1}envs_lookup_sound//.
  apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' rp i p P :
  envs_lookup_delete rp i Δ = Some (p,P,Δ')  of_envs Δ  ?p P  of_envs Δ'.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps :
  envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') 
  of_envs Δ  ?p [] Ps  of_envs Δ'.
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
  { by rewrite intuitionistically_emp left_id. }
  destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
  apply envs_lookup_delete_Some in Hj as [Hj ->].
  destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
  rewrite -intuitionistically_if_sep_2 -assoc.
  rewrite envs_lookup_sound' //; rewrite IH //.
  repeat apply sep_mono=>//; apply intuitionistically_if_flag_mono; by destruct q1.
Qed.

Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
  envs_lookup_delete rp j Δ = Some (p1, P, Δ') 
  envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') 
547
  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 &&& p2, (P :: Ps), Δ'').
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
Proof. rewrite //= => -> //= -> //=. Qed.

Lemma envs_lookup_delete_list_nil Δ rp :
  envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
Proof. done. Qed.

Lemma envs_lookup_snoc Δ i p P :
  envs_lookup i Δ = None  envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc.
Qed.
Lemma envs_lookup_snoc_ne Δ i j p P :
  i  j  envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne.
Qed.

Lemma envs_snoc_sound Δ p i P :
  envs_lookup i Δ = None  of_envs Δ  ?p P - of_envs (envs_snoc Δ p i P).
Proof.
570
  rewrite /envs_lookup /envs_snoc !of_envs_eq=> ?; apply pure_elim_l=> Hwf.
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
  - apply and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
      intros j; destruct (ident_beq_reflect j i); naive_solver.
    + by rewrite intuitionistically_and and_sep_intuitionistically assoc.
  - apply and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
      intros j; destruct (ident_beq_reflect j i); naive_solver.
    + solve_sep_entails.
Qed.

Lemma envs_app_sound Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ' 
  of_envs Δ  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Proof.
587
  rewrite !of_envs_eq /envs_app=> ?; apply pure_elim_l=> Hwf.
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + 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') //.
      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
      solve_sep_entails.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + 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_opL_app. solve_sep_entails.
Qed.

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

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
  of_envs (envs_delete true i p Δ)  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Proof.
615
  rewrite /envs_simple_replace /envs_delete !of_envs_eq=> ?.
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
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + 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') //.
      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
      solve_sep_entails.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + 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_opL_app. solve_sep_entails.
Qed.

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

Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
  of_envs Δ  ?p P  ((if p then  [] Γ else [] Γ) - of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
  of_envs Δ  ?p P  (((if p then  [] Γ else [] Γ) - of_envs Δ')  (?p P - of_envs Δ)).
Proof.
  intros. apply pure_elim with (envs_wf Δ).
  { rewrite of_envs_eq. apply and_elim_l. }
  intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro.
  - rewrite envs_simple_replace_sound'//.
  - apply wand_intro_l, envs_lookup_sound_2; done.
Qed.

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 Δ' 
  of_envs Δ  ?p P  (?p Q - of_envs Δ').
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
  envs_replace i p q Γ Δ = Some Δ' 
  of_envs (envs_delete true i p Δ)  (if q then  [] Γ else [] Γ) - of_envs Δ'.
Proof.
  rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

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

Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
  of_envs Δ  ?p P  ((if q then  [] Γ else [] Γ) - of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

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

Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
691
  = '(p,P)  envs_lookup j Δ; if p : bool then Some (p,P) else None.
692
693
694
695
696
697
698
699
700
Proof.
  rewrite /envs_lookup /envs_clear_spatial.
  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
  by destruct (Γs !! j).
Qed.

Lemma envs_clear_spatial_sound Δ :
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
Proof.
701
  rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
702
703
704
705
706
707
708
  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

Lemma env_spatial_is_nil_intuitionistically Δ :
  env_spatial_is_nil Δ = true  of_envs Δ   of_envs Δ.
Proof.
709
  intros. rewrite !of_envs_eq; destruct Δ as [? []]; simplify_eq/=.
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
  rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and.
  by rewrite persistently_affinely_elim persistently_idemp persistently_pure.
Qed.

Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ 
  envs_lookup i Δ = Some (p,P)  envs_lookup i (envs_delete true 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 Δ rp i j p :
  i  j  envs_lookup i (envs_delete rp j p Δ) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
  - destruct rp=> //. by rewrite env_lookup_env_delete_ne.
  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
Qed.

732
733
734
735
736
Lemma envs_incr_counter_equiv Δ : envs_Forall2 () Δ (envs_incr_counter Δ).
Proof. done. Qed.
Lemma envs_incr_counter_sound Δ : of_envs (envs_incr_counter Δ)  of_envs Δ.
Proof. by f_equiv. Qed.

737
738
739
740
741
742
743
744
Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
  ( j P, envs_lookup j Δ1 = Some (false, P)  envs_lookup j Δ2 = None) 
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
Proof.
  revert Δ1 Δ2.
  induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|].
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
745
  { by rewrite !of_envs_eq !and_elim_l sep_elim_l. }
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
  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 Δ d js Δ1 Δ2 :
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
Proof.
  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
  rewrite {2}envs_clear_spatial_sound.
  rewrite (env_spatial_is_nil_intuitionistically (envs_clear_spatial _)) //.
  rewrite -persistently_and_intuitionistically_sep_l.
  rewrite (and_elim_l (<pers> _)%I)
          persistently_and_intuitionistically_sep_r intuitionistically_elim.
  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 d; simplify_eq/=; solve_sep_entails.
Qed.

771
Lemma env_to_prop_sound Γ : env_to_prop Γ  [] Γ.
772
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
773
774
775
776
777
778
779
780
781
  destruct Γ as [|Γ i P]; simpl; first done.
  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
  - by rewrite right_id.
  - rewrite /= IH (comm _ Q _) assoc. done.
Qed.

Lemma env_to_prop_and_sound Γ : env_to_prop_and Γ  [] Γ.
Proof.
  destruct Γ as [|Γ i P]; simpl; first done.
782
783
784
785
786
  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
  - by rewrite right_id.
  - rewrite /= IH (comm _ Q _) assoc. done.
Qed.
End envs.