coq_tactics.v 37.9 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
From iris.algebra Require Export upred.
From iris.algebra Require Import upred_big_op upred_tactics.
From iris.proofmode Require Export environments.
4
From iris.prelude Require Import stringmap hlist.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
Import uPred.

Local Notation "Γ !! j" := (env_lookup j Γ).
Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
Local Notation "' ( x1 , x2 ) ← y ; z" :=
  (match y with Some (x1,x2) => z | None => None end).
Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
  (match y with Some (x1,x2,x3) => z | None => None end).

Record envs (M : cmraT) :=
  Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
Arguments Envs {_} _ _.
Arguments env_persistent {_} _.
Arguments env_spatial {_} _.

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

Coercion of_envs {M} (Δ : envs M) : uPred M :=
  ( envs_wf Δ   Π env_persistent Δ  Π★ env_spatial Δ)%I.
29
30
31
32
33
34
Instance: Params (@of_envs) 1.

Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
  env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

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

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

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

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

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

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

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

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
99
100
101
102
103
(* Coq versions of the tactics *)
Section tactics.
Context {M : cmraT}.
Implicit Types Γ : env (uPred M).
Implicit Types Δ : envs M.
Implicit Types P Q : uPred M.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
110
111
112
113
114
115
116
117
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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
Proof.
  rewrite /envs_lookup /envs_delete /of_envs=>?; apply const_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
    ecancel [ Π _;  P; Π★ _]%I; apply const_intro.
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=.
    ecancel [ Π _; P; Π★ _]%I; apply const_intro.
    destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh.
Qed.
Lemma envs_lookup_sound' Δ i p P :
  envs_lookup i Δ = Some (p,P)  Δ  (P  envs_delete i p Δ).
134
Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
140
141
Lemma envs_lookup_persistent_sound Δ i P :
  envs_lookup i Δ = Some (true,P)  Δ  ( P  Δ).
Proof.
  intros. apply: always_entails_l. by rewrite envs_lookup_sound // sep_elim_l.
Qed.

Lemma envs_lookup_split Δ i p P :
142
  envs_lookup i Δ = Some (p,P)  Δ  (?p P  (?p P - Δ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
145
146
147
148
149
150
151
152
153
154
Proof.
  rewrite /envs_lookup /of_envs=>?; apply const_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //= always_and_sep always_sep.
    rewrite const_equiv // left_id.
    cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //=. rewrite const_equiv // left_id.
    cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.

Lemma envs_lookup_delete_sound Δ Δ' i p P :
155
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  (?p P  Δ')%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159
160
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
Lemma envs_lookup_delete_sound' Δ Δ' i p P :
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ  (P  Δ')%I.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.

161
Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ'  Δ  (?p Π★ Γ - Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
164
165
166
167
168
169
170
171
Proof.
  rewrite /of_envs /envs_app=> ?; apply const_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γp') //.
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
176
177
178
179
180
181
182
183
184
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
185
  envs_delete i p Δ  (?p Π★ Γ - Δ')%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
189
190
191
192
193
194
195
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
  apply const_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γp') //.
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
200
201
202
203
204
205
206
207
208
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, sep_intro_True_l; [apply const_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γs') // big_sep_app. solve_sep_entails.
Qed.

Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
209
  Δ  (?p P  (?p Π★ Γ - Δ'))%I.
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 Π★ Γ - Δ')%I.
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 Π★ Γ - Δ'))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
225
226
227
228
229
230
231
232
233
234
235
236
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

Lemma envs_split_sound Δ lr js Δ1 Δ2 :
  envs_split lr js Δ = Some (Δ1,Δ2)  Δ  (Δ1  Δ2).
Proof.
  rewrite /envs_split /of_envs=> ?; apply const_elim_sep_l=> Hwf.
  destruct Δ as [Γp Γs], (env_split js _) as [[Γs1 Γs2]|] eqn:?; simplify_eq/=.
  rewrite (env_split_perm Γs) // big_sep_app {1}always_sep_dup'.
  destruct lr; simplify_eq/=; cancel [ Π Γp;  Π Γp; Π★ Γs1; Π★ Γs2]%I;
    destruct Hwf; apply sep_intro_True_l; apply const_intro; constructor;
      naive_solver eauto using env_split_wf_1, env_split_wf_2,
      env_split_fresh_1, env_split_fresh_2.
Qed.

237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
Lemma envs_clear_spatial_sound Δ :
  Δ  (envs_clear_spatial Δ  Π★ env_spatial Δ)%I.
Proof.
  rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
  rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
  destruct Hwf; constructor; simpl; auto using Enil_wf.
Qed.

Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ  (Π★ Γ - Q).
Proof.
  revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
  by rewrite IH wand_curry (comm uPred_sep).
Qed.

Lemma envs_persistent_persistent Δ : envs_persistent Δ = true  PersistentP Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
253
Hint Immediate envs_persistent_persistent : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
254

255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
Global Instance envs_Forall2_refl (R : relation (uPred M)) :
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Global Instance envs_Forall2_sym (R : relation (uPred M)) :
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Global Instance envs_Forall2_trans (R : relation (uPred M)) :
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Global Instance envs_Forall2_antisymm (R R' : relation (uPred M)) :
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Lemma envs_Forall2_impl (R R' : relation (uPred M)) Δ1 Δ2 :
  envs_Forall2 R Δ1 Δ2  ( P Q, R P Q  R' P Q)  envs_Forall2 R' Δ1 Δ2.
Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.

Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; unfold of_envs; simpl in *.
  apply const_elim_sep_l=>Hwf. apply sep_intro_True_l.
  - destruct Hwf; apply const_intro; constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Global Instance of_envs_proper : Proper (envs_Forall2 () ==> ()) (@of_envs M).
Proof.
  intros Δ1 Δ2 ?; apply (anti_symm ()); apply of_envs_mono;
    eapply envs_Forall2_impl; [| |symmetry|]; eauto using equiv_entails.
Qed.
Global Instance Envs_mono (R : relation (uPred M)) :
  Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
Proof. by constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
288
289
290
291
292
293
294
295
(** * Adequacy *)
Lemma tac_adequate P : Envs Enil Enil  P  True  P.
Proof.
  intros <-. rewrite /of_envs /= always_const !right_id.
  apply const_intro; repeat constructor.
Qed.

(** * Basic rules *)
296
Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : ?p P  Q.
297
Arguments to_assumption _ _ _ {_}.
298
Global Instance to_assumption_exact p P : ToAssumption p P P.
299
Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
300
301
302
303
Global Instance to_assumption_always_l p P Q :
  ToAssumption p P Q  ToAssumption p ( P) Q.
Proof. rewrite /ToAssumption=><-. by rewrite always_elim. Qed.
Global Instance to_assumption_always_r P Q :
304
305
306
307
308
309
  ToAssumption true P Q  ToAssumption true P ( Q).
Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.

Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p,P)  ToAssumption p P Q  Δ  Q.
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
311
312
313
314
315
316
317
318
319
320
321

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
  Δ'  Q  Δ  Q.
Proof.
  intros. rewrite envs_simple_replace_sound //.
  destruct p; simpl; by rewrite right_id wand_elim_r.
Qed.
Lemma tac_clear Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ')  Δ'  Q  Δ  Q.
Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
322
323
324
Lemma tac_clear_spatial Δ Δ' Q :
  envs_clear_spatial Δ = Δ'  Δ'  Q  Δ  Q.
Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
325
326
327
328
329
330

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

(** * Pure *)
331
Class ToPure (P : uPred M) (φ : Prop) := to_pure : P   φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
333
334
335
336
337
338
339
340
Arguments to_pure : clear implicits.
Global Instance to_pure_const φ : ToPure ( φ) φ.
Proof. done. Qed.
Global Instance to_pure_eq {A : cofeT} (a b : A) :
  Timeless a  ToPure (a  b) (a  b).
Proof. intros; red. by rewrite timeless_eq. Qed.
Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure ( a) ( a).
Proof. intros; red. by rewrite discrete_valid. Qed.

341
342
343
Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ  φ  Δ  Q.
Proof. intros ->. apply const_intro. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
Lemma tac_pure Δ Δ' i p P φ Q :
  envs_lookup_delete i Δ = Some (p, P, Δ')  ToPure P φ 
  (φ  Δ'  Q)  Δ  Q.
Proof.
  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
  rewrite (to_pure P); by apply const_elim_sep_l.
Qed.

Lemma tac_pure_revert Δ φ Q : Δ  ( φ  Q)  (φ  Δ  Q).
Proof. intros HΔ ?. by rewrite HΔ const_equiv // left_id. Qed.

(** * Later *)
Class StripLaterEnv (Γ1 Γ2 : env (uPred M)) :=
  strip_later_env : env_Forall2 StripLaterR Γ1 Γ2.
Global Instance strip_later_env_nil : StripLaterEnv Enil Enil.
Proof. constructor. Qed.
Global Instance strip_later_env_snoc Γ1 Γ2 i P Q :
  StripLaterEnv Γ1 Γ2  StripLaterR P Q 
  StripLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.

Class StripLaterEnvs (Δ1 Δ2 : envs M) := {
  strip_later_persistent: StripLaterEnv (env_persistent Δ1) (env_persistent Δ2);
  strip_later_spatial: StripLaterEnv (env_spatial Δ1) (env_spatial Δ2)
}.
Global Instance strip_later_envs Γp1 Γp2 Γs1 Γs2 :
  StripLaterEnv Γp1 Γp2  StripLaterEnv Γs1 Γs2 
  StripLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Proof. by split. Qed.
Lemma strip_later_env_sound Δ1 Δ2 : StripLaterEnvs Δ1 Δ2  Δ1   Δ2.
Proof.
  intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
  repeat apply sep_mono; try apply always_mono.
  - rewrite -later_intro; apply const_mono; destruct 1; constructor;
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - induction Hp; rewrite /= ?later_and; auto using and_mono, later_intro.
  - induction Hs; rewrite /= ?later_sep; auto using sep_mono, later_intro.
Qed.

Lemma tac_next Δ Δ' Q Q' :
  StripLaterEnvs Δ Δ'  StripLaterL Q Q'  Δ'  Q'  Δ  Q.
Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.

Lemma tac_löb Δ Δ' i Q :
388
389
  envs_persistent Δ = true 
  envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
390
391
  Δ'  Q  Δ  Q.
Proof.
392
393
394
395
  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
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
Qed.

(** * Always *)
Lemma tac_always_intro Δ Q : envs_persistent Δ = true  Δ  Q  Δ   Q.
Proof. intros. by apply: always_intro. Qed.

Class ToPersistentP (P Q : uPred M) := to_persistentP : P   Q.
Arguments to_persistentP : clear implicits.
Global Instance to_persistentP_always_trans P Q :
  ToPersistentP P Q  ToPersistentP ( P) Q | 0.
Proof. rewrite /ToPersistentP=> ->. by rewrite always_always. Qed.
Global Instance to_persistentP_always P : ToPersistentP ( P) P | 1.
Proof. done. Qed.
Global Instance to_persistentP_persistent P :
  PersistentP P  ToPersistentP P P | 100.
Proof. done. Qed.

Lemma tac_persistent Δ Δ' i p P P' Q :
414
  envs_lookup i Δ = Some (p, P)  ToPersistentP P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
415
416
417
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
  Δ'  Q  Δ  Q.
Proof.
418
419
  intros ??? <-. rewrite envs_replace_sound //; simpl.
  by rewrite right_id (to_persistentP P) always_if_always wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
Qed.

(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
  envs_persistent Δ = true 
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
  Δ'  Q  Δ  (P  Q).
Proof.
  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
  by rewrite right_id always_wand_impl always_elim HQ.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
  ToPersistentP P P' 
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
  Δ'  Q  Δ  (P  Q).
Proof.
  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
  by rewrite right_id {1}(to_persistentP P) always_and_sep_l wand_elim_r.
Qed.
Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ  (φ  Δ  Q)  Δ  (P  Q).
Proof.
  intros. by apply impl_intro_l; rewrite (to_pure P); apply const_elim_l.
Qed.

Lemma tac_wand_intro Δ Δ' i P Q :
  envs_app false (Esnoc Enil i P) Δ = Some Δ'  Δ'  Q  Δ  (P - Q).
Proof.
447
  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
  ToPersistentP P P' 
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
  Δ'  Q  Δ  (P - Q).
Proof.
  intros. rewrite envs_app_sound //; simpl.
  rewrite right_id. by apply wand_mono.
Qed.
Lemma tac_wand_intro_pure Δ P φ Q : ToPure P φ  (φ  Δ  Q)  Δ  (P - Q).
Proof.
  intros. by apply wand_intro_l; rewrite (to_pure P); apply const_elim_sep_l.
Qed.

Class ToWand (R P Q : uPred M) := to_wand : R  (P - Q).
Arguments to_wand : clear implicits.
Global Instance to_wand_wand P Q : ToWand (P - Q) P Q.
Proof. done. Qed.
Global Instance to_wand_impl P Q : ToWand (P  Q) P Q.
Proof. apply impl_wand. Qed.
Global Instance to_wand_iff_l P Q : ToWand (P  Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance to_wand_iff_r P Q : ToWand (P  Q) Q P.
Proof. apply and_elim_r', impl_wand. Qed.
472
473
Global Instance to_wand_always R P Q : ToWand R P Q  ToWand ( R) P Q.
+Proof. rewrite /ToWand=> ->. apply always_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
476
477
478

(* 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, Δ') 
479
  envs_lookup j (if p then Δ else Δ') = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
480
481
482
483
484
485
486
487
488
489
  ToWand R P1 P2 
  match p with
  | true  => envs_simple_replace j q (Esnoc Enil j P2) Δ
  | false => envs_replace j q false (Esnoc Enil j P2) Δ'
             (* remove [i] and make [j] spatial *)
  end = Some Δ'' 
  Δ''  Q  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
490
491
    rewrite assoc (to_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
    by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
493
  - rewrite envs_lookup_sound //; simpl.
    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
494
    by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
495
496
Qed.

497
498
499
500
501
502
503
Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
  to_assert : (R  (P - Q))  Q.
Global Arguments to_assert _ _ _ {_}.
Lemma to_assert_fallthrough P Q : ToAssert P Q P.
Proof. by rewrite /ToAssert wand_elim_r. Qed.

Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
504
  envs_lookup_delete j Δ = Some (q, R, Δ') 
505
  ToWand R P1 P2  ToAssert P1 Q P1' 
Robbert Krebbers's avatar
Robbert Krebbers committed
506
  ('(Δ1,Δ2)  envs_split lr js Δ';
507
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
508
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)
509
  Δ1  P1'  Δ2'  Q  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
Proof.
511
  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
513
514
515
  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.
516
517
518
  rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
  rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
  by rewrite always_if_elim assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
519
520
Qed.

521
522
523
524
525
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
  envs_lookup j Δ = Some (q, R) 
  ToWand R P1 P2  ToPure P1 φ 
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' 
  φ  Δ'  Q  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
Proof.
527
528
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id (to_wand R) (to_pure P1) const_equiv // wand_True wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
529
530
Qed.

531
532
533
534
535
536
Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
  envs_lookup_delete j Δ = Some (q, R, Δ') 
  ToWand R P1 P2 
  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' 
  Δ'  P1  (PersistentP P1  PersistentP P2) 
  Δ''  Q  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Proof.
538
539
540
541
542
543
544
545
546
547
548
  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 (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
    by rewrite wand_elim_r.
  - rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
    rewrite envs_simple_replace_sound //; simpl.
    rewrite (sep_elim_r _ (_ - _)) right_id (to_wand R) always_if_elim.
    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
549
550
551
552
553
554
555
556
557
558
559
Qed.

Lemma tac_revert Δ Δ' i p P Q :
  envs_lookup_delete i Δ = Some (p,P,Δ') 
  Δ'  (if p then  P  Q else P - Q)  Δ  Q.
Proof.
  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p.
  - by rewrite HQ -always_and_sep_l impl_elim_r.
  - by rewrite HQ wand_elim_r.
Qed.

560
561
562
563
564
565
Lemma tac_revert_spatial Δ Q :
  envs_clear_spatial Δ  (env_fold uPred_wand Q (env_spatial Δ))  Δ  Q.
Proof.
  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed.

566
567
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
  ToAssert P Q R 
Robbert Krebbers's avatar
Robbert Krebbers committed
568
  envs_split lr js Δ = Some (Δ1,Δ2) 
569
  envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' 
570
  Δ1  R  Δ2'  Q  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
571
Proof.
572
  intros ??? HP HQ. rewrite envs_split_sound //.
573
  rewrite (envs_app_sound Δ2) //; simpl.
574
  by rewrite right_id HP HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
576
577
578
Qed.

Lemma tac_assert_persistent Δ Δ' j P Q :
  envs_app true (Esnoc Enil j P) Δ = Some Δ' 
579
  Δ  P  PersistentP P  Δ'  Q  Δ  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
580
Proof.
581
  intros ? HP ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
582
583
584
585
  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.

586
(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
587
588
589
590
591
592
593
594
595
596
597
598
not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the
[True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : P1  P2  True  R.
Arguments to_pose_proof : clear implicits.
Instance to_posed_proof_True P : ToPosedProof True P P.
Proof. by rewrite /ToPosedProof. Qed.
Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P - Q).
Proof. rewrite /ToPosedProof. apply entails_wand. Qed.

Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
  P1  P2  ToPosedProof P1 P2 R  envs_app true (Esnoc Enil j R) Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
599
600
  Δ'  Q  Δ  Q.
Proof.
601
602
  intros HP ?? <-. rewrite envs_app_sound //; simpl.
  by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True.
Robbert Krebbers's avatar
Robbert Krebbers committed
603
604
Qed.

605
606
607
608
609
610
611
612
613
614
615
616
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
  envs_lookup_delete i Δ = Some (p, P, Δ') 
  envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' 
  Δ''  Q  Δ  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
  - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
    by rewrite right_id wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
617
Lemma tac_apply Δ Δ' i p R P1 P2 :
618
  envs_lookup_delete i Δ = Some (p, R, Δ')  ToWand R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
619
620
621
622
623
624
625
626
627
  Δ'  P1  Δ  P2.
Proof.
  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
  by rewrite (to_wand R) HP1 wand_elim_l.
Qed.

(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
Ralf Jung's avatar
Ralf Jung committed
628
   {A : cofeT} (x y : A) (Φ : A  uPred M),
629
    Pxy  (x  y) 
Robbert Krebbers's avatar
Robbert Krebbers committed
630
631
632
633
634
635
636
637
638
639
640
    Q  Φ (if lr then y else x) 
    ( n, Proper (dist n ==> dist n) Φ) 
    Δ  Φ (if lr then x else y)  Δ  Q.
Proof.
  intros ? A x y ? HPxy -> ?; apply eq_rewrite; auto.
  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
  destruct lr; auto using eq_sym.
Qed.

Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
  envs_lookup i Δ = Some (p, Pxy) 
641
  envs_lookup j Δ = Some (q, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
642
   {A : cofeT} Δ' x y (Φ : A  uPred M),
643
    Pxy  (x  y) 
Robbert Krebbers's avatar
Robbert Krebbers committed
644
645
646
647
648
649
650
651
    P  Φ (if lr then y else x) 
    ( n, Proper (dist n ==> dist n) Φ) 
    envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' 
    Δ'  Q  Δ  Q.
Proof.
  intros ?? A Δ' x y Φ HPxy HP ?? <-.
  rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
  rewrite sep_elim_l HPxy always_and_sep_r.
652
653
654
655
656
  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
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
Qed.

(** * Conjunction splitting *)
Class AndSplit (P Q1 Q2 : uPred M) := and_split : (Q1  Q2)  P.
Arguments and_split : clear implicits.

Global Instance and_split_and P1 P2 : AndSplit (P1  P2) P1 P2.
Proof. done. Qed.
Global Instance and_split_sep_persistent_l P1 P2 :
  PersistentP P1  AndSplit (P1  P2) P1 P2.
Proof. intros. by rewrite /AndSplit always_and_sep_l. Qed.
Global Instance and_split_sep_persistent_r P1 P2 :
  PersistentP P2  AndSplit (P1  P2) P1 P2.
Proof. intros. by rewrite /AndSplit always_and_sep_r. Qed.

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

(** * Separating conjunction splitting *)
Class SepSplit (P Q1 Q2 : uPred M) := sep_split : (Q1  Q2)  P.
Arguments sep_split : clear implicits.

Global Instance sep_split_sep P1 P2 : SepSplit (P1  P2) P1 P2 | 100.
Proof. done. Qed.
Global Instance sep_split_ownM (a b : M) :
  SepSplit (uPred_ownM (a  b)) (uPred_ownM a) (uPred_ownM b) | 99.
Proof. by rewrite /SepSplit ownM_op. Qed.

Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
  SepSplit P Q1 Q2 
  envs_split lr js Δ = Some (Δ1,Δ2) 
  Δ1  Q1  Δ2  Q2  Δ  P.
Proof.
  intros. rewrite envs_split_sound // -(sep_split P). by apply sep_mono.
Qed.

(** * Combining *)
Lemma tac_combine Δ1 Δ2 Δ3 Δ4 i1 p P1 i2 q P2 j P Q :
  envs_lookup_delete i1 Δ1 = Some (p,P1,Δ2) 
  envs_lookup_delete i2 (if p then Δ1 else Δ2) = Some (q,P2,Δ3) 
  SepSplit P P1 P2 
  envs_app (p && q) (Esnoc Enil j P)
    (if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4 
  Δ4  Q  Δ1  Q.
Proof.
  intros [? ->]%envs_lookup_delete_Some [? ->]%envs_lookup_delete_Some ?? <-.
  destruct p.
  - rewrite envs_lookup_persistent_sound //. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
      by rewrite right_id assoc -always_sep (sep_split P) wand_elim_r.
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
  - rewrite envs_lookup_sound //; simpl. destruct q.
    + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
    + rewrite envs_lookup_sound // envs_app_sound //; simpl.
      by rewrite right_id assoc (sep_split P) wand_elim_r.
Qed.

(** * Conjunction/separating conjunction elimination *)
Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
718
  sep_destruct : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
719
720
Arguments sep_destruct : clear implicits.
Lemma sep_destruct_spatial p P Q1 Q2 : P  (Q1  Q2)  SepDestruct p P Q1 Q2.
721
Proof. rewrite /SepDestruct=> ->. by rewrite always_if_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
722
723
724
725
726
727
728
729

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

Global Instance sep_destruct_and P Q : SepDestruct true (P  Q) P Q.
730
Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
731
732
Global Instance sep_destruct_and_persistent_l P Q :
  PersistentP P  SepDestruct false (P  Q) P Q.
733
Proof. intros; by rewrite /SepDestruct /= always_and_sep_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
734
735
Global Instance sep_destruct_and_persistent_r P Q :
  PersistentP Q  SepDestruct false (P  Q) P Q.
736
Proof. intros; by rewrite /SepDestruct /= always_and_sep_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
737
738
739

Global Instance sep_destruct_later p P Q1 Q2 :
  SepDestruct p P Q1 Q2  SepDestruct p ( P) ( Q1) ( Q2).
740
Proof. by rewrite /SepDestruct -later_sep !always_if_later=> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
741
742

Lemma tac_sep_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
743
  envs_lookup i Δ = Some (p, P)  SepDestruct p P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
744
745
746
  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' 
  Δ'  Q  Δ  Q.
Proof.
747
748
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite (sep_destruct p P) right_id (comm uPred_sep P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
749
750
751
Qed.

(** * Framing *)
Robbert Krebbers's avatar
Robbert Krebbers committed
752
753
754
755
(** The [option] is to account for formulas that can be framed entirely, so
we do not end up with [True]s everywhere. *)
Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
  frame : (R  from_option True mQ)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
756
757
Arguments frame : clear implicits.

758
Global Instance frame_here R : Frame R R None.
Robbert Krebbers's avatar
Robbert Krebbers committed
759
Proof. by rewrite /Frame right_id. Qed.
760
Global Instance frame_sep_l R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
761
  Frame R P1 mQ 
762
  Frame R (P1  P2) (Some $ if mQ is Some Q then Q  P2 else P2)%I | 9.
Robbert Krebbers's avatar
Robbert Krebbers committed
763
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
764
Global Instance frame_sep_r R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
765
  Frame R P2 mQ 
766
  Frame R (P1  P2) (Some $ if mQ is Some Q then P1  Q else P1)%I | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
767
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
768
Global Instance frame_and_l R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
769
  Frame R P1 mQ 
770
  Frame R (P1  P2) (Some $ if mQ is Some Q then Q  P2 else P2)%I | 9.
Robbert Krebbers's avatar
Robbert Krebbers committed
771
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
772
Global Instance frame_and_r R P1 P2 mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
773
  Frame R P2 mQ 
774
  Frame R (P1  P2) (Some $ if mQ is Some Q then P1  Q else P1)%I | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
775
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
776
Global Instance frame_or R P1 P2 mQ1 mQ2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
777
778
779
780
781
782
783
784
785
  Frame R P1 mQ1  Frame R P2 mQ2 
  Frame R (P1  P2) (match mQ1, mQ2 with
                     | Some Q1, Some Q2 => Some (Q1  Q2)%I | _, _ => None
                     end).
Proof.
  rewrite /Frame=> <- <-.
  destruct mQ1 as [Q1|], mQ2 as [Q2|]; simpl; auto with I.
  by rewrite -sep_or_l.
Qed.
786
Global Instance frame_later R P mQ :
Robbert Krebbers's avatar
Robbert Krebbers committed
787
788
789
790
791
  Frame R P mQ  Frame R ( P) (if mQ is Some Q then Some ( Q) else None)%I.
Proof.
  rewrite /Frame=><-.
  by destruct mQ; rewrite /= later_sep -(later_intro R) ?later_True.
Qed.
792
Global Instance frame_exist {A} R (Φ : A  uPred M) mΨ :
Robbert Krebbers's avatar
Robbert Krebbers committed
793
794
  ( a, Frame R (Φ a) (mΨ a)) 
  Frame R ( x, Φ x) (Some ( x, if mΨ x is Some Q then Q else True))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
795
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
796
Global Instance frame_forall {A} R (Φ : A  uPred M) mΨ :
Robbert Krebbers's avatar
Robbert Krebbers committed
797
798
  ( a, Frame R (Φ a) (mΨ a)) 
  Frame R ( x, Φ x) (Some ( x, if mΨ x is Some Q then Q else True))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
799
800
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
801
Lemma tac_frame Δ Δ' i p R P mQ :
802
  envs_lookup_delete i Δ = Some (p, R, Δ')  Frame R P mQ 
Robbert Krebbers's avatar
Robbert Krebbers committed
803
804
  (if mQ is Some Q then (if p then Δ else Δ')  Q else True) 
  Δ  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
805
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
806
807
808
809
810
  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
  - rewrite envs_lookup_persistent_sound // always_elim.
    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
  - rewrite envs_lookup_sound //; simpl.
    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
Robbert Krebbers's avatar
Robbert Krebbers committed
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
Qed.

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

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

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

Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
Ralf Jung's avatar
Ralf Jung committed
833
  envs_lookup i Δ = Some (p, P)  OrDestruct P P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
834
835
836
837
  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 
  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 
  Δ1  Q  Δ2  Q  Δ  Q.
Proof.
838
839
840
841
842
843
  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
  rewrite (or_destruct P) always_if_or sep_or_r; apply or_elim.
  - rewrite (envs_simple_replace_sound' _ Δ1) //.
    by rewrite /= right_id wand_elim_r.
  - rewrite (envs_simple_replace_sound' _ Δ2) //.
    by rewrite /= right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
844
845
846
847
848
849
Qed.

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

850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
Class ForallSpecialize {As} (xs : hlist As)
    (P : uPred M) (Φ : himpl As (uPred M)) :=
  forall_specialize : P  happly Φ xs.
Arguments forall_specialize {_} _ _ _ {_}.

Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
Proof. done. Qed.
Global Instance forall_specialize_cons A As x xs Φ (Ψ : A  himpl As (uPred M)) :
  ( x, ForallSpecialize xs (Φ x) (Ψ x)) 
  ForallSpecialize (hcons x xs) ( x : A, Φ x) Ψ.
Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.

Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
  envs_lookup i Δ = Some (p, P)  ForallSpecialize xs P Φ 
  envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
865
866
  Δ'  Q  Δ  Q.
Proof.
867
868
  intros. rewrite envs_simple_replace_sound //; simpl.
  by rewrite right_id (forall_specialize _ P) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
869
870
871
872
873
874
875
876
877
878
879
880
881
Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
882
883
884
Lemma tac_exist {A} Δ P (Φ : A  uPred M) :
  ExistSplit P Φ  ( a, Δ  Φ a)  Δ  P.
Proof. intros ? [a ?]. rewrite -(exist_split P). eauto using exist_intro'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
885
886
887
888
889
890
891
892

Class ExistDestruct {A} (P : uPred M) (Φ : A  uPred M) :=
  exist_destruct : P  ( x, Φ x).
Arguments exist_destruct {_} _ _ {_}.
Global Instance exist_destruct_exist {A} (Φ : A  uPred M) :
  ExistDestruct ( a, Φ a) Φ.
Proof. done. Qed.
Global Instance exist_destruct_later {A} P (Φ : A  uPred M) :
893
894
  ExistDestruct P Φ  Inhabited A  ExistDestruct ( P) (λ a,  (Φ a))%I.
Proof. rewrite /ExistDestruct=> HP ?. by rewrite HP later_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
895
896

Lemma tac_exist_destruct {A} Δ i p j P (Φ : A  uPred M) Q :
897
  envs_lookup i Δ = Some (p, P)  ExistDestruct P Φ 
Robbert Krebbers's avatar
Robbert Krebbers committed
898
899
900
901
  ( a,  Δ',
    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ'  Δ'  Q) 
  Δ  Q.
Proof.
902
903
904
905
  intros ?? HΦ. rewrite envs_lookup_sound //.
  rewrite (exist_destruct P) always_if_exist sep_exist_r.
  apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
  rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
906
907
Qed.
End tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
908

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