coq_tactics.v 36.1 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 10
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.

11
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14 15 16 17 18 19 20 21 22 23 24
  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
25
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
26 27 28 29 30 31
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
32

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

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.

56 57 58 59 60 61 62 63 64 65 66
Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : bool)
    (Δ : envs M) : option (bool * list (uPred M) * envs M) :=
  match js with
  | [] => Some (true, [], Δ)
  | j :: js =>
     '(p,P,Δ')  envs_lookup_delete j Δ;
     let Δ' := if p then (if remove_persistent then Δ' else Δ) else Δ' in
     '(q,Hs,Δ'')  envs_lookup_delete_list js remove_persistent Δ';
     Some (p && q, P :: Hs, Δ'')
  end.

67 68 69 70 71
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
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
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 Δ).

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

96 97 98
Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
  Envs (env_persistent Δ) Enil.

99 100 101
Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
  Envs Enil (env_spatial Δ).

102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
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
118 119
(* Coq versions of the tactics *)
Section tactics.
120
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122 123 124
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

125
Lemma of_envs_def Δ :
Ralf Jung's avatar
Ralf Jung committed
126
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
127 128
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
129 130 131 132 133 134 135 136 137 138
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 :
139
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  envs_delete i p Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Proof.
141
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
143
  - rewrite (env_lookup_perm Γp) //= persistently_sep.
144
    ecancel [ [] _;  P; [] Γs]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146 147 148
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
149
    ecancel [ [] _; P; [] (env_delete _ _)]%I; apply pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151 152 153
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
154
  envs_lookup i Δ = Some (p,P)  Δ  P  envs_delete i p Δ.
155
Proof. intros. rewrite envs_lookup_sound //. by rewrite persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Lemma envs_lookup_persistent_sound Δ i P :
157
  envs_lookup i Δ = Some (true,P)  Δ   P  Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Proof.
159
  intros. apply (persistently_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161 162
Qed.

Lemma envs_lookup_split Δ i p P :
163
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  (?p P - Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
165
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
167
  - rewrite (env_lookup_perm Γp) //= persistently_sep.
168
    rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
171
    rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173 174 175
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
176
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  ?p P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
179
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

182 183 184 185
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ')  Δ  ?p [] Ps  Δ'.
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
186
  { by rewrite persistently_pure left_id. }
187 188 189
  destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
  apply envs_lookup_delete_Some in Hj as [Hj ->].
  destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
190
  rewrite persistently_if_sep -assoc. destruct q1; simpl.
191
  - destruct rp.
192 193 194
    + rewrite envs_lookup_sound //; simpl. by rewrite IH // (persistently_elim_if q2).
    + rewrite envs_lookup_persistent_sound //. by rewrite IH // (persistently_elim_if q2).
  - rewrite envs_lookup_sound // IH //; simpl. by rewrite persistently_if_elim.
195 196
Qed.

197 198 199 200 201 202 203 204 205 206 207 208 209 210
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 :
211
  envs_lookup i Δ = None  Δ  ?p P - envs_snoc Δ p i P.
212 213 214 215 216 217
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.
218
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
219
    + by rewrite persistently_sep assoc.
220 221
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
222
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
223 224 225
    + solve_sep_entails.
Qed.

226
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
Proof.
228
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230 231
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
232
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
233 234 235 236
    + 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') //.
237
      rewrite big_opL_app persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
238 239
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
240
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
241 242 243
    + 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.
244
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247 248
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
249
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
252
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
253 254
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
255
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
256 257 258 259
    + 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') //.
260
      rewrite big_opL_app persistently_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
261 262
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
263
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
264 265 266
    + 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.
267
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
268 269 270 271
Qed.

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

Lemma envs_replace_sound' Δ Δ' i p q Γ :
276
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278 279 280 281 282 283 284
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 Δ' 
285
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

288 289 290
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
291
Proof.
292 293 294
  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
295 296
Qed.

297
Lemma envs_clear_spatial_sound Δ : Δ  envs_clear_spatial Δ  [] env_spatial Δ.
298
Proof.
299 300
  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].
301 302 303
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

304
Lemma env_spatial_is_nil_persistent Δ :
305
  env_spatial_is_nil Δ = true  Persistent Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
307
Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
308

309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328
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) 
329
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2')  Δ1  Δ2  Δ1'  Δ2'.
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
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 :
345
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
346 347
Proof.
  rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
348
  rewrite {2}envs_clear_spatial_sound sep_elim_l and_sep_r.
349 350 351 352 353 354
  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.

355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373
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 *.
374 375
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
376 377 378 379 380
      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.
381 382
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
383 384 385 386 387
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
388
(** * Adequacy *)
389
Lemma tac_adequate P : (Envs Enil Enil  P)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
390
Proof.
391
  intros <-. rewrite /of_envs /= persistently_pure !right_id.
392
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
393 394 395
Qed.

(** * Basic rules *)
396
Lemma tac_assumption Δ i p P Q :
397
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q  Δ  Q.
398
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
399 400 401 402

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
403
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
404 405 406 407 408
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 :
409
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
410 411 412
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.

(** * False *)
413
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
414 415 416
Proof. by rewrite -(False_elim Q). Qed.

(** * Pure *)
417
Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ  φ  Δ  Q.
418
Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
419

Robbert Krebbers's avatar
Robbert Krebbers committed
420
Lemma tac_pure Δ Δ' i p P φ Q :
421
  envs_lookup_delete i Δ = Some (p, P, Δ')  IntoPure P φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
422 423 424
  (φ  Δ'  Q)  Δ  Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
425
  rewrite (into_pure P); by apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
426 427
Qed.

Ralf Jung's avatar
Ralf Jung committed
428
Lemma tac_pure_revert Δ φ Q : (Δ  ⌜φ⌝  Q)  (φ  Δ  Q).
429
Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
430 431

(** * Later *)
432 433 434 435 436
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)
437 438
}.

439
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
Proof. constructor. Qed.
441 442 443
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
444 445
Proof. by constructor. Qed.

446 447 448
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
449
Proof. by split. Qed.
450

451
Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2  Δ1  ^n Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
Proof.
453 454
  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
  repeat apply sep_mono; try apply persistently_mono.
455
  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
456
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
457 458
  - 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
459 460
Qed.

461 462 463
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
464 465

Lemma tac_löb Δ Δ' i Q :
466
  env_spatial_is_nil Δ = true 
467
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
468
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
Proof.
470 471
  intros ?? HQ. rewrite -(persistently_elim Q) -(löb ( Q)) -persistently_later.
  apply impl_intro_l, (persistently_intro _ _).
472
  rewrite envs_app_sound //; simpl.
473
  by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
474 475 476
Qed.

(** * Always *)
477
Lemma tac_persistently_intro Δ Q :
478 479 480
  (envs_clear_spatial Δ  Q)  Δ   Q.
Proof.
  intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
481
  by apply (persistently_intro _ _).
482
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
483 484

Lemma tac_persistent Δ Δ' i p P P' Q :
485
  envs_lookup i Δ = Some (p, P) 
486
  IntoPersistent p P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
487
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
488
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
Proof.
490
  intros ? HP ? <-. rewrite envs_replace_sound //; simpl.
491
  by rewrite right_id (into_persistent _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
492 493 494 495
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
496
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
497
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
498
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
499
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
  intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
501
  - rewrite (persistent Δ) envs_app_sound //; simpl.
502
    by rewrite right_id -persistently_impl_wand persistently_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
504
    by rewrite and_sep_l right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
505 506
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
507
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
508
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
509
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
Proof.
511
  intros ?? HQ. rewrite envs_app_sound //=; simpl. apply impl_intro_l.
512
  rewrite (_ : P = ?false P) // (into_persistent false P).
513
  by rewrite right_id persistently_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
514
Qed.
515

Robbert Krebbers's avatar
Robbert Krebbers committed
516 517
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
518 519

Lemma tac_wand_intro Δ Δ' i P Q :
520
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
521
Proof.
522
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
523 524
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
525
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
526
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
527
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529 530 531
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
532 533
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
534 535 536 537 538

(* 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, Δ') 
539
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
540
  IntoWand p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
541 542 543 544 545
  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 Δ'' 
546
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
547 548 549
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
550
    rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
551
    + by rewrite persistently_wand persistent_persistently !wand_elim_r.
552
    + by rewrite !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
553 554
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
555
    by rewrite right_id assoc (into_wand _ R) persistently_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
556 557
Qed.

558
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
559
  envs_lookup_delete j Δ = Some (q, R, Δ') 
560
  IntoWand false R P1 P2  ElimModal P1' P1 Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
561
  ('(Δ1,Δ2)  envs_split lr js Δ';
562
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
563
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
564
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
565
Proof.
566
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
567 568 569 570
  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.
571
  rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
572
  rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
573
  by rewrite persistently_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
574 575
Qed.

576 577 578 579 580
Lemma tac_unlock P Q : (P  Q)  P  locked Q.
Proof. by unlock. Qed.

Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
581
  IntoWand false R P1 P2 
582 583 584 585 586 587 588
  ElimModal P1' P1 Q Q 
  (Δ'  P1'  locked Q') 
  Q' = (P2 - Q)%I 
  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
589
  rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
590 591 592 593
  rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
  by rewrite assoc !wand_elim_r.
Qed.

594
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
595
  envs_lookup j Δ = Some (q, R) 
596
  IntoWand false R P1 P2  FromPure P1 φ 
597
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
598
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
Proof.
600
  intros. rewrite envs_simple_replace_sound //; simpl.
601
  rewrite right_id (into_wand _ R) -(from_pure P1) pure_True //.
602
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
603 604
Qed.

605
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
606
  envs_lookup_delete j Δ = Some (q, R, Δ') 
607
  IntoWand false R P1 P2  Persistent P1 
608
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
609 610 611 612 613
  (Δ'  P1)  (Δ''  Q)  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
  rewrite envs_lookup_sound //.
  rewrite -(idemp uPred_and (envs_delete _ _ _)).
614
  rewrite {1}HP1 (persistent P1) persistently_and_sep_l assoc.
615
  rewrite envs_simple_replace_sound' //; simpl.
616
  rewrite right_id (into_wand _ R) (persistently_elim_if q) -persistently_if_sep wand_elim_l.
617 618 619 620 621
  by rewrite wand_elim_r.
Qed.

Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
  envs_lookup j Δ = Some (q,P) 
622
  (Δ  R)  Persistent R 
623 624
  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
Proof.
626
  intros ? HR ?? <-.
627
  rewrite -(idemp uPred_and Δ) {1}HR and_sep_l.
628
  rewrite envs_replace_sound //; simpl.
629
  by rewrite right_id assoc (sep_elim_l R) persistent_persistently wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
630 631 632 633
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
634
  (Δ'  (if p then  P else P) - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
Proof.
636
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
637
  by rewrite HQ /uPred_persistently_if wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
638 639
Qed.

640 641 642 643 644 645 646 647 648 649 650 651 652
Class IntoIH (φ : Prop) (Δ : envs M) (Q : uPred M) :=
  into_ih : φ  Δ  Q.
Global Instance into_ih_entails Δ Q : IntoIH (of_envs Δ  Q) Δ Q.
Proof. by rewrite /IntoIH. Qed.
Global Instance into_ih_forall {A} (φ : A  Prop) Δ Φ :
  ( x, IntoIH (φ x) Δ (Φ x))  IntoIH ( x, φ x) Δ ( x, Φ x) | 2.
Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
  IntoIH φ Δ Q  IntoIH (ψ  φ) Δ (⌜ψ⌝  Q) | 1.
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.

Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P 
653 654 655 656
  env_spatial_is_nil Δ = true 
  (of_envs Δ   P  Q) 
  (of_envs Δ  Q).
Proof.
657
  rewrite /IntoIH. intros HP ? HPQ.
658
  by rewrite -(idemp uPred_and Δ) {1}(persistent Δ) {1}HP // HPQ impl_elim_r.
659 660
Qed.

661
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
662
  ElimModal P' P Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
663
  envs_split lr js Δ = Some (Δ1,Δ2) 
664
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
665
  (Δ1  P')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
666
Proof.
667
  intros ??? HP HQ. rewrite envs_split_sound //.
668
  rewrite (envs_app_sound Δ2) //; simpl.
669
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
670 671
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
672 673 674
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 Δ' 
675
  Persistent P 
676
  (Δ1  P)  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
677
Proof.
678
  intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
679
  rewrite HP sep_elim_l (and_sep_l P) envs_app_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
680
  by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
681 682
Qed.

683 684 685 686 687 688
Lemma tac_assert_pure Δ Δ' j P φ Q :
  envs_app false (Esnoc Enil j P) Δ = Some Δ' 
  FromPure P φ 
  φ  (Δ'  Q)  Δ  Q.
Proof.
  intros ??? <-. rewrite envs_app_sound //; simpl.
689
  by rewrite right_id -(from_pure P) pure_True // -impl_wand True_impl.
690 691
Qed.

692
Lemma tac_pose_proof Δ Δ' j P Q :
693
  P 
694
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
695
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
696
Proof.
697
  intros HP ? <-. rewrite envs_app_sound //; simpl.
698
  by rewrite right_id -HP persistently_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
699 700
Qed.

701 702 703
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 Δ'' 
704
  (Δ''  Q)  Δ  Q.
705 706 707 708 709 710 711 712
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
713
Lemma tac_apply Δ Δ' i p R P1 P2 :
714
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand false R P1 P2 
715
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
716 717
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
718
  by rewrite (into_wand _ R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
719 720 721 722 723
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
724
   {A : ofeT} (x y : A) (Φ : A  uPred M),
725 726
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x))