coq_tactics.v 39.1 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 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
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).

Record envs (M : cmraT) :=
  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 :=
  ( 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 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 80 81 82 83 84 85 86 87 88 89 90 91 92 93

Instance envs_dom {M} : Dom (envs M) stringset := λ Δ,
  dom stringset (env_persistent Δ)  dom stringset (env_spatial Δ).

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 Δ).

(* if [lr = false] then [result = (hyps named js,remainding hyps)],
   if [lr = true] then [result = (remainding hyps,hyps named js)] *)
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 99 100 101 102 103
(* Coq versions of the tactics *)
Section tactics.
Context {M : cmraT}.
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
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 :
  envs_lookup i Δ = Some (p,P) 
  Δ  ((if p then  P else P)  envs_delete i p Δ).
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.
    ecancel [ Π _;  P; Π★ _]%I; apply const_intro.
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
    ecancel [ Π _; P; Π★ _]%I; apply const_intro.
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
  envs_lookup i Δ = Some (p,P)  Δ  (P  envs_delete i p Δ).
Proof.
  intros. rewrite envs_lookup_sound //. by destruct p; rewrite ?always_elim.
Qed.
Lemma envs_lookup_persistent_sound Δ i P :
  envs_lookup i Δ = Some (true,P)  Δ  ( P  Δ).
Proof.
  intros. apply: always_entails_l. by rewrite envs_lookup_sound // sep_elim_l.
Qed.

Lemma envs_lookup_split Δ i p P :
  envs_lookup i Δ = Some (p,P) 
  Δ  ((if p then  P else P)  ((if p then  P else P) - Δ)).
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 :
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  ((if p then  P else P)  Δ')%I.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  (P  Δ')%I.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

Lemma envs_app_sound Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ'  Δ  ((if p then  Π Γ else Π★ Γ) - Δ').
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') //.
      rewrite big_and_app always_and_sep always_sep; solve_sep_entails.
  - 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 Δ' 
  envs_delete i p Δ  ((if p then  Π Γ else Π★ Γ) - Δ')%I.
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') //.
      rewrite big_and_app always_and_sep always_sep; solve_sep_entails.
  - 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 Δ' 
  Δ  ((if p then  P else P) 
       ((if p then  Π Γ else Π★ Γ) - Δ'))%I.
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

Lemma envs_replace_sound' Δ Δ' i p q Γ :
  envs_replace i p q Γ Δ = Some Δ' 
  envs_delete i p Δ  ((if q then  Π Γ else Π★ Γ) - Δ')%I.
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 Δ' 
  Δ  ((if p then  P else P) 
       ((if q then  Π Γ else Π★ Γ) - Δ'))%I.
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

Lemma envs_split_sound Δ lr js Δ1 Δ2 :
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  (Δ1  Δ2).
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'.
  destruct lr; simplify_eq/=; cancel [ Π Γp;  Π Γp; Π★ Γs1; Π★ Γs2]%I;
    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.

243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
Lemma envs_clear_spatial_sound Δ :
  Δ  (envs_clear_spatial Δ  Π★ env_spatial Δ)%I.
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.

Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ  (Π★ Γ - Q).
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
258
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
259
Hint Immediate envs_persistent_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 287 288 289 290 291 292 293
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
294 295 296 297 298 299 300 301
(** * Adequacy *)
Lemma tac_adequate P : Envs Enil Enil  P  True  P.
Proof.
  intros <-. rewrite /of_envs /= always_const !right_id.
  apply const_intro; repeat constructor.
Qed.

(** * Basic rules *)
302 303 304 305 306 307 308 309 310 311 312
Class ToAssumption (p : bool) (P Q : uPred M) :=
  to_assumption : (if p then  P else P)  Q.
Global Instance to_assumption_exact p P : ToAssumption p P P.
Proof. destruct p; by rewrite /ToAssumption ?always_elim. Qed.
Global Instance to_assumption_always P Q :
  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
313 314 315 316 317 318 319 320 321 322 323 324

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
  Δ'  Q  Δ  Q.
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 :
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ'  Q  Δ  Q.
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
325 326 327
Lemma tac_clear_spatial Δ Δ' Q :
  envs_clear_spatial Δ = Δ'  Δ'  Q  Δ  Q.
Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328 329 330 331 332 333

(** * False *)
Lemma tac_ex_falso Δ Q : Δ  False  Δ  Q.
Proof. by rewrite -(False_elim Q). Qed.

(** * Pure *)
334
Class ToPure (P : uPred M) (φ : Prop) := to_pure : P   φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
335 336 337 338 339 340 341 342 343
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.

344 345 346
Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ  φ  Δ  Q.
Proof. intros ->. apply const_intro. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
347 348 349 350 351 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 383 384 385 386 387 388 389 390
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.

Lemma tac_pure_revert Δ φ Q : Δ  ( φ  Q)  (φ  Δ  Q).
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' :
  StripLaterEnvs Δ Δ'  StripLaterL Q Q'  Δ'  Q'  Δ  Q.
Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.

Lemma tac_löb Δ Δ' i Q :
391 392
  envs_persistent Δ = true 
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
393 394
  Δ'  Q  Δ  Q.
Proof.
395 396 397 398
  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
399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563
Qed.

(** * Always *)
Lemma tac_always_intro Δ Q : envs_persistent Δ = true  Δ  Q  Δ   Q.
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 :
  envs_lookup i Δ = Some (p, P)%I  ToPersistentP P P' 
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
  Δ'  Q  Δ  Q.
Proof.
  intros ??? <-. rewrite envs_replace_sound //; simpl. destruct p.
  - by rewrite right_id (to_persistentP P) always_always wand_elim_r.
  - by rewrite right_id (to_persistentP P) wand_elim_r.
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
  envs_persistent Δ = true 
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  Q  Δ  (P  Q).
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 Δ' 
  Δ'  Q  Δ  (P  Q).
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.
Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ  (φ  Δ  Q)  Δ  (P  Q).
Proof.
  intros. by apply impl_intro_l; rewrite (to_pure P); apply const_elim_l.
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  Δ'  Q  Δ  (P - Q).
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
  ToPersistentP P P' 
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
  Δ'  Q  Δ  (P - Q).
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
Lemma tac_wand_intro_pure Δ P φ Q : ToPure P φ  (φ  Δ  Q)  Δ  (P - Q).
Proof.
  intros. by apply wand_intro_l; rewrite (to_pure P); apply const_elim_sep_l.
Qed.

Class ToWand (R P Q : uPred M) := to_wand : R  (P - Q).
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.

(* 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, Δ') 
  envs_lookup j (if p then Δ else Δ') = Some (q, R)%I 
  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 Δ'' 
  Δ''  Q  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
    destruct q.
    + by rewrite assoc (to_wand R) always_wand wand_elim_r right_id wand_elim_r.
    + by rewrite assoc (to_wand R) always_elim wand_elim_r right_id wand_elim_r.
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
    destruct q.
    + by rewrite right_id assoc (to_wand R) always_elim wand_elim_r wand_elim_r.
    + by rewrite assoc (to_wand R) wand_elim_r right_id wand_elim_r.
Qed.

Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ')%I 
  ToWand R P1 P2 
  ('(Δ1,Δ2)  envs_split lr js Δ';
    Δ2'  envs_app (envs_persistent Δ1 && q) (Esnoc Enil j P2) Δ2;
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
  Δ1  P1  Δ2'  Q  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ?? HP1 <-.
  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.
  destruct q, (envs_persistent Δ1) eqn:?; simplify_eq/=.
  - rewrite right_id (to_wand R) (persistentP Δ1) HP1.
    by rewrite assoc -always_sep wand_elim_l wand_elim_r.
  - by rewrite right_id (to_wand R) always_elim assoc HP1 wand_elim_l wand_elim_r.
  - by rewrite right_id (to_wand R) assoc HP1 wand_elim_l wand_elim_r.
  - by rewrite right_id (to_wand R) assoc HP1 wand_elim_l wand_elim_r. 
Qed.

Lemma tac_specialize_range_persistent Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ')%I 
  ToWand R P1 P2  PersistentP P1 
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
  Δ'  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. destruct q.
  - by rewrite right_id (to_wand R) -always_sep wand_elim_l wand_elim_r.
  - by rewrite right_id (to_wand R) always_elim wand_elim_l wand_elim_r.
Qed.

Lemma tac_specialize_domain_persistent Δ Δ' Δ'' j q P1 P2 P2' R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ')%I 
  ToWand R P1 P2  ToPersistentP P2 P2' 
  envs_replace j q true (Esnoc Enil j P2') Δ = Some Δ'' 
  Δ'  P1  Δ''  Q  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
  rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
  rewrite envs_replace_sound //; simpl.
  rewrite (sep_elim_r _ (_ - _)) right_id. destruct q.
  - rewrite (to_wand R) always_elim wand_elim_l.
    by rewrite (to_persistentP P2) always_and_sep_l' wand_elim_r.
  - rewrite (to_wand R) wand_elim_l.
    by rewrite (to_persistentP P2) always_and_sep_l' wand_elim_r.
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  Δ'  (if p then  P  Q else P - Q)  Δ  Q.
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.

564 565 566 567 568 569
Lemma tac_revert_spatial Δ Q :
  envs_clear_spatial Δ  (env_fold uPred_wand Q (env_spatial Δ))  Δ  Q.
Proof.
  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q :
  envs_split lr js Δ = Some (Δ1,Δ2) 
  envs_app (envs_persistent Δ1) (Esnoc Enil j P) Δ2 = Some Δ2' 
  Δ1  P  Δ2'  Q  Δ  Q.
Proof.
  intros ?? HP ?. rewrite envs_split_sound //.
  destruct (envs_persistent Δ1) eqn:?.
  - rewrite (persistentP Δ1) HP envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite HP envs_app_sound //; simpl. by rewrite right_id wand_elim_r.
Qed.

Lemma tac_assert_persistent Δ Δ' j P Q :
  PersistentP P 
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
  Δ  P  Δ'  Q  Δ  Q.
Proof.
  intros ?? HP ?.
  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.

592
(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
593 594 595 596 597 598 599 600 601 602 603 604
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. *)
Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : P1  P2  True  R.
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 :
  P1  P2  ToPosedProof P1 P2 R  envs_app true (Esnoc Enil j R) Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
605 606
  Δ'  Q  Δ  Q.
Proof.
607 608
  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
609 610
Qed.

611 612 613 614 615 616 617 618 619 620 621 622
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 Δ'' 
  Δ''  Q  Δ  Q.
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
623 624 625 626 627 628 629 630 631 632 633
Lemma tac_apply Δ Δ' i p R P1 P2 :
  envs_lookup_delete i Δ = Some (p, R, Δ')%I  ToWand R P1 P2 
  Δ'  P1  Δ  P2.
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
634
   {A : cofeT} (x y : A) (Φ : A  uPred M),
Robbert Krebbers's avatar
Robbert Krebbers committed
635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766
    Pxy  (x  y)%I 
    Q  Φ (if lr then y else x) 
    ( n, Proper (dist n ==> dist n) Φ) 
    Δ  Φ (if lr then x else y)  Δ  Q.
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) 
  envs_lookup j Δ = Some (q, P)%I 
   {A : cofeT} Δ' x y (Φ : A  uPred M),
    Pxy  (x  y)%I 
    P  Φ (if lr then y else x) 
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
    Δ'  Q  Δ  Q.
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.
  rewrite (envs_simple_replace_sound _ _ j) //; simpl. destruct q.
  - rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
    + apply (eq_rewrite x y (λ y,  Φ y - Δ')%I); eauto with I. solve_proper.
    + apply (eq_rewrite y x (λ y,  Φ y - Δ')%I); eauto using eq_sym with I.
      solve_proper.
  - rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
    + apply (eq_rewrite x y (λ y, Φ y - Δ')%I); eauto with I. solve_proper.
    + apply (eq_rewrite y x (λ y, Φ y - Δ')%I); eauto using eq_sym with I.
      solve_proper.
Qed.

(** * Conjunction splitting *)
Class AndSplit (P Q1 Q2 : uPred M) := and_split : (Q1  Q2)  P.
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.

Lemma tac_and_split Δ P Q1 Q2 : AndSplit P Q1 Q2  Δ  Q1  Δ  Q2  Δ  P.
Proof. intros. rewrite -(and_split P). by apply and_intro. Qed.

(** * Separating conjunction splitting *)
Class SepSplit (P Q1 Q2 : uPred M) := sep_split : (Q1  Q2)  P.
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.

Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
  SepSplit P Q1 Q2 
  envs_split lr js Δ = Some (Δ1,Δ2) 
  Δ1  Q1  Δ2  Q2  Δ  P.
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 
  Δ4  Q  Δ1  Q.
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) :=
  sep_destruct : if p then  P   (Q1  Q2) else P  (Q1  Q2).
Arguments sep_destruct : clear implicits.
Lemma sep_destruct_spatial p P Q1 Q2 : P  (Q1  Q2)  SepDestruct p P Q1 Q2.
Proof. destruct p; simpl=>->; by rewrite ?sep_and. Qed.

Global Instance sep_destruct_sep p P Q : SepDestruct p (P  Q) P Q.
Proof. by apply sep_destruct_spatial. Qed.
Global Instance sep_destruct_ownM p (a b : M) :
  SepDestruct p (uPred_ownM (a  b)) (uPred_ownM a) (uPred_ownM b).
Proof. apply sep_destruct_spatial. by rewrite ownM_op. Qed.

Global Instance sep_destruct_and P Q : SepDestruct true (P  Q) P Q.
Proof. done. Qed.
Global Instance sep_destruct_and_persistent_l P Q :
  PersistentP P  SepDestruct false (P  Q) P Q.
Proof. intros; red. by rewrite always_and_sep_l. Qed.
Global Instance sep_destruct_and_persistent_r P Q :
  PersistentP Q  SepDestruct false (P  Q) P Q.
Proof. intros; red. by rewrite always_and_sep_r. Qed.

Global Instance sep_destruct_later p P Q1 Q2 :
  SepDestruct p P Q1 Q2  SepDestruct p ( P) ( Q1) ( Q2).
Proof.
  destruct p=> /= HP.
  - by rewrite -later_and !always_later HP.
  - by rewrite -later_sep HP.
Qed.

Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
  envs_lookup i Δ = Some (p, P)%I  SepDestruct p P P1 P2 
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
  Δ'  Q  Δ  Q.
Proof.
  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
  - by rewrite (sep_destruct true P) right_id (comm uPred_and) wand_elim_r.
  - by rewrite (sep_destruct false P) right_id (comm uPred_sep P1) wand_elim_r.
Qed.

(** * Framing *)
Robbert Krebbers's avatar
Robbert Krebbers committed
767 768 769 770
(** 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)) :=
  frame : (R  from_option True mQ)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
771 772
Arguments frame : clear implicits.

773
Global Instance frame_here R : Frame R R None.
Robbert Krebbers's avatar
Robbert Krebbers committed
774
Proof. by rewrite /Frame right_id. Qed.
775
Global Instance frame_sep_l R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
776
  Frame R P1 mQ 
777
  Frame R (P1  P2) (Some $ if mQ is Some Q then Q  P2 else P2)%I | 9.
Robbert Krebbers's avatar
Robbert Krebbers committed
778
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
779
Global Instance frame_sep_r R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
780
  Frame R P2 mQ 
781
  Frame R (P1  P2) (Some $ if mQ is Some Q then P1  Q else P1)%I | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
782
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
783
Global Instance frame_and_l R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
784
  Frame R P1 mQ 
785
  Frame R (P1  P2) (Some $ if mQ is Some Q then Q  P2 else P2)%I | 9.
Robbert Krebbers's avatar
Robbert Krebbers committed
786
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
787
Global Instance frame_and_r R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
788
  Frame R P2 mQ 
789
  Frame R (P1  P2) (Some $ if mQ is Some Q then P1  Q else P1)%I | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
790
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
791
Global Instance frame_or R P1 P2 mQ1 mQ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
792 793 794 795 796 797 798 799 800
  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.
801
Global Instance frame_later R P mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
802 803 804 805 806
  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.
807
Global Instance frame_exist {A} R (Φ : A  uPred M) mΨ :
Robbert Krebbers's avatar
Robbert Krebbers committed
808 809
  ( 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
810
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
811
Global Instance frame_forall {A} R (Φ : A  uPred M) mΨ :
Robbert Krebbers's avatar
Robbert Krebbers committed
812 813
  ( 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
814 815
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
816 817 818 819
Lemma tac_frame Δ Δ' i p R P mQ :
  envs_lookup_delete i Δ = Some (p, R, Δ')%I  Frame R P mQ 
  (if mQ is Some Q then (if p then Δ else Δ')  Q else True) 
  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
820
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
821 822 823 824 825
  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
  - rewrite envs_lookup_persistent_sound // always_elim.
    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
  - rewrite envs_lookup_sound //; simpl.
    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
Robbert Krebbers's avatar
Robbert Krebbers committed
826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847
Qed.

(** * Disjunction *)
Class OrSplit (P Q1 Q2 : uPred M) := or_split : (Q1  Q2)  P.
Arguments or_split : clear implicits.
Global Instance or_split_or P1 P2 : OrSplit (P1  P2) P1 P2.
Proof. done. Qed.

Lemma tac_or_l Δ P Q1 Q2 : OrSplit P Q1 Q2  Δ  Q1  Δ  P.
Proof. intros. rewrite -(or_split P). by apply or_intro_l'. Qed.
Lemma tac_or_r Δ P Q1 Q2 : OrSplit P Q1 Q2  Δ  Q2  Δ  P.
Proof. intros. rewrite -(or_split P). by apply or_intro_r'. Qed.

Class OrDestruct P Q1 Q2 := or_destruct : P  (Q1  Q2).
Arguments or_destruct : clear implicits.
Global Instance or_destruct_or P Q : OrDestruct (P  Q) P Q.
Proof. done. Qed.
Global Instance or_destruct_later P Q1 Q2 :
  OrDestruct P Q1 Q2  OrDestruct ( P) ( Q1) ( Q2).
Proof. rewrite /OrDestruct=>->. by rewrite later_or. Qed.

Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
Ralf Jung's avatar
Ralf Jung committed
848
  envs_lookup i Δ = Some (p, P)  OrDestruct P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869
  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 
  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 
  Δ1  Q  Δ2  Q  Δ  Q.
Proof.
  intros ???? HP1 HP2. rewrite envs_lookup_sound //. destruct p.
  - rewrite (or_destruct P) always_or sep_or_r; apply or_elim. simpl.
    + 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.
  - rewrite (or_destruct P) sep_or_r; apply or_elim.
    + 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.
Qed.

(** * Forall *)
Lemma tac_forall_intro {A} Δ (Φ : A  uPred M) : ( a, Δ  Φ a)  Δ  ( a, Φ a).
Proof. apply forall_intro. Qed.

870 871 872 873 874 875 876 877 878 879 880 881 882 883 884
Class ForallSpecialize {As} (xs : hlist As)
    (P : uPred M) (Φ : himpl As (uPred M)) :=
  forall_specialize : P  happly Φ xs.
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 Φ 
  envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
885 886
  Δ'  Q  Δ  Q.
Proof.
887 888 889
  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
  - by rewrite right_id (forall_specialize _ P) wand_elim_r.
  - by rewrite right_id (forall_specialize _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
890 891 892 893 894 895 896 897 898 899 900 901 902
Qed.

Lemma tac_forall_revert {A} Δ (Φ : A  uPred M) :
  Δ  ( a, Φ a)  ( a, Δ  Φ a).
Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.

(** * Existential *)
Class ExistSplit {A} (P : uPred M) (Φ : A  uPred M) :=
  exist_split : ( x, Φ x)  P.
Arguments exist_split {_} _ _ {_}.
Global Instance exist_split_exist {A} (Φ: A  uPred M): ExistSplit ( a, Φ a) Φ.
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
903 904 905
Lemma tac_exist {A} Δ P (Φ : A  uPred M) :
  ExistSplit P Φ  ( a, Δ  Φ a)  Δ  P.
Proof. intros ? [a ?]. rewrite -(exist_split P). eauto using exist_intro'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
906 907 908 909 910 911 912 913

Class ExistDestruct {A} (P : uPred M) (Φ : A  uPred M) :=
  exist_destruct : P  ( x, Φ x).
Arguments exist_destruct {_} _ _ {_}.
Global Instance exist_destruct_exist {A} (Φ : A  uPred M) :
  ExistDestruct ( a, Φ a) Φ.
Proof. done. Qed.
Global Instance exist_destruct_later {A} P (Φ : A  uPred M) :
914 915
  ExistDestruct P Φ  Inhabited A  ExistDestruct ( P) (λ a,  (Φ a))%I.
Proof. rewrite /ExistDestruct=> HP ?. by rewrite HP later_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933

Lemma tac_exist_destruct {A} Δ i p j P (Φ : A  uPred M) Q :
  envs_lookup i Δ = Some (p, P)%I  ExistDestruct P Φ 
  ( a,  Δ',
    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ'  Δ'  Q) 
  Δ  Q.
Proof.
  intros ?? HΦ. rewrite envs_lookup_sound //. destruct p.
  - rewrite (exist_destruct P) always_exist sep_exist_r.
    apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
    rewrite envs_simple_replace_sound' //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite (exist_destruct P) sep_exist_r.
    apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
    rewrite envs_simple_replace_sound' //; simpl.
    by rewrite right_id wand_elim_r.
Qed.
End tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
934

935 936
Hint Extern 0 (ToPosedProof True _ _) =>
  class_apply @to_posed_proof_True : typeclass_instances.