coq_tactics.v 30.2 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
378
Qed.

(** * Always *)
379
Lemma tac_always_intro Δ Q : envs_persistent Δ = true  (Δ  Q)  Δ   Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
380
381
382
Proof. intros. by apply: always_intro. Qed.

Lemma tac_persistent Δ Δ' i p P P' Q :
383
  envs_lookup i Δ = Some (p, P)  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
384
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
385
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
Proof.
387
  intros ??? <-. rewrite envs_replace_sound //; simpl.
388
  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
389
390
391
392
393
394
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
  envs_persistent Δ = true 
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
395
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
396
397
398
399
400
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 :
401
  IntoPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
403
  (Δ'  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
405
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
406
  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
Qed.
408
Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ  (φ  Δ  Q)  Δ  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
409
Proof.
410
  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
412
413
Qed.

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

453
454
455
Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
  into_assert : R  (P - Q)  Q.
Global Arguments into_assert _ _ _ {_}.
456
Lemma into_assert_default P Q : IntoAssert P Q P.
457
Proof. by rewrite /IntoAssert wand_elim_r. Qed.
458
459

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

477
478
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
  envs_lookup j Δ = Some (q, R) 
479
  IntoWand R P1 P2  FromPure P1 φ 
480
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
481
  φ  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
Proof.
483
  intros. rewrite envs_simple_replace_sound //; simpl.
484
  by rewrite right_id (into_wand R) -(from_pure P1) // wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
Qed.

487
488
Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
489
  IntoWand R P1 P2 
490
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
491
492
  (Δ'  P1)  (PersistentP P1  PersistentP P2) 
  (Δ''  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
493
Proof.
494
495
496
497
498
  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.
499
    rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
500
501
502
    by rewrite wand_elim_r.
  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
    rewrite envs_simple_replace_sound //; simpl.
503
    rewrite (sep_elim_r _ (_ - _)) right_id (into_wand R) always_if_elim.
504
    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
505
506
507
508
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
509
  (Δ'  if p then  P  Q else P - Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
511
512
513
514
515
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.

516
Lemma tac_revert_spatial Δ Q :
517
  (envs_clear_spatial Δ  env_fold uPred_wand Q (env_spatial Δ))  Δ  Q.
518
519
520
521
Proof.
  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed.

522
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
523
  IntoAssert P Q R 
Robbert Krebbers's avatar
Robbert Krebbers committed
524
  envs_split lr js Δ = Some (Δ1,Δ2) 
525
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
526
  (Δ1  R)  (Δ2'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
527
Proof.
528
  intros ??? HP HQ. rewrite envs_split_sound //.
529
  rewrite (envs_app_sound Δ2) //; simpl.
530
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
532
533
534
Qed.

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
535
  (Δ  P)  PersistentP P  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Proof.
537
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
539
540
541
  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.

542
(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
543
not as [H : True -★ Q]. The class [IntoPosedProof] is used to strip off the
544
545
[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. *)
546
547
548
549
550
551
552
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.
553
554

Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
555
556
  (P1  P2)  IntoPosedProof P1 P2 R 
  envs_app true (Esnoc Enil j R) Δ = Some Δ' 
557
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
558
Proof.
559
  intros HP ?? <-. rewrite envs_app_sound //; simpl.
560
  by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
562
Qed.

563
564
565
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 Δ'' 
566
  (Δ''  Q)  Δ  Q.
567
568
569
570
571
572
573
574
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
575
Lemma tac_apply Δ Δ' i p R P1 P2 :
576
  envs_lookup_delete i Δ = Some (p, R, Δ')  IntoWand R P1 P2 
577
  (Δ'  P1)  Δ  P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
578
579
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
580
  by rewrite (into_wand R) HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
581
582
583
584
585
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
Ralf Jung's avatar
Ralf Jung committed
586
   {A : cofeT} (x y : A) (Φ : A  uPred M),
587
588
    (Pxy  x  y) 
    (Q  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
589
    ( n, Proper (dist n ==> dist n) Φ) 
590
    (Δ  Φ (if lr then x else y))  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
592
593
594
595
596
597
598
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) 
599
  envs_lookup j Δ = Some (q, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
600
   {A : cofeT} Δ' x y (Φ : A  uPred M),
601
602
    (Pxy  x  y) 
    (P  Φ (if lr then y else x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
603
604
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
605
    (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
606
607
608
609
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.
610
611
612
613
614
  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
615
616
617
Qed.

(** * Conjunction splitting *)
618
619
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
620
621
622

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

(** * Conjunction/separating conjunction elimination *)
Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
655
  envs_lookup i Δ = Some (p, P)  IntoSep p P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
656
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
657
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
658
Proof.
659
  intros. rewrite envs_simple_replace_sound //; simpl.
660
  by rewrite (into_sep p P) right_id (comm uPred_sep P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
661
662
663
Qed.

(** * Framing *)
664
665
666
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
667
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
668
  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
669
670
  - 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
671
672
673
Qed.

(** * Disjunction *)
674
675
676
677
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
678
679

Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
680
  envs_lookup i Δ = Some (p, P)  IntoOr P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
681
682
  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 
  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 
683
  (Δ1  Q)  (Δ2  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
684
Proof.
685
  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
686
  rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
687
688
689
690
  - 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
691
692
693
Qed.

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

697
Class ForallSpecialize {As} (xs : hlist As)
698
  (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P  Φ xs.
699
700
701
702
703
704
705
706
707
708
709
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 Φ 
710
  envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ' 
711
  (Δ'  Q)  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
712
Proof.
713
714
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id (forall_specialize _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
716
717
Qed.

Lemma tac_forall_revert {A} Δ (Φ : A  uPred M) :
718
  (Δ   a, Φ a)   a, Δ  Φ a.
Robbert Krebbers's avatar
Robbert Krebbers committed
719
720
721
Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.

(** * Existential *)
722
723
724
725
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
726
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A  uPred M) Q :
727
  envs_lookup i Δ = Some (p, P)  IntoExist P Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
728
  ( a,  Δ',
729
    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ'  (Δ'  Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
730
731
  Δ  Q.
Proof.
732
  intros ?? HΦ. rewrite envs_lookup_sound //.
733
  rewrite (into_exist P) always_if_exist sep_exist_r.
734
735
  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
736
737
Qed.
End tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
738

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