coq_tactics.v 33.4 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.
4
From iris.prelude Require Import stringmap hlist.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import uPred.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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

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

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.

53 54 55 56 57
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
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
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 Δ).

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

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

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

88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
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
105 106
(* Coq versions of the tactics *)
Section tactics.
107
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
108 109 110 111
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

112
Lemma of_envs_def Δ :
113
  of_envs Δ = ( envs_wf Δ   [] env_persistent Δ  [] env_spatial Δ)%I.
114 115
Proof. done. Qed.

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

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

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

169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190
Lemma envs_lookup_snoc Δ i p P :
  envs_lookup i Δ = None  envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc.
Qed.
Lemma envs_lookup_snoc_ne Δ i j p P :
  i  j  envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne.
Qed.

Lemma envs_snoc_sound Δ p i P :
  envs_lookup i Δ = None  Δ  ?p P - envs_snoc Δ p i P.
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.
      intros j; case_decide; naive_solver.
191
    + by rewrite always_sep assoc.
192 193 194 195 196 197
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
      intros j; case_decide; naive_solver.
    + solve_sep_entails.
Qed.

198
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Proof.
200
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202 203
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
204
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
205 206 207 208
    + 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') //.
209
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
210 211
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
212
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214 215 216 217 218 219 220
    + 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 Δ' 
221
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
222 223
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
224
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
225 226
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
227
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229 230 231
    + 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') //.
232
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
233 234
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
235
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
236 237 238 239 240 241 242 243
    + 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 Δ' 
244
  Δ  ?p P  (?p [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
248
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252 253 254 255 256
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 Δ' 
257
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

260 261 262
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
263
Proof.
264 265 266
  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
267 268
Qed.

269
Lemma envs_clear_spatial_sound Δ : Δ  envs_clear_spatial Δ  [] env_spatial Δ.
270
Proof.
271 272
  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].
273 274 275
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

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

281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
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) 
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2')  Δ1  Δ2  Δ1'  Δ2'.
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 :
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
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.

327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345
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 *.
346 347
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
348 349 350 351 352
      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.
353 354
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
355 356 357 358 359
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
360
(** * Adequacy *)
361
Lemma tac_adequate P : (Envs Enil Enil  P)  True  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Proof.
363 364
  intros <-. rewrite /of_envs /= always_pure !right_id.
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
365 366 367
Qed.

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

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
375
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
376 377 378 379 380
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 :
381
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
382 383 384
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.

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

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

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

400
Lemma tac_pure_revert Δ φ Q : (Δ   φ  Q)  (φ  Δ  Q).
401
Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
402 403

(** * Later *)
404 405 406 407 408
Class IntoLaterEnv (Γ1 Γ2 : env (uPred M)) :=
  into_later_env : env_Forall2 IntoLater Γ1 Γ2.
Class IntoLaterEnvs (Δ1 Δ2 : envs M) := {
  into_later_persistent: IntoLaterEnv (env_persistent Δ1) (env_persistent Δ2);
  into_later_spatial: IntoLaterEnv (env_spatial Δ1) (env_spatial Δ2)
409 410
}.

411
Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
Proof. constructor. Qed.
413 414 415
Global Instance into_later_env_snoc Γ1 Γ2 i P Q :
  IntoLaterEnv Γ1 Γ2  IntoLater P Q 
  IntoLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
416 417
Proof. by constructor. Qed.

418 419 420
Global Instance into_later_envs Γp1 Γp2 Γs1 Γs2 :
  IntoLaterEnv Γp1 Γp2  IntoLaterEnv Γs1 Γs2 
  IntoLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Proof. by split. Qed.
422

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

Lemma tac_next Δ Δ' Q Q' :
434 435
  IntoLaterEnvs Δ Δ'  FromLater Q Q'  (Δ'  Q')  Δ  Q.
Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
436 437

Lemma tac_löb Δ Δ' i Q :
438
  env_spatial_is_nil Δ = true 
439
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
440
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
Proof.
442 443 444 445
  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
446 447 448
Qed.

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

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

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
463
  env_spatial_is_nil Δ = true 
Robbert Krebbers's avatar
Robbert Krebbers committed
464
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
465
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
466 467 468 469 470
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 :
471
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
472
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
473
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
474 475
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
476
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
Qed.
478
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
479
Proof.
480
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
481 482 483
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
484
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
Proof.
486
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
487 488
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
489
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
490
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
491
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
492 493 494 495
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
496
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
497
Proof.
498
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
499 500 501 502 503 504
Qed.

(* 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, Δ') 
505
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
506
  IntoWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
507 508 509 510 511
  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 Δ'' 
512
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
513 514 515
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
516
    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
517
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
518 519
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
520
    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
521 522
Qed.

523
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
524
  envs_lookup_delete j Δ = Some (q, R, Δ') 
525
  IntoWand R P1 P2  ElimModal P1' P1 Q Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
526
  ('(Δ1,Δ2)  envs_split lr js Δ';
527
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
528
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
529
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
Proof.
531
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
532 533 534 535
  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.
536
  rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
537
  rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
538
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
539 540
Qed.

541
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
542
  envs_lookup j Δ = Some (q, R) 
543
  IntoWand R P1 P2  FromPure P1 φ 
544
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
545
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
546
Proof.
547
  intros. rewrite envs_simple_replace_sound //; simpl.
548 549
  rewrite right_id (into_wand R) -(from_pure P1) pure_equiv //.
  by rewrite wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
550 551
Qed.

552
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
553
  envs_lookup_delete j Δ = Some (q, R, Δ') 
554
  IntoWand R P1 P2  PersistentP P1 
555
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571
  (Δ'  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
572
Proof.
573 574 575 576
  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
577 578 579 580
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
581
  (Δ'  if p then  P  Q else P - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
582 583 584 585 586 587
Proof.
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
  - by rewrite HQ -always_and_sep_l impl_elim_r.
  - by rewrite HQ wand_elim_r.
Qed.

588 589 590 591 592 593 594 595 596 597
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.

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

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
611
  (Δ  P)  PersistentP P  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
Proof.
613
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
614 615 616 617
  rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
  by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
Qed.

618 619 620
Lemma tac_pose_proof Δ Δ' j P Q :
  (True  P) 
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
621
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
Proof.
623 624
  intros HP ? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -HP always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
625 626
Qed.

627 628 629
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 Δ'' 
630
  (Δ''  Q)  Δ  Q.
631 632 633 634 635 636 637 638
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
639
Lemma tac_apply Δ Δ' i p R P1 P2 :
640
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand R P1 P2 
641
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
642 643
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
644
  by rewrite (into_wand R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
645 646 647 648 649
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
Ralf Jung's avatar
Ralf Jung committed
650
   {A : cofeT} (x y : A) (Φ : A  uPred M),
651 652
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
653
    ( n, Proper (dist n ==> dist n) Φ) 
654
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
655
Proof.
656
  intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
657
  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
658
  destruct lr; auto using internal_eq_sym.
Robbert Krebbers's avatar
Robbert Krebbers committed
659 660 661 662
Qed.

Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
663
  envs_lookup j Δ = Some (q, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
664
   {A : cofeT} Δ' x y (Φ : A  uPred M),
665 666
    (Pxy  x  y) 
    (P  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
667 668
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
669
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
670 671 672 673
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.
674 675
  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
  rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
676 677 678 679
  - apply (internal_eq_rewrite x y (λ y, ?q Φ y - Δ')%I);
      eauto with I. solve_proper.
  - apply (internal_eq_rewrite y x (λ y, ?q Φ y - Δ')%I);
      eauto using internal_eq_sym with I.
680
    solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
681 682 683
Qed.

(** * Conjunction splitting *)
684 685
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
686 687 688

(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
689
  FromSep P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
690
  envs_split lr js Δ = Some (Δ1,Δ2) 
691
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
692
Proof.
693
  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
694 695 696 697 698 699
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) 
700
  FromSep P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
701 702
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
703
  (Δ4  Q)  Δ1  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
704 705 706 707 708
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.
709
      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
710
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
711
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
712 713
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
714
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
716
      by rewrite right_id assoc (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
717 718 719
Qed.

(** * Conjunction/separating conjunction elimination *)
720 721
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
722
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
723
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
724
Proof.
725
  intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
726
  by destruct p; rewrite /= ?right_id (comm _ P1) ?always_and_sep wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
727 728
Qed.

729 730 731 732 733 734 735 736 737 738 739 740 741 742
(* Using this tactic, one can destruct a (non-separating) conjunction in the
spatial context as long as one of the conjuncts is thrown away. It corresponds
to the principle of "external choice" in linear logic. *)
Lemma tac_and_destruct_choice Δ Δ' i p (lr : bool) j P P1 P2 Q :
  envs_lookup i Δ = Some (p, P)  IntoAnd true P P1 P2 
  envs_simple_replace i p (Esnoc Enil j (if lr then P1 else P2)) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Proof.
  intros. rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id (into_and true P). destruct lr.
  - by rewrite and_elim_l wand_elim_r.
  - by rewrite and_elim_r wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
743
(** * Framing *)
744 745 746 747
Lemma tac_frame_pure Δ (φ : Prop) P Q :
  φ  Frame ( φ) P Q  (Δ  Q)  Δ  P.
Proof. intros ?? ->. by rewrite -(frame ( φ) P) pure_equiv // left_id. Qed.

748 749 750
Lemma tac_frame Δ Δ' i p R P Q :
  envs_lookup_delete i Δ = Some (p, R, Δ')  Frame R P Q 
  ((if p then Δ else Δ')  Q)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
751
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
752
  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
753 754
  - by rewrite envs_lookup_persistent_sound // always_elim -(frame R P) HQ.
  - rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
755 756 757
Qed.

(** * Disjunction *)
758 759 760 761
Lemma tac_or_l Δ P Q1 Q2 : FromOr P Q1 Q2  (Δ  Q1)  Δ  P.
Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
Lemma tac_or_r Δ P Q1 Q2 : FromOr P Q1 Q2  (Δ  Q2)  Δ  P.
Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
762 763

Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
764
  envs_lookup i Δ = Some (p, P)  IntoOr P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
765 766
  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 
  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 
767
  (Δ1  Q)  (Δ2  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
768
Proof.
769
  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
770
  rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
771 772 773 774
  - rewrite (envs_simple_replace_sound' _ Δ1) //.
    by rewrite /= right_id wand_elim_r.
  - rewrite (envs_simple_replace_sound' _ Δ2) //.
    by rewrite /= right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
775 776 777
Qed.

(** * Forall *)
778
Lemma tac_forall_intro {A} Δ (Φ : A  uPred M) : ( a, Δ  Φ a)  Δ   a, Φ a.
Robbert Krebbers's avatar
Robbert Krebbers committed
779 780
Proof. apply forall_intro. Qed.

781
Class ForallSpecialize {As} (xs : hlist As)
782
  (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P  Φ xs.
783 784 785 786 787 788 789 790 791 792 793
Arguments forall_specialize {_} _ _ _ {_}.

Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
Proof. done. Qed.
Global Instance forall_specialize_cons A As x xs Φ (Ψ : A  himpl As (uPred M)) :
  ( x, ForallSpecialize xs (Φ x) (Ψ x)) 
  ForallSpecialize (hcons x xs) ( x : A, Φ x) Ψ.
Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.

Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
  envs_lookup i Δ = Some (p, P)  ForallSpecialize xs P Φ 
794
  envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ' 
795
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
796
Proof.
797 798
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id (forall_specialize _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
799 800 801
Qed.

Lemma tac_forall_revert {A} Δ (Φ : A  uPred M) :
802
  (Δ   a, Φ a)   a, Δ  Φ a.
Robbert Krebbers's avatar
Robbert Krebbers committed
803 804 805
Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.

(** * Existential *)
806 807 808 809
Lemma tac_exist {A} Δ P (Φ : A  uPred M) :
  FromExist P Φ  ( a, Δ  Φ a)  Δ  P.
Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
810
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A  uPred M) Q :
811
  envs_lookup i Δ = Some (p, P)  IntoExist P Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
812
  ( a,  Δ',
813
    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ'  (Δ'  Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
814 815
  Δ  Q.
Proof.
816
  intros ?? HΦ. rewrite envs_lookup_sound //.
817
  rewrite (into_exist P) always_if_exist sep_exist_r.
818 819
  apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
  rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
820
Qed.
821

822 823 824
(** * Modalities *)
Lemma tac_modal_intro Δ P Q : IntoModal Q P  (Δ  Q)  Δ  P.
Proof. rewrite /IntoModal. by intros <- ->. Qed.
825

826
Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
827
  envs_lookup i Δ = Some (p, P) 
828
  ElimModal P P' Q Q' 
829 830 831 832
  envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' 
  (Δ'  Q')  Δ  Q.
Proof.
  intros ??? HΔ. rewrite envs_replace_sound //; simpl.