coq_tactics.v 34.1 KB
Newer Older
1 2
From iris.base_logic Require Export base_logic.
From iris.base_logic Require Import big_op tactics.
3
From iris.proofmode Require Export environments classes.
4
From iris.prelude Require Import stringmap hlist.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import uPred.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
Record envs (M : ucmraT) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11 12 13 14 15 16 17 18 19 20 21
  Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

Record envs_wf {M} (Δ : envs M) := {
  env_persistent_valid : env_wf (env_persistent Δ);
  env_spatial_valid : env_wf (env_spatial Δ);
  envs_disjoint i : env_persistent Δ !! i = None  env_spatial Δ !! i = None
}.

Coercion of_envs {M} (Δ : envs M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
22
  (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
23 24 25 26 27 28
Instance: Params (@of_envs) 1.

Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
  env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

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

Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
  let (Γp,Γs) := Δ in
  match env_lookup i Γp with
  | Some P => Some (true, P) | None => P  env_lookup i Γs; Some (false, P)
  end.

Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
  let (Γp,Γs) := Δ in
  match p with
  | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
  end.

Definition envs_lookup_delete {M} (i : string)
    (Δ : envs M) : option (bool * uPred M * envs M) :=
  let (Γp,Γs) := Δ in
  match env_lookup_delete i Γp with
  | Some (P,Γp') => Some (true, P, Envs Γp' Γs)
  | None => '(P,Γs')  env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
  end.

53 54 55 56 57
Definition envs_snoc {M} (Δ : envs M)
    (p : bool) (j : string) (P : uPred M) : envs M :=
  let (Γp,Γs) := Δ in
  if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).

Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
Definition envs_app {M} (p : bool)
    (Γ : env (uPred M)) (Δ : envs M) : option (envs M) :=
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_app Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_app Γ Γs; Some (Envs Γp Γs')
  end.

Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  let (Γp,Γs) := Δ in
  match p with
  | true => _  env_app Γ Γs; Γp'  env_replace i Γ Γp; Some (Envs Γp' Γs)
  | false => _  env_app Γ Γp; Γs'  env_replace i Γ Γs; Some (Envs Γp Γs')
  end.

Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
    (Δ : envs M) : option (envs M) :=
  if eqb p q then envs_simple_replace i p Γ Δ
  else envs_app q Γ (envs_delete i p Δ).

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

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

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

88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
Fixpoint envs_split_go {M}
    (js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
  match js with
  | [] => Some (Δ1, Δ2)
  | j :: js =>
     '(p,P,Δ1')  envs_lookup_delete j Δ1;
     if p then envs_split_go js Δ1 Δ2 else
     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
  end.
(* if [lr = true] then [result = (remaining hyps, hyps named js)] and
   if [lr = false] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {M} (lr : bool)
    (js : list string) (Δ : envs M) : option (envs M * envs M) :=
  '(Δ1,Δ2)  envs_split_go js Δ (envs_clear_spatial Δ);
  if lr then Some (Δ1,Δ2) else Some (Δ2,Δ1).


Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
(* Coq versions of the tactics *)
Section tactics.
107
Context {M : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
108 109 110 111
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

112
Lemma of_envs_def Δ :
Ralf Jung's avatar
Ralf Jung committed
113
  of_envs Δ = (envs_wf Δ⌝   [] env_persistent Δ  [] env_spatial Δ)%I.
114 115
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
116 117 118 119 120 121 122 123 124 125
Lemma envs_lookup_delete_Some Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ')
   envs_lookup i Δ = Some (p,P)  Δ' = envs_delete i p Δ.
Proof.
  rewrite /envs_lookup /envs_delete /envs_lookup_delete.
  destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct.
  destruct (Γp !! i), (Γs !! i); naive_solver.
Qed.

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

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

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

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

Lemma envs_snoc_sound Δ p i P :
183
  envs_lookup i Δ = None  Δ  ?p P - envs_snoc Δ p i P.
184 185 186 187 188 189
Proof.
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
190
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
191
    + by rewrite always_sep assoc.
192 193
  - apply sep_intro_True_l; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
194
      intros j; destruct (strings.string_beq_reflect j i); naive_solver.
195 196 197
    + solve_sep_entails.
Qed.

198
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Proof.
200
  rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202 203
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
204
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
205 206 207 208
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γp') //.
209
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
210 211
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
212
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214 215 216 217 218 219 220
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
221
  envs_delete i p Δ  ?p [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
222 223
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
224
  apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
225 226
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
227
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229 230 231
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γp') //.
232
      rewrite big_sep_app always_sep. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
233 234
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
235
    apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
236 237 238 239 240 241 242 243
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

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

Lemma envs_replace_sound' Δ Δ' i p q Γ :
248
  envs_replace i p q Γ Δ = Some Δ'  envs_delete i p Δ  ?q [] Γ - Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252 253 254 255 256
Proof.
  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
257
  Δ  ?p P  (?q [] Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

260 261 262
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
  = '(p,P)  envs_lookup j Δ; if p then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Proof.
264 265 266
  rewrite /envs_lookup /envs_clear_spatial.
  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
  by destruct (Γs !! j).
Robbert Krebbers's avatar
Robbert Krebbers committed
267 268
Qed.

269
Lemma envs_clear_spatial_sound Δ : Δ  envs_clear_spatial Δ  [] env_spatial Δ.
270
Proof.
271 272
  rewrite /of_envs /envs_clear_spatial /=; apply pure_elim_sep_l=> Hwf.
  rewrite right_id -assoc; apply sep_intro_True_l; [apply pure_intro|done].
273 274 275
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

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

281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ 
  envs_lookup i Δ = Some (p,P)  envs_lookup i (envs_delete i p Δ) = None.
Proof.
  rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - rewrite env_lookup_env_delete //. revert Hlookup.
    destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _).
  - rewrite env_lookup_env_delete //. by destruct (Γp !! _).
Qed.
Lemma envs_lookup_envs_delete_ne Δ i j p :
  i  j  envs_lookup i (envs_delete j p Δ) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
  - by rewrite env_lookup_env_delete_ne.
  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
Qed.

Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
  ( j P, envs_lookup j Δ1 = Some (false, P)  envs_lookup j Δ2 = None) 
301
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2')  Δ1  Δ2  Δ1'  Δ2'.
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
Proof.
  revert Δ1 Δ2 Δ1' Δ2'.
  induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
  apply pure_elim with (envs_wf Δ1); [unfold of_envs; solve_sep_entails|]=> Hwf.
  destruct (envs_lookup_delete j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq; auto.
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
  rewrite -(IH _ _ _ _ _ HΔ); last first.
  { intros j' P'; destruct (decide (j = j')) as [->|].
    - by rewrite (envs_lookup_envs_delete _ _ _ P).
    - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
Lemma envs_split_sound Δ lr js Δ1 Δ2 :
317
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  Δ1  Δ2.
318 319 320 321 322 323 324 325 326
Proof.
  rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
  rewrite {2}envs_clear_spatial_sound sep_elim_l always_and_sep_r.
  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
  apply envs_split_go_sound in HΔ as ->; last first.
  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
  destruct lr; simplify_eq; solve_sep_entails.
Qed.

327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345
Global Instance envs_Forall2_refl (R : relation (uPred M)) :
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Global Instance envs_Forall2_sym (R : relation (uPred M)) :
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Global Instance envs_Forall2_trans (R : relation (uPred M)) :
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Lemma envs_Forall2_impl (R R' : relation (uPred M)) Δ1 Δ2 :
  envs_Forall2 R Δ1 Δ2  ( P Q, R P Q  R' P Q)  envs_Forall2 R' Δ1 Δ2.
Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.

Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in *.
346 347
  apply pure_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply pure_intro; constructor;
348 349 350 351 352
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Global Instance of_envs_proper : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
353 354
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
355 356 357 358 359
Qed.
Global Instance Envs_mono (R : relation (uPred M)) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
Proof. by constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
360
(** * Adequacy *)
361
Lemma tac_adequate P : (Envs Enil Enil  P)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Proof.
363 364
  intros <-. rewrite /of_envs /= always_pure !right_id.
  apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
365 366 367
Qed.

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

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
375
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
376 377 378 379 380
Proof.
  intros. rewrite envs_simple_replace_sound //.
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.
Lemma tac_clear Δ Δ' i p P Q :
381
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
382 383 384
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.

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

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

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

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

(** * Later *)
404 405 406 407 408
Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
  into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
  into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
  into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
409 410
}.

411
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
Proof. constructor. Qed.
413 414 415
Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
  IntoLaterNEnv n Γ1 Γ2  IntoLaterN n P Q 
  IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
416 417
Proof. by constructor. Qed.

418 419 420
Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
  IntoLaterNEnv n Γp1 Γp2  IntoLaterNEnv n Γs1 Γs2 
  IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Proof. by split. Qed.
422

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

433 434 435
Lemma tac_next Δ Δ' n Q Q' :
  FromLaterN n Q Q'  IntoLaterNEnvs n Δ Δ'  (Δ'  Q')  Δ  Q.
Proof. intros ?? HQ. by rewrite -(from_laterN n Q) into_laterN_env_sound HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
436 437

Lemma tac_löb Δ Δ' i Q :
438
  env_spatial_is_nil Δ = true 
439
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
440
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
Proof.
442 443 444 445
  intros ?? HQ. rewrite -(always_elim Q) -(löb ( Q)) -always_later.
  apply impl_intro_l, (always_intro _ _).
  rewrite envs_app_sound //; simpl.
  by rewrite right_id always_and_sep_l' wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
446 447 448
Qed.

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

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

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
463
  env_spatial_is_nil Δ = true 
Robbert Krebbers's avatar
Robbert Krebbers committed
464
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
465
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
466 467 468 469 470
Proof.
  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
  by rewrite right_id always_wand_impl always_elim HQ.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
471
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
472
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
473
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
474 475
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
476
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
Qed.
478
Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
Ralf Jung's avatar
Ralf Jung committed
479
  (φ  Δ  ⌜ψ⌝)  Δ  ⌜φ  ψ⌝.
480
Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
481
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
Proof.
483
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
484 485 486
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
487
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
Proof.
489
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
490 491
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
492
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
493
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
494
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
495 496 497 498
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
499
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
Proof.
501
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
502 503 504 505 506 507
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, Δ') 
508
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
509
  IntoWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
510 511 512 513 514
  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 Δ'' 
515
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
516 517 518
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
519
    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
520
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
521 522
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
523
    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
524 525
Qed.

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

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

555
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
556
  envs_lookup_delete j Δ = Some (q, R, Δ') 
557
  IntoWand R P1 P2  PersistentP P1 
558
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574
  (Δ'  P1)  (Δ''  Q)  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
  rewrite envs_lookup_sound //.
  rewrite -(idemp uPred_and (envs_delete _ _ _)).
  rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
  rewrite envs_simple_replace_sound' //; simpl.
  rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
  by rewrite wand_elim_r.
Qed.

Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
  envs_lookup j Δ = Some (q,P) 
  (Δ  R)  PersistentP R 
  envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
Proof.
576 577 578 579
  intros ? HR ?? <-.
  rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
  rewrite envs_replace_sound //; simpl.
  by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
580 581 582 583
Qed.

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

590 591 592 593 594 595 596 597 598 599
Lemma tac_revert_ih Δ P Q :
  env_spatial_is_nil Δ = true 
  (of_envs Δ  P) 
  (of_envs Δ   P  Q) 
  (of_envs Δ  Q).
Proof.
  intros ? HP HPQ.
  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
Qed.

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

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
613
  (Δ  P)  PersistentP P  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Proof.
615
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
616 617 618 619
  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.

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

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

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

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

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

(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
691
  FromSep P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
692
  envs_split lr js Δ = Some (Δ1,Δ2) 
693
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
694
Proof.
695
  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed