diff --git a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst b/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst index 6675cd07e26f6..c3c9a5aa77f17 100644 --- a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst +++ b/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`) 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