coq_tactics.v 43.1 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Export upred.
2
From iris.algebra Require Import upred_big_op upred_tactics gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
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
Proof.
120
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
123
    ecancel [ [] _;  P; [] _]%I; apply pure_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 pure_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
Proof.
144
  rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
147
    rewrite pure_equiv // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
148 149
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
150
    rewrite (env_lookup_perm Γs) //=. rewrite pure_equiv // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154
    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
Proof.
163
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
164 165 166
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
167
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169 170 171
    + 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
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
176
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179 180 181 182 183 184
    + 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
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
188
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
189 190
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
191
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
192 193 194 195
    + 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
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
200
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202 203 204 205 206 207 208
    + 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
Proof.
228
  rewrite /envs_split /of_envs=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230
  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;
232
    destruct Hwf; apply sep_intro_True_l; apply pure_intro; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
233 234 235 236
      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
Proof.
239 240
  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].
241 242 243
  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
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 *.
273 274
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
275 276 277 278 279 280 281 282 283 284 285 286
      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
Proof.
290 291
  intros <-. rewrite /of_envs /= always_pure !right_id.
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
292 293 294
Qed.

(** * Basic rules *)
295 296 297 298 299 300 301 302 303 304
Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : ?p P  Q.
Arguments from_assumption _ _ _ {_}.
Global Instance from_assumption_exact p P : FromAssumption p P P.
Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
Global Instance from_assumption_always_l p P Q :
  FromAssumption p P Q  FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
Global Instance from_assumption_always_r P Q :
  FromAssumption true P Q  FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
305 306

Lemma tac_assumption Δ i p P Q :
307
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q  Δ  Q.
308
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 331 332
Class IsPure (P : uPred M) (φ : Prop) := is_pure : P ⊣⊢  φ.
Arguments is_pure : clear implicits.
Global Instance is_pure_pure φ : IsPure ( φ) φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
333
Proof. done. Qed.
334 335
Global Instance is_pure_eq {A : cofeT} (a b : A) :
  Timeless a  IsPure (a  b) (a  b).
Robbert Krebbers's avatar
Robbert Krebbers committed
336
Proof. intros; red. by rewrite timeless_eq. Qed.
337
Global Instance is_pure_valid `{CMRADiscrete A} (a : A) : IsPure ( a) ( a).
Robbert Krebbers's avatar
Robbert Krebbers committed
338 339
Proof. intros; red. by rewrite discrete_valid. Qed.

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

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

351
Lemma tac_pure_revert Δ φ Q : (Δ   φ  Q)  (φ  Δ  Q).
352
Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
353 354

(** * Later *)
355 356 357 358 359 360 361 362 363
Class IntoLater (P Q : uPred M) := into_later : P   Q.
Arguments into_later _ _ {_}.
Class FromLater (P Q : uPred M) := from_later :  Q  P.
Arguments from_later _ _ {_}.
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)
364 365
}.

366
Global Instance into_later_fallthrough P : IntoLater P P | 1000.
367
Proof. apply later_intro. Qed.
368
Global Instance into_later_later P : IntoLater ( P) P.
369
Proof. done. Qed.
370 371
Global Instance into_later_and P1 P2 Q1 Q2 :
  IntoLater P1 Q1  IntoLater P2 Q2  IntoLater (P1  P2) (Q1  Q2).
372
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
373 374
Global Instance into_later_or P1 P2 Q1 Q2 :
  IntoLater P1 Q1  IntoLater P2 Q2  IntoLater (P1  P2) (Q1  Q2).
375
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
376 377
Global Instance into_later_sep P1 P2 Q1 Q2 :
  IntoLater P1 Q1  IntoLater P2 Q2  IntoLater (P1  P2) (Q1  Q2).
378 379
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.

380
Global Instance into_later_big_sepM `{Countable K} {A}
381
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
382 383
  ( x k, IntoLater (Φ k x) (Ψ k x)) 
  IntoLater ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
384
Proof.
385
  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
386
Qed.
387
Global Instance into_later_big_sepS `{Countable A}
388
    (Φ Ψ : A  uPred M) (X : gset A) :
389 390
  ( x, IntoLater (Φ x) (Ψ x)) 
  IntoLater ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
391
Proof.
392
  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
393 394
Qed.

395
Global Instance from_later_later P : FromLater ( P) P.
396
Proof. done. Qed.
397 398
Global Instance from_later_and P1 P2 Q1 Q2 :
  FromLater P1 Q1  FromLater P2 Q2  FromLater (P1  P2) (Q1  Q2).
399
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
400 401
Global Instance from_later_or P1 P2 Q1 Q2 :
  FromLater P1 Q1  FromLater P2 Q2  FromLater (P1  P2) (Q1  Q2).
402
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
403 404
Global Instance from_later_sep P1 P2 Q1 Q2 :
  FromLater P1 Q1  FromLater P2 Q2  FromLater (P1  P2) (Q1  Q2).
405 406
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.

407
Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
Proof. constructor. Qed.
409 410 411
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
412 413
Proof. by constructor. Qed.

414 415 416
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
417
Proof. by split. Qed.
418

419
Lemma into_later_env_sound Δ1 Δ2 : IntoLaterEnvs Δ1 Δ2  Δ1   Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
420 421 422
Proof.
  intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
  repeat apply sep_mono; try apply always_mono.
423
  - rewrite -later_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
424 425 426 427 428 429
      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' :
430 431
  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
432 433

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

(** * Always *)
445
Lemma tac_always_intro Δ Q : envs_persistent Δ = true  (Δ  Q)  Δ   Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
446 447
Proof. intros. by apply: always_intro. Qed.

448 449 450 451 452 453
Class IntoPersistentP (P Q : uPred M) := into_persistentP : P   Q.
Arguments into_persistentP : clear implicits.
Global Instance into_persistentP_always_trans P Q :
  IntoPersistentP P Q  IntoPersistentP ( P) Q | 0.
Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
Global Instance into_persistentP_always P : IntoPersistentP ( P) P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
Proof. done. Qed.
455 456
Global Instance into_persistentP_persistent P :
  PersistentP P  IntoPersistentP P P | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
457 458 459
Proof. done. Qed.

Lemma tac_persistent Δ Δ' i p P P' Q :
460
  envs_lookup i Δ = Some (p, P)  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
461
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
462
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
Proof.
464
  intros ??? <-. rewrite envs_replace_sound //; simpl.
465
  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
466 467 468 469 470 471
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
  envs_persistent Δ = true 
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
472
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
473 474 475 476 477
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 :
478
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
479
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
480
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
481 482
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
483
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
484
Qed.
485
Lemma tac_impl_intro_pure Δ P φ Q : IsPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
486
Proof.
487
  intros. by apply impl_intro_l; rewrite (is_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
488 489 490
Qed.

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

508 509 510
Class IntoWand (R P Q : uPred M) := into_wand : R  P - Q.
Arguments into_wand : clear implicits.
Global Instance into_wand_wand P Q : IntoWand (P - Q) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
511
Proof. done. Qed.
512
Global Instance into_wand_impl P Q : IntoWand (P  Q) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
513
Proof. apply impl_wand. Qed.
514
Global Instance into_wand_iff_l P Q : IntoWand (P  Q) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
Proof. by apply and_elim_l', impl_wand. Qed.
516
Global Instance into_wand_iff_r P Q : IntoWand (P  Q) Q P.
Robbert Krebbers's avatar
Robbert Krebbers committed
517
Proof. apply and_elim_r', impl_wand. Qed.
518 519
Global Instance into_wand_always R P Q : IntoWand R P Q  IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
520 521 522 523 524

(* 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, Δ') 
525
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
526
  IntoWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
527 528 529 530 531
  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 Δ'' 
532
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
533 534 535
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
536
    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
537
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
538 539
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
540
    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
541 542
Qed.

543 544 545 546 547
Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
  into_assert : R  (P - Q)  Q.
Global Arguments into_assert _ _ _ {_}.
Lemma into_assert_fallthrough P Q : IntoAssert P Q P.
Proof. by rewrite /IntoAssert wand_elim_r. Qed.
548 549

Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
550
  envs_lookup_delete j Δ = Some (q, R, Δ') 
551
  IntoWand R P1 P2  IntoAssert P1 Q P1' 
Robbert Krebbers's avatar
Robbert Krebbers committed
552
  ('(Δ1,Δ2)  envs_split lr js Δ';
553
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
554
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
555
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
556
Proof.
557
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
558 559 560 561
  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.
562 563
  rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
  rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
564
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
565 566
Qed.

567 568
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
  envs_lookup j Δ = Some (q, R) 
569
  IntoWand R P1 P2  IsPure P1 φ 
570
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
571
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
572
Proof.
573
  intros. rewrite envs_simple_replace_sound //; simpl.
574
  by rewrite right_id (into_wand R) (is_pure P1) pure_equiv // wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
575 576
Qed.

577 578
Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
579
  IntoWand R P1 P2 
580
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
581 582
  (Δ'  P1)  (PersistentP P1  PersistentP P2) 
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
583
Proof.
584 585 586 587 588
  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.
589
    rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
590 591 592
    by rewrite wand_elim_r.
  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
    rewrite envs_simple_replace_sound //; simpl.
593
    rewrite (sep_elim_r _ (_ - _)) right_id (into_wand R) always_if_elim.
594
    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
595 596 597 598
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
599
  (Δ'  if p then  P  Q else P - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
600 601 602 603 604 605
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.

606
Lemma tac_revert_spatial Δ Q :
607
  (envs_clear_spatial Δ  env_fold uPred_wand Q (env_spatial Δ))  Δ  Q.
608 609 610 611
Proof.
  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed.

612
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
613
  IntoAssert P Q R 
Robbert Krebbers's avatar
Robbert Krebbers committed
614
  envs_split lr js Δ = Some (Δ1,Δ2) 
615
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
616
  (Δ1  R)  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
617
Proof.
618
  intros ??? HP HQ. rewrite envs_split_sound //.
619
  rewrite (envs_app_sound Δ2) //; simpl.
620
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
621 622 623 624
Qed.

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
625
  (Δ  P)  PersistentP P  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
626
Proof.
627
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
628 629 630 631
  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.

632
(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
633
not as [H : True -★ Q]. The class [IntoPosedProof] is used to strip off the
634 635
[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. *)
636 637 638 639 640 641 642
Class IntoPosedProof (P1 P2 R : uPred M) :=
  into_pose_proof : (P1  P2)  True  R.
Arguments into_pose_proof : clear implicits.
Instance to_posed_proof_True P : IntoPosedProof True P P.
Proof. by rewrite /IntoPosedProof. Qed.
Global Instance to_posed_proof_wand P Q : IntoPosedProof P Q (P - Q).
Proof. rewrite /IntoPosedProof. apply entails_wand. Qed.
643 644

Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
645 646
  (P1  P2)  IntoPosedProof P1 P2 R 
  envs_app true (Esnoc Enil j R) Δ = Some Δ' 
647
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
648
Proof.
649
  intros HP ?? <-. rewrite envs_app_sound //; simpl.
650
  by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
651 652
Qed.

653 654 655
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 Δ'' 
656
  (Δ''  Q)  Δ  Q.
657 658 659 660 661 662 663 664
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
665
Lemma tac_apply Δ Δ' i p R P1 P2 :
666
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand R P1 P2 
667
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
668 669
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
670
  by rewrite (into_wand R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
671 672 673 674 675
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
Ralf Jung's avatar
Ralf Jung committed
676
   {A : cofeT} (x y : A) (Φ : A  uPred M),
677 678
    (Pxy  x  y) 
    (Q ⊣⊢ Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
679
    ( n, Proper (dist n ==> dist n) Φ) 
680
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
681 682 683 684 685 686 687 688
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) 
689
  envs_lookup j Δ = Some (q, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
690
   {A : cofeT} Δ' x y (Φ : A  uPred M),
691 692
    (Pxy  x  y) 
    (P ⊣⊢ Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
693 694
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
695
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
696 697 698 699
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.
700 701 702 703 704
  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
705 706 707
Qed.

(** * Conjunction splitting *)
708 709
Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1  Q2  P.
Arguments from_and : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
710

711
Global Instance from_and_and P1 P2 : FromAnd (P1  P2) P1 P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
712
Proof. done. Qed.
713 714 715 716 717 718 719 720 721 722 723 724 725 726 727
Global Instance from_and_sep_persistent_l P1 P2 :
  PersistentP P1  FromAnd (P1  P2) P1 P2.
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
  PersistentP P2  FromAnd (P1  P2) P1 P2.
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
Global Instance from_and_always P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
Global Instance from_and_later P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.

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
728 729

(** * Separating conjunction splitting *)
730 731
Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1  Q2  P.
Arguments from_sep : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
732

733
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
734
Proof. done. Qed.
735 736 737 738 739 740 741 742 743 744 745
Global Instance from_sep_always P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
Global Instance from_sep_later P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.

Global Instance from_sep_ownM (a b : M) :
  FromSep (uPred_ownM (a  b)) (uPred_ownM a) (uPred_ownM b) | 99.
Proof. by rewrite /FromSep ownM_op. Qed.
Global Instance from_sep_big_sepM
746
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) m :
747 748
  ( k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
  FromSep ([ map] k  x  m, Φ k x)
749 750
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
Proof.
751
  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
752
Qed.
753 754 755
Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) X :
  ( x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) 
  FromSep ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
756
Proof.
757
  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
758
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
759 760

Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
761
  FromSep P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
762
  envs_split lr js Δ = Some (Δ1,Δ2) 
763
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
764
Proof.
765
  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
766 767 768 769 770 771
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) 
772
  FromSep P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
773 774
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
775
  (Δ4  Q)  Δ1  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
776 777 778 779 780
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.
781
      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
782
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
783
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
784 785
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
786
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
787
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
788
      by rewrite right_id assoc (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
789 790 791
Qed.

(** * Conjunction/separating conjunction elimination *)
792 793 794 795 796 797 798 799 800
Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : ?p P  ?p (Q1  Q2).
Arguments into_sep : clear implicits.
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a  b1  b2.
Arguments into_op {_} _ _ _ {_}.

Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a  b) a b.
Proof. by rewrite /IntoOp. Qed.
Global Instance into_op_persistent {A : cmraT} (a : A) :
  Persistent a  IntoOp a a a.
801
Proof. intros; apply (persistent_dup a). Qed.
802 803 804
Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
  IntoOp a b1 b2  IntoOp a' b1' b2' 
  IntoOp (a,a') (b1,b1') (b2,b2').
805
Proof. by constructor. Qed.
806 807
Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
  IntoOp a b1 b2  IntoOp (Some a) (Some b1) (Some b2).
808 809
Proof. by constructor. Qed.

810 811 812 813 814
Global Instance into_sep_sep p P Q : IntoSep p (P  Q) P Q.
Proof. rewrite /IntoSep. by rewrite always_if_sep. Qed.
Global Instance into_sep_ownM p (a b1 b2 : M) :
  IntoOp a b1 b2 
  IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
815
Proof.
816
  rewrite /IntoOp /IntoSep=> ->. by rewrite ownM_op always_if_sep.
817
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
818

819 820 821 822 823 824 825 826
Global Instance into_sep_and P Q : IntoSep true (P  Q) P Q.
Proof. by rewrite /IntoSep /= always_and_sep. Qed.
Global Instance into_sep_and_persistent_l P Q :
  PersistentP P  IntoSep false (P  Q) P Q.
Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
Global Instance into_sep_and_persistent_r P Q :
  PersistentP Q  IntoSep false (P  Q) P Q.
Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
827

828 829 830
Global Instance into_sep_later p P Q1 Q2 :
  IntoSep p P Q1 Q2  IntoSep p ( P) ( Q1) ( Q2).
Proof. by rewrite /IntoSep -later_sep !always_if_later=> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
831

832
Global Instance into_sep_big_sepM
833
    `{Countable K} {A} (Φ Ψ1 Ψ2 : K  A  uPred M) p m :
834 835
  ( k x, IntoSep p (Φ k x) (Ψ1 k x) (Ψ2 k x)) 
  IntoSep p ([ map] k  x  m, Φ k x)
836 837
    ([ map] k  x  m, Ψ1 k x) ([ map] k  x  m, Ψ2 k x).
Proof.
838
  rewrite /IntoSep=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
839 840
  by apply big_sepM_mono.
Qed.
841 842 843
Global Instance into_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A  uPred M) p X :
  ( x, IntoSep p (Φ x) (Ψ1 x) (Ψ2 x)) 
  IntoSep p ([ set] x  X, Φ x) ([ set] x  X, Ψ1 x) ([ set] x  X, Ψ2 x).
844
Proof.
845
  rewrite /IntoSep=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
846 847 848
  by apply big_sepS_mono.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
849
Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
850
  envs_lookup i Δ = Some (p, P)  IntoSep p P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
851
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
852
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
853
Proof.
854
  intros. rewrite envs_simple_replace_sound //; simpl.
855
  by rewrite (into_sep p P) right_id (comm uPred_sep P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
856 857 858
Qed.

(** * Framing *)
859
Class Frame (R P Q : uPred M) := frame : R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
860 861
Arguments frame : clear implicits.

862
Global Instance frame_here R : Frame R R True.
Robbert Krebbers's avatar
Robbert Krebbers committed
863
Proof. by rewrite /Frame right_id. Qed.
864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917

Class MakeSep (P Q PQ : uPred M) := make_sep : P  Q ⊣⊢ PQ.
Global Instance make_sep_true_l P : MakeSep True P P.
Proof. by rewrite /MakeSep left_id. Qed.
Global Instance make_sep_true_r P : MakeSep P True P.
Proof. by rewrite /MakeSep right_id. Qed.
Global Instance make_sep_fallthrough P Q : MakeSep P Q (P  Q) | 100.
Proof. done. Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
  Frame R P1 Q  MakeSep Q P2 Q'  Frame R (P1  P2) Q' | 9.
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
Global Instance frame_sep_r R P1 P2 Q Q' :
  Frame R P2 Q  MakeSep P1 Q Q'  Frame R (P1  P2) Q' | 10.
Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.

Class MakeAnd (P Q PQ : uPred M) := make_and : P  Q ⊣⊢ PQ.
Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed.
Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed.
Global Instance make_and_fallthrough P Q : MakeSep P Q (P  Q) | 100.
Proof. done. Qed.
Global Instance frame_and_l R P1 P2 Q Q' :
  Frame R P1 Q  MakeAnd Q P2 Q'  Frame R (P1  P2) Q' | 9.
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
Global Instance frame_and_r R P1 P2 Q Q' :
  Frame R P2 Q  MakeAnd P1 Q Q'  Frame R (P1  P2) Q' | 10.
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.

Class MakeOr (P Q PQ : uPred M) := make_or : P  Q ⊣⊢ PQ.
Global Instance make_or_true_l P : MakeOr True P True.
Proof. by rewrite /MakeOr left_absorb. Qed.
Global Instance make_or_true_r P : MakeOr P True True.
Proof. by rewrite /MakeOr right_absorb. Qed.
Global Instance make_or_fallthrough P Q : MakeOr P Q (P  Q) | 100.
Proof. done. Qed.
Global Instance frame_or R P1 P2 Q1 Q2 Q :
  Frame R P1 Q1  Frame R P2 Q2