ltac_tactics.v 163 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
From iris.proofmode Require Export classes notation.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.prelude Require Import options.
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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
(** Tactic used for solving side-conditions arising from TC resolution in [iMod]
and [iInv]. *)
29
Ltac iSolveSideCondition :=
30
  split_and?; try solve [ fast_done | solve_ndisj | iSolveTC ].
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
Tactic Notation "iMatchHyp" tactic1(tac) :=
  match goal with
  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
  end.

67
68
69
70
71
72
73
74
75
76
77
78
79
Tactic Notation "iSelect" open_constr(pat) tactic1(tac) :=
  lazymatch goal with
  | |- context[ environments.Esnoc _ ?x pat ] =>
    (* Before runnig [tac] on the hypothesis name [x] we must first unify the
       pattern [pat] with the term it matched against. This forces every evar
       coming from [pat] (and in particular from the [_] it contains and from
       the implicit arguments it uses) to be instantiated. If we do not do so
       then shelved goals are produced for every such evar. *)
    lazymatch iTypeOf x with
    | Some (_,?T) => unify T pat; tac x
    end
  end.

80
81
82
83
84
(** * Start a proof *)
Tactic Notation "iStartProof" :=
  lazymatch goal with
  | |- envs_entails _ _ => idtac
  | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
85
               [iSolveTC || fail "iStartProof: not a BI assertion"
86
               |notypeclasses refine (tac_start _ _)]
87
88
89
90
91
92
93
94
95
96
  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
Yusuke Matsushita's avatar
Yusuke Matsushita committed
97
    type_term has a non-negligible performance impact. *)
98
99
100
101
102
103
104
105
    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) _ _ _);
106
               [iSolveTC || fail "iStartProof: not a BI assertion"
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
109
110
111
112
113
               |apply tac_start]
  end.

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

(** * Generate a fresh identifier *)
117
118
119
120
121
(** 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. *)
122
Ltac iFresh :=
123
124
125
126
  (* 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 *)
127
  let start :=
128
    lazymatch goal with
129
    | _ => iStartProof
130
    end in
131
132
133
134
  let c :=
    lazymatch goal with
    | |- envs_entails (Envs _ _ ?c) _ => c
    end in
135
  let inc :=
136
137
138
    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
139
      change_no_check (envs_entails (Envs Δp Δs c') Q)
140
141
    end in
  constr:(IAnon c).
142
143
144

(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
145
  eapply tac_rename with H1 H2 _ _; (* (i:=H1) (j:=H2) *)
146
147
148
    [pm_reflexivity ||
     let H1 := pretty_ident H1 in
     fail "iRename:" H1 "not found"
149
150
151
152
153
154
155
    |pm_reduce;
     lazymatch goal with
       | |- False =>
         let H2 := pretty_ident H2 in
         fail "iRename:" H2 "not fresh"
       | _ => idtac (* subgoal *)
     end].
156

157
158
159
Tactic Notation "iRename" "select" open_constr(pat) "into" constr(n) :=
  iSelect pat ltac:(fun H => iRename H into n).

160
161
162
(** Elaborated selection patterns, unlike the type [sel_pat], contains
only specific identifiers, and no wildcards like `#` (with the
exception of the pure selection pattern `%`) *)
163
Inductive esel_pat :=
164
  | ESelPure
165
  | ESelIdent : (* whether the ident is intuitionistic *) bool  ident  esel_pat.
166

Ralf Jung's avatar
Ralf Jung committed
167
Local Ltac iElaborateSelPat_go pat Δ Hs :=
168
169
170
  lazymatch pat with
  | [] => eval cbv in Hs
  | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)
171
  | SelIntuitionistic :: ?pat =>
172
    let Hs' := pm_eval (env_dom (env_intuitionistic Δ)) in
173
    let Δ' := pm_eval (envs_clear_intuitionistic Δ) in
174
175
    iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
  | SelSpatial :: ?pat =>
176
177
    let Hs' := pm_eval (env_dom (env_spatial Δ)) in
    let Δ' := pm_eval (envs_clear_spatial Δ) in
178
179
    iElaborateSelPat_go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
  | SelIdent ?H :: ?pat =>
180
    lazymatch pm_eval (envs_lookup_delete false H Δ) with
181
    | Some (?p,_,?Δ') =>  iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs)
182
183
184
    | None =>
      let H := pretty_ident H in
      fail "iElaborateSelPat:" H "not found"
185
186
    end
  end.
187
188
(** Converts a selection pattern (given as a string) to a list of
elaborated selection patterns. *)
189
190
191
Ltac iElaborateSelPat pat :=
  lazymatch goal with
  | |- envs_entails ?Δ _ =>
192
    let pat := sel_pat.parse pat in iElaborateSelPat_go pat Δ (@nil esel_pat)
193
194
195
  end.

Local Ltac iClearHyp H :=
196
  eapply tac_clear with H _ _; (* (i:=H) *)
197
198
199
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iClear:" H "not found"
200
    |pm_reduce; iSolveTC ||
201
     let H := pretty_ident H in
202
203
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iClear:" H ":" P "not affine and the goal not absorbing"
204
    |pm_reduce].
205

206
207
208
209
210
211
Local Ltac iClear_go Hs :=
  lazymatch Hs with
  | [] => idtac
  | ESelPure :: ?Hs => clear; iClear_go Hs
  | ESelIdent _ ?H :: ?Hs => iClearHyp H; iClear_go Hs
  end.
212
Tactic Notation "iClear" constr(Hs) :=
213
  iStartProof; let Hs := iElaborateSelPat Hs in iClear_go Hs.
214
215
216
217

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

218
219
220
Tactic Notation "iClear" "select" open_constr(pat) :=
  iSelect pat ltac:(fun H => iClear H).

221
(** ** Simplification *)
222
Tactic Notation "iEval" tactic3(t) :=
223
224
225
226
227
228
229
230
231
232
  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 =>
233
    eapply tac_eval_in with H _ _ _;
234
235
      [pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
      |let x := fresh in intros x; t; unfold x; reflexivity
236
      |pm_reduce; iEval_go t Hs]
237
238
  end.

239
Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
240
241
242
243
244
245
246
247
248
249
250
251
252
  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. *)

253
254
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
255
  eapply tac_assumption with H _ _; (* (i:=H) *)
256
    [pm_reflexivity ||
257
     let H := pretty_ident H in
258
     fail "iExact:" H "not found"
259
    |iSolveTC ||
260
     let H := pretty_ident H in
261
262
     let P := match goal with |- FromAssumption _ ?P _ => P end in
     fail "iExact:" H ":" P "does not match goal"
263
    |pm_reduce; iSolveTC ||
264
     let H := pretty_ident H in
265
     fail "iExact: remaining hypotheses not affine and the goal not absorbing"].
266
267
268
269
270
271
272
273

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) =>
274
     first [is_evar i; fail 1 | pm_reflexivity]
275
  | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some (_, ?P) =>
276
     is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
277
  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
278
     first [is_evar i; fail 1 | pm_reflexivity]
279
  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some (_, ?P, _) =>
280
     is_evar i; first [find Γp i P | find Γs i P]; pm_reflexivity
281
282
  end.

283
284
285
286
287
288
289
290
291
292
293
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.

294
295
296
297
298
299
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
300
        eapply (tac_assumption _ j p P);
301
          [pm_reflexivity
302
          |exact Hass
303
          |pm_reduce; iSolveTC ||
304
           fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
305
306
       |assert (P = False%I) as Hass by reflexivity;
        apply (tac_false_destruct _ j p P);
307
          [pm_reflexivity
308
309
310
311
312
          |exact Hass]
       |find p Γ Q]
    end in
  lazymatch goal with
  | |- envs_entails (Envs ?Γp ?Γs _) ?Q =>
313
314
315
     first [find true Γp Q
           |find false Γs Q
           |iAssumptionCoq
316
317
318
319
320
321
           |fail "iAssumption:" Q "not found"]
  end.

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

322
323
(** * Making hypotheses intuitionistic or pure *)
Local Tactic Notation "iIntuitionistic" constr(H) :=
324
  eapply tac_intuitionistic with H _ _ _; (* (i:=H) *)
325
326
    [pm_reflexivity ||
     let H := pretty_ident H in
327
     fail "iIntuitionistic:" H "not found"
328
    |iSolveTC ||
329
     let P := match goal with |- IntoPersistent _ ?P _ => P end in
330
     fail "iIntuitionistic:" P "not persistent"
331
    |pm_reduce; iSolveTC ||
332
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
333
     fail "iIntuitionistic:" P "not affine and the goal not absorbing"
334
    |pm_reduce].
335

336
337
338
339
340
341
342
343
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].

344
Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
345
  eapply tac_pure with H _ _ _; (* (i:=H1) *)
346
347
348
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iPure:" H "not found"
349
    |iSolveTC ||
350
351
     let P := match goal with |- IntoPure ?P _ => P end in
     fail "iPure:" P "not pure"
352
    |pm_reduce; iSolveTC ||
353
354
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iPure:" P "not affine and the goal not absorbing"
355
    |pm_reduce; intros pat].
356
357
358
359

Tactic Notation "iEmpIntro" :=
  iStartProof;
  eapply tac_emp_intro;
360
    [pm_reduce; iSolveTC ||
361
362
363
364
365
     fail "iEmpIntro: spatial context contains non-affine hypotheses"].

Tactic Notation "iPureIntro" :=
  iStartProof;
  eapply tac_pure_intro;
366
    [iSolveTC ||
367
368
     let P := match goal with |- FromPure _ ?P _ => P end in
     fail "iPureIntro:" P "not pure"
369
370
    |pm_reduce; iSolveTC ||
     fail "iPureIntro: spatial context contains non-affine hypotheses"
371
372
373
374
    |].

(** Framing *)
Local Ltac iFrameFinish :=
375
  pm_prettify;
376
377
378
379
380
381
382
383
384
  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);
385
    [iSolveTC || fail "iFrame: cannot frame" φ
386
387
388
389
    |iFrameFinish].

Local Ltac iFrameHyp H :=
  iStartProof;
390
  eapply tac_frame with H _ _ _;
391
392
393
    [pm_reflexivity ||
     let H := pretty_ident H in
     fail "iFrame:" H "not found"
394
    |iSolveTC ||
395
396
     let R := match goal with |- Frame _ ?R _ _ => R end in
     fail "iFrame: cannot frame" R
397
    |pm_reduce; iFrameFinish].
398
399
400
401

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

402
Local Ltac iFrameAnyIntuitionistic :=
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
  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 ).

443
444
445
446
Local Ltac iFrame_go Hs :=
  lazymatch Hs with
  | [] => idtac
  | SelPure :: ?Hs => iFrameAnyPure; iFrame_go Hs
447
  | SelIntuitionistic :: ?Hs => iFrameAnyIntuitionistic; iFrame_go Hs
448
449
450
451
  | SelSpatial :: ?Hs => iFrameAnySpatial; iFrame_go Hs
  | SelIdent ?H :: ?Hs => iFrameHyp H; iFrame_go Hs
  end.

452
Tactic Notation "iFrame" constr(Hs) :=
453
  let Hs := sel_pat.parse Hs in iFrame_go Hs.
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
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.

476
477
478
Tactic Notation "iFrame" "select" open_constr(pat) :=
  iSelect pat ltac:(fun H => iFrame H).

479
480
481
482
483
484
(** * 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 *)
485
486
487
488
489
490
491
492
493
494
495
496
  (* 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 ||
497
         let P := match goal with |- FromForall ?P _ _ => P end in
498
         fail "iIntro: cannot turn" P "into a universal quantifier"
499
500
501
502
503
504
        |let name := lazymatch goal with
                     | |- let _ := (λ name, _) in _ => name
                     end in
         pm_prettify;
         let y := fresh name in
         intros y; revert y; intros x
505
506
         (* subgoal *)]
    end).
507
508
509
510

Local Tactic Notation "iIntro" constr(H) :=
  iStartProof;
  first
511
  [(* (?Q → _) *)
512
    eapply tac_impl_intro with H _ _ _; (* (i:=H) *)
513
      [iSolveTC
514
      |pm_reduce; iSolveTC ||
515
       let P := lazymatch goal with |- Persistent ?P => P end in
516
       let H := pretty_ident H in
517
518
       fail 1 "iIntro: introducing non-persistent" H ":" P
              "into non-empty spatial context"
519
      |iSolveTC
520
521
522
523
524
525
526
527
      |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]
528
  |(* (_ -∗ _) *)
529
    eapply tac_wand_intro with H _ _; (* (i:=H) *)
530
      [iSolveTC
531
532
533
534
535
536
537
      | pm_reduce;
        lazymatch goal with
        | |- False =>
          let H := pretty_ident H in
          fail 1 "iIntro:" H "not fresh"
        | _ => idtac (* subgoal *)
        end]
538
539
  | let H := pretty_ident H in
    fail 1 "iIntro: could not introduce" H ", goal is not a wand or implication" ].
540
541
542
543

Local Tactic Notation "iIntro" "#" constr(H) :=
  iStartProof;
  first
544
  [(* (?P → _) *)
545
   eapply tac_impl_intro_intuitionistic with H _ _ _; (* (i:=H) *)
546
547
548
549
     [iSolveTC
     |iSolveTC ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
      fail 1 "iIntro:" P "not persistent"
550
551
552
553
554
555
556
     |pm_reduce;
      lazymatch goal with
      | |- False =>
        let H := pretty_ident H in
        fail 1 "iIntro:" H "not fresh"
      | _ => idtac (* subgoal *)
      end]
557
  |(* (?P -∗ _) *)
558
   eapply tac_wand_intro_intuitionistic with H _ _ _; (* (i:=H) *)
559
560
561
     [iSolveTC
     |iSolveTC ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
562
      fail 1 "iIntro:" P "not intuitionistic"
563
564
565
     |iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail 1 "iIntro:" P "not affine and the goal not absorbing"
566
567
568
569
570
571
572
     |pm_reduce;
      lazymatch goal with
      | |- False =>
        let H := pretty_ident H in
        fail 1 "iIntro:" H "not fresh"
      | _ => idtac (* subgoal *)
      end]
573
  |fail 1 "iIntro: nothing to introduce"].
574

575
576
577
578
579
580
Local Tactic Notation "iIntro" constr(H) "as" constr(p) :=
  lazymatch p with
  | true => iIntro #H
  | _ =>  iIntro H
  end.

581
Local Tactic Notation "iIntro" "_" :=
582
  iStartProof;
583
  first
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
  [(* (?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"].
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621

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.

622
623
624
625
626
627
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
  let err x :=
    intros x;
    iMatchHyp (fun H P =>
      lazymatch P with
628
629
      | context [x] =>
         let H := pretty_ident H in fail 2 "iRevert:" x "is used in hypothesis" H
630
631
      end) in
  iStartProof;
632
  first [let A := type of x in idtac|fail 1 "iRevert:" x "not in scope"];
633
634
635
636
637
638
  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.

639
640
641
(** 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) :=
642
643
644
645
646
647
648
649
650
651
  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].
652
653

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

655
656
657
658
659
660
661
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
662
    | ESelIdent _ ?H :: ?Hs => iRevertHyp H; go Hs
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
    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 ).
686
687
688
689
690
691
692
693
694
695
696
697
698
699
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 ).
700
701
702
703
704
705
706
707
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 ).
708
709
710
711
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 ).
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733

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 ).
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
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 ).
749
750
751
752
753
754
755
756
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 ).
757
758
759
760
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 ).
761

762
763
764
Tactic Notation "iRevert" "select" open_constr(pat) :=
  iSelect pat ltac:(fun H => iRevert H).

765
(** * The specialize and pose proof tactics *)
766
767
Record iTrm {X As S} :=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
Ralf Jung's avatar
Ralf Jung committed
768
Global Arguments ITrm {_ _ _} _ _ _.
769
770
771
772
773
774
775

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).

776
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
777
  let Δ := iGetCtx in
778
  notypeclasses refine (tac_pose_proof_hyp _ H Hnew _ _);
779
780
781
782
783
784
785
786
787
788
789
790
791
792
    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.
793

794
(* The tactic [iIntoEmpValid] tactic "imports a Coq lemma into the proofmode",
795
i.e., it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
796
797
798
799
800
801
802
803
following shape:

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

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

Examples of such [φ]s are

804
- [⊢ P], in which case [?Q] is unified with [P].
805
806
807
808
809
810
- [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].

811
For example, if goal is [IntoEmpValid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
812
813
814
815
816
817
818
819
[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
820
821
  |(* Case [∀.. x : TT, φ] *)
   notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
822
  |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
823
824
825
826
827
828
829
830
831
832
833
   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) :=
834
  let Hnew := iFresh in
835
  notypeclasses refine (tac_pose_proof _ Hnew _ _ (into_emp_valid_proj _ _ _ lem) _);
836
    [iIntoEmpValid
837
838
839
840
841
    |pm_reduce;
     lazymatch goal with
     | |- False =>
       let Hnew := pretty_ident Hnew in
       fail "iPoseProof:" Hnew "not fresh"
842
     | _ => tac Hnew
843
     end];
844
845
846
  (* Solve all remaining TC premises generated by [iIntoEmpValid] *)
  try iSolveTC.

847
(** There is some hacky stuff going on here: because of Coq bug #6583, unresolved
848
849
850
851
852
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]. *)
853
Local Ltac iSpecializeArgs_go H xs :=
854
855
856
  lazymatch xs with
  | hnil => idtac
  | hcons ?x ?xs =>
857
     notypeclasses refine (tac_forall_specialize _ H _ _ _ _ _ _ _);
858
859
860
861
862
863
864
865
       [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, _ =>
866
867
          notypeclasses refine (@ex_intro A _ x _)
        end; [shelve..|pm_reduce; iSpecializeArgs_go H xs]]
868
  end.
869
870
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
  iSpecializeArgs_go H xs.
871

872
Ltac iSpecializePat_go H1 pats :=
873
874
875
876
877
878
879
  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 =>
880
881
882
883
884
       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" ]
885
886
    | false => idtac
    end in
887
  let Δ := iGetCtx in
888
  lazymatch pats with
889
890
891
    | [] => idtac
    | SForall :: ?pats =>
       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
892
       iSpecializePat_go H1 pats
893
894
895
    | 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
896
       notypeclasses refine (tac_specialize false _ H2 _ H1 _ _ _ _ _ _ _ _ _);
897
898
899
900
901
902
         [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"
903
904
905
906
         |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
909
910
911
912
913
914
915
916
917
    | 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] *)
918
           |iIntro H1 as p]);
919
920
921
922
         (* 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
923
          notypeclasses refine (tac_specialize true _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
924
925
926
927
928
929
930
931
932
933
            [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
934
            |pm_reduce; iSpecializePat_go H1 pats]]
935
    | SPureGoal ?d :: ?pats =>
936
       notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
937
938
939
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
940
941
942
943
944
         |solve_to_wand H1
         |iSolveTC ||
          let Q := match goal with |- FromPure _ ?Q _ => Q end in
          fail "iSpecialize:" Q "not pure"
         |solve_done d (*goal*)
945
946
         |pm_reduce;
          iSpecializePat_go H1 pats]
947
    | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
948
       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
949
950
951
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
952
953
954
955
956
         |solve_to_wand H1
         |iSolveTC ||
          let Q := match goal with |- Persistent ?Q => Q end in
          fail "iSpecialize:" Q "not persistent"
         |iSolveTC
957
         |pm_reduce; iFrame Hs_frame; solve_done d (*goal*)
958
         |pm_reduce; iSpecializePat_go H1 pats]
959
960
    | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats =>
       fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
961
962
    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
       let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
963
964
       notypeclasses refine (tac_specialize_assert _ H1 _
           (if m is GModal then true else false) lr Hs' _ _ _ _ _ _ _ _ _);
965
966
967
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
968
         |solve_to_wand H1
969
         |iSolveTC || fail "iSpecialize: goal not a modality"
970
971
972
         |pm_reduce;
          lazymatch goal with
          | |- False =>
973
            let Hs' := iMissingHypsCore Δ Hs' in
974
975
            fail "iSpecialize: hypotheses" Hs' "not found"
          | _ =>
976
            notypeclasses refine (conj _ _);
977
978
979
              [iFrame Hs_frame; solve_done d (*goal*)
              |iSpecializePat_go H1 pats]
          end]
980
    | SAutoFrame GIntuitionistic :: ?pats =>
981
       notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
982
983
984
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
985
986
987
988
         |solve_to_wand H1
         |iSolveTC ||
          let Q := match goal with |- Persistent ?Q => Q end in
          fail "iSpecialize:" Q "not persistent"
989
         |pm_reduce; solve [iFrame "∗ #"]
990
         |pm_reduce; iSpecializePat_go H1 pats]
991
    | SAutoFrame ?m :: ?pats =>
992
993
       notypeclasses refine (tac_specialize_frame _ H1 _
           (if m is GModal then true else false) _ _ _ _ _ _ _ _ _ _ _);
994
995
996
         [pm_reflexivity ||
          let H1 := pretty_ident H1 in
          fail "iSpecialize:" H1 "not found"
997
         |solve_to_wand H1
998
         |iSolveTC || fail "iSpecialize: goal not a modality"