coq_tactics.v 58.4 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 modality_instances.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import bi.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
37
Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
38 39 40
  env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
78
Definition envs_snoc {PROP} (Δ : envs PROP)
79
    (p : bool) (j : ident) (P : PROP) : envs PROP :=
80 81 82
  let (Γp,Γs) := Δ in
  if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).

Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
Definition envs_app {PROP : bi} (p : bool)
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87 88 89 90
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_app Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_app Γ Γs; Some (Envs Γp Γs')
  end.

91
Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
Robbert Krebbers's avatar
Robbert Krebbers committed
92
    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96 97 98
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_replace i Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_replace i Γ Γs; Some (Envs Γp Γs')
  end.

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

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

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

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
129 130 131 132 133 134
Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
  let fix aux Γ acc :=
    match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P  acc)%I end
  in
  match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.

Robbert Krebbers's avatar
Robbert Krebbers committed
135
(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137 138 139 140 141 142
Section bi_tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Lemma of_envs_eq Δ :
143
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
144 145
Proof. done. Qed.

146 147 148 149 150 151 152 153 154
Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ. 
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 Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157 158 159 160
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.

161
Lemma envs_lookup_sound' Δ rp i p P :
162
  envs_lookup i Δ = Some (p,P) 
163
  of_envs Δ  ?p P  of_envs (envs_delete rp i p Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
167
  - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
168
      naive_solver eauto using env_delete_wf, env_delete_fresh).
169 170 171 172 173
    destruct rp.
    + rewrite (env_lookup_perm Γp) //= affinely_persistently_and.
      by rewrite and_sep_affinely_persistently -assoc.
    + rewrite {1}affinely_persistently_sep_dup {1}(env_lookup_perm Γp) //=.
      by rewrite affinely_persistently_and and_elim_l -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
175 176 177 178
    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.
179 180 181 182
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Lemma envs_lookup_persistent_sound Δ i P :
184
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
185
Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187

Lemma envs_lookup_split Δ i p P :
188
  envs_lookup i Δ = Some (p,P)  of_envs Δ  ?p P  (?p P - of_envs Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
189
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
192
  - rewrite pure_True // left_id (env_lookup_perm Γp) //=
193
      affinely_persistently_and and_sep_affinely_persistently.
194
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
196
    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
197 198 199
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

200 201 202
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
203

204 205
Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps :
  envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') 
206
  of_envs Δ  ?p [] Ps  of_envs Δ'.
207 208
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
209
  { by rewrite affinely_persistently_emp left_id. }
210
  destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
211
  apply envs_lookup_delete_Some in Hj as [Hj ->].
212 213 214 215
  destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
  rewrite -affinely_persistently_if_sep_2 -assoc.
  rewrite envs_lookup_sound' //; rewrite IH //.
  repeat apply sep_mono=>//; apply affinely_persistently_if_flag_mono; by destruct q1.
216 217
Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
218 219 220 221 222 223 224 225 226 227
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, Δ'') 
  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
Proof. rewrite //= => -> //= -> //=. Qed.

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

228 229 230 231 232 233 234 235 236 237 238 239 240 241
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 :
242
  envs_lookup i Δ = None  of_envs Δ  ?p P - of_envs (envs_snoc Δ p i P).
243
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
245 246
  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
247
  - apply and_intro; [apply pure_intro|].
248
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
249
      intros j; destruct (ident_beq_reflect j i); naive_solver.
250
    + by rewrite affinely_persistently_and and_sep_affinely_persistently assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
  - apply and_intro; [apply pure_intro|].
252
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
253
      intros j; destruct (ident_beq_reflect j i); naive_solver.
254 255 256
    + solve_sep_entails.
Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
285 286
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
287
  of_envs (envs_delete true i p Δ)  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
288 289
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
291 292
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295 296 297
    + 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') //.
298
      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
299
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
300 301
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
303 304 305
    + 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.
306
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
307 308
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
314 315
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
316
  of_envs Δ  ?p P  ((if p then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
317 318
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
327
Lemma envs_replace_sound' Δ Δ' i p q Γ :
328
  envs_replace i p q Γ Δ = Some Δ' 
329
  of_envs (envs_delete true i p Δ)  (if q then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
330 331 332 333 334 335
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
341 342
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
343
  of_envs Δ  ?p P  ((if q then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
344 345
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

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

352 353
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
Robbert Krebbers's avatar
Robbert Krebbers committed
354
  = ''(p,P)  envs_lookup j Δ; if p : bool then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
Proof.
356 357 358
  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
359 360
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
361
Lemma envs_clear_spatial_sound Δ :
362
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
363
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
364 365 366
  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.
367 368
Qed.

369
Lemma env_spatial_is_nil_affinely_persistently Δ :
370
  env_spatial_is_nil Δ = true  of_envs Δ   of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
371 372
Proof.
  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
373 374
  rewrite !right_id {1}affinely_and_r persistently_and.
  by rewrite persistently_affinely persistently_idemp persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
375
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
376

377 378
Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ 
379
  envs_lookup i Δ = Some (p,P)  envs_lookup i (envs_delete true i p Δ) = None.
380 381 382 383 384 385 386
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.
387 388
Lemma envs_lookup_envs_delete_ne Δ rp i j p :
  i  j  envs_lookup i (envs_delete rp j p Δ) = envs_lookup i Δ.
389 390
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
391
  - destruct rp=> //. by rewrite env_lookup_env_delete_ne.
392 393 394 395 396
  - 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
397
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
398
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
399
Proof.
400 401
  revert Δ1 Δ2.
  induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
402 403
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite /of_envs !and_elim_l sep_elim_l. }
404 405
  destruct (envs_lookup_delete _ j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq/=; auto.
406 407
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
408 409 410 411
  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. }
412 413
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
414
Lemma envs_split_sound Δ d js Δ1 Δ2 :
415
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
416
Proof.
417
  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
418
  rewrite {2}envs_clear_spatial_sound.
419 420
  rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
  rewrite -persistently_and_affinely_sep_l.
421
  rewrite (and_elim_l (<pers> _)%I)
422
          persistently_and_affinely_sep_r affinely_persistently_elim.
423 424 425
  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=> ->. }
426
  destruct d; simplify_eq/=; solve_sep_entails.
427 428
Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
429 430 431 432 433 434 435 436
Lemma prop_of_env_sound Δ : of_envs Δ  prop_of_env (env_spatial Δ).
Proof.
  destruct Δ as [? Γ]. rewrite /of_envs /= and_elim_r sep_elim_r.
  destruct Γ as [|Γ ? P0]=>//=. revert P0.
  induction Γ as [|Γ IH ? P]=>P0; [rewrite /= right_id //|].
  rewrite /= assoc (comm _ P0 P) IH //.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
437
Global Instance envs_Forall2_refl (R : relation PROP) :
438 439
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
Global Instance envs_Forall2_sym (R : relation PROP) :
441 442
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Global Instance envs_Forall2_trans (R : relation PROP) :
444 445
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
446
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
447 448
  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
449
Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
450 451 452
  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
453
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
454
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
455 456
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
457 458 459
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
460 461
Global Instance of_envs_proper :
  Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
462
Proof.
463 464
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
465
Qed.
466
Global Instance Envs_proper (R : relation PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
467
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs PROP).
468 469
Proof. by constructor. Qed.

470
Global Instance envs_entails_proper :
471
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails PROP).
472
Proof. rewrite envs_entails_eq. solve_proper. Qed.
473
Global Instance envs_entails_flip_mono :
474
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
475
Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
476

Robbert Krebbers's avatar
Robbert Krebbers committed
477
(** * Adequacy *)
478
Lemma tac_adequate P : envs_entails (Envs Enil Enil) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
479
Proof.
480 481
  rewrite envs_entails_eq /of_envs /= persistently_True_emp
          affinely_persistently_emp left_id=><-.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
483 484 485
Qed.

(** * Basic rules *)
486
Lemma tac_eval Δ Q Q' :
487 488 489
  ( (Q'':=Q'), Q''  Q)  (* We introduce [Q''] as a let binding so that
    tactics like `reflexivity` as called by [rewrite //] do not eagerly unify
    it with [Q]. See [test_iEval] in [tests/proofmode]. *)
490
  envs_entails Δ Q'  envs_entails Δ Q.
491
Proof. by intros <-. Qed.
492

493 494
Lemma tac_eval_in Δ Δ' i p P P' Q :
  envs_lookup i Δ = Some (p, P) 
495
  ( (P'':=P'), P  P') 
496 497 498
  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' 
  envs_entails Δ' Q  envs_entails Δ Q.
Proof.
499 500 501
  rewrite envs_entails_eq /=. intros ? HP ? <-.
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
502
Qed.
503

504 505 506 507 508 509 510
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.

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

515
Instance affine_env_spatial Δ :
516 517 518
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

519 520
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
521

Robbert Krebbers's avatar
Robbert Krebbers committed
522
Lemma tac_assumption Δ Δ' i p P Q :
523
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
524
  FromAssumption p P Q 
525 526
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
527
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
528
Proof.
529
  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
  destruct (env_spatial_is_nil Δ') eqn:?.
531
  - by rewrite (env_spatial_is_nil_affinely_persistently Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
533
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
534 535 536 537

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
538 539
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
Proof.
541
  rewrite envs_entails_eq=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
542
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
543
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
544

Robbert Krebbers's avatar
Robbert Krebbers committed
545
Lemma tac_clear Δ Δ' i p P Q :
546
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
547
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
548
  envs_entails Δ' Q 
549
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Proof.
551
  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
552
  by destruct p; rewrite /= HQ sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
554 555

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

Robbert Krebbers's avatar
Robbert Krebbers committed
559 560 561
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
562
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Proof.
564
  rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
565
  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
566 567
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
568
(** * Pure *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
569 570
(* This relies on the invariant that [FromPure false] implies
   [FromPure true] *)
571 572 573 574 575 576 577 578
Lemma tac_pure_intro Δ Q φ af :
  env_spatial_is_nil Δ = af  FromPure af Q φ  φ  envs_entails Δ Q.
Proof.
  intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af.
  - rewrite env_spatial_is_nil_affinely_persistently //=. f_equiv.
    by apply pure_intro.
  - by apply pure_intro.
Qed.
579

Robbert Krebbers's avatar
Robbert Krebbers committed
580
Lemma tac_pure Δ Δ' i p P φ Q :
581
  envs_lookup_delete true i Δ = Some (p, P, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
582
  IntoPure P φ 
583
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
584
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
Proof.
586
  rewrite envs_entails_eq=> ?? HPQ HQ.
587
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
588
  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
589
    by apply pure_elim_l.
590
  - destruct HPQ.
591
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
592
      by apply pure_elim_l.
593
    + rewrite (into_pure P) -(persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
594
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
595 596
Qed.

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

600
(** * Persistence *)
Robbert Krebbers's avatar
Robbert Krebbers committed
601
Lemma tac_persistent Δ Δ' i p P P' Q :
602
  envs_lookup i Δ = Some (p, P) 
603
  IntoPersistent p P P' 
604
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
605
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
606
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
607
Proof.
608
  rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
609 610 611
  destruct p; simpl.
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
612
    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
613
              (into_persistent _ P) wand_elim_r //.
614
    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
615 616
      by rewrite -{1}absorbingly_affinely_persistently
        absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
617 618 619
Qed.

(** * Implication and wand *)
620 621
Lemma tac_impl_intro Δ Δ' i P P' Q R :
  FromImpl R P Q 
622
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
623
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
624
  FromAffinely P' P 
625
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
626
Proof.
627
  rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
628
  - rewrite (env_spatial_is_nil_affinely_persistently Δ) //; simpl. apply impl_intro_l.
629
    rewrite envs_app_singleton_sound //; simpl.
630 631
    rewrite -(from_affinely P') -affinely_and_lr.
    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
632
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
633
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
634
Qed.
635 636
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
  FromImpl R P Q 
637
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
638
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
639
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
Proof.
Jacques-Henri Jourdan's avatar