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

Declare Reduction env_cbv := cbv [
7
  env_lookup env_fold env_lookup_delete env_delete env_app
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
    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 *)
14
  himpl happly
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
  env_persistent env_spatial envs_persistent
  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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
Ltac iFresh :=
  lazymatch goal with
  |- of_envs ?Δ  _ =>
25
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
     eval vm_compute in (fresh_string_of_set "~" (of_list Hs))
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
  | _ => constr:"~"
  end.

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.

(** * 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
56
    | "★" :: ?Hs => eapply tac_clear_spatial; [env_cbv; reflexivity|go Hs]
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
61
62
63
64
    | ?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) :=
65
66
67
68
  eapply tac_assumption with H _ _; (* (i:=H) *)
    [env_cbv; reflexivity || fail "iExact:" H "not found"
    |let P := match goal with |- ToAssumption _ ?P _ => P end in
     apply _ || fail "iExact:" H ":" P "does not match goal"].
Robbert Krebbers's avatar
Robbert Krebbers committed
69
70
71
72
73
74
75
76
77
78
79
80

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

Robbert Krebbers's avatar
Robbert Krebbers committed
82
Tactic Notation "iAssumption" :=
83
84
85
86
87
88
89
90
91
92
93
94
95
  let Hass := fresh in
  let rec find p Γ Q :=
    match Γ with
    | Esnoc ?Γ ?j ?P => first
       [pose proof (_ : ToAssumption p P Q) as Hass;
        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
96
97
98
99
100

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

(** * Making hypotheses persistent or pure *)
101
Local Tactic Notation "iPersistent" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
104
105
106
107
  eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
    [env_cbv; reflexivity || fail "iPersistent:" H "not found"
    |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
     apply _ || fail "iPersistent:" H ":" Q "not persistent"
    |env_cbv; reflexivity|].

108
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
113
114
  eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
    [env_cbv; reflexivity || fail "iPure:" H "not found"
    |let P := match goal with |- ToPure ?P _ => P end in
     apply _ || fail "iPure:" H ":" P "not pure"
    |intros pat].

115
116
117
118
Tactic Notation "iPureIntro" :=
  eapply tac_pure_intro;
    [let P := match goal with |- ToPure ?P _ => P end in
     apply _ || fail "iPureIntro:" P "not pure"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
119
120

(** * Specialize *)
121
122
123
124
125
126
127
128
129
130
Record iTrm {X As} :=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
Arguments ITrm {_ _} _ _ _.

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

131
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
132
133
134
135
136
137
138
139
  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"
      |apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type"
      |env_cbv; reflexivity|]
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
140

141
Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
145
146
147
  let solve_to_wand H1 :=
    let P := match goal with |- ToWand ?P _ _ => P end in
    apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
  let rec go H1 pats :=
    lazymatch pats with
    | [] => idtac
148
    | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
149
    | SName false ?H2 :: ?pats =>
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
       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"
153
154
155
         |let P := match goal with |- ToWand ?P ?Q _ => P end in
          let Q := match goal with |- ToWand ?P ?Q _ => Q end in
          apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q
Robbert Krebbers's avatar
Robbert Krebbers committed
156
         |env_cbv; reflexivity|go H1 pats]
157
158
    | SName true ?H2 :: ?pats =>
       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
         |env_cbv; reflexivity
         |iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
         |let Q1 := match goal with |- PersistentP ?Q1  _ => Q1 end in
          let Q2 := match goal with |- _  PersistentP ?Q2 => Q2 end in
          first [left; apply _ | right; apply _]
            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
         |go H1 pats]
    | SGoalPersistent :: ?pats =>
       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
         |env_cbv; reflexivity
         |(*goal*)
         |let Q1 := match goal with |- PersistentP ?Q1  _ => Q1 end in
          let Q2 := match goal with |- _  PersistentP ?Q2 => Q2 end in
          first [left; apply _ | right; apply _]
            || fail "iSpecialize:" Q1 "nor" Q2 "persistent"
         |go H1 pats]
    | SGoalPure :: ?pats =>
       eapply tac_specialize_pure with _ H1 _ _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
181
182
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
183
184
185
186
187
         |let Q := match goal with |- ToPure ?Q _ => Q end in
          apply _ || fail "iSpecialize:" Q "not pure"
         |env_cbv; reflexivity
         |(*goal*)
         |go H1 pats]
188
189
    | SGoal ?k ?lr ?Hs :: ?pats =>
       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
192
193
194
195
         |match k with
          | GoalStd => apply to_assert_fallthrough
          | GoalPvs => apply _ || fail "iSpecialize: cannot generate pvs goal"
          end
196
197
         |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
         |(*goal*)
Robbert Krebbers's avatar
Robbert Krebbers committed
198
         |go H1 pats]
199
200
201
202
203
204
    end in let pats := spec_pat.parse pat in go H pats.

Tactic Notation "iSpecialize" open_constr(t) :=
  match t with
  | ITrm ?H ?xs ?pat => iSpecializeArgs H xs; iSpecializePat H pat
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206

(** * Pose proof *)
207
Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
208
209
210
211
212
213
214
215
216
217
  lazymatch type of H1 with
  | string =>
     eapply tac_pose_proof_hyp with _ _ H1 _ H2 _;
       [env_cbv; reflexivity || fail "iPoseProof:" H1 "not found"
       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
  | _ =>
     eapply tac_pose_proof with _ H2 _ _ _; (* (j:=H) *)
       [first [eapply H1|apply uPred.equiv_iff; eapply H1]
       |apply _
       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
  end.

220
221
222
223
224
225
226
227
228
Tactic Notation "iPoseProof" open_constr(t) "as" constr(H) :=
  lazymatch t with
  | ITrm ?H1 ?xs ?pat =>
     iPoseProofCore H1 as H; last (iSpecializeArgs H xs; iSpecializePat H pat)
  | _ => iPoseProofCore t as H
  end.

Tactic Notation "iPoseProof" open_constr(t) :=
  let H := iFresh in iPoseProof t as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230

(** * Apply *)
231
Tactic Notation "iApply" open_constr(t) :=
232
233
234
235
236
237
238
  let finish H := first
    [iExact H
    |eapply tac_apply with _ H _ _ _;
       [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
       |let P := match goal with |- ToWand ?P _ _ => P end in
        apply _ || fail 1 "iApply: cannot apply" H ":" P
       |lazy beta (* reduce betas created by instantiation *)]] in
239
240
241
242
243
244
  let Htmp := iFresh in
  lazymatch t with
  | ITrm ?H ?xs ?pat =>
     iPoseProofCore H as Htmp; last (
       iSpecializeArgs Htmp xs;
       try (iSpecializeArgs Htmp (hcons _ _));
245
       iSpecializePat Htmp pat; last finish Htmp)
246
247
248
  | _ =>
     iPoseProofCore t as Htmp; last (
       try (iSpecializeArgs Htmp (hcons _ _));
249
       finish Htmp)
250
  end; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
252

(** * Revert *)
253
Local Tactic Notation "iForallRevert" ident(x) :=
254
255
256
  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
257
  | _ => revert x; apply tac_forall_revert
258
  end || fail "iRevert: cannot revert" x.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
261

Tactic Notation "iRevert" constr(Hs) :=
  let rec go H2s :=
262
263
264
265
266
267
268
269
270
    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
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
  let Hs := words 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 }.

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

(** * Disjunction *)
Tactic Notation "iLeft" :=
  eapply tac_or_l;
    [let P := match goal with |- OrSplit ?P _ _ => P end in
     apply _ || fail "iLeft:" P "not a disjunction"|].
Tactic Notation "iRight" :=
  eapply tac_or_r;
    [let P := match goal with |- OrSplit ?P _ _ => P end in
     apply _ || fail "iRight:" P "not a disjunction"|].

326
Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
  eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
    [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
    |let P := match goal with |- OrDestruct ?P _ _ => P end in
     apply _ || fail "iOrDestruct:" H ":" P "not a disjunction"
    |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
    |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].

(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
  eapply tac_and_split;
    [let P := match goal with |- AndSplit ?P _ _ => P end in
     apply _ || fail "iSplit:" P "not a conjunction"| |].

Tactic Notation "iSplitL" constr(Hs) :=
  let Hs := words Hs in
  eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
    [let P := match goal with |- SepSplit ?P _ _ => P end in
     apply _ || fail "iSplitL:" P "not a separating conjunction"
    |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs "not found"| |].
Tactic Notation "iSplitR" constr(Hs) :=
  let Hs := words Hs in
  eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
    [let P := match goal with |- SepSplit ?P _ _ => P end in
     apply _ || fail "iSplitR:" P "not a separating conjunction"
    |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs "not found"| |].

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

356
Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
  eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
    [env_cbv; reflexivity || fail "iSepDestruct:" H "not found"
    |let P := match goal with |- SepDestruct _ ?P _ _ => P end in
     apply _ || fail "iSepDestruct:" H ":" P "not separating destructable"
    |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].

Tactic Notation "iFrame" constr(Hs) :=
  let rec go Hs :=
    match Hs with
    | [] => idtac
    | ?H :: ?Hs =>
       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; go Hs]
    end
  in let Hs := words Hs in go Hs.

376
377
378
379
380
381
382
Tactic Notation "iFrame" :=
  let rec go Hs :=
    match Hs with
    | [] => idtac
    | ?H :: ?Hs => try iFrame H; go Hs
    end in
  match goal with
383
  | |- of_envs ?Δ  _ => let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
384
385
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
386
387
388
389
390
391
392
393
394
395
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"
    |let P1 := match goal with |- SepSplit _ ?P1 _ => P1 end in
     let P2 := match goal with |- SepSplit _ _ ?P2 => P2 end in
     apply _ || fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2
    |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].

(** * Existential *)
Robbert Krebbers's avatar
Robbert Krebbers committed
396
397
Tactic Notation "iExists" uconstr(x1) :=
  eapply tac_exist;
Robbert Krebbers's avatar
Robbert Krebbers committed
398
399
    [let P := match goal with |- ExistSplit ?P _ => P end in
     apply _ || fail "iExists:" P "not an existential"
Robbert Krebbers's avatar
Robbert Krebbers committed
400
    |cbv beta; eexists x1].
Robbert Krebbers's avatar
Robbert Krebbers committed
401

Robbert Krebbers's avatar
Robbert Krebbers committed
402
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
403
  iExists x1; iExists x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
405
  iExists x1; iExists x2, x3.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
407
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
408
  iExists x1; iExists x2, x3, x4.
Robbert Krebbers's avatar
Robbert Krebbers committed
409
410
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
411
  iExists x1; iExists x2, x3, x4, x5.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
413
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) "," uconstr(x6) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
414
  iExists x1; iExists x2, x3, x4, x5, x6.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
416
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
417
  iExists x1; iExists x2, x3, x4, x5, x6, x7.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
419
420
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
421
422
  iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.

423
424
Local Tactic Notation "iExistDestruct" constr(H)
    "as" simple_intropattern(x) constr(Hx) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
425
426
427
428
  eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
    [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
    |let P := match goal with |- ExistDestruct ?P _ => P end in
     apply _ || fail "iExistDestruct:" H ":" P "not an existential"|];
429
430
431
432
  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
433
434

(** * Destruct tactic *)
435
Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
436
437
438
  let rec go Hz pat :=
    lazymatch pat with
    | IAnom => idtac
439
    | IAnomPure => iPure Hz as ?
440
    | IDrop => iClear Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
441
    | IFrame => iFrame Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
442
443
    | IName ?y => iRename Hz into y
    | IPersistent ?pat => iPersistent Hz; go Hz pat
444
    | IList [[]] => iExFalso; iExact Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
445
446
447
448
449
450
451
    | IList [[?pat1; ?pat2]] =>
       let Hy := iFresh in iSepDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
    | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
    | _ => fail "iDestruct:" pat "invalid"
    end
  in let pat := intro_pat.parse_one pat in go H pat.

452
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) "}"
Robbert Krebbers's avatar
Robbert Krebbers committed
453
454
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as @ pat.
455
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
456
457
    simple_intropattern(x2) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 } pat.
458
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
459
460
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 } pat.
461
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
462
463
464
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 } pat.
465
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
466
467
468
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 } pat.
469
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
470
471
472
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 } pat.
473
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
476
477
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 } pat.
478
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
479
480
481
482
483
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
    simple_intropattern(x8) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 x8 } pat.

484
485
486
487
488
489
490
491
492
493
494
495
Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
  lazymatch type of lem with
  | string => tac lem
  | iTrm =>
     lazymatch lem with
     | @iTrm string ?H _ hnil ?pat =>
        iSpecializePat H pat; last tac H
     | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
     end
  | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
496
Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
497
  iDestructHelp H as (fun H => iDestructHyp H as pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}"
    constr(pat) :=
500
  iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
501
502
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) "}" constr(pat) :=
503
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
504
505
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
506
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
507
508
509
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
510
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
511
512
513
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) "}" constr(pat) :=
514
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
515
516
517
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
518
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
519
520
521
522
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
    constr(pat) :=
523
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
526
527
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
    simple_intropattern(x8) "}" constr(pat) :=
528
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
529
530

Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
531
  let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
534

(** * Always *)
Tactic Notation "iAlways":=
535
536
  apply tac_always_intro;
    [reflexivity || fail "iAlways: spatial context non-empty"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
537

Robbert Krebbers's avatar
Robbert Krebbers committed
538
539
540
541
542
543
544
(** * Later *)
Tactic Notation "iNext":=
  eapply tac_next;
    [apply _
    |let P := match goal with |- upred_tactics.StripLaterL ?P _ => P end in
     apply _ || fail "iNext:" P "does not contain laters"|].

Robbert Krebbers's avatar
Robbert Krebbers committed
545
(** * Introduction tactic *)
546
547
548
549
550
551
552
553
554
555
556
557
558
559
Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
  [ (* (∀ _, _) *) apply tac_forall_intro; intros x
  | (* (?P → _) *) eapply tac_impl_intro_pure;
     [let P := match goal with |- ToPure ?P _ => P end in
      apply _ || fail "iIntro:" P "not pure"
     |intros x]
  | (* (?P -★ _) *) eapply tac_wand_intro_pure;
     [let P := match goal with |- ToPure ?P _ => P end in
      apply _ || fail "iIntro:" P "not pure"
     |intros x]
  |intros x].

Local Tactic Notation "iIntro" constr(H) := first
  [ (* (?Q → _) *)
560
    eapply tac_impl_intro with _ H; (* (i:=H) *)
561
562
      [reflexivity || fail 1 "iIntro: introducing" H
                             "into non-empty spatial context"
563
      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
564
  | (* (_ -★ _) *)
565
    eapply tac_wand_intro with _ H; (* (i:=H) *)
566
567
      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | fail 1 "iIntro: nothing to introduce" ].
568

569
570
Local Tactic Notation "iIntro" "#" constr(H) := first
  [ (* (?P → _) *)
571
    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
572
573
574
575
      [let P := match goal with |- ToPersistentP ?P _ => P end in
       apply _ || fail 1 "iIntro: " P " not persistent"
      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | (* (?P -★ _) *)
576
    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
577
578
579
580
      [let P := match goal with |- ToPersistentP ?P _ => P end in
       apply _ || fail 1 "iIntro: " P " not persistent"
      |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | fail 1 "iIntro: nothing to introduce" ].
581

582
583
584
585
Local Tactic Notation "iIntroForall" :=
  lazymatch goal with
  | |-  _, ?P => fail
  | |-  _, _ => intro
586
  | |- _  ( x : _, _) => iIntro {x}
587
588
589
590
591
592
593
594
  end.
Local Tactic Notation "iIntro" :=
  lazymatch goal with
  | |- _  ?P => intro
  | |- _  (_ - _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
  | |- _  (_  _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
595
596
597
598
Tactic Notation "iIntros" constr(pat) :=
  let rec go pats :=
    lazymatch pats with
    | [] => idtac
599
600
    | IForall :: ?pats => repeat iIntroForall; go pats
    | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
601
602
    | ISimpl :: ?pats => simpl; go pats
    | IAlways :: ?pats => iAlways; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
603
    | INext :: ?pats => iNext; go pats
604
    | IClear ?Hs :: ?pats => iClear Hs; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
605
606
607
608
    | IPersistent (IName ?H) :: ?pats => iIntro #H; go pats
    | IName ?H :: ?pats => iIntro H; go pats
    | IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
    | IAnom :: ?pats => let H := iFresh in iIntro H; go pats
609
    | IAnomPure :: ?pats => iIntro {?}; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
610
611
612
613
614
615
616
    | IPersistent ?pat :: ?pats =>
       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
    | _ => fail "iIntro: failed with" pats
    end
  in let pats := intro_pat.parse pat in try iProof; go pats.
617
Tactic Notation "iIntros" := iIntros "**".
Robbert Krebbers's avatar
Robbert Krebbers committed
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674

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)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    simple_intropattern(x6) "}" :=
  iIntros { x1 x2 x3 x4 x5 }; iIntro { x6 }.
Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    simple_intropattern(x6) simple_intropattern(x7) "}" :=
  iIntros { x1 x2 x3 x4 x5 x6 }; iIntro { x7 }.
Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    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)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    "}" constr(p) :=
  iIntros { x1 x2 x3 x4 x5 }; iIntros p.
Tactic Notation "iIntros" "{"simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    simple_intropattern(x6) "}" constr(p) :=
  iIntros { x1 x2 x3 x4 x5 x6 }; iIntros p.
Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    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)
    simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
    simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8)
    "}" constr(p) :=
  iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }; iIntros p.

675
676
(* This is pretty ugly, but without Ltac support for manipulating lists of
idents I do not know how to do this better. *)
677
Local Ltac iLöbHelp IH tac_before tac_after :=
678
679
  match goal with
  | |- of_envs ?Δ  _ =>
680
     let Hs := constr:(reverse (env_dom (env_spatial Δ))) in
681
     iRevert ["★"]; tac_before;
682
683
684
     eapply tac_löb with _ IH;
       [reflexivity
       |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|];
685
    tac_after; iIntros Hs
686
687
  end.

688
Tactic Notation "iLöb" "as" constr (IH) := iLöbHelp IH idtac idtac.
689
Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (IH) :=
690
  iLöbHelp IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
691
Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (IH) :=
692
  iLöbHelp IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
693
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (IH) :=
694
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
695
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" "as"
696
    constr (IH):=
697
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
698
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
699
    ident(x5) "}" "as" constr (IH) :=
700
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 })
701
              ltac:(iIntros { x1 x2 x3 x4 x5 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
702
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
703
    ident(x5) ident(x6) "}" "as" constr (IH) :=
704
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
705
              ltac:(iIntros { x1 x2 x3 x4 x5 x6 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
706
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
707
    ident(x5) ident(x6) ident(x7) "}" "as" constr (IH) :=
708
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
709
              ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
710
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
711
    ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (IH) :=
712
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
713
              ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
714
715

(** * Assert *)
716
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
717
  let H := iFresh in
718
  let Hs := spec_pat.parse Hs in
Robbert Krebbers's avatar
Robbert Krebbers committed
719
  lazymatch Hs with
720
  | [SGoalPersistent] =>
Robbert Krebbers's avatar
Robbert Krebbers committed
721
     eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
722
723
724
725
726
727
       [env_cbv; reflexivity
       |(*goal*)
       |apply _ || fail "iAssert:" Q "not persistent"
       |iDestructHyp H as pat]
  | [SGoal ?k ?lr ?Hs] =>
     eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
728
729
730
731
       [match k with
        | GoalStd => apply to_assert_fallthrough
        | GoalPvs => apply _ || fail "iAssert: cannot generate pvs goal"
        end
732
       |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
733
734
735
736
       |env_cbv; reflexivity|
       |iDestructHyp H as pat]
  | ?pat => fail "iAssert: invalid pattern" pat
  end.
737

738
Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
739
  iAssert Q with "[]" as pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
740
741

(** * Rewrite *)
742
Local Ltac iRewriteFindPred :=
Robbert Krebbers's avatar
Robbert Krebbers committed
743
744
745
746
747
748
  match goal with
  | |- _  ?Φ ?x =>
     generalize x;
     match goal with |- ( y, @?Ψ y  _) => unify Φ Ψ; reflexivity end
  end.

749
750
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) :=
  let Heq := iFresh in iPoseProof t as Heq; last (
Robbert Krebbers's avatar
Robbert Krebbers committed
751
752
753
754
755
  eapply (tac_rewrite _ Heq _ _ lr);
    [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
    |let P := match goal with |- ?P  _ => P end in
     reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
    |iRewriteFindPred
756
    |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
757

758
759
Tactic Notation "iRewrite" open_constr(t) := iRewriteCore false t.
Tactic Notation "iRewrite" "-" open_constr(t) := iRewriteCore true t.
Robbert Krebbers's avatar
Robbert Krebbers committed
760

761
762
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) "in" constr(H) :=
  let Heq := iFresh in iPoseProof t as Heq; last (
Robbert Krebbers's avatar
Robbert Krebbers committed
763
764
765
766
767
768
769
  eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
    [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
    |env_cbv; reflexivity || fail "iRewrite:" H "not found"
    |let P := match goal with |- ?P  _ => P end in
     reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
    |iRewriteFindPred
    |intros ??? ->; reflexivity
770
    |env_cbv; reflexivity|lazy beta; iClear Heq]).
771

772
773
774
775
Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
  iRewriteCore false t in H.
Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
  iRewriteCore true t in H.
Robbert Krebbers's avatar
Robbert Krebbers committed
776
777

(* Make sure that by and done solve trivial things in proof mode *)
778
Hint Extern 0 (of_envs _  _) => by iPureIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
779
Hint Extern 0 (of_envs _  _) => iAssumption.
780
Hint Extern 0 (of_envs _  _) => progress iIntros.
781
Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796

(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ★ _)%I) => ...],
but then [eauto] mysteriously fails. See bug 4762 *)
Hint Extern 1 (of_envs _  _) =>
  match goal with
  | |- _  (_  _)%I => iSplit
  | |- _  (_  _)%I => iSplit
  | |- _  ( _)%I => iNext
  | |- _  ( _)%I => iClear "*"; iAlways
  | |- _  ( _, _)%I => iExists _
  end.
Hint Extern 1 (of_envs _  _) =>
  match goal with |- _  (_  _)%I => iLeft end.
Hint Extern 1 (of_envs _  _) =>
  match goal with |- _  (_  _)%I => iRight end.