Merge PR #7284: [sphinx] Start fixing SSR chapter.

2 files changed, 103 insertions, 129 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 63cd0f3ea..3b2009657 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -37,7 +37,7 @@ bookkeeping is performed on the conclusion of the goal, using for that
 purpose a couple of syntactic constructions behaving similar to tacticals
 (and often named as such in this chapter). The ``:`` tactical moves hypotheses
 from the context to the conclusion, while ``=>`` moves hypotheses from the
-conclusion to the context, and in moves back and forth an hypothesis from the
+conclusion to the context, and ``in`` moves back and forth an hypothesis from the
 context to the conclusion for the time of applying an action to it.
 
 While naming hypotheses is commonly done by means of an ``as`` clause in the
@@ -47,20 +47,22 @@ often followed by ``=>`` to explicitly name them. While generalizing the
 goal is normally not explicitly needed in Chapter :ref:`tactics`, it is an
 explicit operation performed by ``:``.
 
+.. seealso:: :ref:`bookkeeping_ssr`
+
 Beside the difference of bookkeeping model, this chapter includes
 specific tactics which have no explicit counterpart in Chapter :ref:`tactics`
-such as tactics to mix forward steps and generalizations as generally
-have or without loss.
+such as tactics to mix forward steps and generalizations as
+:tacn:`generally have` or :tacn:`without loss`.
 
 |SSR| adopts the point of view that rewriting, definition
 expansion and partial evaluation participate all to a same concept of
 rewriting a goal in a larger sense. As such, all these functionalities
-are provided by the rewrite tactic.
+are provided by the :tacn:`rewrite <rewrite (ssreflect)>` tactic.
 
 |SSR| includes a little language of patterns to select subterms in
 tactics or tacticals where it matters. Its most notable application is
-in the rewrite tactic, where patterns are used to specify where the
-rewriting step has to take place.
+in the :tacn:`rewrite <rewrite (ssreflect)>` tactic, where patterns are
+used to specify where the rewriting step has to take place.
 
 Finally, |SSR| supports so-called reflection steps, typically
 allowing to switch back and forth between the computational view and
@@ -87,20 +89,24 @@ Getting started
 ~~~~~~~~~~~~~~~
 
 To be available, the tactics presented in this manual need the
-following minimal set of libraries to loaded: ``ssreflect.v``,
+following minimal set of libraries to be loaded: ``ssreflect.v``,
 ``ssrfun.v`` and ``ssrbool.v``.
 Moreover, these tactics come with a methodology
 specific to the authors of |SSR| and which requires a few options
 to be set in a different way than in their default way. All in all,
 this corresponds to working in the following context:
 
-.. coqtop:: all
+.. coqtop:: in
 
    From Coq Require Import ssreflect ssrfun ssrbool.
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.
 
+.. seealso::
+   :opt:`Implicit Arguments`, :opt:`Strict Implicit`,
+   :opt:`Printing Implicit Defensive`
+
 .. _compatibility_issues_ssr:
 
 
@@ -114,14 +120,14 @@ compatible with the rest of |Coq|, up to a few discrepancies:
 + New keywords (``is``) might clash with variable, constant, tactic or
   tactical names, or with quasi-keywords in tactic or vernacular
   notations.
-+ New tactic(al)s names (``last``, ``done``, ``have``, ``suffices``,
-  ``suff``, ``without loss``, ``wlog``, ``congr``, ``unlock``)
++ New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`,
+  :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`)
   might clash with user tactic names.
 + Identifiers with both leading and trailing ``_``, such as ``_x_``, are
   reserved by |SSR| and cannot appear in scripts.
-+ The extensions to the rewrite tactic are partly incompatible with those
++ The extensions to the :tacn:`rewrite` tactic are partly incompatible with those
   available in current versions of |Coq|; in particular: ``rewrite .. in
-  (type of k)`` or ``rewrite .. in *`` or any other variant of ``rewrite``
+  (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite`
   will not work, and the |SSR| syntax and semantics for occurrence selection
   and rule chaining is different. Use an explicit rewrite direction
   (``rewrite <- …`` or ``rewrite -> …``) to access the |Coq| rewrite tactic.
@@ -139,7 +145,7 @@ compatible with the rest of |Coq|, up to a few discrepancies:
   Note that the full
   syntax of |SSR|’s rewrite and reserved identifiers are enabled
   only if the ssreflect module has been required and if ``SsrSyntax`` has
-  been imported. Thus a file that requires (without importing) ssreflect
+  been imported. Thus a file that requires (without importing) ``ssreflect``
   and imports ``SsrSyntax``, can be required and imported without
   automatically enabling |SSR|’s extended rewrite syntax and
   reserved identifiers.
@@ -148,9 +154,10 @@ compatible with the rest of |Coq|, up to a few discrepancies:
   such as have, set and pose.
 + The generalization of if statements to non-Boolean conditions is turned off
   by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the
-  ``sumXXX`` types (declared in ``ssrfun.v``) and the ``if`` *term* ``is`` *pattern* ``then``
-  *term* ``else`` *term* construct (see :ref:`pattern_conditional_ssr`).  To use the
-  generalized form, turn off the |SSR| Boolean if notation using the command:
+  ``sumXXX`` types (declared in ``ssrfun.v``) and the
+  :n:`if @term is @pattern then @term else @term` construct
+  (see :ref:`pattern_conditional_ssr`).  To use the
+  generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
   ``Close Scope boolean_if_scope``.
 + The following two options can be unset to disable the incompatible
   rewrite syntax and allow reserved identifiers to appear in scripts.
@@ -191,9 +198,9 @@ construct differs from the latter in that
 + The pattern can be nested (deep pattern matching), in particular,
   this allows expression of the form:
 
-.. coqtop:: in
+.. coqdoc::
 
-  let: exist (x, y) p_xy := Hp in … .
+   let: exist (x, y) p_xy := Hp in … .
 
 + The destructured constructor is explicitly given in the pattern, and
   is used for type inference.
@@ -222,11 +229,7 @@ construct differs from the latter in that
 
 
 The ``let:`` construct is just (more legible) notation for the primitive
-|Gallina| expression
-
-.. coqtop:: in
-
-   match term with pattern => term end.
+|Gallina| expression :n:`match @term with @pattern => @term end`.
 
 The |SSR| destructuring assignment supports all the dependent
 match annotations; the full syntax is
@@ -286,28 +289,17 @@ assignment with a refutable pattern, adapted to the pure functional
 setting of |Gallina|, which lacks a ``Match_Failure`` exception.
 
 Like ``let:`` above, the ``if…is`` construct is just (more legible) notation
-for the primitive |Gallina| expression:
-
-.. coqtop:: in
-
-   match term with pattern => term | _ => term end.
+for the primitive |Gallina| expression
+:n:`match @term with @pattern => @term | _ => @term end`.
 
 Similarly, it will always be displayed as the expansion of this form
 in terms of primitive match expressions (where the default expression
 may be replicated).
 
 Explicit pattern testing also largely subsumes the generalization of
-the if construct to all binary data types; compare:
-
-.. coqtop:: in
-
-   if term is inl _ then term else term.
-
-and:
-
-.. coqtop:: in
-
-   if term then term else term.
+the ``if`` construct to all binary data types; compare
+:n:`if @term is inl _ then @term else @term` and
+:n:`if @term then @term else @term`.
 
 The latter appears to be marginally shorter, but it is quite
 ambiguous, and indeed often requires an explicit annotation
@@ -434,7 +426,7 @@ a functional constant, whose implicit arguments are prenex, i.e., the first
 As these prenex implicit arguments are ubiquitous and have often large
 display strings, it is strongly recommended to change the default
 display settings of |Coq| so that they are not printed (except after
-a ``Set Printing All command``). All |SSR| library files thus start
+a ``Set Printing All`` command). All |SSR| library files thus start
 with the incantation
 
 .. coqtop:: all undo
@@ -496,19 +488,10 @@ Definitions
 .. tacn:: pose
    :name: pose (ssreflect)
 
-This tactic allows to add a defined constant to a proof context.
-|SSR| generalizes this tactic in several ways. In particular, the
-|SSR| pose tactic supports *open syntax*: the body of the
-definition does not need surrounding parentheses. For instance:
-
-.. coqtop:: reset
-
-   From Coq Require Import ssreflect.
-   Set Implicit Arguments.
-   Unset Strict Implicit.
-   Unset Printing Implicit Defensive.
-   Lemma test : True.
-   Proof.
+   This tactic allows to add a defined constant to a proof context.
+   |SSR| generalizes this tactic in several ways. In particular, the
+   |SSR| pose tactic supports *open syntax*: the body of the
+   definition does not need surrounding parentheses. For instance:
 
 .. coqtop:: in
 
@@ -518,10 +501,18 @@ is a valid tactic expression.
 
 The pose tactic is also improved for the local definition of higher
 order terms. Local definitions of functions can use the same syntax as
-global ones. For example, the tactic ``pose`` supoprts parameters:
+global ones.
+For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters:
 
 .. example::
 
+   .. coqtop:: reset
+
+      From Coq Require Import ssreflect.
+      Set Implicit Arguments.
+      Unset Strict Implicit.
+      Unset Printing Implicit Defensive.
+
    .. coqtop:: all
 
       Lemma test : True.
@@ -631,7 +622,7 @@ where:
   surrounding the second :token:`term` are mandatory.
 + In the occurrence switch :token:`occ_switch`, if the first element of the
   list is a natural, this element should be a number, and not an Ltac
-  variable. The empty list {} is not interpreted as a valid occurrence
+  variable. The empty list ``{}`` is not interpreted as a valid occurrence
   switch.
 
 The tactic:
@@ -667,7 +658,7 @@ The tactic first tries to find a subterm of the goal matching
 the second :token:`term`
 (and its type), and stops at the first subterm it finds. Then
 the occurrences of this subterm selected by the optional :token:`occ_switch`
-are replaced by :token:`ident` and a definition ``ident := term``
+are replaced by :token:`ident` and a definition :n:`@ident := @term`
 is added to the
 context. If no :token:`occ_switch` is present, then all the occurrences are
 abstracted.
@@ -676,20 +667,20 @@ abstracted.
 Matching
 ````````
 
-The matching algorithm compares a pattern ``term`` with a subterm of the
+The matching algorithm compares a pattern :token:`term` with a subterm of the
 goal by comparing their heads and then pairwise unifying their
 arguments (modulo conversion). Head symbols match under the following
 conditions:
 
 
-+ If the head of ``term`` is a constant, then it should be syntactically
++ If the head of :token:`term` is a constant, then it should be syntactically
   equal to the head symbol of the subterm.
 + If this head is a projection of a canonical structure, then
   canonical structure equations are used for the matching.
 + If the head of term is *not* a constant, the subterm should have the
   same structure (λ abstraction,let…in structure …).
-+ If the head of ``term`` is a hole, the subterm should have at least as
-  many arguments as ``term``.
++ If the head of :token:`term` is a hole, the subterm should have at least as
+  many arguments as :token:`term`.
 
 .. example::
 
@@ -1082,7 +1073,7 @@ constants to the goal.
 
 Because they are tacticals, ``:`` and ``=>`` can be combined, as in
 
-.. coqtop: in
+.. coqtop:: in
 
    move: m le_n_m => p le_n_p.
 
@@ -1147,9 +1138,7 @@ induction on the top variable ``m`` with
    elim=> [|m IHm] n le_n.
 
 The general form of the localization tactical in is also best
-explained in terms of the goal stack:
-
-.. coqtop:: in
+explained in terms of the goal stack::
 
    tactic in a H1 H2 *.
 
@@ -1212,8 +1201,8 @@ product or a ``let…in``, and performs ``hnf`` otherwise.
 
 Of course this tactic is most often used in combination with the
 bookkeeping tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). These
-combinations mostly subsume the ``intros``, ``generalize``, ``revert``, ``rename``,
-``clear`` and ``pattern`` tactics.
+combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, :tacn:`revert`, :tacn:`rename`,
+:tacn:`clear` and :tacn:`pattern` tactics.
 
 
 The case tactic
@@ -1229,15 +1218,11 @@ The |SSR| case tactic has a special behavior on equalities. If the
 top assumption of the goal is an equality, the case tactic “destructs”
 it as a set of equalities between the constructor arguments of its
 left and right hand sides, as per the tactic injection. For example,
-``case`` changes the goal
-
-.. coqtop:: in
+``case`` changes the goal::
 
    (x, y) = (1, 2) -> G.
 
-into
-
-.. coqtop:: in
+into::
 
    x = 1 -> y = 2 -> G.
 
@@ -1289,9 +1274,7 @@ In fact the |SSR| tactic:
 .. tacn:: apply
    :name: apply (ssreflect)
 
-is a synonym for:
-
-.. coqtop:: in
+is a synonym for::
 
    intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top.
 
@@ -1322,18 +1305,14 @@ existential metavariables of sort Prop.
 
    Note that the last ``_`` of the tactic
    ``apply: (ex_intro _ (exist _ y _))``
-   represents a proof that ``y < 3``. Instead of generating the goal
-
-   .. coqtop:: in
+   represents a proof that ``y < 3``. Instead of generating the goal::
 
       0 < proj1_sig (exist (fun n : nat => n < 3) y ?Goal).
 
    the system tries to prove ``y < 3`` calling the trivial tactic.
    If it succeeds, let’s say because the context contains
    ``H : y < 3``, then the
-   system generates the following goal:
-
-   .. coqtop:: in
+   system generates the following goal::
 
       0 < proj1_sig (exist (fun n => n < 3) y H).
 
@@ -1579,7 +1558,7 @@ variables or assumptions from the goal.
 An :token:`s_item` can simplify the set of subgoals or the subgoals themselves:
 
 + ``//`` removes all the “trivial” subgoals that can be resolved by the
-  |SSR| tactic ``done`` described in :ref:`terminators_ssr`, i.e.,
+  |SSR| tactic :tacn:`done` described in :ref:`terminators_ssr`, i.e.,
   it executes ``try done``.
 + ``/=`` simplifies the goal by performing partial evaluation, as per the
   tactic ``simpl`` [#5]_.
@@ -1737,7 +1716,7 @@ new constant as an equation. The tactic:
 
 .. coqtop:: in
 
-  move En: (size l) => n.
+   move En: (size l) => n.
 
 where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and
 adds the fact ``En : size l = n`` to the context.
@@ -1745,7 +1724,7 @@ This is quite different from:
 
 .. coqtop:: in
 
-  pose n := (size l).
+   pose n := (size l).
 
 which generates a definition ``n := (size l)``. It is not possible to
 generalize or rewrite such a definition; on the other hand, it is
@@ -1834,7 +1813,7 @@ compact syntax:
 
 .. coqtop:: in
 
-  case: {2}_ / eqP.
+   case: {2}_ / eqP.
 
 where ``_`` is interpreted as ``(_ == _)`` since
 ``eqP T a b : reflect (a = b) (a == b)`` and reflect is a type family with
@@ -1999,19 +1978,9 @@ into a closing one (similar to now). Its general syntax is:
 .. tacn:: by @tactic
    :name: by
 
-The Ltac expression:
-
-.. coqtop:: in
-
-   by [@tactic | [@tactic | …].
-
-is equivalent to:
-
-.. coqtop:: in
-
-   [by @tactic | by @tactic | ...].
-
-and this form should be preferred to the former.
+The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to
+:n:`[by @tactic | by @tactic | ...]` and this form should be preferred
+to the former.
 
 In the script provided as example in section :ref:`indentation_ssr`, the
 paragraph corresponding to each sub-case ends with a tactic line prefixed
@@ -2021,20 +1990,13 @@ with a ``by``, like in:
 
    by apply/eqP; rewrite -dvdn1.
 
-The by tactical is implemented using the user-defined, and extensible
-done tactic. This done tactic tries to solve the current goal by some
-trivial means and fails if it doesn’t succeed. Indeed, the tactic
-expression:
-
-.. coqtop:: in
+.. tacn:: done
+   :name: done
 
-   by tactic.
-
-is equivalent to:
-
-.. coqtop:: in
-
-   tactic; done.
+The :tacn:`by` tactical is implemented using the user-defined, and extensible
+:tacn:`done` tactic. This :tacn:`done` tactic tries to solve the current goal by some
+trivial means and fails if it doesn’t succeed. Indeed, the tactic
+expression :n:`by @tactic` is equivalent to :n:`@tactic; done`.
 
 Conversely, the tactic
 
@@ -2735,7 +2697,7 @@ type classes inference.
   Full inference for ``ty``. The first subgoal demands a
   proof of such instantiated statement.
 
-+ coqtop::
++ .. coqdoc::
 
      have foo : ty := .
 
@@ -2817,21 +2779,23 @@ Another useful construct is reduction, showing that a particular case
 is in fact general enough to prove a general property. This kind of
 reasoning step usually starts with: “Without loss of generality, we
 can suppose that …”. Formally, this corresponds to the proof of a goal
-G by introducing a cut wlog_statement -> G. Hence the user shall
-provide a proof for both (wlog_statement -> G) -> G and
-wlog_statement -> G. However, such cuts are usually rather
+``G`` by introducing a cut ``wlog_statement -> G``. Hence the user shall
+provide a proof for both ``(wlog_statement -> G) -> G`` and
+``wlog_statement -> G``. However, such cuts are usually rather
 painful to perform by
-hand, because the statement wlog_statement is tedious to write by hand,
+hand, because the statement ``wlog_statement`` is tedious to write by hand,
 and sometimes even to read.
 
-|SSR| implements this kind of reasoning step through the without
-loss tactic, whose short name is ``wlog``. It offers support to describe
+|SSR| implements this kind of reasoning step through the :tacn:`without loss`
+tactic, whose short name is :tacn:`wlog`. It offers support to describe
 the shape of the cut statements, by providing the simplifying
 hypothesis and by pointing at the elements of the initial goals which
 should be generalized. The general syntax of without loss is:
 
 .. tacn:: wlog {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term
    :name: wlog
+.. tacv:: without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term
+   :name: without loss
 
 where each :token:`ident` is a constant in the context
 of the goal. Open syntax is supported for :token:`term`.
@@ -2839,13 +2803,14 @@ of the goal. Open syntax is supported for :token:`term`.
 In its defective form:
 
 .. tacv:: wlog: / @term
+.. tacv:: without loss: / @term
 
 
 on a goal G, it creates two subgoals: a first one to prove the
 formula (term -> G) -> G and a second one to prove the formula
 term -> G.
 
-If the optional list of :token:`itent` is present
+If the optional list of :token:`ident` is present
 on the left side of ``/``, these constants are generalized in the
 premise (term -> G) of the first subgoal. By default bodies of local
 definitions are erased. This behavior can be inhibited by prefixing the
@@ -2858,9 +2823,9 @@ In the second subgoal, the tactic:
    move=> clear_switch i_item.
 
 is performed if at least one of these optional switches is present in
-the ``wlog`` tactic.
+the :tacn:`wlog` tactic.
 
-The ``wlog`` tactic is specially useful when a symmetry argument
+The :tacn:`wlog` tactic is specially useful when a symmetry argument
 simplifies a proof. Here is an example showing the beginning of the
 proof that quotient and reminder of natural number euclidean division
 are unique.
@@ -2881,9 +2846,10 @@ are unique.
      wlog: q1 q2 r1 r2 / q1 <= q2.
        by case (le_gt_dec q1 q2)=> H; last symmetry; eauto with arith.
 
-The ``wlog suff`` variant is simpler, since it cuts wlog_statement instead
-of wlog_statement -> G. It thus opens the goals wlog_statement -> G
-and wlog_statement.
+The ``wlog suff`` variant is simpler, since it cuts ``wlog_statement`` instead
+of ``wlog_statement -> G``. It thus opens the goals
+``wlog_statement -> G``
+and ``wlog_statement``.
 
 In its simplest form the ``generally have : …`` tactic is equivalent to
 ``wlog suff : …`` followed by last first. When the ``have`` tactic is used
@@ -2922,7 +2888,7 @@ Advanced generalization
 The complete syntax for the items on the left hand side of the ``/``
 separator is the following one:
 
-.. tacv wlog … : {? @clear_switch | {? @  } @ident | ( {? @  } @ident := @c_pattern) } / @term
+.. tacv:: wlog … : {? @clear_switch | {? @  } @ident | ( {? @  } @ident := @c_pattern) } / @term
 
 Clear operations are intertwined with generalization operations. This
 helps in particular avoiding dependency issues while generalizing some
@@ -4684,9 +4650,11 @@ Note that the goal interpretation view mechanism supports both ``apply``
 and ``exact`` tactics. As expected, a goal interpretation view command
 exact/term should solve the current goal or it will fail.
 
-*Warning* Goal interpretation view tactics are *not* compatible with
-the bookkeeping tactical ``=>`` since this would be redundant with the
-``apply: term => _`` construction.
+.. warning::
+
+   Goal interpretation view tactics are *not* compatible with
+   the bookkeeping tactical ``=>`` since this would be redundant with the
+   ``apply: term => _`` construction.
 
 
 Boolean reflection
@@ -5390,6 +5358,8 @@ rewrite  see :ref:`rewriting_ssr`
 .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term
 .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic }
+.. tacv:: generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic }
+   :name: generally have
 
 forward  chaining see :ref:`structure_ssr`
 
@@ -5399,7 +5369,11 @@ forward  chaining see :ref:`structure_ssr`
 specializing see :ref:`structure_ssr`
 
 .. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+   :name: suff
+.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+   :name: suffices
 .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
+.. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 
 backchaining see :ref:`structure_ssr`
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 90ca0da43..29c2f8b81 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -971,7 +971,7 @@ quantification or an implication.
       move H0 before H.
 
 .. tacn:: rename @ident into @ident
-   :name: rename ... into ...
+   :name: rename
 
 This renames hypothesis :n:`@ident` into :n:`@ident` in the current context.
 The name of the hypothesis in the proof-term, however, is left unchanged.