Merge branch 'ci/ralf/exists-intro-pattern' into 'master'

Support destructing exists with intro patterns

Closes #310

See merge request iris/iris!658

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 `[%x ...]`.
 
 **Changes in `base_logic`:**
 

docs/proof_mode.md

@@ -328,6 +328,10 @@ _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.
+- `[%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.

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,15 +807,27 @@ 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 [?] *)
-Global Instance into_exist_and_pure P Q φ :
-  IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q) (to_ident_name H).
+(* 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]. *)
+Global Instance into_exist_and_pure PQ P Q (φ : Type) :
+  IntoAnd false PQ P Q →
+  IntoPureT P φ →
+  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 10.
 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 introduced with [?] *)
-Global Instance into_exist_sep_pure 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 (P ∗ Q) (λ _ : φ, Q) (to_ident_name H).

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 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) :=
   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 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) :=
   into_sep : P ⊢ Q1 ∗ Q2.
 Global Arguments IntoSep {_} _%I _%I _%I : simpl never.

iris/proofmode/ltac_tactics.v

@@ -1444,6 +1444,14 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
   | IList [[IDrop; ?pat2]] =>
      iAndDestructChoice Hz as Right Hz;
      iDestructHypGo Hz pat0 pat2
+  (* [% ...] 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 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

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] rather than (?) to indicate iExistDestruct *)
+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.
 
@@ -446,6 +455,37 @@ 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_affine `{!BiAffine PROP} (φ : Prop) P :
+  ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
+Proof.
+  iIntros "[% [% $]]".
+Qed.
+Lemma test_pure_and_sep_destruct_1 (φ : Prop) P :
+  ⌜φ⌝ ∧ (<affine> ⌜φ⌝ ∗ P) -∗ P.
+Proof.
+  iIntros "[% [% $]]".
+Qed.
+Lemma test_pure_and_sep_destruct_2 (φ : Prop) P :
+  ⌜φ⌝ ∧ (⌜φ⌝ ∗ <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.
+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.
@@ -1379,6 +1419,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 [%yy HP2]]".
+  iExists yy.
+  iFrame "HP1 HP2".
+Qed.
+
 End pure_name_tests.
 
 Section tactic_tests.

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 :