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 01/10] 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


From b9d25e994ffa3ebe5b422acd5d14aa675b722354 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 8 Dec 2020 00:10:01 +0100
Subject: [PATCH 02/10] Apply 1 suggestion(s) to 1 file(s)

---
 tests/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 0059095e0..3d150c749 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -251,7 +251,7 @@ 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 (?) *)
+(* use an Iris intro pattern [% H] rather than (?) to indicate iExistDestruct *)
 Lemma test_exists_intro_pattern_anonymous P (Φ: nat → PROP) :
   P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
 Proof.
-- 
GitLab


From 6dc7e98ae9faa67d3444e91e934555653ecb1a60 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Mar 2021 13:44:18 +0100
Subject: [PATCH 03/10] replace iAndDestruct hack for [% %] by more general
 IntoExist instances

---
 iris/proofmode/class_instances.v | 26 ++++++++++++++++++--------
 iris/proofmode/ltac_tactics.v    |  6 +++---
 tests/proofmode.v                | 25 +++++++++++++++++++++++--
 3 files changed, 44 insertions(+), 13 deletions(-)

diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 70c554b24..90e639c96 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -807,22 +807,32 @@ 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 destructed with
+(* Low-priority instance falling back to treating a conjunction with a pure
+left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as
+[% ...]].
+[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).
+Global Instance into_exist_and_pure PQ P Q φ :
+  IntoAnd false PQ P Q →
+  IntoPureT P φ →
+  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100.
 Proof.
-  intros (φ'&->&?). rewrite /IntoExist (into_pure P).
+  intros HPQ (φ'&->&?). rewrite /IntoAnd /= in HPQ.
+  rewrite /IntoExist HPQ (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 destructed with
+(* Low-priority instance falling back to treating a sep. conjunction with a pure
+left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as
+[% ...]].
+[to_ident_name H] makes the default name [H] when [P] is destructed with
 [iExistDestruct] *)
-Global Instance into_exist_sep_pure P Q φ :
+Global Instance into_exist_sep_pure PQ P Q φ :
+  IntoSep PQ P Q →
   IntoPureT P φ →
   TCOr (Affine P) (Absorbing Q) →
-  IntoExist (P ∗ Q) (λ _ : φ, Q) (to_ident_name H).
+  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100.
 Proof.
-  intros (φ'&->&?) ?. rewrite /IntoExist.
+  intros HPQ (φ'&->&?) ?. rewrite /IntoSep in HPQ. rewrite /IntoExist HPQ.
   eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
   rewrite -exist_intro //. apply sep_elim_r, _.
 Qed.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index af6433bb8..6e3753a4d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1456,9 +1456,9 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IList [[IDrop; ?pat2]] =>
      iAndDestructChoice Hz as Right Hz;
      iDestructHypGo Hz 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)
+  (* [% ...] is always interpreted as an existential; there are [IntoExist]
+  instances in place to handle conjunctions with a pure left-hand side this way
+  as well. *)
   | IList [[IPure ?gallina_id; ?pat2]] => iExistDestructPure gallina_id pat2
   | IList [[?pat1; ?pat2]] => iAndDestructAs pat1 pat2
   | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3d150c749..bb095de55 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -455,6 +455,27 @@ Lemma test_iPure_intro_2 (φ : nat → Prop) P Q R `{!Persistent Q} :
   φ 0 → P -∗ Q → R -∗ ∃ x : nat, <affine> ⌜ φ x ⌝ ∗ ⌜ φ x ⌝.
 Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
 
+(* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
+pure. *)
+Lemma test_pure_and_sep_destruct `{!BiAffine PROP} (φ : Prop) (P : PROP) :
+  ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
+Proof.
+  iIntros "[% [% $]]".
+Qed.
+(* Ensure that [% %] also works when the conjunction is *inside* ⌜...⌝ *)
+Lemma test_pure_inner_and_destruct :
+  ⌜False ∧ True⌝ ⊢@{PROP} False.
+Proof.
+  iIntros "[% %]". done.
+Qed.
+
+(* Ensure that [% %] works as a pattern for an existential with a pure body. *)
+Lemma test_exist_pure_destruct :
+  (∃ x, ⌜ x = 0 ⌝) ⊢@{PROP} True.
+Proof.
+  iIntros "[% %]". done.
+Qed.
+
 Lemma test_fresh P Q:
   (P ∗ Q) -∗ (P ∗ Q).
 Proof.
@@ -1391,8 +1412,8 @@ Abort.
 Lemma test_exists_intro_pattern P (Φ: nat → PROP) :
   P ∗ (∃ y:nat, Φ y) -∗ ∃ x, P ∗ Φ x.
 Proof.
-  iIntros "[HP1 [%y HP2]]".
-  iExists y.
+  iIntros "[HP1 [%yy HP2]]".
+  iExists yy.
   iFrame "HP1 HP2".
 Qed.
 
-- 
GitLab


From 754ee8b236573c24cca3a34cbfcf94bed6059aa4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Mar 2021 18:35:51 +0100
Subject: [PATCH 04/10] changelog

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3ac18c6dd..89a56d939 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,11 +25,12 @@ lemma.
 * Demote the Camera structure on `list` to `iris_staging` since its composition
   is not very well-behaved.
 
-**Changes in `proof_mode`:**
+**Changes in `proofmode`:**
 
 * Add support for pure names `%H` in intro patterns. This is now natively
   supported whereas the previous experimental support required installing
   https://gitlab.mpi-sws.org/iris/string-ident.
+* Add support for destructing existentials with the intro pattern `[% ...]`.
 
 **Changes in `base_logic`:**
 
-- 
GitLab


From 06313482b0eb56bb97aab689feb85d91d0e08dda Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Mar 2021 20:14:40 +0100
Subject: [PATCH 05/10] inline only-once-used helper functions

---
 iris/proofmode/ltac_tactics.v | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 6e3753a4d..832061324 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1426,18 +1426,6 @@ 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
@@ -1459,8 +1447,14 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   (* [% ...] is always interpreted as an existential; there are [IntoExist]
   instances in place to handle conjunctions with a pure left-hand side this way
   as well. *)
-  | IList [[IPure ?gallina_id; ?pat2]] => iExistDestructPure gallina_id pat2
-  | IList [[?pat1; ?pat2]] => iAndDestructAs pat1 pat2
+  | IList [[IPure IGallinaAnon; ?pat2]] =>
+     iExistDestruct Hz as ? Hz; iDestructHypGo Hz pat0 pat2
+  | IList [[IPure (IGallinaNamed ?s); ?pat2]] =>
+     let x := string_to_ident s in iExistDestruct Hz as x 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
   | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
   | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"
 
-- 
GitLab


From 6be1cdd22739c0c315ea889aa8c0f0bda87da16d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Mar 2021 20:17:53 +0100
Subject: [PATCH 06/10] more exist destruct test cases

---
 tests/proofmode.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index bb095de55..9628ea7e4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -457,11 +457,21 @@ Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
 
 (* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
 pure. *)
-Lemma test_pure_and_sep_destruct `{!BiAffine PROP} (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) (P : PROP) :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
+Lemma test_pure_and_sep_destruct_1 (φ : Prop) (P : PROP) :
+  ⌜φ⌝ ∧ (<affine> ⌜φ⌝ ∗ P) -∗ P.
+Proof.
+  iIntros "[% [% $]]".
+Qed.
+Lemma test_pure_and_sep_destruct_2 (φ : Prop) (P : PROP) :
+  ⌜φ⌝ ∧ (⌜φ⌝ ∗ <absorb> P) -∗ <absorb> P.
+Proof.
+  iIntros "[% [% $]]".
+Qed.
 (* Ensure that [% %] also works when the conjunction is *inside* ⌜...⌝ *)
 Lemma test_pure_inner_and_destruct :
   ⌜False ∧ True⌝ ⊢@{PROP} False.
-- 
GitLab


From 260e0593a8887b1e985300444057db2c04386d25 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Mar 2021 20:19:33 +0100
Subject: [PATCH 07/10] extend proof_mode.md

---
 docs/proof_mode.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index b383aed63..b1a84922b 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -328,6 +328,9 @@ _introduction patterns_:
   + Either the proposition `P` or `Q` should be persistent.
   + Either `ipat1` or `ipat2` should be `_`, which results in one of the
     conjuncts to be thrown away.
+- `[% ipat]` : existential elimination. Falls back to (separating) conjunction
+  elimination in case the hypothesis is not an existential, so this pattern also
+  works for (separating) conjunctions with a pure left-hand side.
 - `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
   to destruct nested (separating) conjunctions.
 - `[ipat1|ipat2]` : disjunction elimination.
-- 
GitLab


From 7da8952e3cb5783e9dc91ea3abc60fa2706d08a4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Mar 2021 19:28:58 +0100
Subject: [PATCH 08/10] add more tests

---
 tests/proofmode.v         |  6 +++---
 tests/proofmode_monpred.v | 11 +++++++++++
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9628ea7e4..97aa9604a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -457,17 +457,17 @@ Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
 
 (* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
 pure. *)
-Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) P :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
-Lemma test_pure_and_sep_destruct_1 (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_1 (φ : Prop) P :
   ⌜φ⌝ ∧ (<affine> ⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
-Lemma test_pure_and_sep_destruct_2 (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_2 (φ : Prop) P :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ <absorb> P) -∗ <absorb> P.
 Proof.
   iIntros "[% [% $]]".
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 6e69c5c88..80612f2c0 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -103,6 +103,17 @@ Section tests.
     iAssumption.
   Qed.
 
+  Lemma test_monPred_at_and_pure P i j :
+    (monPred_in j ∧ P) i ⊢ ⌜ j ⊑ i ⌝ ∧ P i.
+  Proof.
+    iDestruct 1 as "[% $]". done.
+  Qed.
+  Lemma test_monPred_at_sep_pure P i j :
+    (monPred_in j ∗ <absorb> P) i ⊢ ⌜ j ⊑ i ⌝ ∧ <absorb> P i.
+  Proof.
+    iDestruct 1 as "[% ?]". auto.
+  Qed.
+
   Context (FU : BiFUpd PROP).
 
   Lemma test_apply_fupd_intro_mask_subseteq E1 E2 P :
-- 
GitLab


From f531cc9d66c5b4f40e53e71c369bd36d5e25aed4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Mar 2021 19:29:21 +0100
Subject: [PATCH 09/10] generalize into_and_sep_affine so that generalizing
 just the conjunction instance for IntoExist is sufficient

---
 iris/proofmode/class_instances.v | 34 ++++++++++++++++----------------
 iris/proofmode/classes.v         |  9 +++++++++
 2 files changed, 26 insertions(+), 17 deletions(-)

diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 90e639c96..d28a5f9d1 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -608,9 +608,9 @@ Proof.
   rewrite /IntoAnd /= intuitionistically_sep
     -and_sep_intuitionistically intuitionistically_and //.
 Qed.
-Global Instance into_and_sep_affine P Q :
+Global Instance into_and_sep_affine p P Q :
   TCOr (Affine P) (Absorbing Q) → TCOr (Absorbing P) (Affine Q) →
-  IntoAnd true (P ∗ Q) P Q.
+  IntoAnd p (P ∗ Q) P Q.
 Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
@@ -807,32 +807,32 @@ 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.
-(* Low-priority instance falling back to treating a conjunction with a pure
-left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as
-[% ...]].
+(* This instance is generalized to let us use [iIntros (P) "..."] and
+[as [% ...]]. There is some risk of backtracking here, but that should only
+happen in failing cases (assuming that appropriate modality commuting instances
+are provided for both conjunctions and existential quantification). The
+alternative of providing specialized instances for cases like ⌜P ∧ Q⌝ turned out
+to not be tenable.
+
 [to_ident_name H] makes the default name [H] when [P] is destructed with
-[iExistDestruct] *)
-Global Instance into_exist_and_pure PQ P Q φ :
+[iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
+Global Instance into_exist_and_pure PQ P Q (φ : Type) :
   IntoAnd false PQ P Q →
   IntoPureT P φ →
-  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100.
+  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 10.
 Proof.
   intros HPQ (φ'&->&?). rewrite /IntoAnd /= in HPQ.
   rewrite /IntoExist HPQ (into_pure P).
   apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
 Qed.
-(* Low-priority instance falling back to treating a sep. conjunction with a pure
-left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as
-[% ...]].
-[to_ident_name H] makes the default name [H] when [P] is destructed with
-[iExistDestruct] *)
-Global Instance into_exist_sep_pure PQ P Q φ :
-  IntoSep PQ P Q →
+(* [to_ident_name H] makes the default name [H] when [P] is destructed with
+[iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
+Global Instance into_exist_sep_pure P Q (φ : Type) :
   IntoPureT P φ →
   TCOr (Affine P) (Absorbing Q) →
-  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100.
+  IntoExist (P ∗ Q) (λ _ : φ, Q) (to_ident_name H).
 Proof.
-  intros HPQ (φ'&->&?) ?. rewrite /IntoSep in HPQ. rewrite /IntoExist HPQ.
+  intros (φ'&->&?) ?. rewrite /IntoExist.
   eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
   rewrite -exist_intro //. apply sep_elim_r, _.
 Qed.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index f4e726483..74472b17b 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -176,12 +176,21 @@ Global Arguments from_and {_} _%I _%I _%I {_}.
 Global Hint Mode FromAnd + ! - - : typeclass_instances.
 Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
+(** The [IntoAnd p P Q1 Q2] class is used (together with [IntoSep]) to handle
+[[H1 H2]] destruct patterns. If [p] is [true] then the destruct is happening in
+the intuitionistic context.
+
+The inputs are [p P] and the outputs are [Q1 Q2]. *)
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
   into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
 Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Global Arguments into_and {_} _ _%I _%I _%I {_}.
 Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
+(** The [IntoSep P Q1 Q2] class is used (together with [IntoAnd]) to handle
+[[H1 H2]] destruct patterns.
+
+The input is [P] and the outputs are [Q1 Q2]. *)
 Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
   into_sep : P ⊢ Q1 ∗ Q2.
 Global Arguments IntoSep {_} _%I _%I _%I : simpl never.
-- 
GitLab


From b861419a0605dadcf40de5d25704370512d354f9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Mar 2021 12:03:45 +0100
Subject: [PATCH 10/10] improve comments

---
 CHANGELOG.md                     |  2 +-
 docs/proof_mode.md               | 14 +++++---------
 iris/proofmode/class_instances.v | 12 ++++++------
 iris/proofmode/classes.v         | 10 +++++-----
 4 files changed, 17 insertions(+), 21 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89a56d939..9ea121fed 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,7 +30,7 @@ lemma.
 * Add support for pure names `%H` in intro patterns. This is now natively
   supported whereas the previous experimental support required installing
   https://gitlab.mpi-sws.org/iris/string-ident.
-* Add support for destructing existentials with the intro pattern `[% ...]`.
+* Add support for destructing existentials with the intro pattern `[%x ...]`.
 
 **Changes in `base_logic`:**
 
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index b1a84922b..072747345 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -328,19 +328,15 @@ _introduction patterns_:
   + Either the proposition `P` or `Q` should be persistent.
   + Either `ipat1` or `ipat2` should be `_`, which results in one of the
     conjuncts to be thrown away.
-- `[% ipat]` : existential elimination. Falls back to (separating) conjunction
-  elimination in case the hypothesis is not an existential, so this pattern also
-  works for (separating) conjunctions with a pure left-hand side.
+- `[%x ipat]`/`[% ipat]` : existential elimination, naming the witness `x` or
+  keeping it anonymous. Falls back to (separating) conjunction elimination in
+  case the hypothesis is not an existential, so this pattern also works for
+  (separating) conjunctions with a pure left-hand side.
 - `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
   to destruct nested (separating) conjunctions.
 - `[ipat1|ipat2]` : disjunction elimination.
 - `[]` : false elimination.
-- `%H` : move the hypothesis to the pure Coq context, and name it `H`. Support
-  for the `%H` introduction pattern requires an implementation of the hook
-  `string_to_ident`. Without an implementation of this hook, the `%H` pattern
-  will fail. We provide an implementation of the hook using Ltac2, which works
-  with Coq 8.11 and later, and can be installed with opam; see
-  [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
+- `%H` : move the hypothesis to the pure Coq context, and name it `H`.
 - `%` : move the hypothesis to the pure Coq context (anonymously). Note that if
   `%` is followed by an identifier, and not another token, a space is needed
   to disambiguate from `%H` above.
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index d28a5f9d1..9b02c4647 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -807,12 +807,12 @@ 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.
-(* This instance is generalized to let us use [iIntros (P) "..."] and
-[as [% ...]]. There is some risk of backtracking here, but that should only
-happen in failing cases (assuming that appropriate modality commuting instances
-are provided for both conjunctions and existential quantification). The
-alternative of providing specialized instances for cases like ⌜P ∧ Q⌝ turned out
-to not be tenable.
+(* This instance is generalized to let us use [iDestruct as (P) "..."] and
+[iIntros "[% ...]"] for conjunctions with a pure left-hand side. There is some
+risk of backtracking here, but that should only happen in failing cases
+(assuming that appropriate modality commuting instances are provided for both
+conjunctions and existential quantification). The alternative of providing
+specialized instances for cases like ⌜P ∧ Q⌝ turned out to not be tenable.
 
 [to_ident_name H] makes the default name [H] when [P] is destructed with
 [iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 74472b17b..b00433254 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -176,9 +176,9 @@ Global Arguments from_and {_} _%I _%I _%I {_}.
 Global Hint Mode FromAnd + ! - - : typeclass_instances.
 Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
-(** The [IntoAnd p P Q1 Q2] class is used (together with [IntoSep]) to handle
-[[H1 H2]] destruct patterns. If [p] is [true] then the destruct is happening in
-the intuitionistic context.
+(** The [IntoAnd p P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
+the intuitionistic context ([p = true]) and patterns where one of the two sides
+is discarded ([p = false]).
 
 The inputs are [p P] and the outputs are [Q1 Q2]. *)
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
@@ -187,8 +187,8 @@ Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Global Arguments into_and {_} _ _%I _%I _%I {_}.
 Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
-(** The [IntoSep P Q1 Q2] class is used (together with [IntoAnd]) to handle
-[[H1 H2]] destruct patterns.
+(** The [IntoSep P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
+the spatial context (except when one side is [_], then [IntoAnd] is used).
 
 The input is [P] and the outputs are [Q1 Q2]. *)
 Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
-- 
GitLab