tactics.v 45.7 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
From iris.algebra Require Export upred.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.proofmode Require Export classes notation.
4
From iris.proofmode Require Import class_instances.
5
From iris.prelude Require Import stringmap hlist.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7

Declare Reduction env_cbv := cbv [
8
  env_lookup env_fold env_lookup_delete env_delete env_app
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
11
12
13
14
    env_replace env_split_go env_split
  decide (* operational classes *)
  sumbool_rec sumbool_rect (* sumbool *)
  bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
  assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
  string_eq_dec string_rec string_rect (* strings *)
15
  env_persistent env_spatial env_spatial_is_nil
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  envs_lookup envs_lookup_delete envs_delete envs_app
17
    envs_simple_replace envs_replace envs_split envs_clear_spatial].
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20
Ltac env_cbv :=
  match goal with |- ?u => let v := eval env_cbv in u in change v end.

21
(** * Misc *)
22
23
(* Tactic Notation tactics cannot return terms *)
Ltac iFresh' H :=
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
  lazymatch goal with
  |- of_envs ?Δ  _ =>
26
27
28
     (* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
     first use [cbv] to compute the domain of [Δ] *)
     let Hs := eval cbv in (envs_dom Δ) in
29
30
     eval vm_compute in (fresh_string_of_set H (of_list Hs))
  | _ => H
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  end.
32
Ltac iFresh := iFresh' "~".
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
38
39

Tactic Notation "iTypeOf" constr(H) tactic(tac):=
  let Δ := match goal with |- of_envs ?Δ  _ => Δ end in
  match eval env_cbv in (envs_lookup H Δ) with
  | Some (?p,?P) => tac p P
  end.

40
41
42
43
44
Ltac iMatchGoal tac :=
  match goal with
  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
(** * Start a proof *)
Tactic Notation "iProof" :=
  lazymatch goal with
  | |- of_envs _  _ => fail "iProof: already in Iris proofmode"
  | |- True  _ => apply tac_adequate
  | |- _  _ => apply uPred.wand_entails, tac_adequate
  end.

(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
  eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
    [env_cbv; reflexivity || fail "iRename:" H1 "not found"
    |env_cbv; reflexivity || fail "iRename:" H2 "not fresh"|].

Tactic Notation "iClear" constr(Hs) :=
  let rec go Hs :=
    match Hs with
    | [] => idtac
63
    | "★" :: ?Hs => eapply tac_clear_spatial; [env_cbv; reflexivity|go Hs]
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
68
69
70
71
    | ?H :: ?Hs =>
       eapply tac_clear with _ H _ _; (* (i:=H) *)
         [env_cbv; reflexivity || fail "iClear:" H "not found"|go Hs]
    end in
  let Hs := words Hs in go Hs.

(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
72
73
  eapply tac_assumption with H _ _; (* (i:=H) *)
    [env_cbv; reflexivity || fail "iExact:" H "not found"
74
    |let P := match goal with |- FromAssumption _ ?P _ => P end in
75
     apply _ || fail "iExact:" H ":" P "does not match goal"].
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
79
80
81
82
83
84
85
86
87

Tactic Notation "iAssumptionCore" :=
  let rec find Γ i P :=
    match Γ 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) =>
     first [is_evar i; fail 1 | env_cbv; reflexivity]
  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
     is_evar i; first [find Γp i P | find Γs i P]; env_cbv; reflexivity
  end.
88

Robbert Krebbers's avatar
Robbert Krebbers committed
89
Tactic Notation "iAssumption" :=
90
91
92
93
  let Hass := fresh in
  let rec find p Γ Q :=
    match Γ with
    | Esnoc ?Γ ?j ?P => first
94
       [pose proof (_ : FromAssumption p P Q) as Hass;
95
96
97
98
99
100
101
102
        apply (tac_assumption _ j p P); [env_cbv; reflexivity|apply Hass]
       |find p Γ Q]
    end in
  match goal with
  | |- of_envs (Envs ?Γp ?Γs)  ?Q =>
     first [find true Γp Q | find false Γs Q
           |fail "iAssumption:" Q "not found"]
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
106
107

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

(** * Making hypotheses persistent or pure *)
108
Local Tactic Notation "iPersistent" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
  eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
    [env_cbv; reflexivity || fail "iPersistent:" H "not found"
111
    |let Q := match goal with |- IntoPersistentP ?Q _ => Q end in
112
     apply _ || fail "iPersistent:" Q "not persistent"
Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
    |env_cbv; reflexivity|].

115
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
  eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
    [env_cbv; reflexivity || fail "iPure:" H "not found"
118
    |let P := match goal with |- IntoPure ?P _ => P end in
119
     apply _ || fail "iPure:" P "not pure"
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
    |intros pat].

122
123
Tactic Notation "iPureIntro" :=
  eapply tac_pure_intro;
124
    [let P := match goal with |- FromPure ?P _ => P end in
125
     apply _ || fail "iPureIntro:" P "not pure"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127

(** * Specialize *)
128
129
130
131
132
Record iTrm {X As} :=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
Arguments ITrm {_ _} _ _ _.

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

138
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
139
140
141
142
143
  match xs with
  | hnil => idtac
  | _ =>
    eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
      [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
144
145
      |let P := match goal with |- ForallSpecialize _ ?P _ => P end in
       apply _ || fail 1 "iSpecialize:" P "not a forall of the right arity or type"
Robbert Krebbers's avatar
Robbert Krebbers committed
146
      |cbn [himpl hcurry]; reflexivity|]
147
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
148

149
Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  let solve_to_wand H1 :=
151
    let P := match goal with |- IntoWand ?P _ _ => P end in
152
    apply _ || fail "iSpecialize:" P "not an implication/wand" in
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
  let rec go H1 pats :=
    lazymatch pats with
    | [] => idtac
156
    | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
157
    | SName ?H2 :: ?pats =>
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
160
       eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
         [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
         |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
161
162
         |let P := match goal with |- IntoWand ?P ?Q _ => P end in
          let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
163
          apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
Robbert Krebbers's avatar
Robbert Krebbers committed
164
         |env_cbv; reflexivity|go H1 pats]
165
    | SGoalPersistent :: ?pats =>
166
       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
167
168
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
169
170
         |let Q := match goal with |- PersistentP ?Q => Q end in
          apply _ || fail "iSpecialize:" Q "not persistent"
171
172
173
174
         |env_cbv; reflexivity
         |(*goal*)
         |go H1 pats]
    | SGoalPure :: ?pats =>
175
       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
176
177
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
178
         |let Q := match goal with |- FromPure ?Q _ => Q end in
179
180
181
182
          apply _ || fail "iSpecialize:" Q "not pure"
         |env_cbv; reflexivity
         |(*goal*)
         |go H1 pats]
183
184
    | SGoal ?k ?lr ?Hs :: ?pats =>
       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
187
         |match k with
188
          | GoalStd => apply into_assert_default
189
          | GoalVs => apply _ || fail "iSpecialize: cannot generate view shifted goal"
190
          end
191
192
         |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
         |(*goal*)
Robbert Krebbers's avatar
Robbert Krebbers committed
193
         |go H1 pats]
194
195
    end in let pats := spec_pat.parse pat in go H pats.

196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
(* p = whether the conclusion of the specialized term is persistent. It can
either be a Boolean or an introduction pattern, which will be coerced in true
when it only contains `#` or `%` patterns at the top-level. *)
Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) tactic(tac) :=
  let p :=
    lazymatch type of p with
    | intro_pat => eval cbv in (intro_pat_persistent p)
    | string =>
       let pat := intro_pat.parse_one p in
       eval cbv in (intro_pat_persistent pat)
    | _ => p
    end in
  lazymatch t with
  | ITrm ?H ?xs ?pat =>
    lazymatch p with
    | true =>
       eapply tac_specialize_persistent_helper with _ H _ _ _;
         [env_cbv; reflexivity || fail "iSpecialize:" H "not found"
         |iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
         |let Q := match goal with |- PersistentP ?Q => Q end in
          apply _ || fail "iSpecialize:" Q "not persistent"
         |env_cbv; reflexivity|tac H]
    | false => iSpecializeArgs H xs; iSpecializePat H pat; last (tac H)
    end
220
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222
223
224
225
226
Tactic Notation "iSpecialize" open_constr(t) :=
  iSpecializeCore t as false (fun _ => idtac).
Tactic Notation "iSpecialize" open_constr(t) "#" :=
  iSpecializeCore t as true (fun _ => idtac).

Robbert Krebbers's avatar
Robbert Krebbers committed
227
(** * Pose proof *)
228
229
230
231
232
233
234
235
236
237
238
(* The tactic [iIntoEntails] tactic solves a goal [True ⊢ Q]. The arguments [t]
is a Coq term whose type is of the following shape:

- [∀ (x_1 : A_1) .. (x_n : A_n), True ⊢ Q]
- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -★ P2]
- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊣⊢ P2], in which case [Q] becomes [P1 ↔ P2]

The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [P] for non-dependent arguments [x_i : P]. *)
Tactic Notation "iIntoEntails" open_constr(t) :=
  let rec go t :=
239
240
    let tT := type of t in
    lazymatch eval hnf in tT with
241
242
    | True  _ => apply t
    | _  _ => apply (uPred.entails_wand _ _ t)
243
244
    (* need to use the unfolded version of [⊣⊢] due to the hnf *)
    | uPred_equiv' _ _ => apply (uPred.equiv_iff _ _ t)
245
    | ?P  ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
246
247
248
249
250
251
252
253
    |  _ : ?T, _ =>
       (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
       (* This is a workarround for Coq bug #4969. *)
       let e := fresh in evar (e:id T);
       let e' := eval unfold e in e in clear e; go (t e')
    end
  in go t.

254
Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) :=
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
  let pose_trm t tac :=
    let Htmp := iFresh in
    lazymatch type of t with
    | string =>
       eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
         [env_cbv; reflexivity || fail "iPoseProof:" t "not found"
         |env_cbv; reflexivity || fail "iPoseProof:" Htmp "not fresh"
         |tac Htmp]
    | _ =>
       eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
         [iIntoEntails t
         |env_cbv; reflexivity || fail "iPoseProof:" Htmp "not fresh"
         |tac Htmp]
    end;
    try (apply _) (* solve TC constraints. It is essential that this happens
    after the continuation [tac] has been called. *)
  in lazymatch lem with
  | ITrm ?t ?xs ?pat =>
273
     pose_trm t ltac:(fun Htmp => iSpecializeCore (ITrm Htmp xs pat) as p tac)
274
  | _ => pose_trm lem tac
Robbert Krebbers's avatar
Robbert Krebbers committed
275
276
  end.

277
Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
278
  iPoseProofCore lem as false (fun Htmp => iRename Htmp into H).
Robbert Krebbers's avatar
Robbert Krebbers committed
279
280

(** * Apply *)
281
Tactic Notation "iApply" open_constr(lem) :=
282
283
284
285
  let finish H := first
    [iExact H
    |eapply tac_apply with _ H _ _ _;
       [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
286
       |let P := match goal with |- IntoWand ?P _ _ => P end in
287
        apply _ || fail 1 "iApply: cannot apply" P
288
       |lazy beta (* reduce betas created by instantiation *)]] in
289
290
  lazymatch lem with
  | ITrm ?t ?xs ?pat =>
291
     iPoseProofCore t as false (fun Htmp =>
292
293
       iSpecializeArgs Htmp xs;
       try (iSpecializeArgs Htmp (hcons _ _));
294
       iSpecializePat Htmp pat; last finish Htmp)
295
  | _ =>
296
     iPoseProofCore lem as false (fun Htmp =>
297
       try (iSpecializeArgs Htmp (hcons _ _));
298
       finish Htmp)
299
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
301

(** * Revert *)
302
Local Tactic Notation "iForallRevert" ident(x) :=
303
304
305
  let A := type of x in
  lazymatch type of A with
  | Prop => revert x; apply tac_pure_revert
Robbert Krebbers's avatar
Robbert Krebbers committed
306
  | _ => revert x; apply tac_forall_revert
307
  end || fail "iRevert: cannot revert" x.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
309
310

Tactic Notation "iRevert" constr(Hs) :=
  let rec go H2s :=
311
312
313
314
315
316
317
318
319
    match H2s with
    | [] => idtac
    | "★" :: ?H2s => go H2s; eapply tac_revert_spatial; env_cbv
    | ?H2 :: ?H2s =>
       go H2s;
       eapply tac_revert with _ H2 _ _; (* (i:=H2) *)
         [env_cbv; reflexivity || fail "iRevert:" H2 "not found"
         |env_cbv]
    end in
Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
  let Hs := words Hs in go Hs.

322
Tactic Notation "iRevert" "(" ident(x1) ")" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  iForallRevert x1.
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
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 ).

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) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
350
    constr(Hs) :=
351
352
353
354
355
356
357
358
359
360
361
362
363
  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 ).
Robbert Krebbers's avatar
Robbert Krebbers committed
364
365
366
367

(** * Disjunction *)
Tactic Notation "iLeft" :=
  eapply tac_or_l;
368
    [let P := match goal with |- FromOr ?P _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
369
370
371
     apply _ || fail "iLeft:" P "not a disjunction"|].
Tactic Notation "iRight" :=
  eapply tac_or_r;
372
    [let P := match goal with |- FromOr ?P _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
373
374
     apply _ || fail "iRight:" P "not a disjunction"|].

375
Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
376
377
  eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
    [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
378
    |let P := match goal with |- IntoOr ?P _ _ => P end in
379
     apply _ || fail "iOrDestruct: cannot destruct" P
Robbert Krebbers's avatar
Robbert Krebbers committed
380
381
382
383
384
    |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
    |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].

(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
385
386
387
  lazymatch goal with
  | |- _  _ =>
    eapply tac_and_split;
388
      [let P := match goal with |- FromAnd ?P _ _ => P end in
389
390
391
       apply _ || fail "iSplit:" P "not a conjunction"| |]
  | |- _  _ => apply (anti_symm ())
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
392
393
394
395

Tactic Notation "iSplitL" constr(Hs) :=
  let Hs := words Hs in
  eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
396
    [let P := match goal with |- FromSep ?P _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
397
     apply _ || fail "iSplitL:" P "not a separating conjunction"
398
399
    |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs
                                  "not found in the spatial context"| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
400
401
402
Tactic Notation "iSplitR" constr(Hs) :=
  let Hs := words Hs in
  eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
403
    [let P := match goal with |- FromSep ?P _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
404
     apply _ || fail "iSplitR:" P "not a separating conjunction"
405
406
    |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs
                                  "not found in the spatial context"| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
407
408
409
410

Tactic Notation "iSplitL" := iSplitR "".
Tactic Notation "iSplitR" := iSplitL "".

411
412
413
414
415
416
417
418
419
420
421
422
423
Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
  eapply tac_and_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
    [env_cbv; reflexivity || fail "iAndDestruct:" H "not found"
    |let P := match goal with |- IntoAnd _ ?P _ _ => P end in
     apply _ || fail "iAndDestruct: cannot destruct" P
    |env_cbv; reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|].

Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H') :=
  eapply tac_and_destruct_choice with _ H _ lr H' _ _ _;
    [env_cbv; reflexivity || fail "iAndDestruct:" H "not found"
    |let P := match goal with |- IntoAnd _ ?P _ _ => P end in
     apply _ || fail "iAndDestruct: cannot destruct" P
    |env_cbv; reflexivity || fail "iAndDestruct:" H' " not fresh"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
424
425
426
427
428

Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
  eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
    [env_cbv; reflexivity || fail "iCombine:" H1 "not found"
    |env_cbv; reflexivity || fail "iCombine:" H2 "not found"
429
430
    |let P1 := match goal with |- FromSep _ ?P1 _ => P1 end in
     let P2 := match goal with |- FromSep _ _ ?P2 => P2 end in
431
     apply _ || fail "iCombine: cannot combine" P1 "and" P2
Robbert Krebbers's avatar
Robbert Krebbers committed
432
433
    |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].

434
(** Framing *)
435
436
437
438
439
Local Ltac iFramePure t :=
  let φ := type of t in
  eapply (tac_frame_pure _ _ _ _ t);
    [apply _ || fail "iFrame: cannot frame" φ|].

440
441
442
443
444
445
446
Local Ltac iFrameHyp H :=
  eapply tac_frame with _ H _ _ _;
    [env_cbv; reflexivity || fail "iFrame:" H "not found"
    |let R := match goal with |- Frame ?R _ _ => R end in
     apply _ || fail "iFrame: cannot frame" R
    |lazy iota beta].

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

Local Ltac iFrameAnyPersistent :=
451
452
453
454
455
456
457
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
  match goal with
  | |- of_envs ?Δ  _ =>
     let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
  end.

458
Local Ltac iFrameAnySpatial :=
459
460
461
462
463
464
465
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
  match goal with
  | |- of_envs ?Δ  _ =>
     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
  end.

466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
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 ).

489
490
491
492
Tactic Notation "iFrame" constr(Hs) :=
  let rec go Hs :=
    match Hs with
    | [] => idtac
493
494
495
    | "%" :: ?Hs => iFrameAnyPure; go Hs
    | "#" :: ?Hs => iFrameAnyPersistent; go Hs
    | "★" :: ?Hs => iFrameAnySpatial; go Hs
496
497
498
    | ?H :: ?Hs => iFrameHyp H; go Hs
    end
  in let Hs := words Hs in go Hs.
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
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.
520

Robbert Krebbers's avatar
Robbert Krebbers committed
521
(** * Existential *)
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
Tactic Notation "iExists" uconstr(x1) :=
  eapply tac_exist;
524
    [let P := match goal with |- FromExist ?P _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
525
     apply _ || fail "iExists:" P "not an existential"
Robbert Krebbers's avatar
Robbert Krebbers committed
526
    |cbv beta; eexists x1].
Robbert Krebbers's avatar
Robbert Krebbers committed
527

Robbert Krebbers's avatar
Robbert Krebbers committed
528
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
529
  iExists x1; iExists x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
531
  iExists x1; iExists x2, x3.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
534
  iExists x1; iExists x2, x3, x4.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
536
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
537
  iExists x1; iExists x2, x3, x4, x5.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
539
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) "," uconstr(x6) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
540
  iExists x1; iExists x2, x3, x4, x5, x6.
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
543
  iExists x1; iExists x2, x3, x4, x5, x6, x7.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
545
546
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) ","
    uconstr(x8) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
547
548
  iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.

549
550
Local Tactic Notation "iExistDestruct" constr(H)
    "as" simple_intropattern(x) constr(Hx) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
551
552
  eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
    [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
553
    |let P := match goal with |- IntoExist ?P _ => P end in
554
     apply _ || fail "iExistDestruct: cannot destruct" P|];
555
556
557
558
  let y := fresh in
  intros y; eexists; split;
    [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
    |revert y; intros x].
Robbert Krebbers's avatar
Robbert Krebbers committed
559

Robbert Krebbers's avatar
Robbert Krebbers committed
560
561
562
563
564
565
566
567
568
569
570
571
572
(** * Always *)
Tactic Notation "iAlways":=
  apply tac_always_intro;
    [reflexivity || fail "iAlways: spatial context non-empty"|].

(** * Later *)
Tactic Notation "iNext":=
  eapply tac_next;
    [apply _
    |let P := match goal with |- FromLater ?P _ => P end in
     apply _ || fail "iNext:" P "does not contain laters"|].

Tactic Notation "iTimeless" constr(H) :=
573
  eapply tac_timeless with _ H _ _ _;
574
    [let Q := match goal with |- IsExceptLast ?Q => Q end in
575
     apply _ || fail "iTimeless: cannot remove later when goal is" Q
Robbert Krebbers's avatar
Robbert Krebbers committed
576
    |env_cbv; reflexivity || fail "iTimeless:" H "not found"
577
    |let P := match goal with |- IntoExceptLast ?P _ => P end in
578
     apply _ || fail "iTimeless: cannot turn" P "into ◇"
Robbert Krebbers's avatar
Robbert Krebbers committed
579
580
581
582
583
584
    |env_cbv; reflexivity|].

(** * View shifts *)
Tactic Notation "iVsIntro" :=
  eapply tac_vs_intro;
    [let P := match goal with |- FromVs ?P _ => P end in
585
     apply _ || fail "iVsIntro:" P "not a view shift"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
586
587
588
589
590

Tactic Notation "iVsCore" constr(H) :=
  eapply tac_vs_elim with _ H _ _ _ _;
    [env_cbv; reflexivity || fail "iVs:" H "not found"
    |let P := match goal with |- ElimVs ?P _ _ _ => P end in
591
     let Q := match goal with |- ElimVs _ _ ?Q _ => Q end in
592
     apply _ || fail "iVs: cannot run" P "in" Q
593
                     "because the goal or hypothesis is not a view shift"
Robbert Krebbers's avatar
Robbert Krebbers committed
594
595
    |env_cbv; reflexivity|].

596
(** * Basic destruct tactic *)
597
Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
598
599
600
  let rec go Hz pat :=
    lazymatch pat with
    | IAnom => idtac
601
    | IDrop => iClear Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
602
    | IFrame => iFrame Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
603
    | IName ?y => iRename Hz into y
604
    | IList [[]] => iExFalso; iExact Hz
605
606
    | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as true Hz; go Hz pat1
    | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as false Hz; go Hz pat2
Robbert Krebbers's avatar
Robbert Krebbers committed
607
    | IList [[?pat1; ?pat2]] =>
608
       let Hy := iFresh in iAndDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
Robbert Krebbers's avatar
Robbert Krebbers committed
609
    | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
Robbert Krebbers's avatar
Robbert Krebbers committed
610
611
612
613
    | IPureElim => iPure Hz as ?
    | IAlwaysElim ?pat => iPersistent Hz; go Hz pat
    | ILaterElim ?pat => iTimeless Hz; go Hz pat
    | IVsElim ?pat => iVsCore Hz; go Hz pat
Robbert Krebbers's avatar
Robbert Krebbers committed
614
615
616
617
    | _ => fail "iDestruct:" pat "invalid"
    end
  in let pat := intro_pat.parse_one pat in go H pat.

618
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
619
620
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as @ pat.
621
622
623
624
625
626
627
628
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as ( x2 ) pat.
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 ) pat.
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
629
    constr(pat) :=
630
631
  iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 ) pat.
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
632
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
633
634
635
    simple_intropattern(x5) ")" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 ) pat.
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
636
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
637
638
639
    simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 ) pat.
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
640
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
641
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
642
    constr(pat) :=
643
644
  iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 ) pat.
Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
645
646
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
647
648
    simple_intropattern(x8) ")" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
649
650

(** * Introduction tactic *)
651
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
652
653
  [ (* (∀ _, _) *) apply tac_forall_intro; intros x
  | (* (?P → _) *) eapply tac_impl_intro_pure;
654
     [let P := match goal with |- IntoPure ?P _ => P end in
655
656
657
      apply _ || fail "iIntro:" P "not pure"
     |intros x]
  | (* (?P -★ _) *) eapply tac_wand_intro_pure;
658
     [let P := match goal with |- IntoPure ?P _ => P end in
659
660
661
662
663
664
      apply _ || fail "iIntro:" P "not pure"
     |intros x]
  |intros x].

Local Tactic Notation "iIntro" constr(H) := first
  [ (* (?Q → _) *)
665
    eapply tac_impl_intro with _ H; (* (i:=H) *)
666
667
      [reflexivity || fail 1 "iIntro: introducing" H
                             "into non-empty spatial context"
668
      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
669
  | (* (_ -★ _) *)
670
    eapply tac_wand_intro with _ H; (* (i:=H) *)
671
672
      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | fail 1 "iIntro: nothing to introduce" ].
673

674
675
Local Tactic Notation "iIntro" "#" constr(H) := first
  [ (* (?P → _) *)
676
    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
677
      [let P := match goal with |- IntoPersistentP ?P _ => P end in
678
679
680
       apply _ || fail 1 "iIntro: " P " not persistent"
      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | (* (?P -★ _) *)
681
    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
682
      [let P := match goal with |- IntoPersistentP ?P _ => P end in
683
684
685
       apply _ || fail 1 "iIntro: " P " not persistent"
      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | fail 1 "iIntro: nothing to introduce" ].
686

687
688
689
690
Local Tactic Notation "iIntroForall" :=
  lazymatch goal with
  | |-  _, ?P => fail
  | |-  _, _ => intro
691
  | |- _  ( x : _, _) => iIntro (x)
692
693
694
695
  end.
Local Tactic Notation "iIntro" :=
  lazymatch goal with
  | |- _  ?P => intro
696
697
  | |- _  (_ - _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
  | |- _  (_  _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
698
699
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
700
701
702
703
Tactic Notation "iIntros" constr(pat) :=
  let rec go pats :=
    lazymatch pats with
    | [] => idtac
Robbert Krebbers's avatar
Robbert Krebbers committed
704
705
706
707
708
709
710
711
712
713
    | IPureElim :: ?pats => iIntro (?); go pats
    | IAlwaysElim IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
    | IAnom :: ?pats => let H := iFresh in iIntro H; go pats
    | IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats
    | IName ?H :: ?pats => iIntro H; go pats
    | IPureIntro :: ?pats => iPureIntro; go pats
    | IAlwaysIntro :: ?pats => iAlways; go pats
    | ILaterIntro :: ?pats => iNext; go pats
    | IVsIntro :: ?pats => iVsIntro; go pats
    | ISimpl :: ?pats => simpl; go pats
714
715
    | IForall :: ?pats => repeat iIntroForall; go pats
    | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
716
717
718
719
720
721
722
    | IClear ?cpats :: ?pats =>
       let rec clr cpats :=
         match cpats with
         | [] => go pats
         | (false,?H) :: ?cpats => iClear H; clr cpats
         | (true,?H) :: ?cpats => iFrame H; clr cpats
         end in clr cpats
Robbert Krebbers's avatar
Robbert Krebbers committed
723
    | IAlwaysElim ?pat :: ?pats =>
Robbert Krebbers's avatar
Robbert Krebbers committed
724
725
726
727
728
       let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
    | ?pat :: ?pats =>
       let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
    end
  in let pats := intro_pat.parse pat in try iProof; go pats.
Robbert Krebbers's avatar
Robbert Krebbers committed
729
Tactic Notation "iIntros" := iIntros [IAll].
Robbert Krebbers's avatar
Robbert Krebbers committed
730

731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
  try iProof; iIntro ( x1 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" :=
  iIntros ( x1 ); iIntro ( x2 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) ")" :=
  iIntros ( x1 x2 ); iIntro ( x3 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) simple_intropattern(x4) ")" :=
  iIntros ( x1 x2 x3 ); iIntro ( x4 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5) ")" :=
  iIntros ( x1 x2 x3 x4 ); iIntro ( x5 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
746
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
747
748
749
    simple_intropattern(x6) ")" :=
  iIntros ( x1 x2 x3 x4 x5 ); iIntro ( x6 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
750
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
751
752
753
    simple_intropattern(x6) simple_intropattern(x7) ")" :=
  iIntros ( x1 x2 x3 x4 x5 x6 ); iIntro ( x7 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
754
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
    simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8) ")" :=
  iIntros ( x1 x2 x3 x4 x5 x6 x7 ); iIntro ( x8 ).

Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" constr(p) :=
  iIntros ( x1 ); iIntros p.
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
    ")" constr(p) :=
  iIntros ( x1 x2 ); iIntros p.
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) ")" constr(p) :=
  iIntros ( x1 x2 x3 ); iIntros p.
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) simple_intropattern(x4) ")" constr(p) :=
  iIntros ( x1 x2 x3 x4 ); iIntros p.
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
770
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
771
772
773
    ")" constr(p) :=
  iIntros ( x1 x2 x3 x4 x5 ); iIntros p.
Tactic Notation "iIntros" "("simple_intropattern(x1) simple_intropattern(x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
774
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
775
776
777
    simple_intropattern(x6) ")" constr(p) :=
  iIntros ( x1 x2 x3 x4 x5 x6 ); iIntros p.
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
778
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
779
780
781
    simple_intropattern(x6) simple_intropattern(x7) ")" constr(p) :=
  iIntros ( x1 x2 x3 x4 x5 x6 x7 ); iIntros p.
Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
782
783
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8)
784
785
    ")" constr(p) :=
  iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p.
Robbert Krebbers's avatar
Robbert Krebbers committed
786

787
788
789
Tactic Notation "iRevertIntros" "with" tactic(tac) :=
  match goal with
  | |- of_envs ?Δ  _ =>
790
     let Hs := eval cbv in (reverse (env_dom (env_spatial Δ))) in
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
     iRevert ["★"]; tac; iIntros Hs
  end.
Tactic Notation "iRevertIntros" "(" ident(x1) ")" "with" tactic(tac):=
  iRevertIntros with (iRevert (x1); tac; iIntros (x1)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ")" "with" tactic(tac):=
  iRevertIntros with (iRevert (x1 x2); tac; iIntros (x1 x2)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ")"
    "with" tactic(tac):=
  iRevertIntros with (iRevert (x1 x2 x3); tac; iIntros (x1 x2 x3)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")"
    "with" tactic(tac):=
  iRevertIntros with (iRevert (x1 x2 x3 x4); tac; iIntros (x1 x2 x3 x4)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ")" "with" tactic(tac):=
  iRevertIntros with (iRevert (x1 x2 x3 x4 x5); tac; iIntros (x1 x2 x3 x4 x5)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ")" "with" tactic(tac):=
  iRevertIntros with (iRevert (x1 x2 x3 x4 x5 x6);
    tac; iIntros (x1 x2 x3 x4 x5 x6)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ")" "with" tactic(tac):=
  iRevertIntros with (iRevert (x1 x2 x3 x4 x5 x6 x7);
    tac; iIntros (x1 x2 x3 x4 x5 x6 x7)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ")" "with" tactic(tac):=
  iRevertIntros with (iRevert (x1 x2 x3 x4 x5 x6 x7 x8);
    tac; iIntros (x1 x2 x3 x4 x5 x6 x7 x8)).

819
(** * Destruct tactic *)
820
Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
821
822
823
824
825
826
827
828
829
830
831
832
833
834
  let intro_destruct n :=
    let rec go n' :=
      lazymatch n' with
      | 0 => fail "iDestruct: cannot introduce" n "hypotheses"
      | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
      | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
      end in intros; try iProof; go n in
  lazymatch type of lem with
  | nat => intro_destruct lem
  | Z => (* to make it work in Z_scope. We should just be able to bind
     tactic notation arguments to notation scopes. *)
     let n := eval compute in (Z.to_nat lem) in intro_destruct n
  | string => tac lem
  | iTrm =>
835
     (* only copy the hypothesis when universal quantifiers are instantiated *)
836
     lazymatch lem with
837
838
     | @iTrm string ?H _ hnil ?pat => iSpecializeCore lem as p tac
     | _ => iPoseProofCore lem as p tac
839
     end
840
  | _ => iPoseProofCore lem as p tac
841
842
  end.

843
Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
844
  iDestructCore lem as pat (fun H => iDestructHyp H as pat).
845
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
846
    constr(pat) :=
847
  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 ) pat).
848
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
849
    simple_intropattern(x2) ")" constr(pat) :=
850
  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 ) pat).
851
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
852
    simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
853
  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
854
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
855
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
856
    constr(pat) :=
857
  iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
858
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
859
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
860
    simple_intropattern(x5) ")" constr(pat) :=