Add example of "discriminate" limitation

doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst

@@ -525,25 +525,39 @@ This section describes some special purpose tactics to work with
 
 .. tacn:: discriminate {? @induction_arg }
 
-   Proves any goal for which a hypothesis in the form :n:`@term__1 = @term__2`
-   states an impossible structural equality for an inductive type.
-   If :n:`@induction_arg` is not given, it checks all the hypotheses
-   for impossible equalities.
-   For example, :g:`(S (S O)) = (S O)` is impossible.
+   Proves goals for which a hypothesis or a :term:`premise` in
+   the goal that is convertible to the form :n:`@term__1 = @term__2`
+   has inconsistent constructors between the two sides of
+   the equality (i.e., a contradiction).  The tactic also proves goals
+   in the form :n:`@term__1 <> @term__2` that are inconsistent.
+
+   The tactic relies on the fact that constructors of inductive types are injective
+   and disjoint, i.e. if `C1` and `C2` are distinct constructors of an inductive type then
+   :n:`C1 @term__1 = C1 @term__2` implies that :n:`@term__1 = @term__2` (injectivity)
+   and :n:`C1 @term__1 = C2 @term__2` is a contradiction (disjointedness).
+   For example, :g:`S (S O) = S O` is a contradiction: while
+   the outermost constructors are both `S`, the next ones differ (`S` versus `O`).
+
+   The tactic traverses the normal forms of :n:`@term__1` and :n:`@term__2`,
+   looking for subterms placed in the same positions and whose
+   head symbols are different constructors. If such subterms are present, the
+   equality is impossible and the current goal is completed.
+   Otherwise the tactic fails.  Note that opaque constants are not expanded by
+   δ reductions while computing the head normal form.
+
+   Note that :n:`discriminate` doesn't handle contradictory equalities such as
+   :g:`n = S n`.  In this case you must use :tacn:`induction` (see
+   :ref:`example <discriminate_example>`).
+
+   If :n:`@induction_arg` is not given, the tactic checks all the hypotheses
+   and premises in the goal for impossible equalities.
    If provided, :n:`@induction_arg` is a proof of an equality, typically
    specified as the name of a hypothesis.
 
    If no :n:`@induction_arg` is provided and the goal is in the form
    :n:`@term__1 <> @term__2`, then the tactic behaves like
    :n:`intro @ident; discriminate @ident`.
 
-   The tactic traverses the normal forms of :n:`@term__1` and :n:`@term__2`,
-   looking for subterms :g:`u` and :g:`w` placed in the same positions and whose
-   head symbols are different constructors. If such subterms are present, the
-   equality is impossible and the current goal is completed.
-   Otherwise the tactic fails.  Note that opaque constants are not expanded by
-   δ reductions while computing the normal form.
-
    :n:`@ident`  (in :n:`@induction_arg`)
      Checks the hypothesis :n:`@ident` for impossible equalities.
      If :n:`@ident` is not already in the context, this is equivalent to
@@ -570,6 +584,27 @@ This section describes some special purpose tactics to work with
       type of the hypothesis referred to by :token:`natural`, has uninstantiated
       parameters, these parameters are left as existential variables.
 
+.. _discriminate_example:
+
+   .. example:: :n:`discriminate` limitation: proving `n <> S n`
+
+      .. coqtop:: reset in
+
+         Goal forall n:nat, n <> S n.
+         intro n.
+         induction n.
+
+      .. coqtop:: all
+
+         - discriminate.       (* works: O and (S O) start with different constructors *)
+         - Fail discriminate.  (* fails: discriminate doesn't handle this case *)
+           injection.
+
+      .. coqtop:: in
+
+           assumption.
+           Qed.
+
 .. tacn:: injection {? @induction_arg } {? as {* @simple_intropattern } }
 
    Exploits the property that constructors of