coq_tactics.v 55.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
3
From iris.proofmode Require Export base environments classes modality_instances.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Import bi.
6
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8 9
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
10
(* Coq versions of the tactics *)
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15 16 17
Section bi_tactics.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

Lemma of_envs_eq Δ :
18
  of_envs Δ = (envs_wf Δ⌝   [] env_intuitionistic Δ  [] env_spatial Δ)%I.
19
Proof. done. Qed.
20
(** An environment is a ∗ of something intuitionistic and the spatial environment.
21 22 23 24
TODO: Can we define it as such? *)
Lemma of_envs_eq' Δ :
  of_envs Δ  (envs_wf Δ⌝   [] env_intuitionistic Δ)  [] env_spatial Δ.
Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed.
25

26 27 28 29 30 31 32 33 34
Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ. 
Proof. by destruct Δ. Qed.
Lemma envs_delete_spatial Δ i :
  envs_delete false i false Δ = envs_delete true i false Δ.
Proof. by destruct Δ. Qed.

Lemma envs_lookup_delete_Some Δ Δ' rp i p P :
  envs_lookup_delete rp i Δ = Some (p,P,Δ')
   envs_lookup i Δ = Some (p,P)  Δ' = envs_delete rp i p Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
35 36 37 38 39 40
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.

41
Lemma envs_lookup_sound' Δ rp i p P :
42
  envs_lookup i Δ = Some (p,P) 
43
  of_envs Δ  ?p P  of_envs (envs_delete rp i p Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
47
  - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
Robbert Krebbers's avatar
Robbert Krebbers committed
48
      naive_solver eauto using env_delete_wf, env_delete_fresh).
49
    destruct rp.
50 51 52 53
    + rewrite (env_lookup_perm Γp) //= intuitionistically_and.
      by rewrite and_sep_intuitionistically -assoc.
    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
      by rewrite intuitionistically_and and_elim_l -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56 57 58
    rewrite pure_True ?left_id; last (destruct Hwf; constructor;
      naive_solver eauto using env_delete_wf, env_delete_fresh).
    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
Qed.
59 60 61 62
Lemma envs_lookup_sound Δ i p P :
  envs_lookup i Δ = Some (p,P) 
  of_envs Δ  ?p P  of_envs (envs_delete true i p Δ).
Proof. apply envs_lookup_sound'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Lemma envs_lookup_persistent_sound Δ i P :
64
  envs_lookup i Δ = Some (true,P)  of_envs Δ   P  of_envs Δ.
65
Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
66 67 68 69 70 71 72 73 74 75 76 77 78
Lemma envs_lookup_sound_2 Δ i p P :
  envs_wf Δ  envs_lookup i Δ = Some (p,P) 
  ?p P  of_envs (envs_delete true i p Δ)  of_envs Δ.
Proof.
  rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [envs_wf Δ⌝%I]pure_True // left_id.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
  - rewrite (env_lookup_perm Γp) //= intuitionistically_and
      and_sep_intuitionistically and_elim_r.
    cancel [ P]%I. solve_sep_entails.
  - destruct (Γs !! i) eqn:?; simplify_eq/=.
    rewrite (env_lookup_perm Γs) //= and_elim_r.
    cancel [P]. solve_sep_entails.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80

Lemma envs_lookup_split Δ i p P :
81
  envs_lookup i Δ = Some (p,P)  of_envs Δ  ?p P  (?p P - of_envs Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
83 84 85 86
  intros. apply pure_elim with (envs_wf Δ).
  { rewrite of_envs_eq. apply and_elim_l. }
  intros. rewrite {1}envs_lookup_sound//.
  apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88
Qed.

89 90 91
Lemma envs_lookup_delete_sound Δ Δ' rp i p P :
  envs_lookup_delete rp i Δ = Some (p,P,Δ')  of_envs Δ  ?p P  of_envs Δ'.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92

93 94
Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps :
  envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') 
95
  of_envs Δ  ?p [] Ps  of_envs Δ'.
96 97
Proof.
  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
98
  { by rewrite intuitionistically_emp left_id. }
99
  destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
100
  apply envs_lookup_delete_Some in Hj as [Hj ->].
101
  destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
102
  rewrite -intuitionistically_if_sep_2 -assoc.
103
  rewrite envs_lookup_sound' //; rewrite IH //.
104
  repeat apply sep_mono=>//; apply intuitionistically_if_flag_mono; by destruct q1.
105 106
Qed.

Joseph Tassarotti's avatar
Joseph Tassarotti committed
107 108 109 110 111 112 113 114 115 116
Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
  envs_lookup_delete rp j Δ = Some (p1, P, Δ') 
  envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') 
  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
Proof. rewrite //= => -> //= -> //=. Qed.

Lemma envs_lookup_delete_list_nil Δ rp :
  envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
Proof. done. Qed.

117 118 119 120 121 122 123 124 125 126 127 128 129 130
Lemma envs_lookup_snoc Δ i p P :
  envs_lookup i Δ = None  envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc.
Qed.
Lemma envs_lookup_snoc_ne Δ i j p P :
  i  j  envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_snoc=> ?.
  destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne.
Qed.

Lemma envs_snoc_sound Δ p i P :
131
  envs_lookup i Δ = None  of_envs Δ  ?p P - of_envs (envs_snoc Δ p i P).
132
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
134 135
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  - apply and_intro; [apply pure_intro|].
137
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
138
      intros j; destruct (ident_beq_reflect j i); naive_solver.
139
    + by rewrite intuitionistically_and and_sep_intuitionistically assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  - apply and_intro; [apply pure_intro|].
141
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
142
      intros j; destruct (ident_beq_reflect j i); naive_solver.
143 144 145
    + solve_sep_entails.
Qed.

146
Lemma envs_app_sound Δ Δ' p Γ :
147 148
  envs_app p Γ Δ = Some Δ' 
  of_envs Δ  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157 158
    + 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') //.
159
      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
160
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
164 165 166
    + 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.
167
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
168 169
Qed.

170
Lemma envs_app_singleton_sound Δ Δ' p j Q :
171
  envs_app p (Esnoc Enil j Q) Δ = Some Δ'  of_envs Δ  ?p Q - of_envs Δ'.
172 173
Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
174 175
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' 
176
  of_envs (envs_delete true i p Δ)  (if p then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178
Proof.
  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
183 184 185 186
    + 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') //.
187
      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
188
      solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
189 190
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
    apply wand_intro_l, and_intro; [apply pure_intro|].
Robbert Krebbers's avatar
Robbert Krebbers committed
192 193 194
    + 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.
195
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197
Qed.

198 199
Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
200
  of_envs (envs_delete true i p Δ)  ?p Q - of_envs Δ'.
201 202
Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
203 204
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
205
  of_envs Δ  ?p P  ((if p then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.

208 209 210 211 212 213 214 215 216 217 218
Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P)  envs_simple_replace i p Γ Δ = Some Δ' 
  of_envs Δ  ?p P  (((if p then  [] Γ else [] Γ) - of_envs Δ')  (?p P - of_envs Δ)).
Proof.
  intros. apply pure_elim with (envs_wf Δ).
  { rewrite of_envs_eq. apply and_elim_l. }
  intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro.
  - rewrite envs_simple_replace_sound'//.
  - apply wand_intro_l, envs_lookup_sound_2; done.
Qed.

219 220 221
Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' 
222
  of_envs Δ  ?p P  (?p Q - of_envs Δ').
223 224 225 226
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
227
Lemma envs_replace_sound' Δ Δ' i p q Γ :
228
  envs_replace i p q Γ Δ = Some Δ' 
229
  of_envs (envs_delete true i p Δ)  (if q then  [] Γ else [] Γ) - of_envs Δ'.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
Proof.
231
  rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.

236 237
Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
238
  of_envs (envs_delete true i p Δ)  ?q Q - of_envs Δ'.
239 240
Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
241 242
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P)  envs_replace i p q Γ Δ = Some Δ' 
243
  of_envs Δ  ?p P  ((if q then  [] Γ else [] Γ) - of_envs Δ').
Robbert Krebbers's avatar
Robbert Krebbers committed
244 245
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.

246 247 248
Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
  envs_lookup i Δ = Some (p,P) 
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' 
249
  of_envs Δ  ?p P  (?q Q - of_envs Δ').
250 251
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.

252 253
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
Robbert Krebbers's avatar
Robbert Krebbers committed
254
  = ''(p,P)  envs_lookup j Δ; if p : bool then Some (p,P) else None.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
Proof.
256 257 258
  rewrite /envs_lookup /envs_clear_spatial.
  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
  by destruct (Γs !! j).
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
261
Lemma envs_clear_spatial_sound Δ :
262
  of_envs Δ  of_envs (envs_clear_spatial Δ)  [] env_spatial Δ.
263
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
264 265 266
  rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
267 268
Qed.

269
Lemma env_spatial_is_nil_intuitionistically Δ :
270
  env_spatial_is_nil Δ = true  of_envs Δ   of_envs Δ.
Robbert Krebbers's avatar
Robbert Krebbers committed
271 272
Proof.
  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
273
  rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and.
Ralf Jung's avatar
Ralf Jung committed
274
  by rewrite persistently_affinely_elim persistently_idemp persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
275
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
276

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

Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
  ( j P, envs_lookup j Δ1 = Some (false, P)  envs_lookup j Δ2 = None) 
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') 
298
  of_envs Δ1  of_envs Δ2  of_envs Δ1'  of_envs Δ2'.
299
Proof.
300 301
  revert Δ1 Δ2.
  induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
302 303
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite /of_envs !and_elim_l sep_elim_l. }
304 305
  destruct (envs_lookup_delete _ j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq/=; auto.
306 307
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
308 309 310 311
  rewrite -(IH _ _ _ HΔ); last first.
   { intros j' P'; destruct (decide (j = j')) as [->|].
     - by rewrite (envs_lookup_envs_delete _ _ _ P).
     - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
312 313
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
314
Lemma envs_split_sound Δ d js Δ1 Δ2 :
315
  envs_split d js Δ = Some (Δ1,Δ2)  of_envs Δ  of_envs Δ1  of_envs Δ2.
316
Proof.
317
  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
318
  rewrite {2}envs_clear_spatial_sound.
319 320
  rewrite (env_spatial_is_nil_intuitionistically (envs_clear_spatial _)) //.
  rewrite -persistently_and_intuitionistically_sep_l.
321
  rewrite (and_elim_l (<pers> _)%I)
322
          persistently_and_intuitionistically_sep_r intuitionistically_elim.
323 324 325
  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
  apply envs_split_go_sound in HΔ as ->; last first.
  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
326
  destruct d; simplify_eq/=; solve_sep_entails.
327 328
Qed.

329
Lemma prop_of_env_sound Γ : prop_of_env Γ  [] Γ.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
330
Proof.
331 332 333 334
  destruct Γ as [|Γ ? P]; simpl; first done.
  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
  - by rewrite right_id.
  - rewrite /= IH (comm _ Q _) assoc. done.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
335 336
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
337
Global Instance envs_Forall2_refl (R : relation PROP) :
338 339
  Reflexive R  Reflexive (envs_Forall2 R).
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Global Instance envs_Forall2_sym (R : relation PROP) :
341 342
  Symmetric R  Symmetric (envs_Forall2 R).
Proof. intros ??? [??]; by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
Global Instance envs_Forall2_trans (R : relation PROP) :
344 345
  Transitive R  Transitive (envs_Forall2 R).
Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
346
Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
347 348
  AntiSymm R R'  AntiSymm (envs_Forall2 R) (envs_Forall2 R').
Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
350 351 352
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
353
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
354
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
355 356
  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
  - apply pure_mono=> -[???]. constructor;
357 358 359
      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
  - by repeat f_equiv.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
360 361
Global Instance of_envs_proper :
  Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
362
Proof.
363 364
  intros Δ1 Δ2 HΔ; apply (anti_symm ()); apply of_envs_mono;
    eapply (envs_Forall2_impl ()); [| |symmetry|]; eauto using equiv_entails.
365
Qed.
366
Global Instance Envs_proper (R : relation PROP) :
367
  Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP).
368 369
Proof. by constructor. Qed.

370
Global Instance envs_entails_proper :
371
  Proper (envs_Forall2 () ==> () ==> iff) (@envs_entails PROP).
372
Proof. rewrite envs_entails_eq. solve_proper. Qed.
373
Global Instance envs_entails_flip_mono :
374
  Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
375
Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
376

Robbert Krebbers's avatar
Robbert Krebbers committed
377
(** * Adequacy *)
378
Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
379
Proof.
380 381
  rewrite envs_entails_eq /of_envs /= intuitionistically_True_emp
          left_id=><-.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384 385
Qed.

(** * Basic rules *)
386
Lemma tac_eval Δ Q Q' :
387 388 389
  ( (Q'':=Q'), Q''  Q)  (* We introduce [Q''] as a let binding so that
    tactics like `reflexivity` as called by [rewrite //] do not eagerly unify
    it with [Q]. See [test_iEval] in [tests/proofmode]. *)
390
  envs_entails Δ Q'  envs_entails Δ Q.
391
Proof. by intros <-. Qed.
392

393 394
Lemma tac_eval_in Δ Δ' i p P P' Q :
  envs_lookup i Δ = Some (p, P) 
395
  ( (P'':=P'), P  P') 
396 397 398
  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' 
  envs_entails Δ' Q  envs_entails Δ Q.
Proof.
399 400 401
  rewrite envs_entails_eq /=. intros ? HP ? <-.
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
402
Qed.
403

404 405 406 407 408 409 410
Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed.
Global Instance affine_env_snoc Γ i P :
  Affine P  AffineEnv Γ  AffineEnv (Esnoc Γ i P).
Proof. by constructor. Qed.

411
(* If the BI is affine, no need to walk on the whole environment. *)
412
Global Instance affine_env_bi `(BiAffine PROP) Γ : AffineEnv Γ | 0.
413 414
Proof. induction Γ; apply _. Qed.

415
Instance affine_env_spatial Δ :
416 417 418
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

419 420
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
421

Robbert Krebbers's avatar
Robbert Krebbers committed
422
Lemma tac_assumption Δ Δ' i p P Q :
423
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
424
  FromAssumption p P Q 
425 426
  (if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
427
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
428
Proof.
429
  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
  destruct (env_spatial_is_nil Δ') eqn:?.
431
  - by rewrite (env_spatial_is_nil_intuitionistically Δ') // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
432
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
434 435 436 437

Lemma tac_rename Δ Δ' i j p P Q :
  envs_lookup i Δ = Some (p,P) 
  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' 
438 439
  envs_entails Δ' Q 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
Proof.
441
  rewrite envs_entails_eq=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
442
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
444

Robbert Krebbers's avatar
Robbert Krebbers committed
445
Lemma tac_clear Δ Δ' i p P Q :
446
  envs_lookup_delete true i Δ = Some (p,P,Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
447
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
448
  envs_entails Δ' Q 
449
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
450
Proof.
451
  rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
452
  by destruct p; rewrite /= HQ sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
453
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
454 455

(** * False *)
456
Lemma tac_ex_falso Δ Q : envs_entails Δ False  envs_entails Δ Q.
457
Proof. by rewrite envs_entails_eq -(False_elim Q). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
458

Robbert Krebbers's avatar
Robbert Krebbers committed
459 460 461
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
462
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
Proof.
464
  rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
465
  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
466 467
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
468
(** * Pure *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
469 470
(* This relies on the invariant that [FromPure false] implies
   [FromPure true] *)
471 472 473 474
Lemma tac_pure_intro Δ Q φ af :
  env_spatial_is_nil Δ = af  FromPure af Q φ  φ  envs_entails Δ Q.
Proof.
  intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af.
475 476
  - rewrite env_spatial_is_nil_intuitionistically //= /bi_intuitionistically.
    f_equiv. by apply pure_intro.
477 478
  - by apply pure_intro.
Qed.
479

Robbert Krebbers's avatar
Robbert Krebbers committed
480
Lemma tac_pure Δ Δ' i p P φ Q :
481
  envs_lookup_delete true i Δ = Some (p, P, Δ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
482
  IntoPure P φ 
483
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
484
  (φ  envs_entails Δ' Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
Proof.
486
  rewrite envs_entails_eq=> ?? HPQ HQ.
487
  rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
488
  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
    by apply pure_elim_l.
490
  - destruct HPQ.
491
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
492
      by apply pure_elim_l.
493
    + rewrite (into_pure P) -(persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
494
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
495 496
Qed.

497
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝  Q)  (φ  envs_entails Δ Q).
498
Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
499

500
(** * Persistence *)
Robbert Krebbers's avatar
Robbert Krebbers committed
501
Lemma tac_persistent Δ Δ' i p P P' Q :
502
  envs_lookup i Δ = Some (p, P) 
503
  IntoPersistent p P P' 
504
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
505
  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' 
506
  envs_entails Δ' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
507
Proof.
508
  rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
509
  destruct p; simpl; rewrite /bi_intuitionistically.
510 511
  - by rewrite -(into_persistent _ P) /= wand_elim_r.
  - destruct HPQ.
512
    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
513
              (into_persistent _ P) wand_elim_r //.
514
    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
515
      by rewrite -{1}absorbingly_intuitionistically_into_persistently
516
        absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
517 518 519
Qed.

(** * Implication and wand *)
520 521
Lemma tac_impl_intro Δ Δ' i P P' Q R :
  FromImpl R P Q 
522
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
523
  envs_app false (Esnoc Enil i P') Δ = Some Δ' 
524
  FromAffinely P' P 
525
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
Proof.
527
  rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
528
  - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
529
    rewrite envs_app_singleton_sound //; simpl.
530
    rewrite -(from_affinely P') -affinely_and_lr.
531
    by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
532
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
533
    by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
534
Qed.
535 536
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
  FromImpl R P Q 
537
  IntoPersistent false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
538
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
539
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
Proof.
541
  rewrite /FromImpl envs_entails_eq => <- ?? <-.
542
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
543
  rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
544
  by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
545
Qed.
546 547
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q  envs_entails Δ Q  envs_entails Δ R.
548 549 550
Proof.
  rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
551

552 553
Lemma tac_wand_intro Δ Δ' i P Q R :
  FromWand R P Q 
554
  envs_app false (Esnoc Enil i P) Δ = Some Δ' 
555
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
556
Proof.
557
  rewrite /FromWand envs_entails_eq => <- ? HQ.
558
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Qed.
560 561
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q R :
  FromWand R P Q 
562
  IntoPersistent false P P' 
563
  TCOr (Affine P) (Absorbing Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
564
  envs_app true (Esnoc Enil i P') Δ = Some Δ' 
565
  envs_entails Δ' Q  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
566
Proof.
567
  rewrite /FromWand envs_entails_eq => <- ? HPQ ? HQ.
568
  rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
569
  - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
570
            (into_persistent _ P) wand_elim_r //.
571
  - rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
572
    by rewrite -{1}absorbingly_intuitionistically_into_persistently
573
      absorbingly_sep_l wand_elim_r HQ.
574
Qed.
575 576
Lemma tac_wand_intro_pure Δ P φ Q R :
  FromWand R P Q 
577
  IntoPure P φ 
578
  TCOr (Affine P) (Absorbing Q) 
579
  (φ  envs_entails Δ Q)  envs_entails Δ R.
580
Proof.
581
  rewrite /FromWand envs_entails_eq. intros <- ? HPQ HQ. apply wand_intro_l. destruct HPQ.
582
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
583
    by apply pure_elim_l.
584
  - rewrite (into_pure P) -(persistent_absorbingly_affinely  _ %I) absorbingly_sep_lr.
585
    rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
586
Qed.
587 588
Lemma tac_wand_intro_drop Δ P Q R :
  FromWand R P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
589
  TCOr (Affine P) (Absorbing Q) 
590
  envs_entails Δ Q 
591
  envs_entails Δ R.
592
Proof.
593
  rewrite envs_entails_eq /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
594 595 596 597 598
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 :
599 600
  envs_lookup_delete false i Δ = Some (p, P1, Δ') 
  envs_lookup j Δ' = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
601
  IntoWand q p R P1 P2 
Robbert Krebbers's avatar
Robbert Krebbers committed
602 603 604 605 606
  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 Δ'' 
607
  envs_entails Δ'' Q  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
608
Proof.
609 610 611
  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hj ? Hj' <-.
  rewrite (envs_lookup_sound' _ false) //; simpl. destruct p; simpl.
  - move: Hj; rewrite envs_delete_persistent=> Hj.
612
    rewrite envs_simple_replace_singleton_sound //; simpl.
613 614 615
    rewrite -intuitionistically_if_idemp -intuitionistically_idemp into_wand /=.
    rewrite assoc (intuitionistically_intuitionistically_if q).
    by rewrite intuitionistically_if_sep_2 wand_elim_r wand_elim_r.
616
  - move: Hj Hj'; rewrite envs_delete_spatial=> Hj Hj'.
617 618
    rewrite envs_lookup_sound // (envs_replace_singleton_sound' _ Δ'') //; simpl.
    by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
619 620
Qed.

621
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
622
  envs_lookup_delete true j Δ = Some (q, R, Δ') 
623
  IntoWand q false R P1 P2  AddModal P1' P1 Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
624
  (''(Δ1,Δ2)  envs_split (if neg is true then Right else Left) js Δ';
625
    Δ2'  envs_app false (Esnoc Enil j P2) Δ2;
Robbert Krebbers's avatar
Robbert Krebbers committed
626
    Some (Δ1,Δ2')) = Some (Δ1,Δ2')  (* does not preserve position of [j] *)