coq_tactics.v 33.7 KB
Newer Older
1 2
From iris.base_logic Require Export base_logic.
From iris.base_logic Require Import big_op tactics.
3
From iris.proofmode Require Export environments classes.
Ralf Jung's avatar
Ralf Jung committed
4
From stdpp Require Import stringmap hlist.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Import uPred.
7
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12 13 14 15 16 17 18 19 20 21 22
  Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

Record envs_wf {M} (Δ : envs M) := {
  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
}.

Coercion of_envs {M} (Δ : envs M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
23
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
24 25 26 27 28 29
Instance: Params (@of_envs) 1.

Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
  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
30

31 32
Definition envs_dom {M} (Δ : envs M) : list string :=
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53

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

Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
  let (Γp,Γs) := Δ in
  match p with
  | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
  end.

Definition envs_lookup_delete {M} (i : string)
    (Δ : envs M) : option (bool * uPred M * envs M) :=
  let (Γp,Γs) := Δ in
  match env_lookup_delete i Γp with
  | Some (P,Γp') => Some (true, P, Envs Γp' Γs)
  | None => '(P,Γs')  env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
  end.

54 55 56 57 58
Definition envs_snoc {M} (Δ : envs M)
    (p : bool) (j : string) (P : uPred M) : envs M :=
  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
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
Definition envs_app {M} (p : bool)
    (Γ : env (uPred M)) (Δ : envs M) : option (envs M) :=
  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.

Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  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.

Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

80
Definition env_spatial_is_nil {M} (Δ : envs M) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82
  if env_spatial Δ is Enil then true else false.

83 84 85
Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
  Envs (env_persistent Δ) Enil.

86 87 88
Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
  Envs Enil (env_spatial Δ).

89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
Fixpoint envs_split_go {M}
    (js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
     '(p,P,Δ1')  envs_lookup_delete j Δ1;
     if p then envs_split_go js Δ1 Δ2 else
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
(* if [lr = true] then [result = (remaining hyps, hyps named js)] and
   if [lr = false] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {M} (lr : bool)
    (js : list string) (Δ : envs M) : option (envs M * envs M) :=
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
  if lr then Some (Δ1,Δ2) else Some (Δ2,Δ1).


Robbert Krebbers's avatar
Robbert Krebbers committed
106 107
(* Coq versions of the tactics *)
Section tactics.
108
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
109 110 111 112
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

113
Lemma of_envs_def Δ :
Ralf Jung's avatar
Ralf Jung committed
114
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
115 116
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
117 118 119 120 121 122 123 124 125 126
Lemma envs_lookup_delete_Some Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ')
   envs_lookup i Δ = Some (p,P)  Δ' = envs_delete i p Δ.
Proof.
  rewrite /envs_lookup /envs_delete /envs_lookup_delete.
  destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct.
  destruct (Γp !! i), (Γs !! i); naive_solver.
Qed.

Lemma envs_lookup_sound Δ i p P :
127
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  envs_delete i p Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Proof.
129
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
131
  - rewrite (env_lookup_perm Γp) //= always_sep.
132
    ecancel [ [] _;  P; [] Γs]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135 136
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
137
    ecancel [ [] _; P; [] (env_delete _ _)]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140 141
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
142
  envs_lookup i Δ = Some (p,P)  Δ  P  envs_delete i p Δ.
143
Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Lemma envs_lookup_persistent_sound Δ i P :
145
  envs_lookup i Δ = Some (true,P)  Δ   P  Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
Proof.
147
  intros. apply (always_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
148 149 150
Qed.

Lemma envs_lookup_split Δ i p P :
151
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  (?p P - Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof.
153
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
155
  - rewrite (env_lookup_perm Γp) //= always_sep.
156
    rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
157 158
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
159
    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161 162 163
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
164
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  ?p P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
165 166
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
167
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

170 171 172 173 174 175 176 177 178 179 180 181 182 183
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 :
184
  envs_lookup i Δ = None  Δ  ?p P - envs_snoc Δ p i P.
185 186 187 188 189 190
Proof.
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
191
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
192
    + by rewrite always_sep assoc.
193 194
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
195
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
196 197 198
    + solve_sep_entails.
Qed.

199
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
Proof.
201
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203 204
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
205
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207 208 209
    + 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') //.
210
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
211 212
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
213
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
214 215 216 217 218 219 220 221
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
222
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
225
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
226 227
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
228
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230 231 232
    + 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') //.
233
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
234 235
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
236
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239 240 241 242 243 244
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
245
  Δ  ?p P  (?p [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
246 247 248
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
249
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251 252 253 254 255 256 257
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
258
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

261 262 263
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
  = '(p,P)  envs_lookup j Δ; if p then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
264
Proof.
265 266 267
  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
268 269
Qed.

270
Lemma envs_clear_spatial_sound Δ : Δ  envs_clear_spatial Δ  [] env_spatial Δ.
271
Proof.
272 273
  rewrite /of_envs /envs_clear_spatial /=; apply pure_elim_sep_l=> Hwf.
  rewrite right_id -assoc; apply sep_intro_True_l; [apply pure_intro|done].
274 275 276
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

277 278
Lemma env_spatial_is_nil_persistent Δ :
  env_spatial_is_nil Δ = true  PersistentP Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
280
Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
281

282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301
Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ 
  envs_lookup i Δ = Some (p,P)  envs_lookup i (envs_delete i p Δ) = None.
Proof.
  rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - rewrite env_lookup_env_delete //. revert Hlookup.
    destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _).
  - rewrite env_lookup_env_delete //. by destruct (Γp !! _).
Qed.
Lemma envs_lookup_envs_delete_ne Δ i j p :
  i  j  envs_lookup i (envs_delete j p Δ) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
  - by rewrite env_lookup_env_delete_ne.
  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
Qed.

Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
  ( j P, envs_lookup j Δ1 = Some (false, P)  envs_lookup j Δ2 = None) 
302
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2')  Δ1  Δ2  Δ1'  Δ2'.
303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
Proof.
  revert Δ1 Δ2 Δ1' Δ2'.
  induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
  apply pure_elim with (envs_wf Δ1); [unfold of_envs; solve_sep_entails|]=> Hwf.
  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 Δ lr js Δ1 Δ2 :
318
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
319 320 321 322 323 324 325 326 327
Proof.
  rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
  rewrite {2}envs_clear_spatial_sound sep_elim_l always_and_sep_r.
  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
  apply envs_split_go_sound in HΔ as ->; last first.
  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
  destruct lr; simplify_eq; solve_sep_entails.
Qed.

328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346
Global Instance envs_Forall2_refl (R : relation (uPred M)) :
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Global Instance envs_Forall2_sym (R : relation (uPred M)) :
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Global Instance envs_Forall2_trans (R : relation (uPred M)) :
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
  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 (uPred M)) Δ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.

Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in *.
347 348
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
349 350 351 352 353
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Global Instance of_envs_proper : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
354 355
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
356 357 358 359 360
Qed.
Global Instance Envs_mono (R : relation (uPred M)) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
Proof. by constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
361
(** * Adequacy *)
362
Lemma tac_adequate P : (Envs Enil Enil  P)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
Proof.
364 365
  intros <-. rewrite /of_envs /= always_pure !right_id.
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
366 367 368
Qed.

(** * Basic rules *)
369
Lemma tac_assumption Δ i p P Q :
370
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q  Δ  Q.
371
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
372 373 374 375

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
376
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
377 378 379 380 381
Proof.
  intros. rewrite envs_simple_replace_sound //.
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.
Lemma tac_clear Δ Δ' i p P Q :
382
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384 385
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.

(** * False *)
386
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
387 388 389
Proof. by rewrite -(False_elim Q). Qed.

(** * Pure *)
390
Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ  φ  Δ  Q.
391
Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
392

Robbert Krebbers's avatar
Robbert Krebbers committed
393
Lemma tac_pure Δ Δ' i p P φ Q :
394
  envs_lookup_delete i Δ = Some (p, P, Δ')  IntoPure P φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
395 396 397
  (φ  Δ'  Q)  Δ  Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
398
  rewrite (into_pure P); by apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
399 400
Qed.

Ralf Jung's avatar
Ralf Jung committed
401
Lemma tac_pure_revert Δ φ Q : (Δ  ⌜φ⌝  Q)  (φ  Δ  Q).
402
Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
403 404

(** * Later *)
405 406 407 408 409
Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
  into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
  into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
  into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
410 411
}.

412
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
Proof. constructor. Qed.
414 415 416
Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
  IntoLaterNEnv n Γ1 Γ2  IntoLaterN n P Q 
  IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
417 418
Proof. by constructor. Qed.

419 420 421
Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
  IntoLaterNEnv n Γp1 Γp2  IntoLaterNEnv n Γs1 Γs2 
  IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
422
Proof. by split. Qed.
423

424
Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2  Δ1  ^n Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
425
Proof.
426
  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -always_laterN.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
  repeat apply sep_mono; try apply always_mono.
428
  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
429
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
430 431
  - induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
  - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
432 433
Qed.

434 435 436
Lemma tac_next Δ Δ' n Q Q' :
  FromLaterN n Q Q'  IntoLaterNEnvs n Δ Δ'  (Δ'  Q')  Δ  Q.
Proof. intros ?? HQ. by rewrite -(from_laterN n Q) into_laterN_env_sound HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
437 438

Lemma tac_löb Δ Δ' i Q :
439
  env_spatial_is_nil Δ = true 
440
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
441
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
442
Proof.
443 444 445 446
  intros ?? HQ. rewrite -(always_elim Q) -(löb ( Q)) -always_later.
  apply impl_intro_l, (always_intro _ _).
  rewrite envs_app_sound //; simpl.
  by rewrite right_id always_and_sep_l' wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
447 448 449
Qed.

(** * Always *)
450
Lemma tac_always_intro Δ Q : env_spatial_is_nil Δ = true  (Δ  Q)  Δ   Q.
451
Proof. intros. by apply (always_intro _ _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
452 453

Lemma tac_persistent Δ Δ' i p P P' Q :
454
  envs_lookup i Δ = Some (p, P)  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
455
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
456
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
Proof.
458
  intros ??? <-. rewrite envs_replace_sound //; simpl.
459
  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
460 461 462 463
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
464
  env_spatial_is_nil Δ = true 
Robbert Krebbers's avatar
Robbert Krebbers committed
465
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
466
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
467 468 469 470 471
Proof.
  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
  by rewrite right_id always_wand_impl always_elim HQ.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
472
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
473
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
474
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
475 476
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
477
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
Qed.
479
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
Ralf Jung's avatar
Ralf Jung committed
480
  (φ  Δ  ⌜ψ⌝)  Δ  ⌜φ  ψ⌝.
481
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
482
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
Proof.
484
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
486 487
Lemma tac_impl_intro_drop Δ P Q : (Δ  Q)  Δ  P  Q.
Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
488 489

Lemma tac_wand_intro Δ Δ' i P Q :
490
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
491
Proof.
492
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
493 494
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
495
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
496
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
497
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
498 499 500 501
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
502
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
Proof.
504
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
505
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
506 507
Lemma tac_wand_intro_drop Δ P Q : (Δ  Q)  Δ  P - Q.
Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
508 509 510 511 512

(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
but it is doing some work to keep the order of hypotheses preserved. *)
Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
  envs_lookup_delete i Δ = Some (p, P1, Δ') 
513
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
514
  IntoWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516 517 518 519
  match p with
  | true  => envs_simple_replace j q (Esnoc Enil j P2) Δ
  | false => envs_replace j q false (Esnoc Enil j P2) Δ'
             (* remove [i] and make [j] spatial *)
  end = Some Δ'' 
520
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
521 522 523
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
524
    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
525
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
526 527
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
528
    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
529 530
Qed.

531
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
532
  envs_lookup_delete j Δ = Some (q, R, Δ') 
533
  IntoWand R P1 P2  ElimModal P1' P1 Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
534
  ('(Δ1,Δ2)  envs_split lr js Δ';
535
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
536
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
537
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
Proof.
539
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
540 541 542 543
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
  rewrite (envs_app_sound Δ2) //; simpl.
544
  rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
545
  rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
546
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
547 548
Qed.

549
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
550
  envs_lookup j Δ = Some (q, R) 
551
  IntoWand R P1 P2  FromPure P1 φ 
552
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
553
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Proof.
555
  intros. rewrite envs_simple_replace_sound //; simpl.
556
  rewrite right_id (into_wand R) -(from_pure P1) pure_True //.
557
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
558 559
Qed.

560
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
561
  envs_lookup_delete j Δ = Some (q, R, Δ') 
562
  IntoWand R P1 P2  PersistentP P1 
563
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
  (Δ'  P1)  (Δ''  Q)  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
  rewrite envs_lookup_sound //.
  rewrite -(idemp uPred_and (envs_delete _ _ _)).
  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
  rewrite envs_simple_replace_sound' //; simpl.
  rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
  by rewrite wand_elim_r.
Qed.

Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
  envs_lookup j Δ = Some (q,P) 
  (Δ  R)  PersistentP R 
  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
580
Proof.
581 582 583 584
  intros ? HR ?? <-.
  rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
  rewrite envs_replace_sound //; simpl.
  by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
585 586 587 588
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
589
  (Δ'  (if p then  P else P) - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
590
Proof.
591 592
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
  by rewrite HQ /uPred_always_if wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
593 594
Qed.

595 596 597 598 599 600 601 602 603 604
Lemma tac_revert_ih Δ P Q :
  env_spatial_is_nil Δ = true 
  (of_envs Δ  P) 
  (of_envs Δ   P  Q) 
  (of_envs Δ  Q).
Proof.
  intros ? HP HPQ.
  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
Qed.

605
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
606
  ElimModal P' P Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
607
  envs_split lr js Δ = Some (Δ1,Δ2) 
608
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
609
  (Δ1  P')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
610
Proof.
611
  intros ??? HP HQ. rewrite envs_split_sound //.
612
  rewrite (envs_app_sound Δ2) //; simpl.
613
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
614 615
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
616 617 618 619 620
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
  envs_split lr js Δ = Some (Δ1,Δ2) 
  envs_app false (Esnoc Enil j P) Δ = Some Δ' 
  (Δ1  P)  PersistentP P 
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
622 623 624
  intros ?? HP ? <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
  rewrite HP sep_elim_l (always_and_sep_l P) envs_app_sound //; simpl.
  by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
625 626
Qed.

627
Lemma tac_pose_proof Δ Δ' j P Q :
628
  P 
629
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
630
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
631
Proof.
632 633
  intros HP ? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -HP always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
634 635
Qed.

636 637 638
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' 
639
  (Δ''  Q)  Δ  Q.
640 641 642 643 644 645 646 647
Proof.
  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
648
Lemma tac_apply Δ Δ' i p R P1 P2 :
649
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand R P1 P2 
650
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
651 652
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
653
  by rewrite (into_wand R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
654 655 656 657 658
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
659
   {A : ofeT} (x y : A) (Φ : A  uPred M),
660 661
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x)) 
662
    (NonExpansive Φ) 
663
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
664
Proof.
665
  intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
666
  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
667
  destruct lr; auto using internal_eq_sym.
Robbert Krebbers's avatar
Robbert Krebbers committed
668 669 670 671
Qed.

Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
672
  envs_lookup j Δ = Some (q, P) 
673
   {A : ofeT} Δ' x y (Φ : A  uPred M),
674 675
    (Pxy  x  y) 
    (P  Φ (if lr then y else x)) 
676
    (NonExpansive Φ) 
Robbert Krebbers's avatar
Robbert Krebbers committed
677
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
678
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
679 680 681 682
Proof.
  intros ?? A Δ' x y Φ HPxy HP ?? <-.
  rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
  rewrite sep_elim_l HPxy always_and_sep_r.
683 684
  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
  rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
685
  - apply (internal_eq_rewrite x y (λ y, ?q Φ y - Δ')%I);
686
      eauto with I. solve_proper.
687
  - apply (internal_eq_rewrite y x (λ y, ?q Φ y - Δ')%I);
688
      eauto using internal_eq_sym with I.
689
    solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
690 691 692
Qed.

(** * Conjunction splitting *)
693 694
Lemma tac_and_split Δ P Q1 Q2 : FromAnd P Q1 Q2  (Δ  Q1)  (Δ  Q2)  Δ  P.
Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
695 696 697

(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
698
  FromSep P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
699
  envs_split lr js Δ = Some (Δ1,Δ2) 
700
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
701
Proof.
702
  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
703 704 705 706 707 708
Qed.

(** * Combining *)
Lemma tac_combine Δ1 Δ2 Δ3 Δ4 i1 p P1 i2 q P2 j P Q :
  envs_lookup_delete i1 Δ1 = Some (p,P1,Δ2) 
  envs_lookup_delete i2 (if p then Δ1 else Δ2) = Some (q,P2,Δ3) 
709
  FromSep P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
710 711
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
712
  (Δ4  Q)  Δ1  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
713 714 715 716 717
Proof.
  intros [? ->]%envs_lookup_delete_Some [? ->]%envs_lookup_delete_Some ?? <-.
  destruct p.
  - rewrite envs_lookup_persistent_sound //. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
718
      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
719
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
720
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
721 722
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
723
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
724
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
725
      by rewrite right_id assoc (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
726 727 728
Qed.

(** * Conjunction/separating conjunction elimination *)
729 730
Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
  envs_lookup i Δ = Some (p, P)  IntoAnd p P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
731
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
732
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
733
Proof.
734
  intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).