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

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

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

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

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

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

116
117
118
119
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
120
121

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

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

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

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

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

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

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

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

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

357
Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
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
  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
387
388
Tactic Notation "iExists" uconstr(x1) :=
  eapply tac_exist;
Robbert Krebbers's avatar
Robbert Krebbers committed
389
390
    [let P := match goal with |- ExistSplit ?P _ => P end in
     apply _ || fail "iExists:" P "not an existential"
Robbert Krebbers's avatar
Robbert Krebbers committed
391
    |cbv beta; eexists x1].
Robbert Krebbers's avatar
Robbert Krebbers committed
392

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

749
750
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
751

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

763
764
765
766
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
767
768

(* Make sure that by and done solve trivial things in proof mode *)
769
Hint Extern 0 (of_envs _  _) => by iPureIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
770
Hint Extern 0 (of_envs _  _) => iAssumption.