Allow intro_patterns for destructing existentials using iDestruct.

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".

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) :=