From 6d1a88a5323bc6cc3b6c5a1ab732d39855f15f1a Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 21 Jul 2020 21:25:29 -0500
Subject: [PATCH] Support destructing exists with intro patterns
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The syntax re-uses the existing support for pure names, namely the % and
%H patterns. Using "[% H]" is like `iDestruct ... as (?) "H"` and using
"[%x H]" (with the string-ident plugin) is like `iDestruct ... as (x)
"H"`.

This changes how these patterns are parsed. Previously, both would have
been handled as conjunctions (using IntoAnd or IntoSep, depending on
whether the hypothesis is persistent or not). This means it was possible
for the user to use "[% H]" to destruct a pure hypothesis ⌜φ ∧ ψ⌝ and
put only the first conjunct in the Gallina context, leaving the other
one in the IPM; such patterns will now break, since iExistDestruct
does not handle this use case.
---
 iris/proofmode/class_instances.v |  6 ++++--
 iris/proofmode/ltac_tactics.v    | 20 +++++++++++++++++---
 tests/proofmode.v                | 17 +++++++++++++++++
 3 files changed, 38 insertions(+), 5 deletions(-)

diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 64c39eb32..70c554b24 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -807,14 +807,16 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
 Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name :
   IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
-(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
+(* [to_ident_name H] makes the default name [H] when [P] is destructed with
+[iExistDestruct] *)
 Global Instance into_exist_and_pure P Q φ :
   IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q) (to_ident_name H).
 Proof.
   intros (φ'&->&?). rewrite /IntoExist (into_pure P).
   apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
 Qed.
-(* [to_ident_name H] makes the default name [H] when [P] is introduced with [?] *)
+(* [to_ident_name H] makes the default name [H] when [P] is destructed with
+[iExistDestruct] *)
 Global Instance into_exist_sep_pure P Q φ :
   IntoPureT P φ →
   TCOr (Affine P) (Absorbing Q) →
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 180eeee01..af6433bb8 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1426,6 +1426,18 @@ Tactic Notation "iModCore" constr(H) :=
 
 (** [pat0] is the unparsed pattern, and is only used in error messages *)
 Local Ltac iDestructHypGo Hz pat0 pat :=
+  let iAndDestructAs pat1 pat2 :=
+      let Hy := iFresh in
+      iAndDestruct Hz as Hz Hy;
+      iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2 in
+  let iExistDestructPure gallina_id pat2 :=
+      lazymatch gallina_id with
+      | IGallinaAnon =>
+        iExistDestruct Hz as ? Hz; iDestructHypGo Hz pat0 pat2
+      | IGallinaNamed ?s =>
+        let x := string_to_ident s in
+        iExistDestruct Hz as x Hz; iDestructHypGo Hz pat0 pat2
+      end in
   lazymatch pat with
   | IFresh =>
      lazymatch Hz with
@@ -1444,9 +1456,11 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IList [[IDrop; ?pat2]] =>
      iAndDestructChoice Hz as Right Hz;
      iDestructHypGo Hz pat0 pat2
-  | IList [[?pat1; ?pat2]] =>
-     let Hy := iFresh in iAndDestruct Hz as Hz Hy;
-     iDestructHypGo Hz pat0 pat1; iDestructHypGo Hy pat0 pat2
+  (* heuristic to fallback to [iAndDestruct] when both patterns are pure, since
+  the instances for [IntoAnd] are more general than for [IntoExist]. *)
+  | IList [[IPure ?id1; IPure ?id2]] => iAndDestructAs (IPure id1) (IPure id2)
+  | IList [[IPure ?gallina_id; ?pat2]] => iExistDestructPure gallina_id pat2
+  | IList [[?pat1; ?pat2]] => iAndDestructAs pat1 pat2
   | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
   | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"
 
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9940220a3..0059095e0 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -251,6 +251,15 @@ Lemma test_iDestruct_exists_automatic_def P :
   an_exists P -∗ ∃ k, ▷^k P.
 Proof. iDestruct 1 as (?) "H". by iExists an_exists_name. Qed.
 
+(* use an Iris intro pattern [% H] to indicate iExistDestruct rather than (?) *)
+Lemma test_exists_intro_pattern_anonymous P (Φ: nat → PROP) :
+  P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
+Proof.
+  iIntros "[HP1 [% HP2]]".
+  iExists y.
+  iFrame "HP1 HP2".
+Qed.
+
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P.
 Proof. iIntros (??) "H". auto. Qed.
 
@@ -1379,6 +1388,14 @@ Proof.
   Fail iIntros "[H %H]".
 Abort.
 
+Lemma test_exists_intro_pattern P (Φ: nat → PROP) :
+  P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
+Proof.
+  iIntros "[HP1 [%y HP2]]".
+  iExists y.
+  iFrame "HP1 HP2".
+Qed.
+
 End pure_name_tests.
 
 Section tactic_tests.
-- 
GitLab