tactics.v 33.9 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
25
26
Ltac iFresh :=
  lazymatch goal with
  |- of_envs ?Δ  _ =>
      match goal with
      | _ => eval vm_compute in (fresh_string_of_set "~" (dom stringset Δ))
27
28
29
30
      | _ =>
         (* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
         let Hs := eval cbv in (dom stringset Δ) in
         eval vm_compute in (fresh_string_of_set "~" Hs)
Robbert Krebbers's avatar
Robbert Krebbers committed
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
56
57
58
      end
  | _ => 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
59
    | "★" :: ?Hs => eapply tac_clear_spatial; [env_cbv; reflexivity|go Hs]
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
62
63
64
65
66
67
    | ?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) :=
68
69
70
71
  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
72
73
74
75
76
77
78
79
80
81
82
83

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

Robbert Krebbers's avatar
Robbert Krebbers committed
85
Tactic Notation "iAssumption" :=
86
87
88
89
90
91
92
93
94
95
96
97
98
  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
99
100
101
102
103

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

(** * Making hypotheses persistent or pure *)
104
Local Tactic Notation "iPersistent" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
108
109
110
  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|].

111
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
114
115
116
117
  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].

118
119
120
121
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
122
123

(** * Specialize *)
124
125
126
127
128
129
130
131
132
133
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).

134
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
135
136
137
138
139
140
141
142
  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
143

144
Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
147
148
149
150
  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
151
    | SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
152
    | SName false ?H2 :: ?pats =>
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
       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"
156
157
158
         |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
159
         |env_cbv; reflexivity|go H1 pats]
160
161
    | SName true ?H2 :: ?pats =>
       eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
         |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
184
185
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
186
187
188
189
190
         |let Q := match goal with |- ToPure ?Q _ => Q end in
          apply _ || fail "iSpecialize:" Q "not pure"
         |env_cbv; reflexivity
         |(*goal*)
         |go H1 pats]
191
192
    | SGoal ?k ?lr ?Hs :: ?pats =>
       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _ _;
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
         [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
         |solve_to_wand H1
195
196
197
198
         |match k with
          | GoalStd => apply to_assert_fallthrough
          | GoalPvs => apply _ || fail "iSpecialize: cannot generate pvs goal"
          end
199
200
         |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
         |(*goal*)
Robbert Krebbers's avatar
Robbert Krebbers committed
201
         |go H1 pats]
202
203
204
205
206
207
    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
208
209

(** * Pose proof *)
210
Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
211
212
213
214
215
216
217
218
219
220
  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
221
222
  end.

223
224
225
226
227
228
229
230
231
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
232
233

(** * Apply *)
234
Tactic Notation "iApply" open_constr(t) :=
235
236
237
238
239
240
241
  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
242
243
244
245
246
247
  let Htmp := iFresh in
  lazymatch t with
  | ITrm ?H ?xs ?pat =>
     iPoseProofCore H as Htmp; last (
       iSpecializeArgs Htmp xs;
       try (iSpecializeArgs Htmp (hcons _ _));
248
       iSpecializePat Htmp pat; last finish Htmp)
249
250
251
  | _ =>
     iPoseProofCore t as Htmp; last (
       try (iSpecializeArgs Htmp (hcons _ _));
252
       finish Htmp)
253
  end; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255

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

Tactic Notation "iRevert" constr(Hs) :=
  let rec go H2s :=
265
266
267
268
269
270
271
272
273
    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
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
326
327
328
  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"|].

329
Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
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
356
357
358
  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 "".

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
395
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
396
  iExists x1; iExists x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
398
  iExists x1; iExists x2, x3.
Robbert Krebbers's avatar
Robbert Krebbers committed
399
400
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
401
  iExists x1; iExists x2, x3, x4.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
403
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
404
  iExists x1; iExists x2, x3, x4, x5.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
406
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) "," uconstr(x6) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
407
  iExists x1; iExists x2, x3, x4, x5, x6.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
409
Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
    uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
410
  iExists x1; iExists x2, x3, x4, x5, x6, x7.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
412
413
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
414
415
  iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.

416
417
Local Tactic Notation "iExistDestruct" constr(H)
    "as" simple_intropattern(x) constr(Hx) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
418
419
420
421
  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"|];
422
423
424
425
  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
426
427

(** * Destruct tactic *)
428
Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
429
430
431
  let rec go Hz pat :=
    lazymatch pat with
    | IAnom => idtac
432
    | IAnomPure => iPure Hz as ?
433
    | IDrop => iClear Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
434
    | IFrame => iFrame Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
435
436
    | IName ?y => iRename Hz into y
    | IPersistent ?pat => iPersistent Hz; go Hz pat
437
    | IList [[]] => iExFalso; iExact Hz
Robbert Krebbers's avatar
Robbert Krebbers committed
438
439
440
441
442
443
444
    | 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.

445
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) "}"
Robbert Krebbers's avatar
Robbert Krebbers committed
446
447
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as @ pat.
448
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
449
450
    simple_intropattern(x2) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 } pat.
451
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
452
453
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 } pat.
454
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
455
456
457
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
  iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 } pat.
458
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
459
460
461
    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.
462
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
    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.
466
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
469
470
    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.
471
Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
Robbert Krebbers's avatar
Robbert Krebbers committed
472
473
474
475
476
    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.

477
478
479
480
481
482
483
484
485
486
487
488
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
489
Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
490
  iDestructHelp H as (fun H => iDestructHyp H as pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
491
492
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}"
    constr(pat) :=
493
  iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
494
495
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) "}" constr(pat) :=
496
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
497
498
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
499
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
500
501
502
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
    constr(pat) :=
503
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
504
505
506
Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
    simple_intropattern(x5) "}" constr(pat) :=
507
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
508
509
510
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) :=
511
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
512
513
514
515
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) :=
516
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
517
518
519
520
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) :=
521
  iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523

Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
524
  let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
526
527

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

Robbert Krebbers's avatar
Robbert Krebbers committed
531
532
533
534
535
536
537
(** * 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
538
(** * Introduction tactic *)
539
540
541
542
543
544
545
546
547
548
549
550
551
552
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 → _) *)
553
    eapply tac_impl_intro with _ H; (* (i:=H) *)
554
555
      [reflexivity || fail 1 "iIntro: introducing" H
                             "into non-empty spatial context"
556
      |env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
557
  | (* (_ -★ _) *)
558
    eapply tac_wand_intro with _ H; (* (i:=H) *)
559
560
      [env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
  | fail 1 "iIntro: nothing to introduce" ].
561

562
563
Local Tactic Notation "iIntro" "#" constr(H) := first
  [ (* (?P → _) *)
564
    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
565
566
567
568
      [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 -★ _) *)
569
    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
570
571
572
573
      [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" ].
574

575
576
577
578
Local Tactic Notation "iIntroForall" :=
  lazymatch goal with
  | |-  _, ?P => fail
  | |-  _, _ => intro
579
  | |- _  ( x : _, _) => iIntro {x}
580
581
582
583
584
585
586
587
  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
588
589
590
591
Tactic Notation "iIntros" constr(pat) :=
  let rec go pats :=
    lazymatch pats with
    | [] => idtac
592
593
    | IForall :: ?pats => repeat iIntroForall; go pats
    | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
594
595
    | ISimpl :: ?pats => simpl; go pats
    | IAlways :: ?pats => iAlways; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
596
    | INext :: ?pats => iNext; go pats
597
    | IClear ?Hs :: ?pats => iClear Hs; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
598
599
600
601
    | 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
602
    | IAnomPure :: ?pats => iIntro {?}; go pats
Robbert Krebbers's avatar
Robbert Krebbers committed
603
604
605
606
607
608
609
    | 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.
610
Tactic Notation "iIntros" := iIntros "**".
Robbert Krebbers's avatar
Robbert Krebbers committed
611
612
613
614
615
616
617
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

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.

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

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

(** * Assert *)
709
Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
710
  let H := iFresh in
711
  let Hs := spec_pat.parse Hs in
Robbert Krebbers's avatar
Robbert Krebbers committed
712
  lazymatch Hs with
713
  | [SGoalPersistent] =>
Robbert Krebbers's avatar
Robbert Krebbers committed
714
     eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
715
716
717
718
719
720
       [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) *)
721
722
723
724
       [match k with
        | GoalStd => apply to_assert_fallthrough
        | GoalPvs => apply _ || fail "iAssert: cannot generate pvs goal"
        end
725
       |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
726
727
728
729
       |env_cbv; reflexivity|
       |iDestructHyp H as pat]
  | ?pat => fail "iAssert: invalid pattern" pat
  end.
730

Robbert Krebbers's avatar
Robbert Krebbers committed
731
Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
732
  iAssert Q with "[]" as pat.
Robbert Krebbers's avatar
Robbert Krebbers committed
733
734

(** * Rewrite *)
735
Local Ltac iRewriteFindPred :=
Robbert Krebbers's avatar
Robbert Krebbers committed
736
737
738
739
740
741
  match goal with
  | |- _  ?Φ ?x =>
     generalize x;
     match goal with |- ( y, @?Ψ y  _) => unify Φ Ψ; reflexivity end
  end.

742
743
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
744
745
746
747
748
  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
749
    |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
750

751
752
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
753

754
755
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
756
757
758
759
760
761
762
  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
763
    |env_cbv; reflexivity|lazy beta; iClear Heq]).
764

765
766
767
768
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
769
770

(* Make sure that by and done solve trivial things in proof mode *)
771
Hint Extern 0 (of_envs _  _) => by iPureIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
772
Hint Extern 0 (of_envs _  _) => iAssumption.
773
Hint Extern 0 (of_envs _  _) => progress iIntros.
774
Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789

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