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

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

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

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

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

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

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

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

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

52 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

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

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

140 141 142 143 144 145 146 147 148
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
149 150 151 152 153 154
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.

155
Lemma envs_lookup_sound' Δ rp i p P :
156
  envs_lookup i Δ = Some (p,P) 
157
  of_envs Δ  ?p P  of_envs (envs_delete rp i p Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
161
  - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
162
      naive_solver eauto using env_delete_wf, env_delete_fresh).
163 164 165 166 167
    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
168
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171 172
    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.
173 174 175 176
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
177
Lemma envs_lookup_persistent_sound Δ i P :
178
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
179
Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181

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

194 195 196
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
197

198 199
Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps :
  envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') 
200
  of_envs Δ  ?p [] Ps  of_envs Δ'.
201 202
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
203
  { by rewrite affinely_persistently_emp left_id. }
204
  destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
205
  apply envs_lookup_delete_Some in Hj as [Hj ->].
206 207 208 209
  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.
210 211
Qed.

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
298 299
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
300
  of_envs Δ  ?p P  ((if p then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

303 304 305
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 Δ' 
306
  of_envs Δ  ?p P  (?p Q - of_envs Δ').
307 308 309 310
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
325 326
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
327
  of_envs Δ  ?p P  ((if q then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
328 329
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
345
Lemma envs_clear_spatial_sound Δ :
346
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
347
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
348 349 350
  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.
351 352
Qed.

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

361 362
Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ 
363
  envs_lookup i Δ = Some (p,P)  envs_lookup i (envs_delete true i p Δ) = None.
364 365 366 367 368 369 370
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.
371 372
Lemma envs_lookup_envs_delete_ne Δ rp i j p :
  i  j  envs_lookup i (envs_delete rp j p Δ) = envs_lookup i Δ.
373 374
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
375
  - destruct rp=> //. by rewrite env_lookup_env_delete_ne.
376 377 378 379 380
  - 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
381
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
382
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
383
Proof.
384 385
  revert Δ1 Δ2.
  induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
386 387
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite /of_envs !and_elim_l sep_elim_l. }
388 389
  destruct (envs_lookup_delete _ j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq/=; auto.
390 391
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
392 393 394 395
  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. }
396 397
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
398
Lemma envs_split_sound Δ d js Δ1 Δ2 :
399
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
400
Proof.
401
  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  rewrite {2}envs_clear_spatial_sound.
403 404
  rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
  rewrite -persistently_and_affinely_sep_l.
405
  rewrite (and_elim_l (bi_persistently _)%I)
406
          persistently_and_affinely_sep_r affinely_persistently_elim.
407 408 409
  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=> ->. }
410
  destruct d; simplify_eq/=; solve_sep_entails.
411 412
Qed.

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

446
Global Instance envs_entails_proper :
447
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails PROP).
448
Proof. rewrite envs_entails_eq. solve_proper. Qed.
449
Global Instance envs_entails_flip_mono :
450
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
451
Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
452

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

(** * Basic rules *)
462
Lemma tac_eval Δ Q Q' :
463 464 465
  ( (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]. *)
466
  envs_entails Δ Q'  envs_entails Δ Q.
467
Proof. by intros <-. Qed.
468

469 470
Lemma tac_eval_in Δ Δ' i p P P' Q :
  envs_lookup i Δ = Some (p, P) 
471
  ( (P'':=P'), P  P') 
472 473 474
  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' 
  envs_entails Δ' Q  envs_entails Δ Q.
Proof.
475 476 477
  rewrite envs_entails_eq /=. intros ? HP ? <-.
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
478
Qed.
479

480 481 482 483 484 485 486
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.

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

491
Instance affine_env_spatial Δ :
492 493 494
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

495 496
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
497

Robbert Krebbers's avatar
Robbert Krebbers committed
498
Lemma tac_assumption Δ Δ' i p P Q :
499
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
500
  FromAssumption p P Q 
501 502
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
503
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
504
Proof.
505
  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
506
  destruct (env_spatial_is_nil Δ') eqn:?.
507
  - by rewrite (env_spatial_is_nil_affinely_persistently Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
508
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
509
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
510 511 512 513

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
514 515
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
516
Proof.
517
  rewrite envs_entails_eq=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
518
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
519
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
520

Robbert Krebbers's avatar
Robbert Krebbers committed
521
Lemma tac_clear Δ Δ' i p P Q :
522
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
523
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
524
  envs_entails Δ' Q 
525
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
Proof.
527
  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
528
  by destruct p; rewrite /= HQ sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
529
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
530 531

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

Robbert Krebbers's avatar
Robbert Krebbers committed
535 536 537
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
538
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
539
Proof.
540
  rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
541
  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
542 543
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
544
(** * Pure *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
545 546
(* This relies on the invariant that [FromPure false] implies
   [FromPure true] *)
547 548 549 550 551 552 553 554
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.
555

Robbert Krebbers's avatar
Robbert Krebbers committed
556
Lemma tac_pure Δ Δ' i p P φ Q :
557
  envs_lookup_delete true i Δ = Some (p, P, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
558
  IntoPure P φ 
559
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
560
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
Proof.
562
  rewrite envs_entails_eq=> ?? HPQ HQ.
563
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
564
  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
565
    by apply pure_elim_l.
566
  - destruct HPQ.
567
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
568
      by apply pure_elim_l.
569 570
    + rewrite (into_pure P) (persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
571 572
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
576 577 578 579 580 581 582 583
(** * Always modalities *)
Class FilterPersistentEnv
    (M : always_modality PROP) (C : PROP  Prop) (Γ1 Γ2 : env PROP) := {
  filter_persistent_env :
    ( P, C P   P  M ( P)) 
     ([] Γ1)  M ( ([] Γ2));
  filter_persistent_env_wf : env_wf Γ1  env_wf Γ2;
  filter_persistent_env_dom i : Γ1 !! i = None  Γ2 !! i = None;
584
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609
Global Instance filter_persistent_env_nil M C : FilterPersistentEnv M C Enil Enil.
Proof.
  split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
  by rewrite affinely_emp -always_modality_emp.
Qed.
Global Instance filter_persistent_env_snoc M (C : PROP  Prop) Γ Γ' i P :
  C P 
  FilterPersistentEnv M C Γ Γ' 
  FilterPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
Proof.
  intros ? [HΓ Hwf Hdom]; split; simpl.
  - intros HC. rewrite affinely_persistently_and HC // HΓ //.
    by rewrite always_modality_and -affinely_persistently_and.
  - inversion 1; constructor; auto.
  - intros j. destruct (ident_beq _ _); naive_solver.
Qed.
Global Instance filter_persistent_env_snoc_not M (C : PROP  Prop) Γ Γ' i P :
  FilterPersistentEnv M C Γ Γ' 
  FilterPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
Proof.
  intros [HΓ Hwf Hdom]; split; simpl.
  - intros HC. by rewrite and_elim_r HΓ.
  - inversion 1; auto.
  - intros j. destruct (ident_beq _ _); naive_solver.
Qed.
610

Robbert Krebbers's avatar
Robbert Krebbers committed
611 612 613 614 615 616 617
Class FilterSpatialEnv
    (M : always_modality PROP) (C : PROP  Prop) (Γ1 Γ2 : env PROP) := {
  filter_spatial_env :
    ( P, C P  P  M P)  ( P, Absorbing (M P)) 
    ([] Γ1)  M ([] Γ2);
  filter_spatial_env_wf : env_wf Γ1  env_wf Γ2;
  filter_spatial_env_dom i : Γ1 !! i = None  Γ2 !! i = None;
618
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640
Global Instance filter_spatial_env_nil M C : FilterSpatialEnv M C Enil Enil.
Proof. split=> // HC /=. by rewrite -always_modality_emp. Qed.
Global Instance filter_spatial_env_snoc M (C : PROP  Prop) Γ Γ' i P :
  C P 
  FilterSpatialEnv M C Γ Γ' 
  FilterSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
Proof.
  intros ? [HΓ Hwf Hdom]; split; simpl.
  - intros HC ?. by rewrite {1}(HC P) // HΓ // always_modality_sep.
  - inversion 1; constructor; auto.
  - intros j. destruct (ident_beq _ _); naive_solver.
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
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
Ltac tac_always_cases :=
  simplify_eq/=;
  repeat match goal with
  | H : TCAnd _ _ |- _ => destruct H
  | H : TCEq ?x _ |- _ => inversion H; subst x; clear H
  | H : TCForall _ _ |- _ => apply TCForall_Forall in H
  | H : FilterPersistentEnv _ _ _ _ |- _ => destruct H
  | H : FilterSpatialEnv _ _ _ _ |- _ => destruct H
  end; simpl; auto using Enil_wf.

Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
  FromAlways M Q' Q 
  match always_modality_persistent_spec M with
  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
  | AIEnvFilter C => FilterPersistentEnv M C Γp Γp'
  | AIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
  | AIEnvClear => TCEq Γp' Enil
  | AIEnvId => TCEq Γp Γp'
  end 
  match always_modality_spatial_spec M with
  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
  | AIEnvFilter C => FilterSpatialEnv M C Γs Γs'
  | AIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
  | AIEnvClear => TCEq Γs' Enil
  | AIEnvId => TCEq Γs Γs'
  end 
  envs_entails (Envs Γp' Γs') Q  envs_entails (Envs Γp Γs) Q'.
Proof.
670
  rewrite envs_entails_eq /FromAlways /of_envs /= => <- HΓp HΓs <-.
Robbert Krebbers's avatar
Robbert Krebbers committed
671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693
  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')).
  { split; simpl in *.
    - destruct (always_modality_persistent_spec M); tac_always_cases.
    - destruct (always_modality_spatial_spec M); tac_always_cases.
    - destruct (always_modality_persistent_spec M),
        (always_modality_spatial_spec M); tac_always_cases; naive_solver. }
  rewrite pure_True // left_id. rewrite -always_modality_sep. apply sep_mono.
  - destruct (always_modality_persistent_spec M) eqn:?; tac_always_cases.
    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
        persistently_True_emp affinely_persistently_emp.
    + eauto using always_modality_persistent_forall_big_and.
    + eauto using always_modality_persistent_filter.
    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
        persistently_True_emp affinely_persistently_emp.
    + eauto using always_modality_persistent_id.
  - destruct (always_modality_spatial_spec M) eqn:?; tac_always_cases.
    + by rewrite -always_modality_emp.
    + eauto using always_modality_spatial_forall_big_sep.
    + eauto using always_modality_spatial_filter,
        always_modality_spatial_filter_absorbing.
    + rewrite -(always_modality_spatial_clear M) // -always_modality_emp.
      by rewrite -absorbingly_True_emp absorbingly_pure -True_intro.
    + by destruct (always_modality_spatial_id M).
694
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
695 696

Lemma tac_persistent Δ Δ' i p P P' Q :
697
  envs_lookup i Δ = Some (p, P)