tactics.v 84.1 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
Tactic Notation "iStartProof" :=
  lazymatch goal with
  | |- envs_entails _ _ => idtac
  | |- ?φ => 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. *)
70
Tactic Notation "iStartProof" uconstr(PROP) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  lazymatch goal with
72
  | |- @envs_entails ?PROP' _ _ =>
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
73 74
    (* 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
75
    let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
76

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
77
  (* We eta-expand [as_valid_2], in order to make sure that
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
78 79
     [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
80 81
     [bi_car _], and hence trigger the canonical structures mechanism
     to find the corresponding bi. *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
82
  | |- ?φ => eapply (λ P : PROP, @as_valid_2 φ _ P);
83
               [apply _ || fail "iStartProof: not a Bi entailment"
84
               |apply tac_adequate]
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86
  end.

87

88 89
(** * Simplification *)
Tactic Notation "iEval" tactic(t) :=
90
  iStartProof; try (eapply tac_eval; [t; reflexivity|]).
91 92 93

Tactic Notation "iSimpl" := iEval simpl.

Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
  eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
97 98
    [env_reflexivity || fail "iRename:" H1 "not found"
    |env_reflexivity || fail "iRename:" H2 "not fresh"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
99

100 101
Local Inductive esel_pat :=
  | ESelPure
102
  | ESelIdent : bool  ident  esel_pat.
103

104
Ltac iElaborateSelPat pat :=
105 106
  let rec go pat Δ Hs :=
    lazymatch pat with
107
    | [] => eval cbv in Hs
108 109 110 111
    | 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
112
       go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
113 114 115
    | SelSpatial :: ?pat =>
       let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
       let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
116 117
       go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
    | SelIdent ?H :: ?pat =>
118
       lazymatch eval env_cbv in (envs_lookup_delete false H Δ) with
119
       | Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
120 121 122 123
       | None => fail "iElaborateSelPat:" H "not found"
       end
    end in
  lazymatch goal with
124
  | |- envs_entails ?Δ _ =>
125 126 127
    let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
  end.

128 129
Local Ltac iClearHyp H :=
  eapply tac_clear with _ H _ _; (* (i:=H) *)
130 131 132 133 134
    [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"
    |].
135

Robbert Krebbers's avatar
Robbert Krebbers committed
136 137
Tactic Notation "iClear" constr(Hs) :=
  let rec go Hs :=
138
    lazymatch Hs with
Robbert Krebbers's avatar
Robbert Krebbers committed
139
    | [] => idtac
140
    | ESelPure :: ?Hs => clear; go Hs
141
    | ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
Robbert Krebbers's avatar
Robbert Krebbers committed
142
    end in
143
  let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
144

145 146
Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
  iClear Hs; clear xs.
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149

(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  eapply tac_assumption with _ H _ _; (* (i:=H) *)
151
    [env_reflexivity || fail "iExact:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153
    |apply _ ||
     let P := match goal with |- FromAssumption _ ?P _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156
     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
157 158 159

Tactic Notation "iAssumptionCore" :=
  let rec find Γ i P :=
160
    lazymatch Γ with
Robbert Krebbers's avatar
Robbert Krebbers committed
161
    | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j|find Γ i P]
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163 164
    end in
  match goal with
  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
165
     first [is_evar i; fail 1 | env_reflexivity]
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
167
     is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
168
  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
169
     first [is_evar i; fail 1 | env_reflexivity]
170
  | |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
171
     is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
Robbert Krebbers's avatar
Robbert Krebbers committed
172
  end.
173

Robbert Krebbers's avatar
Robbert Krebbers committed
174
Tactic Notation "iAssumption" :=
175 176
  let Hass := fresh in
  let rec find p Γ Q :=
177
    lazymatch Γ with
178
    | Esnoc ?Γ ?j ?P => first
179
       [pose proof (_ : FromAssumption p P Q) as Hass;
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182 183 184 185 186 187 188
        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]
189 190
       |find p Γ Q]
    end in
191
  lazymatch goal with
192
  | |- envs_entails (Envs ?Γp ?Γs) ?Q =>
193 194 195
     first [find true Γp Q | find false Γs Q
           |fail "iAssumption:" Q "not found"]
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197 198 199 200

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

(** * Making hypotheses persistent or pure *)
201
Local Tactic Notation "iPersistent" constr(H) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
202
  eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
203
    [env_reflexivity || fail "iPersistent:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
204
    |apply _ ||
Robbert Krebbers's avatar
Robbert Krebbers committed
205 206 207
     let P := match goal with |- IntoPersistent _ ?P _ => P end in
     fail "iPersistent:" P "not persistent"
    |env_cbv; apply _ ||
208 209
     let P := match goal with |- TCOr (Affine ?P) _ => P end in
     fail "iPersistent:" P "not affine and the goal not absorbing"
210
    |env_reflexivity|].
Robbert Krebbers's avatar
Robbert Krebbers committed
211

212
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
213
  eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
214
    [env_reflexivity || fail "iPure:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
215 216 217
    |apply _ ||
     let P := match goal with |- IntoPure ?P _ => P end in
     fail "iPure:" P "not pure"
Robbert Krebbers's avatar
Robbert Krebbers committed
218
    |env_cbv; apply _ ||
219 220
     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
221 222
    |intros pat].

Robbert Krebbers's avatar
Robbert Krebbers committed
223 224 225
Tactic Notation "iEmpIntro" :=
  iStartProof;
  eapply tac_emp_intro;
226 227
    [env_cbv; apply _ ||
     fail "iEmpIntro: spatial context contains non-affine hypotheses"].
Robbert Krebbers's avatar
Robbert Krebbers committed
228

229
Tactic Notation "iPureIntro" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
230
  iStartProof;
231
  eapply tac_pure_intro;
232 233
    [env_reflexivity
    |apply _ ||
234
     let P := match goal with |- FromPure _ ?P _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
235 236
     fail "iPureIntro:" P "not pure"
    |].
Robbert Krebbers's avatar
Robbert Krebbers committed
237

238 239 240 241
(** Framing *)
Local Ltac iFrameFinish :=
  lazy iota beta;
  try match goal with
242
  | |- envs_entails _ True => by iPureIntro
243
  | |- envs_entails _ emp => iEmpIntro
244 245 246
  end.

Local Ltac iFramePure t :=
247
  iStartProof;
248 249 250 251 252 253
  let φ := type of t in
  eapply (tac_frame_pure _ _ _ _ t);
    [apply _ || fail "iFrame: cannot frame" φ
    |iFrameFinish].

Local Ltac iFrameHyp H :=
254
  iStartProof;
255
  eapply tac_frame with _ H _ _ _;
256
    [env_reflexivity || fail "iFrame:" H "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258 259
    |apply _ ||
     let R := match goal with |- Frame _ ?R _ _ => R end in
     fail "iFrame: cannot frame" R
260 261 262 263 264 265
    |iFrameFinish].

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

Local Ltac iFrameAnyPersistent :=
266
  iStartProof;
267 268 269
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
  match goal with
270
  | |- envs_entails ?Δ _ =>
271 272 273 274
     let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
  end.

Local Ltac iFrameAnySpatial :=
275
  iStartProof;
276 277 278
  let rec go Hs :=
    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
  match goal with
279
  | |- envs_entails ?Δ _ =>
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
     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 :=
308
    lazymatch Hs with
309
    | [] => idtac
310 311 312
    | SelPure :: ?Hs => iFrameAnyPure; go Hs
    | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
    | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
313
    | SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
314
    end
315
  in let Hs := sel_pat.parse Hs in go Hs.
316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337
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.

338 339
(** * Basic introduction tactics *)
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
340 341 342 343 344 345 346 347 348 349 350 351 352 353
  (* In the case the goal starts with an [let x := _ in _], we do not
     want to unfold x and start the proof mode. Instead, we want to
     use intros. So [iStartProof] has to be called only if [intros]
     fails *)
  intros x ||
    (iStartProof;
     lazymatch goal with
     | |- envs_entails _ _ =>
       eapply tac_forall_intro;
       [apply _ ||
              let P := match goal with |- FromForall ?P _ => P end in
              fail "iIntro: cannot turn" P "into a universal quantifier"
       |lazy beta; intros x]
     end).
354 355 356 357 358

Local Tactic Notation "iIntro" constr(H) :=
  iStartProof;
  first
  [ (* (?Q → _) *)
359 360 361
    eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
      [apply _
      |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 370 371
    eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
      [apply _
      | env_reflexivity || fail 1 "iIntro:" H "not fresh"
Robbert Krebbers's avatar
Robbert Krebbers committed
372
      |]
373
  | fail "iIntro: nothing to introduce" ].
374 375 376 377 378

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

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

Local Tactic Notation "iIntroForall" :=
  lazymatch goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
416
  | |-  _, ?P => fail (* actually an →, this is handled by iIntro below *)
417
  | |-  _, _ => intro
418 419 420 421 422 423
  | |- let _ := _ in _ => intro
  | |- _ =>
    iStartProof;
    lazymatch goal with
    | |- envs_entails _ ( x : _, _) => let x' := fresh x in iIntro (x')
    end
424 425 426 427
  end.
Local Tactic Notation "iIntro" :=
  lazymatch goal with
  | |- _  ?P => intro
428 429 430 431 432 433
  | |- _ =>
    iStartProof;
    lazymatch goal with
    | |- envs_entails _ (_ - _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
    | |- envs_entails _ (_  _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
    end
434 435
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
436
(** * Specialize *)
437 438 439 440 441
Record iTrm {X As} :=
  ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : string }.
Arguments ITrm {_ _} _ _ _.

Notation "( H $! x1 .. xn )" :=
442
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
443
Notation "( H $! x1 .. xn 'with' pat )" :=
444
  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
445 446
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).

447
(*
Robbert Krebbers's avatar
Robbert Krebbers committed
448 449 450 451 452
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`.
453
*)
454
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
455
  let rec go xs :=
456
    lazymatch xs with
457
    | hnil => apply id (* Finally, trigger TC *)
458
    | hcons ?x ?xs =>
459
       eapply tac_forall_specialize with _ H _ _ _; (* (i:=H) (a:=x) *)
460 461
         [env_reflexivity || fail "iSpecialize:" H "not found"
         |typeclasses eauto ||
Robbert Krebbers's avatar
Robbert Krebbers committed
462
          let P := match goal with |- IntoForall ?P _ => P end in
463
          fail "iSpecialize: cannot instantiate" P "with" x
Robbert Krebbers's avatar
Robbert Krebbers committed
464 465 466
         |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
467
          is a hole, [refine] will generate an additional goal. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
468
          | |-  _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |]
469
          end; [env_reflexivity|go xs]]
470 471
    end in
  go xs.
Robbert Krebbers's avatar
Robbert Krebbers committed
472

473
Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
474
  let solve_to_wand H1 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
475
    apply _ ||
Robbert Krebbers's avatar
Robbert Krebbers committed
476
    let P := match goal with |- IntoWand _ _ ?P _ _ => P end in
Robbert Krebbers's avatar
Robbert Krebbers committed
477
    fail "iSpecialize:" P "not an implication/wand" in
478 479 480 481 482 483 484 485
  let solve_done d :=
    lazymatch d with
    | true =>
       done ||
       let Q := match goal with |- envs_entails _ ?Q => Q end in
       fail "iSpecialize: cannot solve" Q "using done"
    | false => idtac
    end in
Robbert Krebbers's avatar
Robbert Krebbers committed
486 487 488
  let rec go H1 pats :=
    lazymatch pats with
    | [] => idtac
489
    | SForall :: ?pats =>
Ralf Jung's avatar
Ralf Jung committed
490
       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
491
       go H1 pats
492
    | SIdent ?H2 :: ?pats =>
Robbert Krebbers's avatar
Robbert Krebbers committed
493
       eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
494 495
         [env_reflexivity || fail "iSpecialize:" H2 "not found"
         |env_reflexivity || fail "iSpecialize:" H1 "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
496
         |apply _ ||
Robbert Krebbers's avatar
Robbert Krebbers committed
497 498
          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
499
          fail "iSpecialize: cannot instantiate" P "with" Q
500
         |env_reflexivity|go H1 pats]
501 502
    | SPureGoal ?d :: ?pats =>
       eapply tac_specialize_assert_pure with _ H1 _ _ _ _ _;
503
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
504
         |solve_to_wand H1
Robbert Krebbers's avatar
Robbert Krebbers committed
505
         |apply _ ||
506
          let Q := match goal with |- FromPure _ ?Q _ => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
507
          fail "iSpecialize:" Q "not pure"
508
         |env_reflexivity
509
         |solve_done d (*goal*)
510
         |go H1 pats]
511
    | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
512
       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _ _;
513
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
514
         |solve_to_wand H1
Robbert Krebbers's avatar
Robbert Krebbers committed
515
         |apply _ ||
516
          let Q := match goal with |- Persistent ?Q => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
517
          fail "iSpecialize:" Q "not persistent"
518
         |apply _
519
         |env_reflexivity
520
         |iFrame Hs_frame; solve_done d (*goal*)
521
         |go H1 pats]
522 523 524
    | SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
       fail "iSpecialize: cannot select hypotheses for persistent premise"
    | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
525
       let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
526
       eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
527
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
Robbert Krebbers's avatar
Robbert Krebbers committed
528
         |solve_to_wand H1
529
         |lazymatch m with
530
          | GSpatial => apply add_modal_id
531
          | GModal => apply _ || fail "iSpecialize: goal not a modality"
532
          end
533 534
         |env_reflexivity ||
          let Hs' := iMissingHyps Hs' in
535
          fail "iSpecialize: hypotheses" Hs' "not found"
536
         |iFrame Hs_frame; solve_done d (*goal*)
Robbert Krebbers's avatar
Robbert Krebbers committed
537
         |go H1 pats]
538 539
    | SAutoFrame GPersistent :: ?pats =>
       eapply tac_specialize_assert_persistent with _ _ H1 _ _ _ _;
540
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
541
         |solve_to_wand H1
Robbert Krebbers's avatar
Robbert Krebbers committed
542
         |apply _ ||
543
          let Q := match goal with |- Persistent ?Q => Q end in
Robbert Krebbers's avatar
Robbert Krebbers committed
544
          fail "iSpecialize:" Q "not persistent"
545
         |env_reflexivity
546 547 548 549
         |solve [iFrame "∗ #"]
         |go H1 pats]
    | SAutoFrame ?m :: ?pats =>
       eapply tac_specialize_frame with _ H1 _ _ _ _ _ _;
550
         [env_reflexivity || fail "iSpecialize:" H1 "not found"
551 552
         |solve_to_wand H1
         |lazymatch m with
553
          | GSpatial => apply add_modal_id
554 555
          | GModal => apply _ || fail "iSpecialize: goal not a modality"
          end
556 557 558 559 560
         |first
            [apply tac_unlock_emp
            |apply tac_unlock_True
            |iFrame "∗ #"; apply tac_unlock
            |fail "iSpecialize: premise cannot be solved by framing"]
561
         |reflexivity]; iIntro H1; go H1 pats
562 563
    end in let pats := spec_pat.parse pat in go H pats.

Robbert Krebbers's avatar
Robbert Krebbers committed
564
(* The argument [p] denotes whether the conclusion of the specialized term is
565 566 567
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
568 569 570 571 572
`#` 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). *)
573 574
Tactic Notation "iSpecializeCore" open_constr(H)
    "with" open_constr(xs) open_constr(pat) "as" constr(p) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
575
  let p := intro_pat_persistent p in
576 577 578 579 580
  let pat := spec_pat.parse pat in
  let H :=
    lazymatch type of H with
    | string => constr:(INamed H)
    | _ => H
581
    end in
582 583 584 585 586 587 588 589 590
  iSpecializeArgs H xs;
  lazymatch type of H with
  | ident =>
    (* 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. *)
591
    let pat := spec_pat.parse pat in
592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619
    lazymatch eval compute in
      (p && bool_decide (pat  []) && negb (existsb spec_pat_modal pat)) with
    | true =>
       (* FIXME: do something reasonable when the BI is not affine *)
       eapply tac_specialize_persistent_helper with _ H _ _ _ _;
         [env_reflexivity || fail "iSpecialize:" H "not found"
         |iSpecializePat H pat; last (iExact H)
         |apply _ ||
          let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
          fail "iSpecialize:" Q "not persistent"
         |env_cbv; apply _ ||
          let Q := match goal with |- TCAnd _ (Affine ?Q) => Q end in
          fail "iSpecialize:" Q "not affine"
         |env_reflexivity
         |(* goal *)]
    | false => iSpecializePat H pat
    end
  | _ => fail "iSpecialize:" H "should be a hypothesis, use iPoseProof instead"
  end.

Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
  lazymatch type of t with
  | string => iSpecializeCore t with hnil "" as p
  | ident => iSpecializeCore t with hnil "" as p
  | _ =>
    lazymatch t with
    | ITrm ?H ?xs ?pat => iSpecializeCore H with xs pat as p
    | _ => fail "iSpecialize:" t "should be a proof mode term"
620
    end
621
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
622

623
Tactic Notation "iSpecialize" open_constr(t) :=
624 625 626
  iSpecializeCore t as false.
Tactic Notation "iSpecialize" open_constr(t) "as" "#" :=
  iSpecializeCore t as true.
627

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

632
- [∀ (x_1 : A_1) .. (x_n : A_n), uPred_valid Q]
633
- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -∗ P2]
634 635 636 637
- [∀ (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]. *)
638
Tactic Notation "iIntoValid" open_constr(t) :=
639
  let rec go t :=
640 641 642 643 644 645 646 647
    (* We try two reduction tactics for the type of t before trying to
       specialize it. We first try the head normal form in order to
       unfold all the definition that could hide an entailment.  Then,
       we try the much weaker [eval cbv zeta], because entailment is
       not necessarilly opaque, and could be unfolded by [hnf].

       However, for calling type class search, we only use [cbv zeta]
       in order to make sure we do not unfold [bi_valid]. *)
648
    let tT := type of t in
649
    first
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
650 651
      [ let tT' := eval hnf in tT in go_specialize t tT'
      | let tT' := eval cbv zeta in tT in go_specialize t tT'
652 653 654 655 656 657 658 659 660
      | let tT' := eval cbv zeta in tT in
        eapply (as_valid_1 tT);
          (* Doing [apply _] here fails because that will try to solve all evars
          whose type is a typeclass, in dependency order (according to Matthieu).
          If one fails, it aborts.  However, we rely on progress on the main goal
          ([AsValid ...])  to unify some of these evars and hence enable progress
          elsewhere.  With [typeclasses eauto], that seems to work better. *)
          [solve [ typeclasses eauto with typeclass_instances ] ||
                   fail "iPoseProof: not a BI assertion"|exact t]]
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
661
  with go_specialize t tT :=
662 663 664
    lazymatch tT with                (* We do not use hnf of tT, because, if
                                        entailment is not opaque, then it would
                                        unfold it. *)
665 666 667
    | ?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
668
      (* This is a workarround for Coq bug #6583. *)
669 670
      let e := fresh in evar (e:id T);
      let e' := eval unfold e in e in clear e; go (t e')
671 672
    end
  in
673
  go t.
674

675 676
(* 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
677 678 679 680 681 682
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.
*)
683 684
Tactic Notation "iPoseProofCore" open_constr(lem)
    "as" constr(p) constr(lazy_tc) tactic(tac) :=
685
  iStartProof;
686
  let Htmp := iFresh in
687 688
  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
689 690 691 692 693 694
  let spec_tac _ :=
    lazymatch lem with
    | ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
    | _ => idtac
    end in
  let go goal_tac :=
695
    lazymatch type of t with
696
    | ident =>
697
       eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
698 699
         [env_reflexivity || fail "iPoseProof:" t "not found"
         |env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
700
         |goal_tac ()]
701 702
    | _ =>
       eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
703
         [iIntoValid t
704
         |env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
705
         |goal_tac ()]
706
    end;
707 708 709 710
    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
711 712 713
  end.

(** * Apply *)
714
Tactic Notation "iApplyHyp" constr(H) :=
715 716
  let rec go H := first
    [eapply tac_apply with _ H _ _ _;
717
      [env_reflexivity
718 719
      |apply _
      |lazy beta (* reduce betas created by instantiation *)]
720
    |iSpecializePat H "[]"; last go H] in
721 722 723 724 725 726 727 728
  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
729 730

(** * Revert *)
731
Local Tactic Notation "iForallRevert" ident(x) :=
732 733 734 735 736 737
  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
738
  iStartProof;
739 740
  let A := type of x in
  lazymatch type of A with
741 742 743
  | 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
744 745

Tactic Notation "iRevert" constr(Hs) :=
746 747
  let rec go Hs :=
    lazymatch Hs with
748
    | [] => idtac
749 750 751
    | ESelPure :: ?Hs =>
       repeat match goal with x : _ |- _ => revert x end;
       go Hs
752
    | ESelIdent _ ?H :: ?Hs =>
753
       eapply tac_revert with _ H _ _; (* (i:=H2) *)
754
         [env_reflexivity || fail "iRevert:" H "not found"
755
         |env_cbv; go Hs]
756
    end in
Robbert Krebbers's avatar
Robbert Krebbers committed
757
  let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
Robbert Krebbers's avatar
Robbert Krebbers committed
758

759
Tactic Notation "iRevert" "(" ident(x1) ")" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
760
  iForallRevert x1.
761 762 763 764 765 766 767 768 769 770 771 772 773 774 775