coq_tactics.v 39.9 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
From iris.algebra Require Export upred.
From iris.algebra Require Import upred_big_op upred_tactics.
From iris.proofmode Require Export environments.
4
From iris.prelude Require Import stringmap hlist.
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6 7 8 9 10 11 12 13
Import uPred.

Local Notation "Γ !! j" := (env_lookup j Γ).
Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
Local Notation "' ( x1 , x2 ) ← y ; z" :=
  (match y with Some (x1,x2) => z | None => None end).
Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
  (match y with Some (x1,x2,x3) => z | None => None end).

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

36 37
Definition envs_dom {M} (Δ : envs M) : list string :=
  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79

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.

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 81
(* if [lr = false] then [result = (hyps named js, remaining hyps)],
   if [lr = true] then [result = (remaining hyps, hyps named js)] *)
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84 85 86 87 88 89 90 91 92 93
Definition envs_split {M}
    (lr : bool) (js : list string) (Δ : envs M) : option (envs M * envs M) :=
  let (Γp,Γs) := Δ in
  '(Γs1,Γs2)  env_split js Γs;
  match lr with
  | false  => Some (Envs Γp Γs1, Envs Γp Γs2)
  | true => Some (Envs Γp Γs2, Envs Γp Γs1)
  end.

Definition envs_persistent {M} (Δ : envs M) :=
  if env_spatial Δ is Enil then true else false.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
97 98
(* Coq versions of the tactics *)
Section tactics.
99
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
100 101 102 103
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

104
Lemma of_envs_def Δ :
105
  of_envs Δ = ( envs_wf Δ   [] env_persistent Δ  [] env_spatial Δ)%I.
106 107
Proof. done. Qed.

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

Lemma envs_lookup_split Δ i p P :
142
  envs_lookup i Δ = Some (p,P)  Δ  ?p P  (?p P - Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144 145 146 147 148 149 150 151 152 153 154
Proof.
  rewrite /envs_lookup /of_envs=>?; apply const_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
    rewrite const_equiv // left_id.
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=. rewrite const_equiv // left_id.
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
155
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  ?p P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
158
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  P  Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

161
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163 164 165 166 167 168 169 170 171
Proof.
  rewrite /of_envs /envs_app=> ?; apply const_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + 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') //.
172 173
      rewrite big_and_app always_and_sep always_sep (big_sep_and Γ).
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
174 175 176 177 178 179 180 181 182 183 184
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + 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 Δ' 
185
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187 188 189 190 191 192 193 194 195
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
  apply const_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + 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') //.
196 197
      rewrite big_and_app always_and_sep always_sep (big_sep_and Γ).
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
198 199 200 201 202 203 204 205 206 207 208
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + 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 Δ' 
209
  Δ  ?p P  (?p [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
210 211 212
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
213
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
214 215 216 217 218 219 220 221
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 Δ' 
222
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224 225
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

Lemma envs_split_sound Δ lr js Δ1 Δ2 :
226
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228 229 230
Proof.
  rewrite /envs_split /of_envs=> ?; apply const_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=.
  rewrite (env_split_perm Γs) // big_sep_app {1}always_sep_dup'.
231
  destruct lr; simplify_eq/=; cancel [ [] Γp;  [] Γp; [] Γs1; [] Γs2]%I;
Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235 236
    destruct Hwf; apply sep_intro_True_l; apply const_intro; constructor;
      naive_solver eauto using env_split_wf_1, env_split_wf_2,
      env_split_fresh_1, env_split_fresh_2.
Qed.

237
Lemma envs_clear_spatial_sound Δ : Δ  envs_clear_spatial Δ  [] env_spatial Δ.
238 239 240 241 242 243
Proof.
  rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
  rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

244
Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ  ([] Γ - Q).
245 246 247 248 249 250
Proof.
  revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
  by rewrite IH wand_curry (comm uPred_sep).
Qed.

Lemma envs_persistent_persistent Δ : envs_persistent Δ = true  PersistentP Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
252
Hint Immediate envs_persistent_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
253

254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
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 *.
  apply const_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply const_intro; constructor;
      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.
  intros Δ1 Δ2 ?; apply (anti_symm ()); apply of_envs_mono;
    eapply envs_Forall2_impl; [| |symmetry|]; eauto using equiv_entails.
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
287
(** * Adequacy *)
288
Lemma tac_adequate P : (Envs Enil Enil  P)  True  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
289 290 291 292 293 294
Proof.
  intros <-. rewrite /of_envs /= always_const !right_id.
  apply const_intro; repeat constructor.
Qed.

(** * Basic rules *)
295
Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : ?p P  Q.
296
Arguments to_assumption _ _ _ {_}.
297
Global Instance to_assumption_exact p P : ToAssumption p P P.
298
Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
299 300 301 302
Global Instance to_assumption_always_l p P Q :
  ToAssumption p P Q  ToAssumption p ( P) Q.
Proof. rewrite /ToAssumption=><-. by rewrite always_elim. Qed.
Global Instance to_assumption_always_r P Q :
303 304 305 306 307 308
  ToAssumption true P Q  ToAssumption true P ( Q).
Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.

Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p,P)  ToAssumption p P Q  Δ  Q.
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
309 310 311 312

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
313
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315 316 317 318
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 :
319
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
321
Lemma tac_clear_spatial Δ Δ' Q :
322
  envs_clear_spatial Δ = Δ'  (Δ'  Q)  Δ  Q.
323
Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
324 325

(** * False *)
326
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
327 328 329
Proof. by rewrite -(False_elim Q). Qed.

(** * Pure *)
330
Class ToPure (P : uPred M) (φ : Prop) := to_pure : P   φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
331 332 333 334 335 336 337 338 339
Arguments to_pure : clear implicits.
Global Instance to_pure_const φ : ToPure ( φ) φ.
Proof. done. Qed.
Global Instance to_pure_eq {A : cofeT} (a b : A) :
  Timeless a  ToPure (a  b) (a  b).
Proof. intros; red. by rewrite timeless_eq. Qed.
Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure ( a) ( a).
Proof. intros; red. by rewrite discrete_valid. Qed.

340 341 342
Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ  φ  Δ  Q.
Proof. intros ->. apply const_intro. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
343 344 345 346 347 348 349 350
Lemma tac_pure Δ Δ' i p P φ Q :
  envs_lookup_delete i Δ = Some (p, P, Δ')  ToPure P φ 
  (φ  Δ'  Q)  Δ  Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
  rewrite (to_pure P); by apply const_elim_sep_l.
Qed.

351
Lemma tac_pure_revert Δ φ Q : (Δ   φ  Q)  (φ  Δ  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382
Proof. intros HΔ ?. by rewrite HΔ const_equiv // left_id. Qed.

(** * Later *)
Class StripLaterEnv (Γ1 Γ2 : env (uPred M)) :=
  strip_later_env : env_Forall2 StripLaterR Γ1 Γ2.
Global Instance strip_later_env_nil : StripLaterEnv Enil Enil.
Proof. constructor. Qed.
Global Instance strip_later_env_snoc Γ1 Γ2 i P Q :
  StripLaterEnv Γ1 Γ2  StripLaterR P Q 
  StripLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.

Class StripLaterEnvs (Δ1 Δ2 : envs M) := {
  strip_later_persistent: StripLaterEnv (env_persistent Δ1) (env_persistent Δ2);
  strip_later_spatial: StripLaterEnv (env_spatial Δ1) (env_spatial Δ2)
}.
Global Instance strip_later_envs Γp1 Γp2 Γs1 Γs2 :
  StripLaterEnv Γp1 Γp2  StripLaterEnv Γs1 Γs2 
  StripLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Proof. by split. Qed.
Lemma strip_later_env_sound Δ1 Δ2 : StripLaterEnvs Δ1 Δ2  Δ1   Δ2.
Proof.
  intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
  repeat apply sep_mono; try apply always_mono.
  - rewrite -later_intro; apply const_mono; destruct 1; constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - induction Hp; rewrite /= ?later_and; auto using and_mono, later_intro.
  - induction Hs; rewrite /= ?later_sep; auto using sep_mono, later_intro.
Qed.

Lemma tac_next Δ Δ' Q Q' :
383
  StripLaterEnvs Δ Δ'  StripLaterL Q Q'  (Δ'  Q')  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
384 385 386
Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.

Lemma tac_löb Δ Δ' i Q :
387 388
  envs_persistent Δ = true 
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
389
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
390
Proof.
391 392 393 394
  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
395 396 397
Qed.

(** * Always *)
398
Lemma tac_always_intro Δ Q : envs_persistent Δ = true  (Δ  Q)  Δ   Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
399 400 401 402 403 404 405 406 407 408 409 410 411 412
Proof. intros. by apply: always_intro. Qed.

Class ToPersistentP (P Q : uPred M) := to_persistentP : P   Q.
Arguments to_persistentP : clear implicits.
Global Instance to_persistentP_always_trans P Q :
  ToPersistentP P Q  ToPersistentP ( P) Q | 0.
Proof. rewrite /ToPersistentP=> ->. by rewrite always_always. Qed.
Global Instance to_persistentP_always P : ToPersistentP ( P) P | 1.
Proof. done. Qed.
Global Instance to_persistentP_persistent P :
  PersistentP P  ToPersistentP P P | 100.
Proof. done. Qed.

Lemma tac_persistent Δ Δ' i p P P' Q :
413
  envs_lookup i Δ = Some (p, P)  ToPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
414
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
415
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
416
Proof.
417 418
  intros ??? <-. rewrite envs_replace_sound //; simpl.
  by rewrite right_id (to_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
419 420 421 422 423 424
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
  envs_persistent Δ = true 
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
425
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
426 427 428 429 430 431 432
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 :
  ToPersistentP P P' 
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
433
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
434 435 436 437
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
  by rewrite right_id {1}(to_persistentP P) always_and_sep_l wand_elim_r.
Qed.
438
Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
439 440 441 442 443
Proof.
  intros. by apply impl_intro_l; rewrite (to_pure P); apply const_elim_l.
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
444
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
445
Proof.
446
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
447 448 449 450
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
  ToPersistentP P P' 
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
451
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
452 453 454 455
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
456
Lemma tac_wand_intro_pure Δ P φ Q : ToPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
457 458 459 460
Proof.
  intros. by apply wand_intro_l; rewrite (to_pure P); apply const_elim_sep_l.
Qed.

461
Class ToWand (R P Q : uPred M) := to_wand : R  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
462 463 464 465 466 467 468 469 470
Arguments to_wand : clear implicits.
Global Instance to_wand_wand P Q : ToWand (P - Q) P Q.
Proof. done. Qed.
Global Instance to_wand_impl P Q : ToWand (P  Q) P Q.
Proof. apply impl_wand. Qed.
Global Instance to_wand_iff_l P Q : ToWand (P  Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance to_wand_iff_r P Q : ToWand (P  Q) Q P.
Proof. apply and_elim_r', impl_wand. Qed.
471 472
Global Instance to_wand_always R P Q : ToWand R P Q  ToWand ( R) P Q.
+Proof. rewrite /ToWand=> ->. apply always_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
473 474 475 476 477

(* 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, Δ') 
478
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
479 480 481 482 483 484
  ToWand R P1 P2 
  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 Δ'' 
485
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
486 487 488
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
489 490
    rewrite assoc (to_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
491 492
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
493
    by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
494 495
Qed.

496
Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
497
  to_assert : R  (P - Q)  Q.
498 499 500 501 502
Global Arguments to_assert _ _ _ {_}.
Lemma to_assert_fallthrough P Q : ToAssert P Q P.
Proof. by rewrite /ToAssert wand_elim_r. Qed.

Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
503
  envs_lookup_delete j Δ = Some (q, R, Δ') 
504
  ToWand R P1 P2  ToAssert P1 Q P1' 
Robbert Krebbers's avatar
Robbert Krebbers committed
505
  ('(Δ1,Δ2)  envs_split lr js Δ';
506
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
507
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
508
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
509
Proof.
510
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
511 512 513 514
  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.
515 516 517
  rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
  rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
518 519
Qed.

520 521 522 523
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
  envs_lookup j Δ = Some (q, R) 
  ToWand R P1 P2  ToPure P1 φ 
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
524
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
Proof.
526 527
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id (to_wand R) (to_pure P1) const_equiv // wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529
Qed.

530 531 532 533
Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
  ToWand R P1 P2 
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
534 535
  (Δ'  P1)  (PersistentP P1  PersistentP P2) 
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Proof.
537 538 539 540 541 542 543 544 545 546 547
  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 (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
    by rewrite wand_elim_r.
  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
    rewrite envs_simple_replace_sound //; simpl.
    rewrite (sep_elim_r _ (_ - _)) right_id (to_wand R) always_if_elim.
    by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
548 549 550 551
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
552
  (Δ'  if p then  P  Q else P - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
553 554 555 556 557 558
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.

559
Lemma tac_revert_spatial Δ Q :
560
  (envs_clear_spatial Δ  env_fold uPred_wand Q (env_spatial Δ))  Δ  Q.
561 562 563 564
Proof.
  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed.

565 566
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
  ToAssert P Q R 
Robbert Krebbers's avatar
Robbert Krebbers committed
567
  envs_split lr js Δ = Some (Δ1,Δ2) 
568
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
569
  (Δ1  R)  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
570
Proof.
571
  intros ??? HP HQ. rewrite envs_split_sound //.
572
  rewrite (envs_app_sound Δ2) //; simpl.
573
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
574 575 576 577
Qed.

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
578
  (Δ  P)  PersistentP P  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
579
Proof.
580
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
581 582 583 584
  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.

585
(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
586 587 588
not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the
[True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
589
Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : (P1  P2)  True  R.
590 591 592 593 594 595 596
Arguments to_pose_proof : clear implicits.
Instance to_posed_proof_True P : ToPosedProof True P P.
Proof. by rewrite /ToPosedProof. Qed.
Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P - Q).
Proof. rewrite /ToPosedProof. apply entails_wand. Qed.

Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
597 598
  (P1  P2)  ToPosedProof P1 P2 R  envs_app true (Esnoc Enil j R) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
Proof.
600 601
  intros HP ?? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
602 603
Qed.

604 605 606
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 Δ'' 
607
  (Δ''  Q)  Δ  Q.
608 609 610 611 612 613 614 615
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
616
Lemma tac_apply Δ Δ' i p R P1 P2 :
617
  envs_lookup_delete i Δ = Some (p, R, Δ')  ToWand R P1 P2 
618
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
619 620 621 622 623 624 625 626
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
  by rewrite (to_wand R) HP1 wand_elim_l.
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
Ralf Jung's avatar
Ralf Jung committed
627
   {A : cofeT} (x y : A) (Φ : A  uPred M),
628 629
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
630
    ( n, Proper (dist n ==> dist n) Φ) 
631
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
632 633 634 635 636 637 638 639
Proof.
  intros ? A x y ? HPxy -> ?; apply eq_rewrite; auto.
  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
  destruct lr; auto using eq_sym.
Qed.

Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
640
  envs_lookup j Δ = Some (q, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
641
   {A : cofeT} Δ' x y (Φ : A  uPred M),
642 643
    (Pxy  x  y) 
    (P  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
644 645
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
646
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
647 648 649 650
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.
651 652 653 654 655
  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
  rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
  - apply (eq_rewrite x y (λ y, ?q Φ y - Δ')%I); eauto with I. solve_proper.
  - apply (eq_rewrite y x (λ y, ?q Φ y - Δ')%I); eauto using eq_sym with I.
    solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
656 657 658
Qed.

(** * Conjunction splitting *)
659
Class AndSplit (P Q1 Q2 : uPred M) := and_split : Q1  Q2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
660 661 662 663 664 665 666 667 668 669 670
Arguments and_split : clear implicits.

Global Instance and_split_and P1 P2 : AndSplit (P1  P2) P1 P2.
Proof. done. Qed.
Global Instance and_split_sep_persistent_l P1 P2 :
  PersistentP P1  AndSplit (P1  P2) P1 P2.
Proof. intros. by rewrite /AndSplit always_and_sep_l. Qed.
Global Instance and_split_sep_persistent_r P1 P2 :
  PersistentP P2  AndSplit (P1  P2) P1 P2.
Proof. intros. by rewrite /AndSplit always_and_sep_r. Qed.

671
Lemma tac_and_split Δ P Q1 Q2 : AndSplit P Q1 Q2  (Δ  Q1)  (Δ  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
672 673 674
Proof. intros. rewrite -(and_split P). by apply and_intro. Qed.

(** * Separating conjunction splitting *)
675
Class SepSplit (P Q1 Q2 : uPred M) := sep_split : Q1  Q2  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
676 677 678 679 680 681 682
Arguments sep_split : clear implicits.

Global Instance sep_split_sep P1 P2 : SepSplit (P1  P2) P1 P2 | 100.
Proof. done. Qed.
Global Instance sep_split_ownM (a b : M) :
  SepSplit (uPred_ownM (a  b)) (uPred_ownM a) (uPred_ownM b) | 99.
Proof. by rewrite /SepSplit ownM_op. Qed.
683 684 685 686 687 688 689 690 691 692 693 694 695 696
Global Instance sep_split_big_sepM
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) m :
  ( k x, SepSplit (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
  SepSplit ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
Proof.
  rewrite /SepSplit=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
Qed.
Global Instance sep_split_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) X :
  ( x, SepSplit (Φ x) (Ψ1 x) (Ψ2 x)) 
  SepSplit ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
Proof.
  rewrite /SepSplit=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
697 698 699 700

Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
  SepSplit P Q1 Q2 
  envs_split lr js Δ = Some (Δ1,Δ2) 
701
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
702 703 704 705 706 707 708 709 710 711 712
Proof.
  intros. rewrite envs_split_sound // -(sep_split P). by apply sep_mono.
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) 
  SepSplit P P1 P2 
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
713
  (Δ4  Q)  Δ1  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730
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.
      by rewrite right_id assoc -always_sep (sep_split P) wand_elim_r.
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
      by rewrite right_id assoc (sep_split P) wand_elim_r.
Qed.

(** * Conjunction/separating conjunction elimination *)
Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
731
  sep_destruct : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
732
Arguments sep_destruct : clear implicits.
733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749
Class OpDestruct {A : cmraT} (a b1 b2 : A) :=
  op_destruct : a  b1  b2.
Arguments op_destruct {_} _ _ _ {_}.

Global Instance op_destruct_op {A : cmraT} (a b : A) : OpDestruct (a  b) a b.
Proof. by rewrite /OpDestruct. Qed.
Global Instance op_destruct_persistent {A : cmraT} (a : A) :
  Persistent a  OpDestruct a a a.
Proof. intros; apply (persistent_dup a). Qed.
Global Instance op_destruct_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
  OpDestruct a b1 b2  OpDestruct a' b1' b2' 
  OpDestruct (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
Global Instance op_destruct_Some {A : cmraT} (a : A) b1 b2 :
  OpDestruct a b1 b2  OpDestruct (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
750
Global Instance sep_destruct_sep p P Q : SepDestruct p (P  Q) P Q.
751 752 753 754 755 756 757
Proof. rewrite /SepDestruct. by rewrite always_if_sep. Qed.
Global Instance sep_destruct_ownM p (a b1 b2 : M) :
  OpDestruct a b1 b2 
  SepDestruct p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
  rewrite /OpDestruct /SepDestruct=> ->. by rewrite ownM_op always_if_sep.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
758 759

Global Instance sep_destruct_and P Q : SepDestruct true (P  Q) P Q.
760
Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
761 762
Global Instance sep_destruct_and_persistent_l P Q :
  PersistentP P  SepDestruct false (P  Q) P Q.
763
Proof. intros; by rewrite /SepDestruct /= always_and_sep_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
764 765
Global Instance sep_destruct_and_persistent_r P Q :
  PersistentP Q  SepDestruct false (P  Q) P Q.
766
Proof. intros; by rewrite /SepDestruct /= always_and_sep_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
767 768 769

Global Instance sep_destruct_later p P Q1 Q2 :
  SepDestruct p P Q1 Q2  SepDestruct p ( P) ( Q1) ( Q2).
770
Proof. by rewrite /SepDestruct -later_sep !always_if_later=> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
771

772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
Global Instance sep_destruct_big_sepM
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) p m :
  ( k x, SepDestruct p (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
  SepDestruct p ([ map] k  x  m, Φ k x)
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
Proof.
  rewrite /SepDestruct=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
  by apply big_sepM_mono.
Qed.
Global Instance sep_destruct_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) p X :
  ( x, SepDestruct p (Φ x) (Ψ1 x) (Ψ2 x)) 
  SepDestruct p ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
Proof.
  rewrite /SepDestruct=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
  by apply big_sepS_mono.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
789
Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
790
  envs_lookup i Δ = Some (p, P)  SepDestruct p P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
791
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
792
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
793
Proof.
794 795
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite (sep_destruct p P) right_id (comm uPred_sep P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
796 797 798
Qed.

(** * Framing *)
Robbert Krebbers's avatar
Robbert Krebbers committed
799 800 801
(** The [option] is to account for formulas that can be framed entirely, so
we do not end up with [True]s everywhere. *)
Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
802
  frame : R  from_option id True mQ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
803 804
Arguments frame : clear implicits.

805
Global Instance frame_here R : Frame R R None.
Robbert Krebbers's avatar
Robbert Krebbers committed
806
Proof. by rewrite /Frame right_id. Qed.
807
Global Instance frame_sep_l R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
808
  Frame R P1 mQ 
809
  Frame R (P1  P2) (Some $ if mQ is Some Q then Q  P2 else P2)%I | 9.
Robbert Krebbers's avatar
Robbert Krebbers committed
810
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
811
Global Instance frame_sep_r R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
812
  Frame R P2 mQ 
813
  Frame R (P1  P2) (Some $ if mQ is Some Q then P1  Q else P1)%I | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
814
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
815
Global Instance frame_and_l R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
816
  Frame R P1 mQ 
817
  Frame R (P1  P2) (Some $ if mQ is Some Q then Q  P2 else P2)%I | 9.
Robbert Krebbers's avatar
Robbert Krebbers committed
818
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
819
Global Instance frame_and_r R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
820
  Frame R P2 mQ 
821
  Frame R (P1  P2) (Some $ if mQ is Some Q then P1  Q else P1)%I | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
822
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
823
Global Instance frame_or R P1 P2 mQ1 mQ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
824 825 826 827 828 829 830 831 832
  Frame R P1 mQ1  Frame R P2 mQ2 
  Frame R (P1  P2) (match mQ1, mQ2 with
                     | Some Q1, Some Q2 => Some (Q1  Q2)%I | _, _ => None
                     end).
Proof.
  rewrite /Frame=> <- <-.
  destruct mQ1 as [Q1|], mQ2 as [Q2|]; simpl; auto with I.
  by rewrite -sep_or_l.
Qed.
833
Global Instance frame_later R P mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
834 835 836 837 838
  Frame R P mQ  Frame R ( P) (if mQ is Some Q then Some ( Q) else None)%I.
Proof.
  rewrite /Frame=><-.
  by destruct mQ; rewrite /= later_sep -(later_intro R) ?later_True.
Qed.
839
Global Instance frame_exist {A} R (Φ : A  uPred M) mΨ :
Robbert Krebbers's avatar
Robbert Krebbers committed
840 841
  ( a, Frame R (Φ a) (mΨ a)) 
  Frame R ( x, Φ x) (Some ( x, if mΨ x is Some Q then Q else True))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
842
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
843
Global Instance frame_forall {A} R (Φ : A  uPred M) mΨ :
Robbert Krebbers's avatar
Robbert Krebbers committed
844 845
  ( a, Frame R (Φ a) (mΨ a)) 
  Frame R ( x, Φ x) (Some ( x, if mΨ x is Some Q then Q else True))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
846 847
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
848
Lemma tac_frame Δ Δ' i p R P mQ :
849
  envs_lookup_delete i Δ = Some (p, R, Δ')  Frame R P mQ 
Robbert Krebbers's avatar
Robbert Krebbers committed
850 851
  (if mQ is Some Q then (if p then Δ else Δ')  Q else True) 
  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
852