Review #2

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

@@ -128,6 +128,8 @@ analysis on inductive or co-inductive objects (see :ref:`variants`).
 
    Performs case analysis by generating a subgoal for each constructor of the
    inductive or co-inductive type in the :n:`@one_term` in :n:`@induction_arg`.
+   :n:`@one_term` (or the conclusion of its type--example
+   :ref:`here<example_destruct_ind_concl>`) must be of inductive or co-inductive type.
    In each new subgoal, the tactic replaces :n:`@one_term` with the associated
    constructor (applied to its arguments).   Unlike :tacn:`induction`,
    :tacn:`destruct` generates no induction hypothesis.
@@ -188,6 +190,25 @@ analysis on inductive or co-inductive objects (see :ref:`variants`).
      Makes the tactic equivalent to
      :tacn:`induction` :n:`{+, @induction_clause } @induction_principle`.
 
+.. _example_destruct_ind_concl:
+
+   .. example:: :tacn:`destruct` on a type with a conclusion that is an inductive type
+
+      .. coqtop:: reset in
+
+         Parameter A B C D : Prop.
+
+      .. coqtop:: all
+
+         Goal (A -> B \/ C) -> D.
+         intros until 1.
+         destruct H.
+         Show 2.
+         Show 3.
+
+      The single tactic `destruct 1` is equivalent to the
+      :tacn:`intros` and :tacn:`destruct` used here.
+
    .. tacn:: edestruct {+, @induction_clause } {? @induction_principle }
 
       If the type of :n:`@one_term` (in :n:`@induction_arg`) has
@@ -260,8 +281,7 @@ Induction
    In the case of dependent products, the tactic tries to find an instance for
    which the induction principle applies and otherwise fails.
 
-   Most parameters behave as they do in :tacn:`destruct`, with the following
-   differences:
+   Most parameters behave as they do in :tacn:`destruct`:
 
    + If :n:`@one_term` (in :n:`@induction_arg`)
      is an identifier :n:`@ident` denoting a quantified variable of the
@@ -284,19 +304,19 @@ Induction
      :n:`induction (@ident)`).
 
    :n:`{+, @induction_clause }`
-     If no :n:`induction_principle` clause is provided, this is equivalent to doing
+     If no :n:`@induction_principle` clause is provided, this is equivalent to doing
      :n:`induction` on the first :n:`@induction_clause` followed by :n:`destruct`
      on any subsequent clauses.
 
    :n:`@induction_principle`
-     :n:`one_term` specifies which :term:`induction principle` to use and, optionally,
+     :n:`@one_term` specifies which :term:`induction principle` to use and, optionally,
      what bindings
      to apply to the induction principle.  The number of :n:`@induction_clause`\s
      must be the same as the number of parameters of the induction principle.
 
      If unspecified, the tactic applies the appropriate :term:`induction principle`
      that was automatically generated when the inductive type was declared based
-     on the type of the goal.
+     on the sort of the goal.
 
    .. exn:: Not an inductive product.
       :undocumented:
@@ -334,12 +354,7 @@ Induction
 
    An older, more basic induction tactic.  Unlike :tacn:`induction`, ``elim`` only
    modifies the goal; it does not modify the :term:`local context`.  We recommend
-   using :tacn:`induction` instead where possible.  :n:`@one_term` must have an inductive
-   type.  The tactic applies the appropriate :term:`induction principle` based
-   on the type of the goal.  (For example, if the local context
-   contains :g:`n : nat` and the current goal is :g:`T` of type :g:`Prop`, then
-   :n:`elim k` is equivalent to :tacn:`apply` :n:`nat_ind with (n:=k)` since
-   `nat_ind` is for `Prop` goals.)
+   using :tacn:`induction` instead where possible.
 
    More generally,
    :n:`elim @one_term` also works when the type of :n:`@one_term` is a statement
@@ -359,10 +374,10 @@ Induction
     :n:`@bindings` clause allows instantiating premises of the type of
     :n:`@one_term`.
 
-.. tacn:: eelim @one_term_with_bindings {? using @one_term {? with @bindings } }
+   .. tacn:: eelim @one_term_with_bindings {? using @one_term {? with @bindings } }
 
-   If the type of :n:`@one_term` has dependent premises, this turns them into
-   existential variables to be resolved later on.
+      If the type of :n:`@one_term` has dependent premises, this turns them into
+      existential variables to be resolved later on.
 
 .. tacn:: elimtype @one_term
 
@@ -449,12 +464,13 @@ Induction
       simple_binder ::= @name
       | ( {+ @name } : @term )
 
-   A primitive tactic to start a proof by induction. Generally,
+   A primitive tactic that starts a proof by induction. Generally,
    higher-level tactics such as :tacn:`induction` or :tacn:`elim`
    are easier to use.
 
-   :n:`@ident` is the name of
-   the induction hypothesis. :n:`@natural` tells on which
+   The :n:`@ident`\s (including the first one before the `with`
+   clause) are the names of
+   the induction hypotheses. :n:`@natural` tells on which
    premise of the current goal the induction acts, starting from 1,
    counting both dependent and non-dependent products, but skipping local
    definitions. The current lemma must be composed of at
@@ -472,7 +488,8 @@ Induction
      are :n:`forall @simple_binder__i, @type__i`.
      The identifiers :n:`@ident` (including the first one before the `with` clause)
      are the names of the induction hypotheses. The identifiers
-     :n:`@name` are the respective names of the premises on which the induction
+     :n:`@name` (in the `{ struct ... }` clauses) are the respective names of
+     the premises on which the induction
      is performed in the statements to be proved (if not given, Coq
      guesses what they are).
 
@@ -485,8 +502,7 @@ Induction
    verification that the use of co-inductive hypotheses is correct is
    done only at the time of registering the lemma in the global environment. To
    know if the use of co-induction hypotheses is correct at some time of
-   the interactive development of a proof, use the command :cmd`Guarded`.
-
+   the interactive development of a proof, use the command :cmd:`Guarded`.
 
    :n:`with {+ ( @ident {* @simple_binder } : @type ) }`
      Starts a proof by mutual co-induction. The statements to be