coq_tactics.v 30.5 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.
3
From iris.proofmode Require Export environments classes.
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
Lemma tac_assumption Δ i p P Q :
296
  envs_lookup i Δ = Some (p,P)  FromAssumption p P Q  Δ  Q.
297
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298 299 300 301

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
302
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
303 304 305 306 307
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 :
308
  envs_lookup_delete i Δ = Some (p,P,Δ')  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
310
Lemma tac_clear_spatial Δ Δ' Q :
311
  envs_clear_spatial Δ = Δ'  (Δ'  Q)  Δ  Q.
312
Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314

(** * False *)
315
Lemma tac_ex_falso Δ Q : (Δ  False)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
316 317 318
Proof. by rewrite -(False_elim Q). Qed.

(** * Pure *)
319 320
Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ  φ  Δ  Q.
Proof. intros ??. rewrite -(from_pure Q) //. apply True_intro. Qed.
321

Robbert Krebbers's avatar
Robbert Krebbers committed
322
Lemma tac_pure Δ Δ' i p P φ Q :
323
  envs_lookup_delete i Δ = Some (p, P, Δ')  IntoPure P φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
324 325 326
  (φ  Δ'  Q)  Δ  Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
327
  rewrite (into_pure P); by apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
328 329
Qed.

330
Lemma tac_pure_revert Δ φ Q : (Δ   φ  Q)  (φ  Δ  Q).
331
Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
332 333

(** * Later *)
334 335 336 337 338
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)
339 340
}.

341
Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
Proof. constructor. Qed.
343 344 345
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
346 347
Proof. by constructor. Qed.

348 349 350
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
351
Proof. by split. Qed.
352

353
Lemma into_later_env_sound Δ1 Δ2 : IntoLaterEnvs Δ1 Δ2  Δ1   Δ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
354 355 356
Proof.
  intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
  repeat apply sep_mono; try apply always_mono.
357
  - rewrite -later_intro; apply pure_mono; destruct 1; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
358 359 360 361 362 363
      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' :
364 365
  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
366 367

Lemma tac_löb Δ Δ' i Q :
368 369
  envs_persistent Δ = true 
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
370
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
371
Proof.
372 373 374 375
  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
376 377
Qed.

378 379 380 381 382 383 384 385 386 387
Lemma tac_timeless Δ Δ' i p P Q :
  TimelessElim Q 
  envs_lookup i Δ = Some (p,  P)%I  TimelessP P 
  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' 
  (Δ'  Q)  Δ  Q.
Proof.
  intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
  rewrite always_if_later right_id. by apply timeless_elim.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
388
(** * Always *)
389
Lemma tac_always_intro Δ Q : envs_persistent Δ = true  (Δ  Q)  Δ   Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
390 391 392
Proof. intros. by apply: always_intro. Qed.

Lemma tac_persistent Δ Δ' i p P P' Q :
393
  envs_lookup i Δ = Some (p, P)  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
394
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
395
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
396
Proof.
397
  intros ??? <-. rewrite envs_replace_sound //; simpl.
398
  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
399 400 401 402 403 404
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
  envs_persistent Δ = true 
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
405
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
406 407 408 409 410
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 :
411
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
412
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
413
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
414 415
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
416
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
417
Qed.
418
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
419
Proof.
420
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
421 422 423
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
424
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
425
Proof.
426
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
427 428
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
429
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
430
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
431
  (Δ'  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
432 433 434 435
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
436
Lemma tac_wand_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
437
Proof.
438
  intros. by apply wand_intro_l; rewrite (into_pure P); apply pure_elim_sep_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
439 440 441 442 443 444
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, Δ') 
445
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
446
  IntoWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
447 448 449 450 451
  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 Δ'' 
452
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
453 454 455
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
456
    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
457
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
458 459
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
460
    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
461 462
Qed.

463 464 465
Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
  into_assert : R  (P - Q)  Q.
Global Arguments into_assert _ _ _ {_}.
466
Lemma into_assert_default P Q : IntoAssert P Q P.
467
Proof. by rewrite /IntoAssert wand_elim_r. Qed.
468 469

Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
470
  envs_lookup_delete j Δ = Some (q, R, Δ') 
471
  IntoWand R P1 P2  IntoAssert P1 Q P1' 
Robbert Krebbers's avatar
Robbert Krebbers committed
472
  ('(Δ1,Δ2)  envs_split lr js Δ';
473
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
474
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
475
  (Δ1  P1')  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
Proof.
477
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
478 479 480 481
  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.
482 483
  rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
  rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
484
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
485 486
Qed.

487 488
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
  envs_lookup j Δ = Some (q, R) 
489
  IntoWand R P1 P2  FromPure P1 φ 
490
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
491
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
Proof.
493
  intros. rewrite envs_simple_replace_sound //; simpl.
494
  by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
495 496
Qed.

497 498
Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
499
  IntoWand R P1 P2 
500
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
501 502
  (Δ'  P1)  (PersistentP P1  PersistentP P2) 
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
Proof.
504 505 506 507 508
  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.
509
    rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
510 511 512
    by rewrite wand_elim_r.
  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
    rewrite envs_simple_replace_sound //; simpl.
513
    rewrite (sep_elim_r _ (_ - _)) right_id (into_wand R) always_if_elim.
514
    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
515 516 517 518
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
519
  (Δ'  if p then  P  Q else P - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
520 521 522 523 524 525
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.

526
Lemma tac_revert_spatial Δ Q :
527
  (envs_clear_spatial Δ  env_fold uPred_wand Q (env_spatial Δ))  Δ  Q.
528 529 530 531
Proof.
  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed.

532
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
533
  IntoAssert P Q R 
Robbert Krebbers's avatar
Robbert Krebbers committed
534
  envs_split lr js Δ = Some (Δ1,Δ2) 
535
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
536
  (Δ1  R)  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Proof.
538
  intros ??? HP HQ. rewrite envs_split_sound //.
539
  rewrite (envs_app_sound Δ2) //; simpl.
540
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
541 542 543 544
Qed.

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
545
  (Δ  P)  PersistentP P  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
546
Proof.
547
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
548 549 550 551
  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.

552
(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
553
not as [H : True -★ Q]. The class [IntoPosedProof] is used to strip off the
554 555
[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. *)
556 557 558 559 560 561 562
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.
563 564

Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
565 566
  (P1  P2)  IntoPosedProof P1 P2 R 
  envs_app true (Esnoc Enil j R) Δ = Some Δ' 
567
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
568
Proof.
569
  intros HP ?? <-. rewrite envs_app_sound //; simpl.
570
  by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
571 572
Qed.

573 574 575
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 Δ'' 
576
  (Δ''  Q)  Δ  Q.
577 578 579 580 581 582 583 584
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
585
Lemma tac_apply Δ Δ' i p R P1 P2 :
586
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand R P1 P2 
587
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
588 589
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
590
  by rewrite (into_wand R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
591 592 593 594 595
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
Ralf Jung's avatar
Ralf Jung committed
596
   {A : cofeT} (x y : A) (Φ : A  uPred M),
597 598
    (Pxy  x  y) 
    (Q ⊣⊢ Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
599
    ( n, Proper (dist n ==> dist n) Φ) 
600
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
601 602 603 604 605 606 607 608
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) 
609
  envs_lookup j Δ = Some (q, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
610
   {A : cofeT} Δ' x y (Φ : A  uPred M),
611 612
    (Pxy  x  y) 
    (P ⊣⊢ Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
613 614
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
615
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
616 617 618 619
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.
620 621 622 623 624
  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
625 626 627
Qed.

(** * Conjunction splitting *)
628 629
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
630 631 632

(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
633
  FromSep P Q1 Q2 
Robbert Krebbers's avatar
Robbert Krebbers committed
634
  envs_split lr js Δ = Some (Δ1,Δ2) 
635
  (Δ1  Q1)  (Δ2  Q2)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
636
Proof.
637
  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
638 639 640 641 642 643
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) 
644
  FromSep P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
645 646
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
647
  (Δ4  Q)  Δ1  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
648 649 650 651 652
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.
653
      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
655
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
656 657
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
658
      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
659
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
660
      by rewrite right_id assoc (from_sep P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
661 662 663 664
Qed.

(** * Conjunction/separating conjunction elimination *)
Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
665
  envs_lookup i Δ = Some (p, P)  IntoSep p P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
666
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
667
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
668
Proof.
669
  intros. rewrite envs_simple_replace_sound //; simpl.
670
  by rewrite (into_sep p P) right_id (comm uPred_sep P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
671 672 673
Qed.

(** * Framing *)
674 675 676
Lemma tac_frame Δ Δ' i p R P Q :
  envs_lookup_delete i Δ = Some (p, R, Δ')  Frame R P Q 
  ((if p then Δ else Δ')  Q)  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
677
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
678
  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
679 680
  - by rewrite envs_lookup_persistent_sound // always_elim -(frame R P) HQ.
  - rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
681 682 683
Qed.

(** * Disjunction *)
684 685 686 687
Lemma tac_or_l Δ P Q1 Q2 : FromOr P Q1 Q2  (Δ  Q1)  Δ  P.
Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
Lemma tac_or_r Δ P Q1 Q2 : FromOr P Q1 Q2  (Δ  Q2)  Δ  P.
Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
688 689

Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
690
  envs_lookup i Δ = Some (p, P)  IntoOr P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
691 692
  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 
  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 
693
  (Δ1  Q)  (Δ2  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
694
Proof.
695
  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
696
  rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
697 698 699 700
  - rewrite (envs_simple_replace_sound' _ Δ1) //.
    by rewrite /= right_id wand_elim_r.
  - rewrite (envs_simple_replace_sound' _ Δ2) //.
    by rewrite /= right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
701 702 703
Qed.

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

707
Class ForallSpecialize {As} (xs : hlist As)
708
  (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P  Φ xs.
709 710 711 712 713 714 715 716 717 718 719
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 Φ 
720
  envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ' 
721
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
722
Proof.
723 724
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id (forall_specialize _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
725 726 727
Qed.

Lemma tac_forall_revert {A} Δ (Φ : A  uPred M) :
728
  (Δ   a, Φ a)   a, Δ  Φ a.
Robbert Krebbers's avatar
Robbert Krebbers committed
729 730 731
Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
736
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A  uPred M) Q :
737
  envs_lookup i Δ = Some (p, P)  IntoExist P Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
738
  ( a,  Δ',
739
    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ'  (Δ'  Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
740 741
  Δ  Q.
Proof.
742
  intros ?? HΦ. rewrite envs_lookup_sound //.
743
  rewrite (into_exist P) always_if_exist sep_exist_r.
744 745
  apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
  rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
746 747
Qed.
End tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
748

749
Hint Extern 0 (IntoPosedProof True _ _) =>
750
  class_apply @to_posed_proof_True : typeclass_instances.