tactics.v 82.8 KB
Newer Older
1
From iris.proofmode Require Import coq_tactics.
2
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
3
From iris.bi Require Export bi big_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris.proofmode Require Export classes notation.
5
From iris.proofmode Require Import class_instances.
6
From stdpp Require Import hlist pretty.
7
Set Default Proof Using "Type".
8
Export ident.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10

Declare Reduction env_cbv := cbv [
11
  option_bind
12
  beq ascii_beq string_beq positive_beq ident_beq
13
14
  env_lookup env_lookup_delete env_delete env_app env_replace env_dom
  env_persistent env_spatial env_spatial_is_nil envs_dom
15
  envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
16
17
    envs_simple_replace envs_replace envs_split
    envs_clear_spatial envs_clear_persistent
18
    envs_split_go envs_split].
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
Ltac env_cbv :=
  match goal with |- ?u => let v := eval env_cbv in u in change v end.
21
Ltac env_reflexivity := env_cbv; exact eq_refl.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

23
(** * Misc *)
24
(* Tactic Notation tactics cannot return terms *)
25
Ltac iFresh :=
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  lazymatch goal with
27
  |- envs_entails ?Δ _ =>
28
29
30
     (* [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
31
32
33
34
35
36
     eval vm_compute in
       (IAnon (match Hs with
         | [] => 1
         | _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
         end))%positive
  | _ => constr:(IAnon 1)
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
  end.

39
40
41
Ltac iMissingHyps Hs :=
  let Δ :=
    lazymatch goal with
42
    | |- envs_entails ?Δ _ => Δ
43
44
45
46
47
    | |- context[ envs_split _ _ ?Δ ] => Δ
    end in
  let Hhyps := eval env_cbv in (envs_dom Δ) in
  eval vm_compute in (list_difference Hs Hhyps).

48
Ltac iTypeOf H :=
49
  let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
50
  eval env_cbv in (envs_lookup H Δ).
Robbert Krebbers's avatar
Robbert Krebbers committed
51

52
Tactic Notation "iMatchHyp" tactic1(tac) :=
53
54
55
56
  match goal with
  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
57
(** * Start a proof *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
Tactic Notation "iStartProof" :=
  lazymatch goal with
  | |- envs_entails _ _ => idtac

  (* In the case the goal starts with a let, we want [iIntros (x)] to
     not unfold the variable, but instead introduce it as with Coq's
     intros.*)
  | |- let _ := _ in _ => fail

  | |- ?φ => eapply (as_valid_2 φ);
               [apply _ || fail "iStartProof: not a Bi entailment"
               |apply tac_adequate]
  end.

(* Same as above, with 2 differences :
   - We can specify a BI in which we want the proof to be done
   - If the goal starts with a let or a ∀, they are automatically
     introduced. *)
76
Tactic Notation "iStartProof" uconstr(PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  lazymatch goal with
78
  | |- @envs_entails ?PROP' _ _ =>
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
79
80
    (* This cannot be shared with the other [iStartProof], because
    type_term has a non-negligeable performance impact. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
81
    let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
82
83
84

  | |- let _ := _ in _ => intro
  | |-  _, _ => intro
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
85
86

  (* We eta-expand [as_valid_2], in order to make sure that
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
87
88
     [iStartProof PROP] works even if [PROP] is the carrier type. In
     this case, typing this expression will end up unifying PROP with
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
89
90
     [bi_car _], and hence trigger the canonical structures mechanism
     to find the corresponding bi. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
91
  | |- ?φ => eapply (λ P : PROP, @as_valid_2 φ _ P);
92
               [apply _ || fail "iStartProof: not a Bi entailment"
93
               |apply tac_adequate]
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
  end.

96

97
98
99
100
101
102
103
(** * Simplification *)
Tactic Notation "iEval" tactic(t) :=
  try iStartProof;
  try (eapply tac_eval; [t; reflexivity|]).

Tactic Notation "iSimpl" := iEval simpl.

Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
  eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
107
108
    [env_reflexivity || fail "iRename:" H1 "not found"
    |env_reflexivity || fail "iRename:" H2 "not fresh"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
109

110
111
Local Inductive esel_pat :=
  | ESelPure
112
  | ESelIdent : bool  ident  esel_pat.
113

114
Ltac iElaborateSelPat pat :=
115
116
  let rec go pat Δ Hs :=
    lazymatch pat with
117
    | [] => eval cbv in Hs
118
119
120
121
    | SelPure :: ?pat => go pat Δ (ESelPure :: Hs)
    | SelPersistent :: ?pat =>
       let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
       let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
122
       go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
123
124
125
    | SelSpatial :: ?pat =>
       let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
       let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
126
127
       go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
    | SelIdent ?H :: ?pat =>
128
       lazymatch eval env_cbv in (envs_lookup_delete H Δ) with
129
       | Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
130
131
132
133
       | None => fail "iElaborateSelPat:" H "not found"
       end
    end in
  lazymatch goal with
134
  | |- envs_entails ?Δ _ =>
135
136
137
    let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
  end.

138
139
Local Ltac iClearHyp H :=
  eapply tac_clear with _ H _ _; (* (i:=H) *)
140
141
142
143
144
    [env_reflexivity || fail "iClear:" H "not found"
    |env_cbv; apply _ ||
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iClear:" H ":" P "not affine and the goal not absorbing"
    |].
145

Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
Tactic Notation "iClear" constr(Hs) :=
  let rec go Hs :=
148
    lazymatch Hs with
Robbert Krebbers's avatar
Robbert Krebbers committed
149
    | [] => idtac
150
    | ESelPure :: ?Hs => clear; go Hs
151
    | ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
Robbert Krebbers's avatar
Robbert Krebbers committed
152
    end in
153
  let Hs := iElaborateSelPat Hs in go Hs.
154

155
156
Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
  iClear Hs; clear xs.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
159

(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  eapply tac_assumption with _ H _ _; (* (i:=H) *)
161
    [env_reflexivity || fail "iExact:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
    |apply _ ||
     let P := match goal with |- FromAssumption _ ?P _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
166
     fail "iExact:" H ":" P "does not match goal"
    |env_cbv; apply _ ||
     fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
169

Tactic Notation "iAssumptionCore" :=
  let rec find Γ i P :=
170
    lazymatch Γ with
Robbert Krebbers's avatar
Robbert Krebbers committed
171
    | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j|find Γ i P]
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
    end in
  match goal with
  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
175
     first [is_evar i; fail 1 | env_reflexivity]
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
177
     is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
178
  | |- envs_lookup_delete ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
179
     first [is_evar i; fail 1 | env_reflexivity]
180
  | |- envs_lookup_delete ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
181
     is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  end.
183

Robbert Krebbers's avatar
Robbert Krebbers committed
184
Tactic Notation "iAssumption" :=
185
186
  let Hass := fresh in
  let rec find p Γ Q :=
187
    lazymatch Γ with
188
    | Esnoc ?Γ ?j ?P => first
189
       [pose proof (_ : FromAssumption p P Q) as Hass;
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
192
193
194
195
196
197
198
        eapply (tac_assumption _ _ j p P);
          [env_reflexivity
          |apply Hass
          |env_cbv; apply _ ||
           fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
       |assert (P = False%I) as Hass by reflexivity;
        apply (tac_false_destruct _ j p P);
          [env_reflexivity
          |exact Hass]
199
200
       |find p Γ Q]
    end in
201
  lazymatch goal with
202
  | |- envs_entails (Envs ?Γp ?Γs) ?Q =>
203
204
205
     first [find true Γp Q | find false Γs Q
           |fail "iAssumption:" Q "not found"]
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
208
209
210

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

(** * Making hypotheses persistent or pure *)
211
Local Tactic Notation "iPersistent" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
212
  eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
213
    [env_reflexivity || fail "iPersistent:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
214
    |apply _ ||
Robbert Krebbers's avatar
Robbert Krebbers committed
215
216
217
     let P := match goal with |- IntoPersistent _ ?P _ => P end in
     fail "iPersistent:" P "not persistent"
    |env_cbv; apply _ ||
218
219
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iPersistent:" P "not affine and the goal not absorbing"
220
    |env_reflexivity|].
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
223
  eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
224
    [env_reflexivity || fail "iPure:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
225
226
227
    |apply _ ||
     let P := match goal with |- IntoPure ?P _ => P end in
     fail "iPure:" P "not pure"
Robbert Krebbers's avatar
Robbert Krebbers committed
228
    |env_cbv; apply _ ||
229
230
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iPure:" P "not affine and the goal not absorbing"
Robbert Krebbers's avatar
Robbert Krebbers committed
231
232
    |intros pat].

Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
235
Tactic Notation "iEmpIntro" :=
  iStartProof;
  eapply tac_emp_intro;
236
237
    [env_cbv; apply _ ||
     fail "iEmpIntro: spatial context contains non-affine hypotheses"].
Robbert Krebbers's avatar
Robbert Krebbers committed
238

239
Tactic Notation "iPureIntro" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
240
  iStartProof;
241
  eapply tac_pure_intro;
Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
244
245
    [apply _ ||
     let P := match goal with |- FromPure ?P _ => P end in
     fail "iPureIntro:" P "not pure"
    |].
Robbert Krebbers's avatar
Robbert Krebbers committed
246

247
248
249
250
(** Framing *)
Local Ltac iFrameFinish :=
  lazy iota beta;
  try match goal with
251
252
  | |- envs_entails _ True => exact (bi.pure_intro _ _ I)
  | |- envs_entails _ emp => iEmpIntro
253
254
255
256
257
258
259
260
261
262
  end.

Local Ltac iFramePure t :=
  let φ := type of t in
  eapply (tac_frame_pure _ _ _ _ t);
    [apply _ || fail "iFrame: cannot frame" φ
    |iFrameFinish].

Local Ltac iFrameHyp H :=
  eapply tac_frame with _ H _ _ _;
263
    [env_reflexivity || fail "iFrame:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
264
265
266
    |apply _ ||
     let R := match goal with |- Frame _ ?R _ _ => R end in
     fail "iFrame: cannot frame" R
267
268
269
270
271
272
273
274
275
    |iFrameFinish].

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

Local Ltac iFrameAnyPersistent :=
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
  match goal with
276
  | |- envs_entails ?Δ _ =>
277
278
279
280
281
282
283
     let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
  end.

Local Ltac iFrameAnySpatial :=
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
  match goal with
284
  | |- envs_entails ?Δ _ =>
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
     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
  end.

Tactic Notation "iFrame" := iFrameAnySpatial.

Tactic Notation "iFrame" "(" constr(t1) ")" :=
  iFramePure t1.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" :=
  iFramePure t1; iFrame ( t2 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" :=
  iFramePure t1; iFrame ( t2 t3 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) ")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ).
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) constr(t8)")" :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ).

Tactic Notation "iFrame" constr(Hs) :=
  let rec go Hs :=
313
    lazymatch Hs with
314
    | [] => idtac
315
316
317
    | SelPure :: ?Hs => iFrameAnyPure; go Hs
    | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
    | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
318
    | SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
319
    end
320
  in let Hs := sel_pat.parse Hs in go Hs.
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
  iFramePure t1; iFrame Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4) ")"
    constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) ")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 ) Hs.
Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
    constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
  iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.

343
344
345
(** * Basic introduction tactics *)
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
  try iStartProof;
346
  lazymatch goal with
347
  | |- envs_entails _ _ =>
348
    eapply tac_forall_intro;
Robbert Krebbers's avatar
Robbert Krebbers committed
349
      [apply _ ||
350
351
352
353
354
       let P := match goal with |- FromForall ?P _ => P end in
       fail "iIntro: cannot turn" P "into a universal quantifier"
      |lazy beta; intros x]
  | |- _ => intros x
  end.
355
356
357
358
359

Local Tactic Notation "iIntro" constr(H) :=
  iStartProof;
  first
  [ (* (?Q → _) *)
360
    eapply tac_impl_intro with _ H _; (* (i:=H) *)
Robbert Krebbers's avatar
Robbert Krebbers committed
361
      [env_cbv; apply _ ||
362
       let P := lazymatch goal with |- Persistent ?P => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
363
364
       fail 1 "iIntro: introducing non-persistent" H ":" P
              "into non-empty spatial context"
Robbert Krebbers's avatar
Robbert Krebbers committed
365
      |env_reflexivity || fail 1 "iIntro:" H "not fresh"
366
      |apply _
Robbert Krebbers's avatar
Robbert Krebbers committed
367
      |]
368
369
  | (* (_ -∗ _) *)
    eapply tac_wand_intro with _ H; (* (i:=H) *)
Robbert Krebbers's avatar
Robbert Krebbers committed
370
371
      [env_reflexivity || fail 1 "iIntro:" H "not fresh"
      |]
372
  | fail "iIntro: nothing to introduce" ].
373
374
375
376
377
378

Local Tactic Notation "iIntro" "#" constr(H) :=
  iStartProof;
  first
  [ (* (?P → _) *)
    eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
Robbert Krebbers's avatar
Robbert Krebbers committed
379
      [apply _ ||
380
       let P := match goal with |- IntoPersistent _ ?P _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
381
       fail 1 "iIntro:" P "not persistent"
Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
      |env_reflexivity || fail 1 "iIntro:" H "not fresh"
      |]
384
385
  | (* (?P -∗ _) *)
    eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
Robbert Krebbers's avatar
Robbert Krebbers committed
386
      [apply _ ||
387
       let P := match goal with |- IntoPersistent _ ?P _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
388
389
       fail 1 "iIntro:" P "not persistent"
      |apply _ ||
390
391
       let P := match goal with |- TCOr (Affine ?P) _ => P end in
       fail 1 "iIntro:" P "not affine and the goal not absorbing"
Robbert Krebbers's avatar
Robbert Krebbers committed
392
393
      |env_reflexivity || fail 1 "iIntro:" H "not fresh"
      |]
394
  | fail "iIntro: nothing to introduce" ].
395
396
397
398
399

Local Tactic Notation "iIntro" "_" :=
  try iStartProof;
  first
  [ (* (?Q → _) *) apply tac_impl_intro_drop
Robbert Krebbers's avatar
Robbert Krebbers committed
400
401
402
403
404
405
  | (* (_ -∗ _) *)
    apply tac_wand_intro_drop;
      [apply _ ||
       let P := match goal with |- TCOr (Affine ?P) _ => P end in
       fail 1 "iIntro:" P "not affine and the goal not absorbing"
      |]
406
407
408
409
410
411
  | (* (∀ _, _) *) iIntro (_)
  | fail 1 "iIntro: nothing to introduce" ].

Local Tactic Notation "iIntroForall" :=
  try iStartProof;
  lazymatch goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
412
  | |-  _, ?P => fail (* actually an →, this is handled by iIntro below *)
413
  | |-  _, _ => intro
414
  | |- envs_entails _ ( x : _, _) => let x' := fresh x in iIntro (x')
415
416
417
418
419
  end.
Local Tactic Notation "iIntro" :=
  try iStartProof;
  lazymatch goal with
  | |- _  ?P => intro
420
421
  | |- envs_entails _ (_ - _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
  | |- envs_entails _ (_  _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
422
423
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
424
(** * Specialize *)
425
426
427
428
429
Record iTrm {X As} :=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
Arguments ITrm {_ _} _ _ _.

Notation "( H $! x1 .. xn )" :=
430
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
431
Notation "( H $! x1 .. xn 'with' pat )" :=
432
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
433
434
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).

435
(*
Robbert Krebbers's avatar
Robbert Krebbers committed
436
437
438
439
440
There is some hacky stuff going on here: because of Coq bug #6583, unresolved
type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
these holes. To avoid TC being triggered too eagerly, this tactic uses `refine`
at most places instead of `apply`.
441
*)
442
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
443
  let rec go xs :=
444
    lazymatch xs with
445
    | hnil => apply id (* Finally, trigger TC *)
446
    | hcons ?x ?xs =>
447
       eapply tac_forall_specialize with _ H _ _ _; (* (i:=H) (a:=x) *)
448
449
         [env_reflexivity || fail "iSpecialize:" H "not found"
         |typeclasses eauto ||
Robbert Krebbers's avatar
Robbert Krebbers committed
450
          let P := match goal with |- IntoForall ?P _ => P end in
451
          fail "iSpecialize: cannot instantiate" P "with" x
Robbert Krebbers's avatar
Robbert Krebbers committed
452
453
454
         |match goal with (* Force [A] in [ex_intro] to deal with coercions. *)
          | |-  _ : ?A, _ => refine (@ex_intro A _ x (conj _ _)); [|]
          (* If the existentially quantified predicate is non-dependent and [x]
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
455
          is a hole, [refine] will generate an additional goal. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
456
          | |-  _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |]
457
          end; [env_reflexivity|go xs]]
458
459
    end in
  go xs.
Robbert Krebbers's avatar
Robbert Krebbers committed
460

461
Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
462
  let solve_to_wand H1 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
463
    apply _ ||
Robbert Krebbers's avatar
Robbert Krebbers committed
464
    let P := match goal with |- IntoWand _ _ ?P _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
465
    fail "iSpecialize:" P "not an implication/wand" in
Robbert Krebbers's avatar
Robbert Krebbers committed
466
467
468
  let rec go H1 pats :=
    lazymatch pats with
    | [] => idtac
469
    | SForall :: ?pats =>
Ralf Jung's avatar
Ralf Jung committed
470
       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
471
       go H1 pats
472
    | SIdent ?H2 :: ?pats =>
Robbert Krebbers's avatar
Robbert Krebbers committed
473
       eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
474
475
         [env_reflexivity || fail "iSpecialize:" H2 "not found"
         |env_reflexivity || fail "iSpecialize:" H1 "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
476
         |apply _ ||
Robbert Krebbers's avatar
Robbert Krebbers committed
477
478
          let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
          let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
479
          fail "iSpecialize: cannot instantiate" P "with" Q
480
         |env_reflexivity|go H1 pats]
481
482
    | SPureGoal ?d :: ?pats =>
       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
483
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
484
         |solve_to_wand H1
Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
487
         |apply _ ||
          let Q := match goal with |- FromPure ?Q _ => Q end in
          fail "iSpecialize:" Q "not pure"
488
         |env_reflexivity
489
         |done_if d (*goal*)
490
         |go H1 pats]
491
    | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
492
       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _ _;
493
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
494
         |solve_to_wand H1
Robbert Krebbers's avatar
Robbert Krebbers committed
495
         |apply _ ||
496
          let Q := match goal with |- Persistent ?Q => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
497
          fail "iSpecialize:" Q "not persistent"
498
         |apply _
499
         |env_reflexivity
500
         |iFrame Hs_frame; done_if d (*goal*)
501
         |go H1 pats]
502
503
504
    | SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
       fail "iSpecialize: cannot select hypotheses for persistent premise"
    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
505
       let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
506
       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
507
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
508
         |solve_to_wand H1
509
         |lazymatch m with
510
          | GSpatial => apply add_modal_id
511
          | GModal => apply _ || fail "iSpecialize: goal not a modality"
512
          end
513
514
         |env_reflexivity ||
          let Hs' := iMissingHyps Hs' in
515
          fail "iSpecialize: hypotheses" Hs' "not found"
516
         |iFrame Hs_frame; done_if d (*goal*)
Robbert Krebbers's avatar
Robbert Krebbers committed
517
         |go H1 pats]
518
519
    | SAutoFrame GPersistent :: ?pats =>
       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
520
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
521
         |solve_to_wand H1
Robbert Krebbers's avatar
Robbert Krebbers committed
522
         |apply _ ||
523
          let Q := match goal with |- Persistent ?Q => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
524
          fail "iSpecialize:" Q "not persistent"
525
         |env_reflexivity
526
527
528
529
         |solve [iFrame "∗ #"]
         |go H1 pats]
    | SAutoFrame ?m :: ?pats =>
       eapply tac_specialize_frame with _ H1 _ _ _ _ _ _;
530
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
531
532
         |solve_to_wand H1
         |lazymatch m with
533
          | GSpatial => apply add_modal_id
534
535
          | GModal => apply _ || fail "iSpecialize: goal not a modality"
          end
Robbert Krebbers's avatar
Robbert Krebbers committed
536
537
         |iFrame "∗ #"; apply tac_unlock ||
          fail "iSpecialize: premise cannot be solved by framing"
538
         |reflexivity]; iIntro H1; go H1 pats
539
540
    end in let pats := spec_pat.parse pat in go H pats.

Robbert Krebbers's avatar
Robbert Krebbers committed
541
(* The argument [p] denotes whether the conclusion of the specialized term is
542
543
544
persistent. If so, one can use all spatial hypotheses for both proving the
premises and the remaning goal. The argument [p] can either be a Boolean or an
introduction pattern, which will be coerced into [true] when it solely contains
545
546
547
548
549
`#` or `%` patterns at the top-level.

In case the specialization pattern in [t] states that the modality of the goal
should be kept for one of the premises (i.e. [>[H1 .. Hn]] is used) then [p]
defaults to [false] (i.e. spatial hypotheses are not preserved). *)
550
Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
551
  let p := intro_pat_persistent p in
552
  let t :=
553
554
555
556
557
    match type of t with
    | string => constr:(ITrm (INamed t) hnil "")
    | ident => constr:(ITrm t hnil "")
    | _ => t
    end in
558
559
  lazymatch t with
  | ITrm ?H ?xs ?pat =>
560
    let pat := spec_pat.parse pat in
561
    let H := lazymatch type of H with string => constr:(INamed H) | _ => H end in
Robbert Krebbers's avatar
Robbert Krebbers committed
562
    iSpecializeArgs H xs;
563
    lazymatch type of H with
564
    | ident =>
565
566
567
568
569
570
      (* The lemma [tac_specialize_persistent_helper] allows one to use all
      spatial hypotheses for both proving the premises of the lemma we
      specialize as well as those of the remaining goal. We can only use it when
      the result of the specialization is persistent, and no modality is
      eliminated. As an optimization, we do not use this when only universal
      quantifiers are instantiated. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
571
      let pat := spec_pat.parse pat in
572
      lazymatch eval compute in
573
        (p && bool_decide (pat  []) && negb (existsb spec_pat_modal pat)) with
574
      | true =>
575
         (* FIXME: do something reasonable when the BI is not affine *)
Robbert Krebbers's avatar
Robbert Krebbers committed
576
         eapply tac_specialize_persistent_helper with _ H _ _ _ _;
577
           [env_reflexivity || fail "iSpecialize:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
578
           |iSpecializePat H pat; last (iExact H)
Robbert Krebbers's avatar
Robbert Krebbers committed
579
           |apply _ ||
Robbert Krebbers's avatar
Robbert Krebbers committed
580
            let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
581
            fail "iSpecialize:" Q "not persistent"
Robbert Krebbers's avatar
Robbert Krebbers committed
582
           |env_cbv; apply _ ||
583
            let Q := match goal with |- TCAnd _ (Affine ?Q) => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
584
585
586
587
            fail "iSpecialize:" Q "not affine"
           |env_reflexivity
           |(* goal *)]
      | false => iSpecializePat H pat
588
589
      end
    | _ => fail "iSpecialize:" H "should be a hypothesis, use iPoseProof instead"
590
    end
591
  | _ => fail "iSpecialize:" t "should be a proof mode term"
592
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
593

594
Tactic Notation "iSpecialize" open_constr(t) :=
595
596
597
  iSpecializeCore t as false.
Tactic Notation "iSpecialize" open_constr(t) "as" "#" :=
  iSpecializeCore t as true.
598

Robbert Krebbers's avatar
Robbert Krebbers committed
599
(** * Pose proof *)
600
601
(* The tactic [iIntoValid] tactic solves a goal [uPred_valid Q]. The
arguments [t] is a Coq term whose type is of the following shape:
602

603
- [∀ (x_1 : A_1) .. (x_n : A_n), uPred_valid Q]
604
- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -∗ P2]
605
606
607
608
- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊣⊢ P2], in which case [Q] becomes [P1 ↔ P2]

The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [P] for non-dependent arguments [x_i : P]. *)
609
Tactic Notation "iIntoValid" open_constr(t) :=
610
  let rec go t :=
611
    let tT := type of t in
612
613
614
615
    lazymatch eval hnf in tT with
    | ?P  ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
    |  _ : ?T, _ =>
      (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
616
      (* This is a workarround for Coq bug #6583. *)
617
618
619
      let e := fresh in evar (e:id T);
      let e' := eval unfold e in e in clear e; go (t e')
    | _ =>
620
      let tT' := eval cbv zeta in tT in apply (as_valid_1 tT');
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
621
        [apply _ || fail "iPoseProof: not a BI assertion"|exact t]
622
    end in
623
  go t.
624

625
626
(* The tactic [tac] is called with a temporary fresh name [H]. The argument
[lazy_tc] denotes whether type class inference on the premises of [lem] should
627
628
629
630
631
632
be performed before (if false) or after (if true) [tac H] is called.

The tactic [iApply] uses laxy type class inference, so that evars can first be
instantiated by matching with the goal, whereas [iDestruct] does not, because
eliminations may not be performed when type classes have not been resolved.
*)
633
634
635
636
Tactic Notation "iPoseProofCore" open_constr(lem)
    "as" constr(p) constr(lazy_tc) tactic(tac) :=
  try iStartProof;
  let Htmp := iFresh in
637
638
  let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
  let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
639
640
641
642
643
644
  let spec_tac _ :=
    lazymatch lem with
    | ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
    | _ => idtac
    end in
  let go goal_tac :=
645
    lazymatch type of t with
646
    | ident =>
647
       eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
648
649
         [env_reflexivity || fail "iPoseProof:" t "not found"
         |env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
650
         |goal_tac ()]
651
652
    | _ =>
       eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
653
         [iIntoValid t
654
         |env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
655
         |goal_tac ()]
656
    end;
657
658
659
660
    try (apply _) in
  lazymatch eval compute in lazy_tc with
  | true => go ltac:(fun _ => spec_tac (); last (tac Htmp))
  | false => go spec_tac; last (tac Htmp)
Robbert Krebbers's avatar
Robbert Krebbers committed
661
662
663
  end.

(** * Apply *)
664
Tactic Notation "iApplyHyp" constr(H) :=
665
666
  let rec go H := first
    [eapply tac_apply with _ H _ _ _;
667
      [env_reflexivity
668
669
      |apply _
      |lazy beta (* reduce betas created by instantiation *)]
670
    |iSpecializePat H "[]"; last go H] in
671
672
673
674
675
676
677
678
  iExact H ||
  go H ||
  lazymatch iTypeOf H with
  | Some (_,?Q) => fail "iApply: cannot apply" Q
  end.

Tactic Notation "iApply" open_constr(lem) :=
  iPoseProofCore lem as false true (fun H => iApplyHyp H).
Robbert Krebbers's avatar
Robbert Krebbers committed
679
680

(** * Revert *)
681
Local Tactic Notation "iForallRevert" ident(x) :=
682
683
684
685
686
687
  let err x :=
    intros x;
    iMatchHyp (fun H P =>
      lazymatch P with
      | context [x] => fail 2 "iRevert:" x "is used in hypothesis" H
      end) in
Robbert Krebbers's avatar
Robbert Krebbers committed
688
  iStartProof;
689
690
  let A := type of x in
  lazymatch type of A with
691
692
693
  | Prop => revert x; first [apply tac_pure_revert|err x]
  | _ => revert x; first [apply tac_forall_revert|err x]
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
694
695

Tactic Notation "iRevert" constr(Hs) :=
696
697
  let rec go Hs :=
    lazymatch Hs with
698
    | [] => idtac
699
700
701
    | ESelPure :: ?Hs =>
       repeat match goal with x : _ |- _ => revert x end;
       go Hs
702
    | ESelIdent _ ?H :: ?Hs =>
703
       eapply tac_revert with _ H _ _; (* (i:=H2) *)
704
         [env_reflexivity || fail "iRevert:" H "not found"
705
         |env_cbv; go Hs]
706
    end in
Robbert Krebbers's avatar
Robbert Krebbers committed
707
  let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
Robbert Krebbers's avatar
Robbert Krebbers committed
708

709
Tactic Notation "iRevert" "(" ident(x1) ")" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
710
  iForallRevert x1.
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ")" :=
  iForallRevert x2; iRevert ( x1 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ")" :=
  iForallRevert x3; iRevert ( x1 x2 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" :=
  iForallRevert x4; iRevert ( x1 x2 x3 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ")" :=
  iForallRevert x5; iRevert ( x1 x2 x3 x4 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ")" :=
  iForallRevert x6; iRevert ( x1 x2 x3 x4 x5 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ")" :=
  iForallRevert x7; iRevert ( x1 x2 x3 x4 x5 x6 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ")" :=
  iForallRevert x8; iRevert ( x1 x2 x3 x4 x5 x6 x7 ).

Tactic Notation "iRevert" "(" ident(x1) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")"
Robbert Krebbers's avatar
Robbert Krebbers committed
737
    constr(Hs) :=
738
739
740
741
742
743
744
745
746
747
748
749
750
  iRevert Hs; iRevert ( x1 x2 x3 x4 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
    ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
  iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 ).
Robbert Krebbers's avatar
Robbert Krebbers committed
751
752
753

(** * Disjunction *)
Tactic Notation "iLeft" :=
754
  iStartProof;
Robbert Krebbers's avatar
Robbert Krebbers committed
755
  eapply tac_or_l;
Robbert Krebbers's avatar
Robbert Krebbers committed
756
757
758
759
    [apply _ ||
     let P := match goal with |- FromOr ?P _ _ => P end in
     fail "iLeft:" P "not a disjunction"
    |].
Robbert Krebbers's avatar
Robbert Krebbers committed
760
Tactic Notation "iRight" :=
761
  iStartProof;
Robbert Krebbers's avatar
Robbert Krebbers committed
762
  eapply tac_or_r;
Robbert Krebbers's avatar
Robbert Krebbers committed
763
764
765
766
    [apply _ ||
     let P := match goal with |- FromOr ?P _ _ => P end in
     fail "iRight:" P "not a disjunction"
    |].
Robbert Krebbers's avatar
Robbert Krebbers committed
767

768
Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
769
  eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
770
    [env_reflexivity || fail "iOrDestruct:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
771
772
773
    |apply _ ||
     let P := match goal with |- IntoOr ?P _ _ => P end in
     fail "iOrDestruct: cannot destruct" P
774
    |env_reflexivity || fail "iOrDestruct:" H1 "not fresh"
Robbert Krebbers's avatar
Robbert Krebbers committed
775
776
    |env_reflexivity || fail "iOrDestruct:" H2 "not fresh"
    | |].
Robbert Krebbers's avatar
Robbert Krebbers committed
777
778
779

(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
780
  iStartProof;
781
782
  eapply tac_and_split;
    [apply _ ||
783
     let P := match goal with |- FromAnd ?P _ _ => P end in
784
     fail "iSplit:" P "not a conjunction"| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
785
786

Tactic Notation "iSplitL" constr(Hs) :=
787
  iStartProof;