From e5c102c396f09c4fcfb7b402f904270249916fe7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Mar 2017 15:06:04 +0200
Subject: [PATCH] Version of iPoseProof with intro pattern.
---
ProofMode.md | 6 ++++--
theories/proofmode/tactics.v | 37 +++++++++++++++++++++++++++++++++---
2 files changed, 38 insertions(+), 5 deletions(-)
diff --git a/ProofMode.md b/ProofMode.md
index 773baa3ff..dbbe030f4 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -39,8 +39,10 @@ Context management
implications/wands of a hypothesis whose conclusion is persistent. In this
case, all hypotheses can be used for proving the premises, as well as for
the resulting goal.
-- `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
- `H`.
+- `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
+ eliminates it. This tactic is essentially the same as `iDestruct` with the
+ difference that when `pm_trm` is a non-univerisally quantified spatial
+ hypothesis, it will not throw the hypothesis away.
- `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
hypothesis `P` to the current goal. The specialization pattern `spat`
specifies which hypotheses will be consumed by proving `P`. The introduction
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 7ad7a193a..89c42bdc7 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -554,9 +554,6 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
| false => go spec_tac; last (tac Htmp)
end.
-Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
- iPoseProofCore lem as false false (fun Htmp => iRename Htmp into H).
-
(** * Apply *)
Tactic Notation "iApply" open_constr(lem) :=
let rec go H := first
@@ -1172,6 +1169,40 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
iDestructCore lem as true (fun H => iPure H as pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
+ constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+ constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+ simple_intropattern(x5) ")" constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+ simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
+ simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
+ constr(pat) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iPoseProof" open_constr(lem) "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) :=
+ iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+
(** * Induction *)
Tactic Notation "iInductionCore" constr(x)
"as" simple_intropattern(pat) constr(IH) :=
--
GitLab