tactics.v 34.7 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
  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" :=
336
337
338
339
340
341
342
  lazymatch goal with
  | |- _  _ =>
    eapply tac_and_split;
      [let P := match goal with |- AndSplit ?P _ _ => P end in
       apply _ || fail "iSplit:" P "not a conjunction"| |]
  | |- _  _ => apply (anti_symm ())
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359

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

360
Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
  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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
390
391
392
393
394
395
396
397
398
399
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
400
401
Tactic Notation "iExists" uconstr(x1) :=
  eapply tac_exist;
Robbert Krebbers's avatar
Robbert Krebbers committed
402
403
    [let P := match goal with |- ExistSplit ?P _ => P end in
     apply _ || fail "iExists:" P "not an existential"
Robbert Krebbers's avatar
Robbert Krebbers committed
404
    |cbv beta; eexists x1].
Robbert Krebbers's avatar
Robbert Krebbers committed
405

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

427
428
Local Tactic Notation "iExistDestruct" constr(H)
    "as" simple_intropattern(x) constr(Hx) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
429
430
431
432
  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"|];
433
434
435
436
  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
437

438
(** * Basic destruct tactic *)
439
Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
440
441
442
  let rec go Hz pat :=
    lazymatch pat with
    | IAnom => idtac
443
    | IAnomPure => iPure Hz as ?
444
    | IDrop => iClear Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
445
    | IFrame => iFrame Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
446
447
    | IName ?y => iRename Hz into y
    | IPersistent ?pat => iPersistent Hz; go Hz pat
448
    | IList [[]] => iExFalso; iExact Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
449
450
451
452
453
454
455
    | 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.

456
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) "}"
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as @ pat.
459
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
460
461
    simple_intropattern(x2) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 } pat.
462
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 } 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) "}"
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 } 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) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 } pat.
473
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
476
    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.
477
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
478
479
480
481
    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.
482
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
483
484
485
486
487
488
489
    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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
493
494
495
496
497
498
499
(** * 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
500
(** * Introduction tactic *)
501
502
503
504
505
506
507
508
509
510
511
512
513
514
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 → _) *)
515
    eapply tac_impl_intro with _ H; (* (i:=H) *)
516
517
      [reflexivity || fail 1 "iIntro: introducing" H
                             "into non-empty spatial context"
518
      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
519
  | (* (_ -★ _) *)
520
    eapply tac_wand_intro with _ H; (* (i:=H) *)
521
522
      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | fail 1 "iIntro: nothing to introduce" ].
523

524
525
Local Tactic Notation "iIntro" "#" constr(H) := first
  [ (* (?P → _) *)
526
    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
527
528
529
530
      [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 -★ _) *)
531
    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
532
533
534
535
      [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" ].
536

537
538
539
540
Local Tactic Notation "iIntroForall" :=
  lazymatch goal with
  | |-  _, ?P => fail
  | |-  _, _ => intro
541
  | |- _  ( x : _, _) => iIntro {x}
542
543
544
545
546
547
548
549
  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
550
551
552
553
Tactic Notation "iIntros" constr(pat) :=
  let rec go pats :=
    lazymatch pats with
    | [] => idtac
554
555
    | IForall :: ?pats => repeat iIntroForall; go pats
    | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
556
557
    | ISimpl :: ?pats => simpl; go pats
    | IAlways :: ?pats => iAlways; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
558
    | INext :: ?pats => iNext; go pats
559
    | IClear ?Hs :: ?pats => iClear Hs; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
560
561
562
563
    | 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
564
    | IAnomPure :: ?pats => iIntro {?}; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
565
566
567
568
569
570
571
    | 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.
572
Tactic Notation "iIntros" := iIntros "**".
Robbert Krebbers's avatar
Robbert Krebbers committed
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629

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.

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
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
(** * Destruct tactic *)
Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
  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 =>
     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.

Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
  iDestructHelp H as (fun H => iDestructHyp H as pat).
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}"
    constr(pat) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat).
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) "}" constr(pat) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat).
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) "}" constr(pat) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
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) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
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) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
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) :=
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).

Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
  let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.

691
692
(* This is pretty ugly, but without Ltac support for manipulating lists of
idents I do not know how to do this better. *)
693
Local Ltac iLöbHelp IH tac_before tac_after :=
694
695
  match goal with
  | |- of_envs ?Δ  _ =>
696
     let Hs := constr:(reverse (env_dom (env_spatial Δ))) in
697
     iRevert ["★"]; tac_before;
698
699
700
     eapply tac_löb with _ IH;
       [reflexivity
       |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|];
701
    tac_after; iIntros Hs
702
703
  end.

704
Tactic Notation "iLöb" "as" constr (IH) := iLöbHelp IH idtac idtac.
705
Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (IH) :=
706
  iLöbHelp IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
707
Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (IH) :=
708
  iLöbHelp IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
709
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (IH) :=
710
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
711
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" "as"
712
    constr (IH):=
713
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
714
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
715
    ident(x5) "}" "as" constr (IH) :=
716
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 })
717
              ltac:(iIntros { x1 x2 x3 x4 x5 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
718
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
719
    ident(x5) ident(x6) "}" "as" constr (IH) :=
720
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
721
              ltac:(iIntros { x1 x2 x3 x4 x5 x6 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
722
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
723
    ident(x5) ident(x6) ident(x7) "}" "as" constr (IH) :=
724
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
725
              ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
726
Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
727
    ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (IH) :=
728
  iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
729
              ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
Robbert Krebbers's avatar
Robbert Krebbers committed
730
731

(** * Assert *)
732
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
733
  let H := iFresh in
734
  let Hs := spec_pat.parse Hs in
Robbert Krebbers's avatar
Robbert Krebbers committed
735
  lazymatch Hs with
736
  | [SGoalPersistent] =>
Robbert Krebbers's avatar
Robbert Krebbers committed
737
     eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
738
739
740
741
742
743
       [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) *)
744
745
746
747
       [match k with
        | GoalStd => apply to_assert_fallthrough
        | GoalPvs => apply _ || fail "iAssert: cannot generate pvs goal"
        end
748
       |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
749
750
751
752
       |env_cbv; reflexivity|
       |iDestructHyp H as pat]
  | ?pat => fail "iAssert: invalid pattern" pat
  end.
753

754
Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
755
  iAssert Q with "[]" as pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
756
757

(** * Rewrite *)
758
Local Ltac iRewriteFindPred :=
Robbert Krebbers's avatar
Robbert Krebbers committed
759
760
761
762
763
764
  match goal with
  | |- _  ?Φ ?x =>
     generalize x;
     match goal with |- ( y, @?Ψ y  _) => unify Φ Ψ; reflexivity end
  end.

765
766
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
767
768
769
770
771
  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
772
    |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
773

774
775
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
776

777
778
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
779
780
781
782
783
784
785
  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
786
    |env_cbv; reflexivity|lazy beta; iClear Heq]).
787

788
789
790
791
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
792
793

(* Make sure that by and done solve trivial things in proof mode *)
794
Hint Extern 0 (of_envs _  _) => by iPureIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
795
Hint Extern 0 (of_envs _  _) => iAssumption.
796
Hint Extern 0 (of_envs _  _) => progress iIntros.
797
Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812

(* 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.