From 84481877eeb2fccdcb783b67459720c971c3fb43 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 22 Jan 2017 10:25:16 +0100
Subject: [PATCH] Add [] spec patterns for missing premises of iApply.
This fixes issue #51.
---
theories/proofmode/tactics.v | 13 +++++++------
theories/tests/proofmode.v | 4 ++++
2 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index f899393a3..af482f59e 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -426,13 +426,14 @@ Tactic Notation "iApply" open_constr(lem) :=
| ITrm ?t ?xs ?pat => constr:(ITrm t xs ("*" +:+ pat))
| _ => constr:(ITrm lem hnil "*")
end in
- iPoseProofCore lem as false true (fun H => first
- [iExact H
- |eapply tac_apply with _ H _ _ _;
+ let rec go H := first
+ [eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity
- |let P := match goal with |- IntoWand ?P _ _ => P end in
- apply _ || fail 1 "iApply: cannot apply" P
- |lazy beta (* reduce betas created by instantiation *)]]).
+ |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|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 147edd8e6..f8302508d 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -116,3 +116,7 @@ Proof.
iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". }
done.
Qed.
+
+Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
+ (P -∗ Q -∗ True -∗ True -∗ R) -∗ P -∗ Q -∗ R.
+Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
--
GitLab