From ab19e50e344b743eab2315ab31e3b93b400498bb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 May 2016 15:44:46 +0200
Subject: [PATCH] Allow intro_patterns for destructing existentials using
iDestruct.
---
heap_lang/lib/lock.v | 2 +-
proofmode/tactics.v | 9 ++++++---
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 688af41d9..35b66fde0 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -66,7 +66,7 @@ Lemma acquire_spec l R (Φ : val → iProp) :
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
- iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl HR]"; destruct b.
+ iInv N as "Hinv". iDestruct "Hinv" as { [] } "[Hl HR]".
- wp_cas_fail. iSplitL "Hl".
+ iNext. iExists true. by iSplit.
+ wp_if. by iApply "IH".
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 1b9806269..222ae275c 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -402,13 +402,16 @@ Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
uconstr(x8) :=
iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.
-Local Tactic Notation "iExistDestruct" constr(H) "as" ident(x) constr(Hx) :=
+Local Tactic Notation "iExistDestruct" constr(H)
+ "as" simple_intropattern(x) constr(Hx) :=
eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
[env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
|let P := match goal with |- ExistDestruct ?P _ => P end in
apply _ || fail "iExistDestruct:" H ":" P "not an existential"|];
- intros x; eexists; split;
- [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"|].
+ let y := fresh in
+ intros y; eexists; split;
+ [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
+ |revert y; intros x].
(** * Destruct tactic *)
Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
--
GitLab