From 09ab191c7a7664a3cff7f941a5cfa17b27a6a372 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 1 Dec 2020 14:35:40 +0100
Subject: [PATCH] Make iDestruct consume wands when it's supposed to

`iDestruct ("H" with "HP")` where "H" is persistent is supposed to
consume "H" if it isn't a forall. Due to a bug in the tactic, this
behavior was never triggered and "H" was always left alone.
---
 iris/base_logic/lib/boxes.v   |  2 +-
 iris/proofmode/ltac_tactics.v | 10 ++++++++--
 tests/proofmode.v             | 26 ++++++++++++++++++++++++++
 3 files changed, 35 insertions(+), 3 deletions(-)

diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 8f0620e03..f070ae1d4 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -247,7 +247,7 @@ Lemma slice_iff E q f P Q Q' γ b :
 Proof.
   iIntros (??) "#HQQ' #Hs Hb". destruct b.
   - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
-    iDestruct ("HQQ'" with "HQ") as "HQ'".
+    iPoseProof ("HQQ'" with "HQ") as "HQ'".
     iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
     iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
     iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 47127e687..43465aca8 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1992,6 +1992,12 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
   iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with tac.
 
 (** * Destruct tactic *)
+
+(** [CopyDestruct] is an internal class used by the [iDestruct] tactic to
+identify universally quantified hypotheses that should be copied and not be
+consumed when they are specialized in proofmode terms.
+
+Not intended for user extensibility. *)
 Class CopyDestruct {PROP : bi} (P : PROP).
 Arguments CopyDestruct {_} _%I.
 Hint Mode CopyDestruct + ! : typeclass_instances.
@@ -2013,8 +2019,8 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
     | string => constr:(Some (INamed lem))
     | iTrm =>
        lazymatch lem with
-       | @iTrm ident ?H _ _ => constr:(Some H)
-       | @iTrm string ?H _ _ => constr:(Some (INamed H))
+       | @ITrm ident _ _?H _ _ => constr:(Some H)
+       | @ITrm string _ _ ?H _ _ => constr:(Some (INamed H))
        | _ => constr:(@None ident)
        end
     | _ => constr:(@None ident)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index ef03c12c6..d41770c47 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -93,6 +93,32 @@ Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
   Q ∗ (Q -∗ P) -∗ P.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
 
+Lemma test_iDestruct_specialize_wand P Q :
+  Q ∗ □(Q -∗ P) -∗ P.
+Proof.
+  iIntros "[HQ #HQP]".
+  (* iDestruct specializes, consuming the hypothesis *)
+  iDestruct ("HQP" with "HQ") as "HQP". done.
+Qed.
+
+Lemma test_iPoseProof_copy_wand P Q :
+  Q ∗ □(Q -∗ P) -∗ P ∗ (Q -∗ P).
+Proof.
+  iIntros "[HQ #HQP]".
+  (* in contrast with [iDestruct], [iPoseProof] leaves "HQP" alone *)
+  iPoseProof ("HQP" with "HQ") as "HP".
+  iFrame "HP HQP".
+Qed.
+
+Lemma test_iDestruct_pose_forall (Φ: nat → PROP) :
+  □(∀ (x:nat), Φ x) -∗ Φ 0 ∗ Φ 1.
+Proof.
+  iIntros "#H".
+  (* iDestruct does not consume "H" because it's a [∀] *)
+  iDestruct ("H" $! 0) as "$".
+  iDestruct ("H" $! 1) as "$".
+Qed.
+
 Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
   Q ∗ (Q -∗ P) -∗ P ∗ Q.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
-- 
GitLab