coq_tactics.v 46 KB
Newer Older
1
From iris.bi Require Export bi telescopes.
2
From iris.proofmode Require Export base environments classes modality_instances.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.prelude Require Import options.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Import bi.
5
Import env_notations.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
8
Local Open Scope lazy_bool_scope.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
16
(** * Starting and stopping the proof mode *)
17
Lemma tac_start P : envs_entails (Envs Enil Enil 1) P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Proof.
19
  rewrite envs_entails_unseal !of_envs_eq /=.
20
  rewrite intuitionistically_True_emp left_id=><-.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  apply and_intro=> //. apply pure_intro; repeat constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
26
27
28
Lemma tac_stop Δ P :
  (match env_intuitionistic Δ, env_spatial Δ with
   | Enil, Γs => env_to_prop Γs
   | Γp, Enil =>  env_to_prop_and Γp
   | Γp, Γs =>  env_to_prop_and Γp  env_to_prop Γs
29
   end  P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
  envs_entails Δ P.
Proof.
32
  rewrite envs_entails_unseal !of_envs_eq. intros <-.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
  rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
  destruct (env_intuitionistic Δ), (env_spatial Δ);
    by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
38
(** * Basic rules *)
39
Lemma tac_eval Δ Q Q' :
40
41
42
  ( (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]. *)
43
  envs_entails Δ Q'  envs_entails Δ Q.
44
Proof. by intros <-. Qed.
45

46
Lemma tac_eval_in Δ i p P P' Q :
47
  envs_lookup i Δ = Some (p, P) 
48
  ( (P'':=P'), P  P') 
49
50
51
52
53
  match envs_simple_replace i p (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
54
Proof.
55
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
56
  rewrite envs_entails_unseal /=. intros ? HP ?.
57
58
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
59
Qed.
60

61
62
63
64
65
66
67
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.

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

72
Local Instance affine_env_spatial Δ :
73
74
75
  AffineEnv (env_spatial Δ)  Affine ([] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.

76
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ)  envs_entails Δ emp.
77
Proof. intros. by rewrite envs_entails_unseal (affine (of_envs Δ)). Qed.
78

Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
81
  FromAssumption p P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
  (let Δ' := envs_delete true i p Δ in
   if env_spatial_is_nil Δ' then TCTrue
84
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) 
85
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof.
87
  intros ?? H. rewrite envs_entails_unseal envs_lookup_sound //.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
  simpl in *. destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92

93
94
95
96
97
98
99
100
Lemma tac_assumption_coq Δ P Q :
  ( P) 
  FromAssumption true P Q 
  (if env_spatial_is_nil Δ then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ))) 
  envs_entails Δ Q.
Proof.
  rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
101
  rewrite envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
102
103
104
105
106
107
  rewrite -bi.intuitionistically_emp HP HPQ.
  destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
  - destruct H; by rewrite sep_elim_l.
Qed.

108
Lemma tac_rename Δ i j p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  envs_lookup i Δ = Some (p,P) 
110
111
112
113
  match envs_simple_replace i p (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
114
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
Proof.
116
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
117
  rewrite envs_entails_unseal=> ??. rewrite envs_simple_replace_singleton_sound //.
118
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
120

121
122
Lemma tac_clear Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
124
  envs_entails (envs_delete true i p Δ) Q 
125
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Proof.
127
  rewrite envs_entails_unseal=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
128
  by destruct p; rewrite /= sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131

(** * False *)
132
Lemma tac_ex_falso Δ Q : envs_entails Δ False  envs_entails Δ Q.
133
Proof. by rewrite envs_entails_unseal -(False_elim Q). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134

Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) 
  P = False%I 
138
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof.
140
  rewrite envs_entails_unseal => ??. subst. rewrite envs_lookup_sound //; simpl.
141
  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
144
(** * Pure *)
145
146
147
148
149
Lemma tac_pure_intro Δ Q φ a :
  FromPure a Q φ 
  (if a then AffineEnv (env_spatial Δ) else TCTrue) 
  φ 
  envs_entails Δ Q.
150
Proof.
151
  intros ???. rewrite envs_entails_unseal -(from_pure a Q). destruct a; simpl.
152
  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp.
153
154
  - by apply pure_intro.
Qed.
155

156
157
Lemma tac_pure Δ i p P φ Q :
  envs_lookup i Δ = Some (p, P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  IntoPure P φ 
159
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
160
  (φ  envs_entails (envs_delete true i p Δ) Q)  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
Proof.
162
  rewrite envs_entails_unseal=> ?? HPQ HQ.
163
  rewrite envs_lookup_sound //; simpl. destruct p; simpl.
164
  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
    by apply pure_elim_l.
166
  - destruct HPQ.
167
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
168
      by apply pure_elim_l.
169
    + rewrite (into_pure P) -(persistent_absorbingly_affinely  _ ) absorbingly_sep_lr.
170
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
172
Qed.

173
174
175
176
177
Lemma tac_pure_revert Δ φ P Q :
  FromAffinely P  φ  
  envs_entails Δ (P - Q) 
  (φ  envs_entails Δ Q).
Proof.
178
  rewrite /FromAffinely envs_entails_unseal. intros <- -> ?.
179
  by rewrite pure_True // affinely_True_emp left_id.
180
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
181

182
(** * Intuitionistic *)
183
Lemma tac_intuitionistic Δ i j p P P' Q :
184
  envs_lookup i Δ = Some (p, P) 
185
  IntoPersistent p P P' 
186
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) 
187
  match envs_replace i p true (Esnoc Enil j P') Δ with
188
189
190
191
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
Proof.
193
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
194
  rewrite envs_entails_unseal=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
195
  destruct p; simpl; rewrite /bi_intuitionistically.
196
  - by rewrite -(into_persistent true P) /= wand_elim_r.
197
  - destruct HPQ.
198
    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
199
              (into_persistent _ P) wand_elim_r //.
200
    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
201
      by rewrite -{1}absorbingly_intuitionistically_into_persistently
202
        absorbingly_sep_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
Qed.

205
Lemma tac_spatial Δ i j p P P' Q :
206
207
  envs_lookup i Δ = Some (p, P) 
  (if p then FromAffinely P' P else TCEq P' P) 
208
  match envs_replace i p false (Esnoc Enil j P') Δ with
209
210
211
212
213
214
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Proof.
  intros ? HP. destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
215
  rewrite envs_entails_unseal=> <-. rewrite envs_replace_singleton_sound //; simpl.
216
217
218
219
220
  destruct p; simpl; last destruct HP.
  - by rewrite intuitionistically_affinely (from_affinely P' P) wand_elim_r.
  - by rewrite wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
221
(** * Implication and wand *)
222
Lemma tac_impl_intro Δ i P P' Q R :
223
  FromImpl R P Q 
224
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) 
225
  FromAffinely P' P 
226
227
228
229
230
  match envs_app false (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
Proof.
232
  destruct (envs_app _ _ _) eqn:?; last done.
233
  rewrite /FromImpl envs_entails_unseal => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
234
  - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
235
    rewrite envs_app_singleton_sound //; simpl.
236
    rewrite -(from_affinely P' P) -affinely_and_lr.
237
    by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
238
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
239
    by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
Qed.
241
Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
242
  FromImpl R P Q 
243
  IntoPersistent false P P' 
244
245
246
247
248
  match envs_app true (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
Proof.
250
  destruct (envs_app _ _ _) eqn:?; last done.
251
  rewrite /FromImpl envs_entails_unseal => <- ??.
252
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
253
  rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
254
  by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
255
Qed.
256
257
Lemma tac_impl_intro_drop Δ P Q R :
  FromImpl R P Q  envs_entails Δ Q  envs_entails Δ R.
258
Proof.
259
  rewrite /FromImpl envs_entails_unseal => <- ?. apply impl_intro_l. by rewrite and_elim_r.
260
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
261

262
Lemma tac_wand_intro Δ i P Q R :
263
  FromWand R P Q 
264
265
266
267
268
  match envs_app false (Esnoc Enil i P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
Proof.
270
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
271
  rewrite /FromWand envs_entails_unseal => <- HQ.
272
  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
Qed.
274
275

Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
276
  FromWand R P Q 
277
  IntoPersistent false P P' 
278
  TCOr (Affine P) (Absorbing Q) 
279
280
281
282
283
  match envs_app true (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ R.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Proof.
285
  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
286
  rewrite /FromWand envs_entails_unseal => <- ? HPQ HQ.
287
  rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
288
  - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
289
            (into_persistent _ P) wand_elim_r //.
290
  - rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
Ralf Jung's avatar
Ralf Jung committed
291
    by rewrite -{1}absorbingly_intuitionistically_into_persistently
292
      absorbingly_sep_l wand_elim_r HQ.
293
Qed.
294
295
Lemma tac_wand_intro_drop Δ P Q R :
  FromWand R P Q 
Robbert Krebbers's avatar
Robbert Krebbers committed
296
  TCOr (Affine P) (Absorbing Q) 
297
  envs_entails Δ Q 
298
  envs_entails Δ R.
299
Proof.
300
  rewrite envs_entails_unseal /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
303
304
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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
305
306
307
Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
  envs_lookup i Δ = Some (p, P1) 
  let Δ' := envs_delete remove_intuitionistic i p Δ in
308
  envs_lookup j Δ' = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
309
  IntoWand q p R P1 P2 
310
  match envs_replace j q (p &&& q) (Esnoc Enil j P2) Δ' with
311
312
313
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Proof.
315
  rewrite envs_entails_unseal /IntoWand. intros ?? HR ?.
316
  destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
317
318
319
320
321
322
  rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
  rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
  - rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp.
    rewrite {1}(intuitionistically_intuitionistically_if q).
    by rewrite HR assoc intuitionistically_if_sep_2 !wand_elim_r.
  - by rewrite HR assoc !wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
324
Qed.

325
Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
326
  envs_lookup j Δ = Some (q, R) 
327
328
  IntoWand q false R P1 P2 
  (if am then AddModal P1' P1 Q else TCEq P1' P1) 
329
  match
330
331
    '(Δ1,Δ2)  envs_split (if neg is true then Right else Left)
                          js (envs_delete true j q Δ);
332
    Δ2'  envs_app (negb am &&& q &&& env_spatial_is_nil Δ1) (Esnoc Enil j P2) Δ2;
333
334
335
336
337
338
339
    Some (Δ1,Δ2') (* does not preserve position of [j] *)
  with
  | Some (Δ1,Δ2') =>
     (* The constructor [conj] of [∧] still stores the contexts [Δ1] and [Δ2'] *)
     envs_entails Δ1 P1'  envs_entails Δ2' Q
  | None => False
  end  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Proof.
341
  rewrite envs_entails_unseal. intros ?? Hmod HQ.
342
343
  destruct (_ = _) as [[Δ1 Δ2']|] eqn:?; last done.
  destruct HQ as [HP1 HQ].
Robbert Krebbers's avatar
Robbert Krebbers committed
344
345
346
  destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
    destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
  rewrite envs_lookup_sound // envs_split_sound //.
347
  rewrite (envs_app_singleton_sound Δ2) //; simpl.
348
349
350
351
352
353
354
355
  rewrite -intuitionistically_if_idemp (into_wand q false) /=.
  destruct (negb am &&& q &&& env_spatial_is_nil Δ1) eqn:Hp; simpl.
  - move: Hp. rewrite !lazy_andb_true negb_true. intros [[-> ->] ?]; simpl.
    destruct Hmod. rewrite env_spatial_is_nil_intuitionistically // HP1.
    by rewrite assoc intuitionistically_sep_2 wand_elim_l wand_elim_r HQ.
  - rewrite intuitionistically_if_elim HP1. destruct am; last destruct Hmod.
    + by rewrite assoc -(comm _ P1') -assoc wand_trans HQ.
    + by rewrite assoc wand_elim_l wand_elim_r HQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
357
Qed.

358
Lemma tac_unlock_emp Δ Q : envs_entails Δ Q  envs_entails Δ (emp  locked Q).
359
Proof. rewrite envs_entails_unseal=> ->. by rewrite -lock left_id. Qed.
360
Lemma tac_unlock_True Δ Q : envs_entails Δ Q  envs_entails Δ (True  locked Q).
361
Proof. rewrite envs_entails_unseal=> ->. by rewrite -lock -True_sep_2. Qed.
362
Lemma tac_unlock Δ Q : envs_entails Δ Q  envs_entails Δ (locked Q).
363
364
Proof. by unlock. Qed.

365
Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
366
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
367
  IntoWand q false R P1 P2 
368
  (if am then AddModal P1' P1 Q else TCEq P1' P1) 
369
  envs_entails (envs_delete true j q Δ) (P1'  locked Q') 
370
  Q' = (P2 - Q)%I 
371
  envs_entails Δ Q.
372
Proof.
373
  rewrite envs_entails_unseal. intros ?? Hmod HPQ ->.
374
  rewrite envs_lookup_sound //. rewrite HPQ -lock.
375
376
  rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
  destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
377
378
Qed.

379
Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
380
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
381
  IntoWand q true R P1 P2 
382
  FromPure a P1 φ 
383
384
385
386
387
388
  φ 
  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
389
Proof.
390
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
391
  rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
392
  rewrite -intuitionistically_if_idemp (into_wand q true) /=.
393
  rewrite -(from_pure a P1) pure_True //.
394
  rewrite -affinely_affinely_if affinely_True_emp.
395
  by rewrite intuitionistically_emp left_id wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
396
397
Qed.

398
399
Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
  envs_lookup j Δ = Some (q, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
400
401
  IntoWand q true R P1 P2 
  Persistent P1 
402
  IntoAbsorbingly P1' P1 
403
  envs_entails (envs_delete true j q Δ) P1' 
404
405
406
407
  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
408
Proof.
409
  rewrite envs_entails_unseal => ???? HP1 HQ.
410
411
  destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
  rewrite -HQ envs_lookup_sound //.
412
  rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
413
  rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
414
  rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
Ralf Jung's avatar
Ralf Jung committed
415
  rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
416
417
  rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
  rewrite (intuitionistically_intuitionistically_if q).
418
  by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
419
420
Qed.

421
Lemma tac_specialize_intuitionistic_helper Δ j q P R R' Q :
422
  envs_lookup j Δ = Some (q,P) 
Robbert Krebbers's avatar
Robbert Krebbers committed
423
  (if q then TCTrue else BiAffine PROP) 
424
  envs_entails Δ (<absorb> R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
425
  IntoPersistent false R R' 
426
427
428
429
  match envs_replace j q true (Esnoc Enil j R') Δ with
  | Some Δ'' => envs_entails Δ'' Q
  | None => False
  end  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
Proof.
431
  rewrite envs_entails_unseal => ?? HR ??.
432
433
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
  rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
434
  rewrite envs_replace_singleton_sound //; destruct q; simpl.
435
  - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
Robbert Krebbers's avatar
Robbert Krebbers committed
436
437
      absorbingly_elim_persistently sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
438
  - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
Robbert Krebbers's avatar
Robbert Krebbers committed
439
440
      (into_persistent _ R) sep_elim_r
      persistently_and_intuitionistically_sep_l wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
442
Qed.

443
444
(* A special version of [tac_assumption] that does not do any of the
[FromAssumption] magic. *)
445
Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
446
  envs_lookup i Δ = Some (q,P) 
447
  envs_entails Δ (<absorb> P).
448
Proof.
449
  rewrite envs_entails_unseal /bi_absorbingly=> /envs_lookup_sound=> ->.
Ralf Jung's avatar
Ralf Jung committed
450
  rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
451
452
Qed.

453
454
455
456
457
Lemma tac_revert Δ i Q :
  match envs_lookup_delete true i Δ with
  | Some (p,P,Δ') => envs_entails Δ' ((if p then  P else P)%I - Q)
  | None => False
  end 
458
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
459
Proof.
460
  rewrite envs_entails_unseal => HQ.
461
462
  destruct (envs_lookup_delete _ _ _) as [[[p P] Δ']|] eqn:?; last done.
  rewrite envs_lookup_delete_sound //=.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
  rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
464
465
Qed.

466
Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
467
  into_ih : φ   of_envs Δ  Q.
468
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
469
Proof. by rewrite envs_entails_unseal /IntoIH bi.intuitionistically_elim. Qed.
470
Global Instance into_ih_forall {A} (φ : A  Prop) Δ Φ :
471
  ( x, IntoIH (φ x) Δ (Φ x))  IntoIH ( x, φ x) Δ ( x, Φ x) | 2.
472
473
Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
474
  IntoIH φ Δ Q  IntoIH (ψ  φ) Δ (⌜ψ⌝  Q) | 1.
475
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
476
477
478
479
480
481
482
483
484
485
486
487
488
(** The instances [into_ih_Forall] and [into_ih_Forall2] are used to support
induction principles for mutual inductive types such as finitely branching trees:

  Inductive ntree := Tree : list ntree → ntree.

  Lemma ntree_ind (P : ntree → Prop) :
    (∀ l, Forall P l → P (Tree l)) → ∀ t, P t.

Note 1: We need an [IntoIH] instance for any predicate transformer (like
[Forall]) that is used in induction principles. However, since nested induction
with lists is most common, we currently only support [Forall] and [Forall2].

Note 2: We could also write the instance [into_ih_Forall] using the big operator
Robbert Krebbers's avatar
Tweaks.    
Robbert Krebbers committed
489
for conjunction, or using the forall quantifier. We use the big operator
490
491
because that corresponds most closely to [Forall], and we use the version with
separating conjunction because we do not have a binary version of the big
Robbert Krebbers's avatar
Tweaks.    
Robbert Krebbers committed
492
493
operator for conjunctions, and want to treat [Forall] and [Forall2]
consistently. *)
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
Global Instance into_ih_Forall {A} (φ : A  Prop) l Δ Φ :
  ( x, IntoIH (φ x) Δ (Φ x)) 
  IntoIH (Forall φ l) Δ ([ list] x  l,  Φ x) | 2.
Proof.
  rewrite /IntoIH=> HΔ. induction 1 as [|x l ? IH]; simpl.
  { apply (affine _). }
  rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
  apply intuitionistically_intro', HΔ; auto.
Qed.
Global Instance into_ih_Forall2 {A B} (φ : A  B  Prop) l1 l2 Δ Φ :
  ( x1 x2, IntoIH (φ x1 x2) Δ (Φ x1 x2)) 
  IntoIH (Forall2 φ l1 l2) Δ ([ list] x1;x2  l1;l2,  Φ x1 x2) | 2.
Proof.
  rewrite /IntoIH=> HΔ. induction 1 as [|x1 x2 l1 l2 ? IH]; simpl.
  { apply (affine _). }
  rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
  apply intuitionistically_intro', HΔ; auto.
Qed.
512
513
514

Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
  IntoIH φ Δ P 
515
  env_spatial_is_nil Δ = true 
516
  envs_entails Δ (<pers> P  Q) 
517
  envs_entails Δ Q.
518
Proof.
519
  rewrite /IntoIH envs_entails_unseal. intros HP ? HPQ.
520
  rewrite (env_spatial_is_nil_intuitionistically Δ) //.
521
522
523
  rewrite -(idemp bi_and ( (of_envs Δ))%I).
  rewrite -{1}intuitionistically_idemp {1}intuitionistically_into_persistently_1.
  by rewrite {1}HP // intuitionistically_elim HPQ impl_elim_r.
524
525
Qed.

526
527
528
529
530
Lemma tac_assert Δ j P Q :
  match envs_app true (Esnoc Enil j (P - P)%I) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end  envs_entails Δ Q.
531
Proof.
532
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
533
  rewrite envs_entails_unseal=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
534
  by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
535
536
Qed.

537
Definition IntoEmpValid (φ : Type) (P : PROP) := φ   P.
538
539
540
(** These lemmas are [Defined] because the guardedness checker must see
through them. See https://gitlab.mpi-sws.org/iris/iris/issues/274. For the
same reason, their bodies use as little automation as possible. *)
541
Lemma into_emp_valid_here φ P : AsEmpValid φ P  IntoEmpValid φ P.
542
Proof. by intros [??]. Defined.
543
544
Lemma into_emp_valid_impl (φ ψ : Type) P :
  φ  IntoEmpValid ψ P  IntoEmpValid (φ  ψ) P.
545
Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
546
547
Lemma into_emp_valid_forall {A} (φ : A  Type) P x :
  IntoEmpValid (φ x) P  IntoEmpValid ( x : A, φ x) P.
548
Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
549
550
551
Lemma into_emp_valid_tforall {TT : tele} (φ : TT  Prop) P x :
  IntoEmpValid (φ x) P  IntoEmpValid (.. x : TT, φ x) P.
Proof. rewrite /IntoEmpValid tforall_forall=> Hi1 Hi2. apply Hi1, Hi2. Defined.
552
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P  φ   P.
553
554
555
556
557
558
559
Proof. intros HP. apply HP. Defined.

(** When called by the proof mode, the proof of [P] is produced by calling
[into_emp_valid_proj]. That call must be transparent to the guardedness
checker, per https://gitlab.mpi-sws.org/iris/iris/issues/274; hence, it must
be done _outside_ [tac_pose_proof], so the latter can remain opaque. *)
Lemma tac_pose_proof Δ j P Q :
Gregory Malecha's avatar
Gregory Malecha committed
560
  ( P) 
561
562
563
564
565
  match envs_app true (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
566
Proof.
567
  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
568
  rewrite envs_entails_unseal => HP <-. rewrite envs_app_singleton_sound //=.
569
  by rewrite -HP /= intuitionistically_emp emp_wand.
Robbert Krebbers's avatar
Robbert Krebbers committed
570
571
Qed.

572
573
574
575
576
577
578
579
580
581
Lemma tac_pose_proof_hyp Δ i j Q :
  match envs_lookup_delete false i Δ with
  | None => False
  | Some (p, P, Δ') =>
    match envs_app p (Esnoc Enil j P) Δ' with
    | None => False
    | Some Δ'' => envs_entails Δ'' Q
    end
  end 
  envs_entails Δ Q.
582
Proof.
583
584
  destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
  destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
585
  rewrite envs_entails_unseal. move: Hlookup. rewrite envs_lookup_delete_Some.
586
  intros [? ->] <-.
587
588
  rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
  by rewrite wand_elim_r.
589
590
Qed.

591
592
Lemma tac_apply Δ i p R P1 P2 :
  envs_lookup i Δ = Some (p, R) 
Robbert Krebbers's avatar
Robbert Krebbers committed
593
  IntoWand p false R P1 P2 
594
  envs_entails (envs_delete true i p Δ) P1  envs_entails Δ P2.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
Proof.
596
  rewrite envs_entails_unseal => ?? HP1. rewrite envs_lookup_sound //.
597
  by rewrite (into_wand p false) /= HP1 wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
598
599
600
Qed.

(** * Conjunction splitting *)
601
Lemma tac_and_split Δ P Q1 Q2 :
602
  FromAnd P Q1 Q2  envs_entails Δ Q1  envs_entails Δ Q2  envs_entails Δ P.
603
Proof. rewrite envs_entails_unseal. intros. rewrite -(from_and P). by apply and_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
605

(** * Separating conjunction splitting *)
606
Lemma tac_sep_split Δ d js P Q1 Q2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
607
  FromSep P Q1 Q2 
608
609
610
611
  match envs_split d js Δ with
  | None => False
  | Some (Δ1,Δ2) => envs_entails Δ1 Q1  envs_entails Δ2 Q2
  end  envs_entails Δ P.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
Proof.
613
  destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
614
  rewrite envs_entails_unseal=>? [HQ1 HQ2].
615
  rewrite envs_split_sound //. by rewrite HQ1 HQ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
617
618
Qed.

(** * Combining *)
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Class FromSeps {PROP : bi} (P : PROP) (Qs : list PROP) :=
620
  from_seps : [] Qs  P.
Ralf Jung's avatar
Ralf Jung committed
621
622
Local Arguments FromSeps {_} _%I _%I.
Local Arguments from_seps {_} _%I _%I {_}.
623

Robbert Krebbers's avatar
Robbert Krebbers committed
624
625
Global Instance from_seps_nil : @FromSeps PROP emp [].
Proof. by rewrite /FromSeps. Qed.
626
627
628
Global Instance from_seps_singleton P : FromSeps P [P] | 1.
Proof. by rewrite /FromSeps /= right_id. Qed.
Global Instance from_seps_cons P P' Q Qs :
Robbert Krebbers's avatar
Robbert Krebbers committed
629
630
  FromSeps P' Qs  FromSep P Q P'  FromSeps P (Q :: Qs) | 2.
Proof. by rewrite /FromSeps /FromSep /= => ->. Qed.
631
632

Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
633
  envs_lookup_delete_list false js Δ1 = Some (p, Ps, Δ2) 
634
635
  FromSeps P Ps 
  envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 
636
  envs_entails Δ3 Q  envs_entails Δ1 Q.
637
Proof.
638
  rewrite envs_entails_unseal => ??? <-. rewrite envs_lookup_delete_list_sound //.
639
  rewrite from_seps. rewrite envs_app_singleton_sound //=.
640
  by rewrite wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
641
642
643
Qed.

(** * Conjunction/separating conjunction elimination *)
644
Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
645
646
  envs_lookup i Δ = Some (p, P) 
  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) 
647
648
649
650
651
  match envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end 
  envs_entails Δ Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
652
Proof.
653
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
654
  rewrite envs_entails_unseal. intros. rewrite envs_simple_replace_sound //=. destruct p.
655
  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
656
  - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
657
658
Qed.

659
660
661
(* Using this tactic, one can destruct a (non-separating) conjunction in the
spatial context as long as one of the conjuncts is thrown away. It corresponds
to the principle of "external choice" in linear logic. *)
662
Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
663
  envs_lookup i Δ = Some (p, P) 
664
665
  (if p then IntoAnd p P P1 P2 : Type else
    TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
666
      (if d is Left then TCOr (Affine P2) (Absorbing Q)
667
       else TCOr (Affine P1) (Absorbing Q)))) 
668
669
670
671
  match envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end  envs_entails Δ Q.
672
Proof.