Commit b861419a authored by Ralf Jung's avatar Ralf Jung
Browse files

improve comments

parent f531cc9d
...@@ -30,7 +30,7 @@ lemma. ...@@ -30,7 +30,7 @@ lemma.
* Add support for pure names `%H` in intro patterns. This is now natively * Add support for pure names `%H` in intro patterns. This is now natively
supported whereas the previous experimental support required installing supported whereas the previous experimental support required installing
https://gitlab.mpi-sws.org/iris/string-ident. 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`:** **Changes in `base_logic`:**
......
...@@ -328,19 +328,15 @@ _introduction patterns_: ...@@ -328,19 +328,15 @@ _introduction patterns_:
+ Either the proposition `P` or `Q` should be persistent. + Either the proposition `P` or `Q` should be persistent.
+ Either `ipat1` or `ipat2` should be `_`, which results in one of the + Either `ipat1` or `ipat2` should be `_`, which results in one of the
conjuncts to be thrown away. conjuncts to be thrown away.
- `[% ipat]` : existential elimination. Falls back to (separating) conjunction - `[%x ipat]`/`[% ipat]` : existential elimination, naming the witness `x` or
elimination in case the hypothesis is not an existential, so this pattern also keeping it anonymous. Falls back to (separating) conjunction elimination in
works for (separating) conjunctions with a pure left-hand side. 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 ..]]` - `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
to destruct nested (separating) conjunctions. to destruct nested (separating) conjunctions.
- `[ipat1|ipat2]` : disjunction elimination. - `[ipat1|ipat2]` : disjunction elimination.
- `[]` : false elimination. - `[]` : false elimination.
- `%H` : move the hypothesis to the pure Coq context, and name it `H`. Support - `%H` : move the hypothesis to the pure Coq context, and name it `H`.
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.
- `%` : move the hypothesis to the pure Coq context (anonymously). Note that if - `%` : 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 `%` is followed by an identifier, and not another token, a space is needed
to disambiguate from `%H` above. to disambiguate from `%H` above.
......
...@@ -807,12 +807,12 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed. ...@@ -807,12 +807,12 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
Global Instance into_exist_intuitionistically {A} P (Φ : A PROP) name : Global Instance into_exist_intuitionistically {A} P (Φ : A PROP) name :
IntoExist P Φ name IntoExist ( P) (λ a, (Φ a))%I name. IntoExist P Φ name IntoExist ( P) (λ a, (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed. Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
(* This instance is generalized to let us use [iIntros (P) "..."] and (* This instance is generalized to let us use [iDestruct as (P) "..."] and
[as [% ...]]. There is some risk of backtracking here, but that should only [iIntros "[% ...]"] for conjunctions with a pure left-hand side. There is some
happen in failing cases (assuming that appropriate modality commuting instances risk of backtracking here, but that should only happen in failing cases
are provided for both conjunctions and existential quantification). The (assuming that appropriate modality commuting instances are provided for both
alternative of providing specialized instances for cases like ⌜P ∧ Q⌝ turned out conjunctions and existential quantification). The alternative of providing
to not be tenable. 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 [to_ident_name H] makes the default name [H] when [P] is destructed with
[iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *) [iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
......
...@@ -176,9 +176,9 @@ Global Arguments from_and {_} _%I _%I _%I {_}. ...@@ -176,9 +176,9 @@ Global Arguments from_and {_} _%I _%I _%I {_}.
Global Hint Mode FromAnd + ! - - : typeclass_instances. Global Hint Mode FromAnd + ! - - : typeclass_instances.
Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *) Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
(** The [IntoAnd p P Q1 Q2] class is used (together with [IntoSep]) to handle (** The [IntoAnd p P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
[[H1 H2]] destruct patterns. If [p] is [true] then the destruct is happening in the intuitionistic context ([p = true]) and patterns where one of the two sides
the intuitionistic context. is discarded ([p = false]).
The inputs are [p P] and the outputs are [Q1 Q2]. *) The inputs are [p P] and the outputs are [Q1 Q2]. *)
Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) := Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
...@@ -187,8 +187,8 @@ Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never. ...@@ -187,8 +187,8 @@ Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Global Arguments into_and {_} _ _%I _%I _%I {_}. Global Arguments into_and {_} _ _%I _%I _%I {_}.
Global Hint Mode IntoAnd + + ! - - : typeclass_instances. Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
(** The [IntoSep P Q1 Q2] class is used (together with [IntoAnd]) to handle (** The [IntoSep P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
[[H1 H2]] destruct patterns. the spatial context (except when one side is [_], then [IntoAnd] is used).
The input is [P] and the outputs are [Q1 Q2]. *) The input is [P] and the outputs are [Q1 Q2]. *)
Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) := Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment