environments.v 34 KB
Newer Older
1
From iris.prelude Require Export prelude.
2
From iris.bi Require Export bi.
3
From iris.proofmode Require Import base.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.prelude Require Import options.
5
Import bi.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
8

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

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

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

29
30
Local Open Scope lazy_bool_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
35
36
37
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.
38
Global Instance: Params (@env_to_list) 1 := {}.
39

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
79
80
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).

81
82
83
84
85
86
87
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
88
89
90
Section env.
Context {A : Type}.
Implicit Types Γ : env A.
91
Implicit Types i : ident.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Implicit Types x : A.
93
Local Hint Resolve Esnoc_wf Enil_wf : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
94

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

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.

110
111
112
113
114
115
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
116
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
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.
150
151
  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify; auto using env_app_perm.
  rewrite -Permutation_middle -IH //.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
153
154
Qed.

Lemma env_lookup_delete_correct Γ i :
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  env_lookup_delete i Γ = (x  Γ !! i; Some (x,env_delete i Γ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
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.
160
161

Lemma env_lookup_env_delete Γ j : env_wf Γ  env_delete j Γ !! j = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Proof. induction 1; intros; simplify; eauto. Qed.
163
164
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
165
166
Lemma env_delete_fresh Γ i j : Γ !! i = None  env_delete j Γ !! i = None.
Proof. induction Γ; intros; simplify; eauto. Qed.
167

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

171
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
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
197
198
199
200
201
202
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.
203
204
205
206
207
208
209
210

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
211
End env.
212

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

224
225
226
227
228
229
230
231
232
233
234
235
(** 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
236
using the tactic [change_no_check]. This way, the generated proof term
237
238
contains no additional steps for changing the counter.

Ralf Jung's avatar
Ralf Jung committed
239
240
241
We first define a version [pre_envs_entails] that takes the two contexts
[env_intuitionistic] and [env_spatial] as its arguments. We seal this definition
and then lift it to take the whole proof mode context [Δ : envs PROP]. This is
242
243
244
245
246
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
247
}.
248
249
250
251
252
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.
253
Global Instance: Params (@of_envs') 1 := {}.
254
255
Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
  of_envs' (env_intuitionistic Δ) (env_spatial Δ).
256
Global Instance: Params (@of_envs) 1 := {}.
Ralf Jung's avatar
Ralf Jung committed
257
Global Arguments of_envs : simpl never.
258

259
260
261
262
263
264
265
Definition pre_envs_entails_def {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
  of_envs' Γp Γs  Q.
Definition pre_envs_entails_aux : seal (@pre_envs_entails_def). Proof. by eexists. Qed.
Definition pre_envs_entails := pre_envs_entails_aux.(unseal).
Definition pre_envs_entails_eq : @pre_envs_entails = @pre_envs_entails_def :=
  pre_envs_entails_aux.(seal_eq).

266
Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
267
  pre_envs_entails  PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
268
Definition envs_entails_eq :
269
  @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ  Q).
270
Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
Ralf Jung's avatar
Ralf Jung committed
271
Global Arguments envs_entails {PROP} Δ Q%I.
272
Global Instance: Params (@envs_entails) 1 := {}.
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288

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.

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

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

305
Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
306
307
308
309
    (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
310
311
     '(p,P,Δ')  envs_lookup_delete remove_intuitionistic j Δ;
     '(q,Ps,Δ'')  envs_lookup_delete_list remove_intuitionistic js Δ';
312
     Some ((p:bool) &&& q, P :: Ps, Δ'')
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
344
345
346
  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 Δ).

347
Definition envs_clear_intuitionistic {PROP} (Δ : envs PROP) : envs PROP :=
348
349
350
  Envs Enil (env_spatial Δ) (env_counter Δ).

Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
351
  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
352
353
354
355
356
357

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 =>
358
     '(p,P,Δ1')  envs_lookup_delete true j Δ1;
359
360
361
362
363
364
365
     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) :=
366
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
367
368
  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).

Robbert Krebbers's avatar
Robbert Krebbers committed
369
370
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.
371
Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
Robbert Krebbers's avatar
Robbert Krebbers committed
372
373
374
375
376
377
  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.
378
379
380

Section envs.
Context {PROP : bi}.
381
Implicit Types Γ Γp Γs : env PROP.
382
383
384
385
386
387
388
389
390
391
392
393
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.

394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
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.

410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
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).
432
Proof.
433
  intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply and_mono; simpl in *.
434
435
436
437
  - apply pure_mono=> -[???]. constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
438
439
Global Instance of_envs_proper' :
  Proper (env_Forall2 () ==> env_Forall2 () ==> ()) (@of_envs' PROP).
440
Proof.
441
  intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply (anti_symm ()); apply of_envs_mono';
442
    eapply (env_Forall2_impl ()); by eauto using equiv_entails_1_1.
443
Qed.
444
445
446
447
448
449

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.

450
451
452
453
454
455
456
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.
457
458
459
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.
460
461
462
463
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.

464
Lemma envs_delete_intuitionistic Δ i : envs_delete false i true Δ = Δ.
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
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.
483
484
  rewrite /envs_lookup /envs_delete !of_envs_eq=>?.
  apply pure_elim_l=> Hwf.
485
486
487
488
489
490
  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.
491
    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
492
493
494
495
496
497
498
499
500
501
      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.
502
Lemma envs_lookup_intuitionistic_sound Δ i P :
503
504
505
506
507
508
  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.
509
510
  rewrite /envs_lookup !of_envs_eq=>Hwf ?.
  rewrite [envs_wf Δ⌝%I]pure_True // left_id.
511
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
512
513
  - by rewrite (env_lookup_perm Γp) //= intuitionistically_and
      and_sep_intuitionistically and_elim_r assoc.
514
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
515
    by rewrite (env_lookup_perm Γs) //= and_elim_r !assoc (comm _ P).
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
547
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, Δ'') 
548
  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 &&& p2, (P :: Ps), Δ'').
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
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.
571
  rewrite /envs_lookup /envs_snoc !of_envs_eq=> ?; apply pure_elim_l=> Hwf.
572
573
574
575
576
577
578
579
580
  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.
581
    + by rewrite !assoc (comm _ P).
582
583
584
585
586
587
Qed.

Lemma envs_app_sound Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ' 
  of_envs Δ  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Proof.
588
  rewrite !of_envs_eq /envs_app=> ?; apply pure_elim_l=> Hwf.
589
590
591
592
593
594
595
596
597
  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.
598
      by rewrite assoc.
599
600
601
602
603
604
  - 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.
605
    + by rewrite (env_app_perm _ _ Γs') // big_opL_app !assoc (comm _ ([] Γ)%I).
606
607
608
609
610
611
612
613
614
615
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.
616
  rewrite /envs_simple_replace /envs_delete !of_envs_eq=> ?.
617
618
619
620
621
622
623
624
625
  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.
626
      by rewrite assoc.
627
628
629
630
631
632
  - 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.
633
634
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app.
      by rewrite !assoc (comm _ ([] Γ)%I).
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
691
692
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 Δ)
693
  = '(p,P)  envs_lookup j Δ; if p : bool then Some (p,P) else None.
694
695
696
697
698
699
700
701
702
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.
703
  rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
704
705
706
707
708
709
710
  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.
711
  intros. rewrite !of_envs_eq; destruct Δ as [? []]; simplify_eq/=.
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
  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.

734
735
736
737
738
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.

739
740
741
742
743
744
745
746
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].
747
  { by rewrite !of_envs_eq !and_elim_l sep_elim_l. }
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
  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=> ->. }
770
  destruct d; simplify_eq/=; [|done]. by rewrite comm.
771
772
Qed.

773
Lemma env_to_prop_sound Γ : env_to_prop Γ  [] Γ.
774
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
775
776
777
778
779
780
781
782
783
  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.
784
785
786
787
788
  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
  - by rewrite right_id.
  - rewrite /= IH (comm _ Q _) assoc. done.
Qed.
End envs.