diff options
| author | Erik Martin-Dorel | 2019-11-01 01:59:07 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-11-01 04:43:15 +0100 |
| commit | f7c078d1a16a9554fb320a85b4c7d33499037484 (patch) | |
| tree | 57b72a08ba6f51e8898922ecae03e969789e122b | |
| parent | 1857d474d06b23df32c16be26225ee174ad4d6c1 (diff) | |
[ssr] Update doc for under w.r.t. setoid-like relations
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3db771b0ba..e70f9d7716 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3757,8 +3757,10 @@ involves the following steps: 4. Then :tacn:`under` checks that the first n subgoals are (quantified) Leibniz equalities, double implications or - registered Setoid equalities between a term and an evar - (e.g. ``m - m = ?F2 m`` in the running example). + registered relations (w.r.t. Class ``RewriteRelation``) between a + term and an evar, e.g. ``m - m = ?F2 m`` in the running example. + (This support for setoid-like relations is enabled as soon as we do + both ``Require Import ssreflect.`` and ``Require Setoid.``) 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. @@ -3770,7 +3772,10 @@ involves the following steps: by using a regular :tacn:`rewrite` tactic. 7. Interactive editing of the first n goals has to be signalled by - using the :tacn:`over` tactic or rewrite rule (see below). + using the :tacn:`over` tactic or rewrite rule (see below), which + requires that the underlying relation is reflexive. (The running + example deals with Leibniz equality, but ``PreOrder`` relations are + also supported, for example.) 8. Finally, a post-processing step is performed in the main goal to keep the name(s) for the bound variables chosen by the user in @@ -3796,6 +3801,10 @@ displayed as ``'Under[ … ]``): This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. +Note that a rewrite rule ``UnderE`` is available as well, if one wants +to "unprotect" the evar, without closing the goal automatically (e.g., +to instantiate it manually with another rule than reflexivity). + .. _under_one_liner: One-liner mode |