From 211dc7cad10da872d2840f73acd85eed0b82f7b4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 28 Aug 2017 17:05:44 +0200
Subject: [PATCH] Optimize wp_apply and improve its error reporting.
We now first iPoseProof the lemma and instantiate its premises before trying
to search for the sub-term where to apply. As a result, instantiation of the
premises of the applied lemmas happens only once, instead of it being done for
each sub-term as obtained by reshape_expr.
---
theories/heap_lang/proofmode.v | 16 ++++++++++------
theories/proofmode/tactics.v | 16 +++++++++-------
2 files changed, 19 insertions(+), 13 deletions(-)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a793ec715..2a891fa17 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -219,12 +219,16 @@ Qed.
End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
- iStartProof;
- lazymatch goal with
- | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
- wp_bind_core K; iApply lem; try iNext; simpl)
- | _ => fail "wp_apply: not a 'wp'"
- end.
+ iPoseProofCore lem as false true (fun H =>
+ lazymatch goal with
+ | |- _ ⊢ wp ?E ?e ?Q =>
+ reshape_expr e ltac:(fun K e' =>
+ wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
+ lazymatch iTypeOf H with
+ | Some (_,?P) => fail "wp_apply: cannot apply" P
+ end
+ | _ => fail "wp_apply: not a 'wp'"
+ end).
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
iStartProof;
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ae5797679..3ae23afbe 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -564,19 +564,21 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end.
(** * Apply *)
-Tactic Notation "iApply" open_constr(lem) :=
+Tactic Notation "iApplyHyp" constr(H) :=
let rec go H := first
[eapply tac_apply with _ H _ _ _;
[env_reflexivity
|apply _
|lazy beta (* reduce betas created by instantiation *)]
|iSpecializePat H "[]"; last go H] in
- iPoseProofCore lem as false true (fun H => first
- [iExact H
- |go H
- |lazymatch iTypeOf H with
- | Some (_,?Q) => fail 1 "iApply: cannot apply" Q
- end]).
+ 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).
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
--
GitLab