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] 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