ltac_tactics.v 157 KB
Newer Older
1
From stdpp Require Import namespaces hlist pretty.
2
From iris.bi Require Export bi telescopes.
3
4
From iris.proofmode Require Import base intro_patterns spec_patterns
                                   sel_patterns coq_tactics reduction.
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
From iris.proofmode Require Export classes notation.
Set Default Proof Using "Type".
Export ident.

(** For most of the tactics, we want to have tight control over the order and
way in which type class inference is performed. To that end, many tactics make
use of [notypeclasses refine] and the [iSolveTC] tactic to manually invoke type
class inference.

The tactic [iSolveTC] does not use [apply _], as that often leads to issues
because it will try to solve all evars whose type is a typeclass, in
dependency order (according to Matthieu). If one fails, it aborts. However, we
generally rely on progress on the main goal to be solved to make progress
elsewhere. With [typeclasses eauto], that seems to work better.

A drawback of [typeclasses eauto] is that it is multi-success, i.e. whenever
subsequent tactics fail, it will backtrack to [typeclasses eauto] to try the
next type class instance. This is almost always undesired and leads to poor
performance and horrible error messages, so we wrap it in a [once]. *)
Ltac iSolveTC :=
  solve [once (typeclasses eauto)].

27
28
29
(** Tactic used for solving side-conditions arising from TC resolution in iMod
and iInv. *)
Ltac iSolveSideCondition :=
30
  split_and?; try solve [ fast_done | solve_ndisj ].
31

32
33
34
35
36
37
38
(** Used for printing [string]s and [ident]s. *)
Ltac pretty_ident H :=
  lazymatch H with
  | INamed ?H => H
  | ?H => H
  end.

39
40
(** * Misc *)

41
42
43
44
45
46
47
Ltac iGetCtx :=
  lazymatch goal with
  | |- envs_entails ?Δ _ => Δ
  | |- context[ envs_split _ _ ?Δ ] => Δ
  end.

Ltac iMissingHypsCore Δ Hs :=
48
  let Hhyps := pm_eval (envs_dom Δ) in
49
50
  eval vm_compute in (list_difference Hs Hhyps).

51
52
53
54
Ltac iMissingHyps Hs :=
  let Δ := iGetCtx in
  iMissingHypsCore Δ Hs.

55
56
Ltac iTypeOf H :=
  let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
57
  pm_eval (envs_lookup H Δ).
58

59
60
61
Ltac iBiOfGoal :=
  match goal with |- @envs_entails ?PROP _ _ => PROP end.

62
63
64
65
66
67
68
69
70
71
Tactic Notation "iMatchHyp" tactic1(tac) :=
  match goal with
  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
  end.

(** * Start a proof *)
Tactic Notation "iStartProof" :=
  lazymatch goal with
  | |- envs_entails _ _ => idtac
  | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
72
               [iSolveTC || fail "iStartProof: not a BI assertion"
73
               |notypeclasses refine (tac_start _ _)]
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
  end.

(* Same as above, with 2 differences :
   - We can specify a BI in which we want the proof to be done
   - If the goal starts with a let or a ∀, they are automatically
     introduced. *)
Tactic Notation "iStartProof" uconstr(PROP) :=
  lazymatch goal with
  | |- @envs_entails ?PROP' _ _ =>
    (* This cannot be shared with the other [iStartProof], because
    type_term has a non-negligeable performance impact. *)
    let x := type_term (eq_refl : @eq Type PROP PROP') in idtac

  (* We eta-expand [as_emp_valid_2], in order to make sure that
     [iStartProof PROP] works even if [PROP] is the carrier type. In
     this case, typing this expression will end up unifying PROP with
     [bi_car _], and hence trigger the canonical structures mechanism
     to find the corresponding bi. *)
  | |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
93
               [iSolveTC || fail "iStartProof: not a BI assertion"
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
97
98
99
100
               |apply tac_start]
  end.

Tactic Notation "iStopProof" :=
  lazymatch goal with
  | |- envs_entails _ _ => apply tac_stop; pm_reduce
  | |- _ => fail "iStopProof: proofmode not started"
101
102
103
  end.

(** * Generate a fresh identifier *)
104
105
106
107
108
(** The tactic [iFresh] bumps the fresh name counter in the proof mode
environment and returns the old value.

Note that we use [Ltac] instead of [Tactic Notation] since [Tactic Notation]
tactics can only have side-effects, but cannot return terms. *)
109
Ltac iFresh :=
110
111
112
113
  (* We make use of an Ltac hack to allow the [iFresh] tactic to both have a
  side-effect (i.e. to bump the counter) and to return a value (the fresh name).
  We do this by wrapped the side-effect under a [match] in a let-binding. See
  https://stackoverflow.com/a/46178884 *)
114
  let start :=
115
    lazymatch goal with
116
    | _ => iStartProof
117
    end in
118
119
120
121
  let c :=
    lazymatch goal with
    | |- envs_entails (Envs _ _ ?c) _ => c
    end in
122
  let inc :=
123
124
125
    lazymatch goal with
    | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
      let c' := eval vm_compute in (Pos.succ c) in
Ralf Jung's avatar
Ralf Jung committed
126
      change_no_check (envs_entails (Envs Δp Δs c') Q)
127
128
    end in
  constr:(IAnon c).
129
130
131

(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
132
  eapply tac_rename with H1 H2 _ _; (* (i:=H1) (j:=H2) *)
133
134
135
    [pm_reflexivity ||
     let H1 := pretty_ident H1 in
     fail "iRename:" H1 "not found"
136
137
138
139
140
141
142
    |pm_reduce;
     lazymatch goal with
       | |- False =>
         let H2 := pretty_ident H2 in
         fail "iRename:" H2 "not fresh"
       | _ => idtac (* subgoal *)
     end].
143

144
145
146
(** Elaborated selection patterns, unlike the type [sel_pat], contains
only specific identifiers, and no wildcards like `#` (with the
exception of the pure selection pattern `%`) *)
147
Inductive esel_pat :=
148
  | ESelPure
149
  | ESelIdent : (* whether the ident is intuitionistic *) bool  ident  esel_pat.
150

Ralf Jung's avatar
Ralf Jung committed
151
Local Ltac iElaborateSelPat_go pat Δ Hs :=
152
153
154
  lazymatch pat with
  | [] => eval cbv in Hs
  | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)
155
  | SelIntuitionistic :: ?pat =>
156
    let Hs' := pm_eval (env_dom (env_intuitionistic Δ)) in
157
    let Δ' := pm_eval (envs_clear_intuitionistic Δ) in
158
159
    iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
  | SelSpatial :: ?pat =>
160
161
    let Hs' := pm_eval (env_dom (env_spatial Δ)) in
    let Δ' := pm_eval (envs_clear_spatial Δ) in
162
163
    iElaborateSelPat_go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
  | SelIdent ?H :: ?pat =>
164
    lazymatch pm_eval (envs_lookup_delete false H Δ) with
165
    | Some (?p,_,?Δ') =>  iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs)
166
167
168
    | None =>
      let H := pretty_ident H in
      fail "iElaborateSelPat:" H "not found"
169
170
    end
  end.
171
172
(** Converts a selection pattern (given as a string) to a list of
elaborated selection patterns. *)
173
174
175
Ltac iElaborateSelPat pat :=
  lazymatch goal with
  | |- envs_entails ?Δ _ =>
176
    let pat := sel_pat.parse pat in iElaborateSelPat_go pat Δ (@nil esel_pat)
177
178
179
  end.

Local Ltac iClearHyp H :=
180
  eapply tac_clear with H _ _; (* (i:=H) *)
181
182
183
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iClear:" H "not found"
184
    |pm_reduce; iSolveTC ||
185
     let H := pretty_ident H in
186
187
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iClear:" H ":" P "not affine and the goal not absorbing"
188
    |pm_reduce].
189

190
191
192
193
194
195
Local Ltac iClear_go Hs :=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs => clear; iClear_go Hs
  | ESelIdent _ ?H :: ?Hs => iClearHyp H; iClear_go Hs
  end.
196
Tactic Notation "iClear" constr(Hs) :=
197
  iStartProof; let Hs := iElaborateSelPat Hs in iClear_go Hs.
198
199
200
201

Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
  iClear Hs; clear xs.

202
(** ** Simplification *)
203
Tactic Notation "iEval" tactic3(t) :=
204
205
206
207
208
209
210
211
212
213
  iStartProof;
  eapply tac_eval;
    [let x := fresh in intros x; t; unfold x; reflexivity
    |].

Local Ltac iEval_go t Hs :=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
  | ESelIdent _ ?H :: ?Hs =>
214
    eapply tac_eval_in with H _ _ _;
215
216
      [pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
      |let x := fresh in intros x; t; unfold x; reflexivity
217
      |pm_reduce; iEval_go t Hs]
218
219
  end.

220
Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
221
222
223
224
225
226
227
228
229
230
231
232
233
  iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.

Tactic Notation "iSimpl" := iEval (simpl).
Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.

(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:

  https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html

PMP told me (= Robbert) in person that this is not possible with the current
Ltac, but it may be possible in Ltac2. *)

234
235
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
236
  eapply tac_assumption with H _ _; (* (i:=H) *)
237
    [pm_reflexivity ||
238
     let H := pretty_ident H in
239
     fail "iExact:" H "not found"
240
    |iSolveTC ||
241
     let H := pretty_ident H in
242
243
     let P := match goal with |- FromAssumption _ ?P _ => P end in
     fail "iExact:" H ":" P "does not match goal"
244
    |pm_reduce; iSolveTC ||
245
     let H := pretty_ident H in
246
     fail "iExact: remaining hypotheses not affine and the goal not absorbing"].
247
248
249
250
251
252
253
254

Tactic Notation "iAssumptionCore" :=
  let rec find Γ i P :=
    lazymatch Γ with
    | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j|find Γ i P]
    end in
  match goal with
  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
255
     first [is_evar i; fail 1 | pm_reflexivity]
256
  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
257
     is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
258
  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
259
     first [is_evar i; fail 1 | pm_reflexivity]
260
  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
261
     is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
262
263
  end.

264
265
266
267
268
269
270
271
272
273
274
Tactic Notation "iAssumptionCoq" :=
  let Hass := fresh in
  match goal with
  | H :  ?P |- envs_entails _ ?Q =>
     pose proof (_ : FromAssumption true P Q) as Hass;
     notypeclasses refine (tac_assumption_coq _ P _ H _ _);
       [exact Hass
       |pm_reduce; iSolveTC ||
        fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
  end.

275
276
277
278
279
280
Tactic Notation "iAssumption" :=
  let Hass := fresh in
  let rec find p Γ Q :=
    lazymatch Γ with
    | Esnoc ?Γ ?j ?P => first
       [pose proof (_ : FromAssumption p P Q) as Hass;
Robbert Krebbers's avatar
Robbert Krebbers committed
281
        eapply (tac_assumption _ j p P);
282
          [pm_reflexivity
283
          |exact Hass
284
          |pm_reduce; iSolveTC ||
285
           fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
286
287
       |assert (P = False%I) as Hass by reflexivity;
        apply (tac_false_destruct _ j p P);
288
          [pm_reflexivity
289
290
291
292
293
          |exact Hass]
       |find p Γ Q]
    end in
  lazymatch goal with
  | |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
294
295
296
     first [find true Γp Q
           |find false Γs Q
           |iAssumptionCoq
297
298
299
300
301
302
           |fail "iAssumption:" Q "not found"]
  end.

(** * False *)
Tactic Notation "iExFalso" := apply tac_ex_falso.

303
304
(** * Making hypotheses intuitionistic or pure *)
Local Tactic Notation "iIntuitionistic" constr(H) :=
305
  eapply tac_intuitionistic with H _ _ _; (* (i:=H) *)
306
307
    [pm_reflexivity ||
     let H := pretty_ident H in
308
     fail "iIntuitionistic:" H "not found"
309
    |iSolveTC ||
310
     let P := match goal with |- IntoPersistent _ ?P _ => P end in
311
     fail "iIntuitionistic:" P "not persistent"
312
    |pm_reduce; iSolveTC ||
313
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
314
     fail "iIntuitionistic:" P "not affine and the goal not absorbing"
315
    |pm_reduce].
316

317
318
319
320
321
322
323
324
Local Tactic Notation "iSpatial" constr(H) :=
  eapply tac_spatial with H _ _ _;
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iSpatial:" H "not found"
    |pm_reduce; iSolveTC
    |pm_reduce].

325
Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
326
  eapply tac_pure with H _ _ _; (* (i:=H1) *)
327
328
329
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iPure:" H "not found"
330
    |iSolveTC ||
331
332
     let P := match goal with |- IntoPure ?P _ => P end in
     fail "iPure:" P "not pure"
333
    |pm_reduce; iSolveTC ||
334
335
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iPure:" P "not affine and the goal not absorbing"
336
    |pm_reduce; intros pat].
337
338
339
340

Tactic Notation "iEmpIntro" :=
  iStartProof;
  eapply tac_emp_intro;
341
    [pm_reduce; iSolveTC ||
342
343
344
345
346
     fail "iEmpIntro: spatial context contains non-affine hypotheses"].

Tactic Notation "iPureIntro" :=
  iStartProof;
  eapply tac_pure_intro;
347
    [iSolveTC ||
348
349
     let P := match goal with |- FromPure _ ?P _ => P end in
     fail "iPureIntro:" P "not pure"
350
351
    |pm_reduce; iSolveTC ||
     fail "iPureIntro: spatial context contains non-affine hypotheses"
352
353
354
355
    |].

(** Framing *)
Local Ltac iFrameFinish :=
356
  pm_prettify;
357
358
359
360
361
362
363
364
365
  try match goal with
  | |- envs_entails _ True => by iPureIntro
  | |- envs_entails _ emp => iEmpIntro
  end.

Local Ltac iFramePure t :=
  iStartProof;
  let φ := type of t in
  eapply (tac_frame_pure _ _ _ _ t);
366
    [iSolveTC || fail "iFrame: cannot frame" φ
367
368
369
370
    |iFrameFinish].

Local Ltac iFrameHyp H :=
  iStartProof;
371
  eapply tac_frame with H _ _ _;
372
373
374
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iFrame:" H "not found"
375
    |iSolveTC ||
376
377
     let R := match goal with |- Frame _ ?R _ _ => R end in
     fail "iFrame: cannot frame" R
378
    |pm_reduce; iFrameFinish].
379
380
381
382

Local Ltac iFrameAnyPure :=
  repeat match goal with H : _ |- _ => iFramePure H end.

383
Local Ltac iFrameAnyIntuitionistic :=
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
  iStartProof;
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
  match goal with
  | |- envs_entails ?Δ _ =>
     let Hs := eval cbv in (env_dom (env_intuitionistic Δ)) in go Hs
  end.

Local Ltac iFrameAnySpatial :=
  iStartProof;
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
  match goal with
  | |- envs_entails ?Δ _ =>
     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
  end.

Tactic Notation "iFrame" := iFrameAnySpatial.

Tactic Notation "iFrame" "(" constr(t1) ")" :=
  iFramePure t1.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" :=
  iFramePure t1; iFrame ( t2 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" :=
  iFramePure t1; iFrame ( t2 t3 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) constr(t8)")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ).

424
425
426
427
Local Ltac iFrame_go Hs :=
  lazymatch Hs with
  | [] => idtac
  | SelPure :: ?Hs => iFrameAnyPure; iFrame_go Hs
428
  | SelIntuitionistic :: ?Hs => iFrameAnyIntuitionistic; iFrame_go Hs
429
430
431
432
  | SelSpatial :: ?Hs => iFrameAnySpatial; iFrame_go Hs
  | SelIdent ?H :: ?Hs => iFrameHyp H; iFrame_go Hs
  end.

433
Tactic Notation "iFrame" constr(Hs) :=
434
  let Hs := sel_pat.parse Hs in iFrame_go Hs.
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
  iFramePure t1; iFrame Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")"
    constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.

(** * Basic introduction tactics *)
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
  (* In the case the goal starts with an [let x := _ in _], we do not
     want to unfold x and start the proof mode. Instead, we want to
     use intros. So [iStartProof] has to be called only if [intros]
     fails *)
463
464
465
466
467
468
469
470
471
472
473
474
475
476
  (* We use [_ || _] instead of [first [..|..]] so that the error in the second
  branch propagates upwards. *)
  (
    (* introduction at the meta level *)
    intros x
  ) || (
    (* introduction in the logic *)
    iStartProof;
    lazymatch goal with
    | |- envs_entails _ _ =>
      eapply tac_forall_intro;
        [iSolveTC ||
         let P := match goal with |- FromForall ?P _ => P end in
         fail "iIntro: cannot turn" P "into a universal quantifier"
477
478
479
480
481
482
        |let name := lazymatch goal with
                     | |- let _ := (λ name, _) in _ => name
                     end in
         pm_prettify;
         let y := fresh name in
         intros y; revert y; intros x
483
484
         (* subgoal *)]
    end).
485
486
487
488

Local Tactic Notation "iIntro" constr(H) :=
  iStartProof;
  first
489
  [(* (?Q → _) *)
490
    eapply tac_impl_intro with H _ _ _; (* (i:=H) *)
491
      [iSolveTC
492
      |pm_reduce; iSolveTC ||
493
494
495
       let P := lazymatch goal with |- Persistent ?P => P end in
       fail 1 "iIntro: introducing non-persistent" H ":" P
              "into non-empty spatial context"
496
      |iSolveTC
497
498
499
500
501
502
503
504
      |pm_reduce;
       let H := pretty_ident H in
        lazymatch goal with
        | |- False =>
          let H := pretty_ident H in
          fail 1 "iIntro:" H "not fresh"
        | _ => idtac (* subgoal *)
        end]
505
  |(* (_ -∗ _) *)
506
    eapply tac_wand_intro with H _ _; (* (i:=H) *)
507
      [iSolveTC
508
509
510
511
512
513
514
      | pm_reduce;
        lazymatch goal with
        | |- False =>
          let H := pretty_ident H in
          fail 1 "iIntro:" H "not fresh"
        | _ => idtac (* subgoal *)
        end]
515
  | fail 1 "iIntro: nothing to introduce" ].
516
517
518
519

Local Tactic Notation "iIntro" "#" constr(H) :=
  iStartProof;
  first
520
  [(* (?P → _) *)
521
   eapply tac_impl_intro_intuitionistic with H _ _ _; (* (i:=H) *)
522
523
524
525
     [iSolveTC
     |iSolveTC ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
      fail 1 "iIntro:" P "not persistent"
526
527
528
529
530
531
532
     |pm_reduce;
      lazymatch goal with
      | |- False =>
        let H := pretty_ident H in
        fail 1 "iIntro:" H "not fresh"
      | _ => idtac (* subgoal *)
      end]
533
  |(* (?P -∗ _) *)
534
   eapply tac_wand_intro_intuitionistic with H _ _ _; (* (i:=H) *)
535
536
537
     [iSolveTC
     |iSolveTC ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
538
      fail 1 "iIntro:" P "not intuitionistic"
539
540
541
     |iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail 1 "iIntro:" P "not affine and the goal not absorbing"
542
543
544
545
546
547
548
     |pm_reduce;
      lazymatch goal with
      | |- False =>
        let H := pretty_ident H in
        fail 1 "iIntro:" H "not fresh"
      | _ => idtac (* subgoal *)
      end]
549
  |fail 1 "iIntro: nothing to introduce"].
550

551
552
553
554
555
556
Local Tactic Notation "iIntro" constr(H) "as" constr(p) :=
  lazymatch p with
  | true => iIntro #H
  | _ =>  iIntro H
  end.

557
Local Tactic Notation "iIntro" "_" :=
558
  iStartProof;
559
  first
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
  [(* (?Q → _) *)
   eapply tac_impl_intro_drop;
     [iSolveTC
     |(* subgoal *)]
  |(* (_ -∗ _) *)
   eapply tac_wand_intro_drop;
     [iSolveTC
     |iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail 1 "iIntro:" P "not affine and the goal not absorbing"
     |(* subgoal *)]
  |(* (∀ _, _) *)
   iIntro (_)
   (* subgoal *)
  |fail 1 "iIntro: nothing to introduce"].
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597

Local Tactic Notation "iIntroForall" :=
  lazymatch goal with
  | |-  _, ?P => fail (* actually an →, this is handled by iIntro below *)
  | |-  _, _ => intro
  | |- let _ := _ in _ => intro
  | |- _ =>
    iStartProof;
    lazymatch goal with
    | |- envs_entails _ ( x : _, _) => let x' := fresh x in iIntro (x')
    end
  end.
Local Tactic Notation "iIntro" :=
  lazymatch goal with
  | |- _  ?P => intro
  | |- _ =>
    iStartProof;
    lazymatch goal with
    | |- envs_entails _ (_ - _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
    | |- envs_entails _ (_  _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
    end
  end.

598
599
600
601
602
603
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
  let err x :=
    intros x;
    iMatchHyp (fun H P =>
      lazymatch P with
604
605
      | context [x] =>
         let H := pretty_ident H in fail 2 "iRevert:" x "is used in hypothesis" H
606
607
      end) in
  iStartProof;
608
  first [let A := type of x in idtac|fail 1 "iRevert:" x "not in scope"];
609
610
611
612
613
614
  let A := type of x in
  lazymatch type of A with
  | Prop => revert x; first [apply tac_pure_revert|err x]
  | _ => revert x; first [apply tac_forall_revert|err x]
  end.

615
616
617
(** The tactic [iRevertHyp H with tac] reverts the hypothesis [H] and calls
[tac] with a Boolean that is [true] iff [H] was in the intuitionistic context. *)
Tactic Notation "iRevertHyp" constr(H) "with" tactic1(tac) :=
618
619
620
621
622
623
624
625
626
627
  eapply tac_revert with H;
    [lazymatch goal with
     | |- match envs_lookup_delete true ?i ?Δ with _ => _ end =>
        lazymatch eval pm_eval in (envs_lookup_delete true i Δ) with
        | Some (?p,_,_) => pm_reduce; tac p
        | None =>
           let H := pretty_ident H in
           fail "iRevert:" H "not found"
        end
     end].
628
629

Tactic Notation "iRevertHyp" constr(H) := iRevertHyp H with (fun _ => idtac).
630

631
632
633
634
635
636
637
Tactic Notation "iRevert" constr(Hs) :=
  let rec go Hs :=
    lazymatch Hs with
    | [] => idtac
    | ESelPure :: ?Hs =>
       repeat match goal with x : _ |- _ => revert x end;
       go Hs
638
    | ESelIdent _ ?H :: ?Hs => iRevertHyp H; go Hs
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
    end in
  iStartProof; let Hs := iElaborateSelPat Hs in go Hs.

Tactic Notation "iRevert" "(" ident(x1) ")" :=
  iForallRevert x1.
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ")" :=
  iForallRevert x2; iRevert ( x1 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ")" :=
  iForallRevert x3; iRevert ( x1 x2 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" :=
  iForallRevert x4; iRevert ( x1 x2 x3 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ")" :=
  iForallRevert x5; iRevert ( x1 x2 x3 x4 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ")" :=
  iForallRevert x6; iRevert ( x1 x2 x3 x4 x5 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ")" :=
  iForallRevert x7; iRevert ( x1 x2 x3 x4 x5 x6 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ")" :=
  iForallRevert x8; iRevert ( x1 x2 x3 x4 x5 x6 x7 ).
662
663
664
665
666
667
668
669
670
671
672
673
674
675
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ")" :=
  iForallRevert x9; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10) ")" :=
  iForallRevert x10; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ")" :=
  iForallRevert x11; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ")" :=
  iForallRevert x12; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ).
676
677
678
679
680
681
682
683
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ident(x13) ")" :=
  iForallRevert x13; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ident(x13) ident(x14) ")" :=
  iForallRevert x14; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ).
684
685
686
687
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" :=
  iForallRevert x15; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709

Tactic Notation "iRevert" "(" ident(x1) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")"
    constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 ).
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ).
725
726
727
728
729
730
731
732
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ident(x13) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ident(x13) ident(x14) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
733
734
735
736
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
    ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ).
737

738
(** * The specialize and pose proof tactics *)
739
740
741
742
743
744
745
746
747
748
Record iTrm {X As S} :=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
Arguments ITrm {_ _ _} _ _ _.

Notation "( H $! x1 .. xn )" :=
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
Notation "( H $! x1 .. xn 'with' pat )" :=
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).

749
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
750
  let Δ := iGetCtx in
751
  notypeclasses refine (tac_pose_proof_hyp _ H Hnew _ _);
752
753
754
755
756
757
758
759
760
761
762
763
764
765
    pm_reduce;
    lazymatch goal with
    | |- False =>
      let lookup := pm_eval (envs_lookup_delete false H Δ) in
      lazymatch lookup with
      | None =>
        let H := pretty_ident H in
        fail "iPoseProof:" H "not found"
      | _ =>
        let Hnew := pretty_ident Hnew in
        fail "iPoseProof:" Hnew "not fresh"
      end
    | _ => idtac
    end.
766

767
(* The tactic [iIntoEmpValid] tactic "imports a Coq lemma into the proofmode",
768
i.e., it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
769
770
771
772
773
774
775
776
following shape:

[∀ (x_1 : A_1) .. (x_n : A_n), φ]

for which we have an instance [AsEmpValid φ ?Q].

Examples of such [φ]s are

777
- [⊢ P], in which case [?Q] is unified with [P].
778
779
780
781
782
783
- [P1 ⊢ P2], in which case [?Q] is unified with [P1 -∗ P2].
- [P1 ⊣⊢ P2], in which case [?Q] is unified with [P1 ↔ P2].

The tactic instantiates each dependent argument [x_i : A_i] with an evar, and
generates a goal [A_i] for each non-dependent argument [x_i : A_i].

784
For example, if goal is [IntoEmpValid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
785
786
787
788
789
790
791
792
[iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
[?Q] with [R1 ?x -∗ R2 ?x]. *)
Ltac iIntoEmpValid_go := first
  [(* Case [φ → ψ] *)
   notypeclasses refine (into_emp_valid_impl _ _ _ _ _);
     [(*goal for [φ] *)|iIntoEmpValid_go]
  |(* Case [∀ x : A, φ] *)
   notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
793
794
  |(* Case [∀.. x : TT, φ] *)
   notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
795
  |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
796
797
798
799
800
801
802
803
804
805
806
   notypeclasses refine (into_emp_valid_here _ _ _)].

Ltac iIntoEmpValid :=
  (* Factor out the base case of the loop to avoid needless backtracking *)
  iIntoEmpValid_go;
    [.. (* goals for premises *)
    |iSolveTC ||
     let φ := lazymatch goal with |- AsEmpValid ?φ _ => φ end in
     fail "iPoseProof:" φ "not a BI assertion"].

Tactic Notation "iPoseProofCoreLem" open_constr(lem) "as" tactic3(tac) :=
807
  let Hnew := iFresh in
808
  notypeclasses refine (tac_pose_proof _ Hnew _ _ (into_emp_valid_proj _ _ _ lem) _);
809
    [iIntoEmpValid
810
811
812
813
814
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let Hnew := pretty_ident Hnew in
       fail "iPoseProof:" Hnew "not fresh"
815
     | _ => tac Hnew
816
     end];
817
818
819
  (* Solve all remaining TC premises generated by [iIntoEmpValid] *)
  try iSolveTC.

820
(** There is some hacky stuff going on here: because of Coq bug #6583, unresolved
821
822
823
824
825
type classes in e.g. the arguments [xs] of [iSpecializeArgs_go] are resolved at
arbitrary moments. That is because tactics like [apply], [split] and [eexists]
wrongly trigger type class search. To avoid TC being triggered too eagerly, the
tactics below use [notypeclasses refine] instead of [apply], [split] and
[eexists]. *)
826
Local Ltac iSpecializeArgs_go H xs :=
827
828
829
  lazymatch xs with
  | hnil => idtac
  | hcons ?x ?xs =>
830
     notypeclasses refine (tac_forall_specialize _ H _ _ _ _ _ _ _);
831
832
833
834
835
836
837
838
       [pm_reflexivity ||
        let H := pretty_ident H in
        fail "iSpecialize:" H "not found"
       |iSolveTC ||
        let P := match goal with |- IntoForall ?P _ => P end in
        fail "iSpecialize: cannot instantiate" P "with" x
       |lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
        | |-  _ : ?A, _ =>
839
840
          notypeclasses refine (@ex_intro A _ x _)
        end; [shelve..|pm_reduce; iSpecializeArgs_go H xs]]
841
  end.
842
843
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
  iSpecializeArgs_go H xs.
844

845
Ltac iSpecializePat_go H1 pats :=
846
847
848
849
850
851
852
  let solve_to_wand H1 :=
    iSolveTC ||
    let P := match goal with |- IntoWand _ _ ?P _ _ => P end in
    fail "iSpecialize:" P "not an implication/wand" in
  let solve_done d :=
    lazymatch d with
    | true =>
853
854
855
856
857
       first [ done
             | let Q := match goal with |- envs_entails _ ?Q => Q end in
               fail 1 "iSpecialize: cannot solve" Q "using done"
             | let Q := match goal with |- ?Q => Q end in
               fail 1 "iSpecialize: cannot solve" Q "using done" ]
858
859
    | false => idtac
    end in
860
  let Δ := iGetCtx in
861
  lazymatch pats with
862
863
864
    | [] => idtac
    | SForall :: ?pats =>
       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
865
       iSpecializePat_go H1 pats
866
867
868
    | SIdent ?H2 [] :: ?pats =>
       (* If we not need to specialize [H2] we can avoid a lot of unncessary
       context manipulation. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
869
       notypeclasses refine (tac_specialize false _ H2 _ H1 _ _ _ _ _ _ _ _ _);
870
871
872
873
874
875
         [pm_reflexivity ||
          let H2 := pretty_ident H2 in
          fail "iSpecialize:" H2 "not found"
         |pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
876
877
878
879
         |iSolveTC ||
          let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
          let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
          fail "iSpecialize: cannot instantiate" P "with" Q
880
         |pm_reduce; iSpecializePat_go H1 pats]
881
882
883
884
885
886
887
888
889
890
    | SIdent ?H2 ?pats1 :: ?pats =>
       (* If [H2] is in the intuitionistic context, we copy it into a new
       hypothesis [Htmp], so that it can be used multiple times. *)
       let H2tmp := iFresh in
       iPoseProofCoreHyp H2 as H2tmp;
       (* Revert [H1] and re-introduce it later so that it will not be consumsed
       by [pats1]. *)
       iRevertHyp H1 with (fun p =>
         iSpecializePat_go H2tmp pats1;
           [.. (* side-conditions of [iSpecialize] *)
891
           |iIntro H1 as p]);
892
893
894
895
         (* We put the stuff below outside of the closure to get less verbose
         Ltac backtraces (which would otherwise include the whole closure). *)
         [.. (* side-conditions of [iSpecialize] *)
         |(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
896
          notypeclasses refine (tac_specialize true _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
897
898
899
900
901
902
903
904
905
906
            [pm_reflexivity ||
             let H2tmp := pretty_ident H2tmp in
             fail "iSpecialize:" H2tmp "not found"
            |pm_reflexivity ||
             let H1 := pretty_ident H1 in
             fail "iSpecialize:" H1 "not found"
            |iSolveTC ||
             let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
             let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
             fail "iSpecialize: cannot instantiate" P "with" Q
907
            |pm_reduce; iSpecializePat_go H1 pats]]
908
    | SPureGoal ?d :: ?pats =>
909
       notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
910
911
912
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
913
914
915
916
917
         |solve_to_wand H1
         |iSolveTC ||
          let Q := match goal with |- FromPure _ ?Q _ => Q end in
          fail "iSpecialize:" Q "not pure"
         |solve_done d (*goal*)
918
919
         |pm_reduce;
          iSpecializePat_go H1 pats]
920
    | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
921
       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
922
923
924
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
925
926
927
928
929
         |solve_to_wand H1
         |iSolveTC ||
          let Q := match goal with |- Persistent ?Q => Q end in
          fail "iSpecialize:" Q "not persistent"
         |iSolveTC
930
         |pm_reduce; iFrame Hs_frame; solve_done d (*goal*)
931
         |pm_reduce; iSpecializePat_go H1 pats]
932
933
    | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats =>
       fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
934
935
    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
       let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
936
937
       notypeclasses refine (tac_specialize_assert _ H1 _
           (if m is GModal then true else false) lr Hs' _ _ _ _ _ _ _ _ _);
938
939
940
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
941
         |solve_to_wand H1
942
         |iSolveTC || fail "iSpecialize: goal not a modality"
943
944
945
         |pm_reduce;
          lazymatch goal with
          | |- False =>
946
            let Hs' := iMissingHypsCore Δ Hs' in
947
948
            fail "iSpecialize: hypotheses" Hs' "not found"
          | _ =>
949
            notypeclasses refine (conj _ _);
950
951
952
              [iFrame Hs_frame; solve_done d (*goal*)
              |iSpecializePat_go H1 pats]
          end]
953
    | SAutoFrame GIntuitionistic :: ?pats =>
954
       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
955
956
957
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
958
959
960
961
         |solve_to_wand H1
         |iSolveTC ||
          let Q := match goal with |- Persistent ?Q => Q end in
          fail "iSpecialize:" Q "not persistent"
962
         |pm_reduce; solve [iFrame "∗ #"]
963
         |pm_reduce; iSpecializePat_go H1 pats]
964
    | SAutoFrame ?m :: ?pats =>
965
966
       notypeclasses refine (tac_specialize_frame _ H1 _
           (if m is GModal then true else false) _ _ _ _ _ _ _ _ _ _ _);
967
968
969
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
970
         |solve_to_wand H1
971
         |iSolveTC || fail "iSpecialize: goal not a modality"
972
973
         |pm_reduce;
          first
974
975
976
977
            [notypeclasses refine (tac_unlock_emp _ _ _)
            |notypeclasses refine (tac_unlock_True _ _ _)
            |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
            |fail "iSpecialize: premise cannot be solved by framing"]
978
979
980
981
982
         |exact eq_refl]; iIntro H1; iSpecializePat_go H1 pats
    end.

Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
  let pats := spec_pat.parse pat in iSpecializePat_go H pats.
983

984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(** The tactics [iSpecialize trm as #] and [iSpecializeCore trm as true] allow
one to use the entire spatial context /twice/: the first time for proving the
premises [Q1 .. Qn] of [H : Q1 -* .. -∗ Qn -∗ R], and the second time for
proving the remaining goal. This is possible if all of the following properties
hold:
1. The conclusion [R] of the hypothesis [H] is persistent.
2. The specialization pattern [[> ..]] for wrapping a modality is not used for
   any of the premises [Q1 .. Qn].
3. The BI is either affine, or the hypothesis [H] resides in the intuitionistic
   context.

The copying of the context for proving the premises of [H] and the remaining
goal is implemented using the lemma [tac_specialize_intuitionistic_helper].

Since the tactic [iSpecialize .. as #] is used a helper to implement
[iDestruct .. as "#.."], [iPoseProof .. as "#.."], [iSpecialize .. as "#.."],
and friends, the behavior on violations of these conditions is as follows:
For faster browsing, not all history is shown. View entire blame