replace iAndDestruct hack for [% %] by more general IntoExist instances

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.

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"

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.