==============================
Reasoning with inductive types
==============================

Applying constructors
---------------------

The tactics presented here specialize :tacn:`apply` and
:tacn:`eapply` to constructors of inductive types.

.. tacn:: constructor {? @nat_or_var } {? with @bindings }

   First does :n:`repeat intro; hnf` on the goal.  If the result is an inductive
   type, then apply the appropriate constructor(s), and otherwise fail.
   If :n:`@nat_or_var` is specified and has the
   value `i`, it uses :n:`apply c__i`, where :n:`c__i` is the i-th constructor
   of :g:`I`.  If not specified, the tactic tries all the constructors,
   which can result in more than one success (e.g. for `\\/`) when using
   backtracking tactics such as `constructor; ...`.  See :tacn:`ltac-seq`.

   :n:`{? with @bindings }`
     If specified, the :n:`apply` is done as :n:`apply … with @bindings`.

     .. warning::

        The terms in :token:`bindings` are checked in the context
        where constructor is executed and not in the context where :tacn:`apply`
        is executed (the introductions are not taken into account).

   .. exn:: Not an inductive product.
      :undocumented:

   .. exn:: Not enough constructors.
      :undocumented:

   .. exn:: The type has no constructors.
      :undocumented:

.. tacn:: split {? with @bindings }

   Equivalent to :n:`constructor 1 {? with @bindings }` when the
   conclusion is an inductive type with a single constructor.  The :n:`@bindings`
   specify any parameters required for the constructor. It is
   typically used to split conjunctions in the conclusion such as `A /\\ B` into
   two new goals `A` and `B`.

.. tacn:: exists {*, @bindings }

   Equivalent to :n:`constructor 1 with @bindings__i` for each set of bindings
   (or just :n:`constructor 1` if there are no :n:`@bindings`)
   when the conclusion is an
   inductive type with a single constructor.  It is typically used on
   existential quantifications in the form `exists x, P x.`

   .. exn:: Not an inductive goal with 1 constructor.
      :undocumented:

.. tacn:: left {? with @bindings }
          right {? with @bindings }

   These tactics apply only if :g:`I` has two constructors, for
   instance in the case of a disjunction `A \\/ B`.
   Then they are respectively equivalent to
   :n:`constructor 1 {? with @bindings }` and
   :n:`constructor 2 {? with @bindings }`.

   .. exn:: Not an inductive goal with 2 constructors.
      :undocumented:

.. tacn:: econstructor {? @nat_or_var {? with @bindings } }
          eexists {*, @bindings }
          esplit {? with @bindings }
          eleft {? with @bindings }
          eright {? with @bindings }

   These tactics behave like :tacn:`constructor`,
   :tacn:`exists`, :tacn:`split`, :tacn:`left` and :tacn:`right`,
   but they introduce existential variables instead of failing
   when a variable can't be instantiated
   (cf. :tacn:`eapply` and :tacn:`apply`).

.. example:: :tacn:`constructor`, :tacn:`left` and :tacn:`right`

   .. coqtop:: reset all

      Print or.  (* or, represented by \/, has two constructors, or_introl and or_intror *)
      Goal  forall P1 P2 : Prop, P1 -> P1 \/ P2.
      constructor 1.  (* equivalent to "left" *)
      apply H.  (* success *)

   In contrast, we won't be able to complete the proof if we select constructor 2:

   .. coqtop:: reset none

      Goal  forall P1 P2 : Prop, P1 -> P1 \/ P2.

   .. coqtop:: all

      constructor 2.  (* equivalent to "right" *)

   You can also apply a constructor by name:

   .. coqtop:: reset none

      Goal  forall P1 P2 : Prop, P1 -> P1 \/ P2.

   .. coqtop:: all

      intros; apply or_introl.  (* equivalent to "left" *)


.. _CaseAnalysisAndInduction:

Case analysis
-------------

The tactics in this section implement case
analysis on inductive or coinductive objects (see :ref:`variants`).

.. comment Notes contrasting the various case analysis tactics:
   https://github.com/coq/coq/pull/14676#discussion_r697904963

.. tacn:: destruct {+, @induction_clause } {? @induction_principle }

   .. insertprodn induction_clause induction_arg

   .. prodn::
      induction_clause ::= @induction_arg {? as @or_and_intropattern } {? eqn : @naming_intropattern } {? @occurrences }
      induction_arg ::= @one_term_with_bindings
      | @natural

   Performs case analysis by generating a subgoal for each constructor of the
   inductive or coinductive type selected by :n:`@induction_arg`.  The selected
   subterm, after possibly doing an :tacn:`intros`, must have
   an inductive or coinductive type.  Unlike :tacn:`induction`,
   :n:`destruct` generates no induction hypothesis.

   In each new subgoal, the tactic replaces the selected subterm with the associated
   constructor applied to its arguments, if any.

   :n:`{+, @induction_clause }`
     Giving multiple :n:`@induction_clause`\s is equivalent to applying :n:`destruct`
     serially on each :n:`@induction_clause`.

   :n:`@induction_arg`
     + If :n:`@one_term` (in :n:`@one_term_with_bindings`)
       is an identifier :n:`@ident`:

       + If :n:`@ident` denotes a quantified variable of the
         goal, then :n:`destruct @ident` behaves like
         :tacn:`intros` :n:`until @ident; destruct @ident`.

       + If :n:`@ident` is no longer dependent in the
         goal after application of :n:`destruct`, it is erased. To avoid erasure,
         use parentheses, as in :n:`destruct (@ident)`.

     + :n:`@one_term` may contain holes that are denoted by “_”. In this case,
       the tactic selects the first subterm that matches the pattern and performs
       case analysis using that subterm.
     + If :n:`@induction_arg` is a :n:`@natural`, then :n:`destruct @natural` behaves like
       :n:`intros until @natural` followed by :n:`destruct` applied to the last
       introduced hypothesis.

   :n:`as @or_and_intropattern`
      Provides names for (or applies further transformations to)
      the variables and hypotheses introduced in each new subgoal.  The
      :token:`or_and_intropattern` must have one :n:`{* @intropattern }`
      for each constructor, given in the order in which the constructors are
      defined.  If there are not enough names, Coq picks fresh names.
      Inner :n:`intropattern`\s can also split introduced hypotheses into
      multiple hypotheses or subgoals.

   :n:`eqn : @naming_intropattern`
      Generates a new hypothesis in each new subgoal that is an equality between
      the term being case-analyzed and the associated constructor (applied to
      its arguments).  The name of the new item may be specified in the
      :n:`@naming_intropattern`.

   :n:`with @bindings`  (in :n:`@one_term_with_bindings`)
      Provides explicit instances for
      the :term:`dependent premises <dependent premise>` of the type of
      :token:`one_term`.

   :n:`@occurrences`
     Selects specific subterms of the goal and/or hypotheses to apply
     the tactic to.  See :ref:`Occurrence clauses <occurrenceclauses>`.
     If it occurs in the :n:`@induction_principle`, then
     there can only be one :n:`@induction_clause`, which can't have its
     own :n:`@occurrences` clause.

   :n:`@induction_principle`
     Makes the tactic equivalent to
     :tacn:`induction` :n:`{+, @induction_clause } @induction_principle`.

   .. _example_destruct_ind_concl:

   .. example:: Using :tacn:`destruct` on an argument with premises

      .. 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 :n:`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
      :term:`dependent premises <dependent premise>` or dependent premises
      whose values are not inferrable from the :n:`with @bindings` clause,
      :n:`edestruct` turns them into existential variables to be resolved later on.

.. tacn:: case {+, @induction_clause } {? @induction_principle }

   An older, more basic tactic to perform case analysis without
   recursion.  We recommend using :tacn:`destruct` instead where possible.
   `case` only modifies the goal; it does not modify the :term:`local context`.

   .. tacn:: ecase {+, @induction_clause } {? @induction_principle }

      If the type of :n:`@one_term` (in :n:`@induction_arg`) has
      :term:`dependent premises <dependent premise>` or dependent premises
      whose values are not inferrable from the :n:`with @bindings` clause,
      :n:`ecase` turns them into existential variables to be resolved later on.

   .. tacn:: case_eq @one_term

      A variant of the :n:`case` tactic that allows
      performing case analysis on a term without completely forgetting its original
      form. This is done by generating equalities between the original form of the
      term and the outcomes of the case analysis.  We recommend using the
      :tacn:`destruct` tactic with an `eqn:` clause instead.

.. tacn:: casetype @one_term
   :undocumented:

.. tacn:: simple destruct {| @ident | @natural }

   Equivalent to :tacn:`intros` :n:`until {| @ident | @natural }; case @ident`
   where :n:`@ident` is a quantified variable of the goal and otherwise fails.

.. tacn:: dependent destruction @ident {? generalizing {+ @ident } } {? using @one_term }
   :undocumented:

   There is a long example of :tacn:`dependent destruction` and an explanation
   of the underlying technique :ref:`here <dependent-induction-examples>`.

Induction
---------

.. tacn:: induction {+, @induction_clause } {? @induction_principle }

   .. insertprodn induction_principle induction_principle

   .. prodn::
      induction_principle ::= using @one_term {? with @bindings } {? @occurrences }

   Applies an :term:`induction principle` to generate a subgoal for
   each constructor of an inductive type.

   If the argument is :term:`dependent <dependent product>` in the conclusion or some
   hypotheses of the goal, the argument is replaced by the appropriate
   constructor in each of the resulting subgoals and induction
   hypotheses are added to the local context using names whose prefix
   is **IH**.  The tactic is similar to :tacn:`destruct`, except that
   `destruct` doesn't generate induction hypotheses.

   :n:`induction` and :tacn:`destruct` are very similar.  Aside from the following
   differences, please refer to the description of :tacn:`destruct` while mentally substituting
   :n:`induction` for :tacn:`destruct`.

   :n:`{+, @induction_clause }`
     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.  The
     optional :n:`with @bindings` gives any values that must be substituted
     into the induction principle.  The number of :n:`@bindings`
     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 sort of the goal.

   .. exn:: Not an inductive product.
      :undocumented:

   .. exn:: Cannot recognize a statement based on @reference.

      The type of the :n:`@induction_arg` (in an :n:`@induction_clause`) must reduce to the
      :n:`@reference` which was inferred as the type the induction
      principle operates on. Note that it is not enough to be convertible, but you can
      work around that with :tacn:`change`:

      .. coqtop:: reset all

         Definition N := nat.
         Axiom strong : forall P, (forall n:N, (forall m:N, m < n -> P m) -> P n)
           -> forall n, P n.

         Axiom P : N -> Prop.

         Goal forall n:nat, P n.
         intros.
         Fail induction n using strong.
         change N in n.
         (* n is now of type N, matching the inferred type that strong operates on *)
         induction n using strong.

   .. exn:: Unable to find an instance for the variables @ident … @ident.

      Use the :n:`with @bindings` clause or the :tacn:`einduction` tactic instead.

   .. example::

      .. coqtop:: reset all

         Lemma induction_test : forall n:nat, n = n -> n <= n.
         intros n H.
         induction n.
         exact (le_n 0).

   .. example:: :n:`induction` with :n:`@occurrences`

      .. coqtop:: reset all

         Lemma induction_test2 : forall n:nat, n = n -> n <= n.
         intros.
         induction n in H |-.
         Show 2.

   .. tacn:: einduction {+, @induction_clause } {? @induction_principle }

      Behaves like :tacn:`induction` except that it does not fail if
      some dependent premise of the type of :n:`@one_term` is not inferrable. Instead,
      the unresolved premises are posed as existential variables to be inferred
      later, in the same way as :tacn:`eapply` does.

.. tacn:: elim @one_term_with_bindings {? using @one_term {? with @bindings } }

   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:`with @bindings`   (in :n:`@one_term_with_bindings`)
     Explicitly gives instances to the premises of the type of :n:`@one_term`
     (see :ref:`bindings`).

   :n:`{? using @one_term {? with @bindings } }`
     Allows explicitly giving an induction principle :n:`@one_term` that
     is not the standard one for the underlying inductive type of :n:`@one_term`. The
     :n:`@bindings` clause allows instantiating premises of the type of
     :n:`@one_term`.

   .. 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.

.. tacn:: elimtype @one_term

   The argument :token:`type` must be inductively defined. :n:`elimtype I` is
   equivalent to :tacn:`cut` :n:`I. intro Hn; elim Hn;` :tacn:`clear` :n:`Hn.` Therefore the
   hypothesis :g:`Hn` will not appear in the context(s) of the subgoal(s).
   Conversely, if :g:`t` is a :n:`@one_term` of (inductive) type :g:`I` that does
   not occur in the goal, then :n:`elim t` is equivalent to
   :n:`elimtype I; only 2:` :tacn:`exact` `t.`

.. tacn:: simple induction {| @ident | @natural }

   Behaves like :n:`intros until {| @ident | @natural }; elim @ident` when
   :n:`@ident` is a quantified variable of the goal.

.. tacn:: dependent induction @ident {? {| generalizing | in } {+ @ident } } {? using @one_term }

   The *experimental* tactic :tacn:`dependent induction` performs
   induction-inversion on an instantiated inductive predicate. One needs to first
   :cmd:`Require` the `Coq.Program.Equality` module to use this tactic. The tactic
   is based on the BasicElim tactic by Conor McBride
   :cite:`DBLP:conf/types/McBride00` and the work of Cristina Cornes around
   inversion :cite:`DBLP:conf/types/CornesT95`. From an instantiated
   inductive predicate and a goal, it generates an equivalent goal where
   the hypothesis has been generalized over its indexes which are then
   constrained by equalities to be the right instances. This permits to
   state lemmas without resorting to manually adding these equalities and
   still get enough information in the proofs.

   :n:`{| generalizing | in } {+ @ident }`
     First generalizes the goal by the given variables so that they are universally
     quantified in the goal.  This is generally what one wants to do with
     variables that are inside constructors in the induction hypothesis.  The other
     ones need not be further generalized.

   There is a long example of :tacn:`dependent induction` and an explanation
   of the underlying technique :ref:`here <dependent-induction-examples>`.

   .. example::

      .. coqtop:: reset all

         Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
         intros n H ; induction H.

      Here we did not get any information on the indexes to help fulfill
      this proof. The problem is that, when we use the ``induction`` tactic, we
      lose information on the hypothesis instance, notably that the second
      argument is 1 here. Dependent induction solves this problem by adding
      the corresponding equality to the context.

      .. coqtop:: reset all

         Require Import Coq.Program.Equality.
         Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
         intros n H ; dependent induction H.

      The subgoal is cleaned up as the tactic tries to automatically
      simplify the subgoals with respect to the generated equalities. In
      this enriched context, it becomes possible to solve this subgoal.

      .. coqtop:: all

         reflexivity.

      Now we are in a contradictory context and the proof can be solved.

      .. coqtop:: all abort

         inversion H.

      This technique works with any inductive predicate. In fact, the
      :tacn:`dependent induction` tactic is just a wrapper around the :tacn:`induction`
      tactic. One can make its own variant by just writing a new tactic
      based on the definition found in ``Coq.Program.Equality``.

   .. seealso:: :tacn:`functional induction`

.. tacn:: fix @ident @natural {? with {+ ( @ident {* @simple_binder } {? %{ struct @name %} } : @type ) } }

   .. insertprodn simple_binder simple_binder

   .. prodn::
      simple_binder ::= @name
      | ( {+ @name } : @term )

   A primitive tactic that starts a proof by induction. Generally,
   higher-level tactics such as :tacn:`induction` or :tacn:`elim`
   are easier to use.

   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
   least :n:`@natural` products.

   As in a fix expression, induction hypotheses must be used on
   structurally smaller arguments. The verification that inductive proof
   arguments are correct is done only when registering the
   lemma in the global environment. To know if the use of induction hypotheses
   is correct during the interactive development of a proof, use
   the command :cmd:`Guarded`.

   :n:`with {+ ( @ident {* @simple_binder } {? %{ struct @name %} } : @type ) }`
     Starts a proof by mutual induction. The statements to be proven
     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` (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).

.. tacn:: cofix @ident {? with {+ ( @ident {* @simple_binder } : @type ) } }

   Starts a proof by coinduction. The :n:`@ident`\s (including the first one
   before the `with` clause) are the
   names of the coinduction hypotheses. As in a cofix expression,
   the use of induction hypotheses must be guarded by a constructor. The
   verification that the use of coinductive hypotheses is correct is
   done only at the time of registering the lemma in the global environment. To
   know if the use of coinduction hypotheses is correct at some time of
   the interactive development of a proof, use the command :cmd:`Guarded`.

   :n:`with {+ ( @ident {* @simple_binder } : @type ) }`
     Starts a proof by mutual coinduction. The statements to be
     proven 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 coinduction hypotheses.

.. _equality-inductive_types:

Equality of inductive types
---------------------------

This section describes some special purpose tactics to work with
:term:`Leibniz equality` of inductive sets or types.

.. 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.
   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
     :n:`intros until @ident; discriminate @ident`.

   :n:`@natural` (in :n:`@induction_arg`)
     Equivalent to :tacn:`intros` :n:`until @natural; discriminate @ident`,
     where :n:`@ident` is the identifier for the last introduced hypothesis.

   :n:`@one_term with @bindings`  (in :n:`@induction_arg`)
     Equivalent to :n:`discriminate @one_term` but uses the given
     bindings to instantiate parameters or hypotheses of :n:`@one_term`.
     :n:`@one_term` must be a proof of :n:`@term__1 = @term__2`.

   .. exn:: No primitive equality found.
      :undocumented:

   .. exn:: Not a discriminable equality.
      :undocumented:

   .. tacn:: ediscriminate {? @induction_arg }

      Works the same as :tacn:`discriminate` but if the type of :token:`one_term`, or the
      type of the hypothesis referred to by :token:`natural`, has uninstantiated
      parameters, these parameters are left as existential variables.

.. tacn:: injection {? @induction_arg } {? as {* @simple_intropattern } }

   Exploits the property that constructors of
   inductive types are injective, i.e. that if :n:`c` is a constructor of an
   inductive type and :n:`c t__1 = c t__2` then
   :n:`t__1 = t__2` are equal too.

   If there is a hypothesis `H` in the form :n:`@term__1 = @term__2`,
   then :n:`injection H` applies the injectivity of constructors as deep as
   possible to derive the equality of subterms of :n:`@term__1` and
   :n:`@term__2` wherever the subterms start to differ. For example, from
   :g:`(S p, S n) = (q, S (S m))` we may derive :g:`S p = q` and
   :g:`n = S m`. The terms must have inductive types and the same head
   constructor, but must not be convertible. If so, the tactic derives the
   equalities and adds them to the current goal as :term:`premises <premise>`
   (except if the :n:`as` clause is used).

   If no :n:`induction_arg` is provided and the current goal is of the form
   :n:`@term <> @term`, :tacn:`injection` is equivalent to
   :n:`intro @ident; injection @ident`.

   :n:`@ident`  (in :n:`@induction_arg`)
     Derives equalities based on constructor injectivity for the hypothesis
     :n:`@ident`.
     If :n:`@ident` is not already in the context, this is equivalent to
     :n:`intros until @ident; injection @ident`.

   :n:`@natural` (in :n:`@induction_arg`)
     Equivalent to :tacn:`intros` :n:`until @natural` followed by
     :n:`injection @ident` where :n:`@ident` is the identifier for the last
     introduced hypothesis.

   :n:`@one_term with @bindings`  (in :n:`@induction_arg`)
     Like :n:`injection @one_term` but uses the given bindings to
     instantiate parameters or hypotheses of :n:`@one_term`.

   :n:`as [= {* @intropattern } ]`
     Specifies names to apply after the injection so
     that all generated equalities become hypotheses, which (unlike :tacn:`intros`)
     may replace existing hypotheses with same name.  The number of
     provided names must not exceed
     the number of newly generated equalities. If it is smaller, fresh
     names are generated for the unspecified items. The original equality is
     erased if it corresponds to a provided name or if the list of provided
     names is incomplete.

     Note that, as a convenience for users, specifying
     :n:`{+ @simple_intropattern }` is treated as if
     :n:`[= {+ @simple_intropattern } ]` was specified.

   .. example::

      Consider the following goal:

      .. coqtop:: in

         Inductive list : Set :=
         | nil : list
         | cons : nat -> list -> list.
         Parameter P : list -> Prop.
         Goal forall l n, P nil -> cons n l = cons 0 nil -> P l.

      .. coqtop:: all

         intros.
         injection H0.

   .. note::
      Beware that injection yields an equality in a sigma type whenever the
      injected object has a dependent type :g:`P` with its two instances in
      different types :n:`(P t__1 … t__n)` and :n:`(P u__1 … u__n)`. If :n:`t__1` and
      :n:`u__1` are the same and have for type an inductive type for which a decidable
      equality has been declared using :cmd:`Scheme Equality`,
      the use of a sigma type is avoided.

   .. exn:: No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop. You can try to use option Set Keep Proof Equalities.
      :undocumented:

   .. exn:: No primitive equality found.
      :undocumented:

   .. exn:: Not a negated primitive equality

      When :n:`@induction_arg` is not provided, the goal must be in the form
      :n:`@term <> @term`.

   .. exn:: Nothing to inject.

      Generated when one side of the equality is not a constructor.

   .. tacn:: einjection {? @induction_arg } {? as {* @simple_intropattern } }

      Works the same as :n:`injection` but if the type of :n:`@one_term`, or the
      type of the hypothesis referred to by :n:`@natural` has uninstantiated
      parameters, these parameters are left as existential variables.

   .. tacn:: simple injection {? @induction_arg }

      Similar to :tacn:`injection`, but always adds the derived equalities
      as new :term:`premises <premise>` in the current goal (instead of as
      new hypotheses) even if the :flag:`Structural Injection` flag is set.

   .. flag:: Structural Injection

      When this :term:`flag` is set, :n:`injection @term` erases the original hypothesis
      and adds the generated equalities as new hypotheses rather than adding them
      to the current goal as :term:`premises <premise>`, as if giving :n:`injection @term as`
      (with an empty list of names). This flag is off by default.

   .. flag:: Keep Proof Equalities

      By default, :tacn:`injection` only creates new equalities between :n:`@term`\s
      whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
      behavior for objects that are proofs of a statement in :g:`Prop`. This :term:`flag`
      controls this behavior.

   .. table:: Keep Equalities @qualid

      This :term:`table` specifies a set of inductive types for which proof
      equalities are always kept by :tacn:`injection`. This overrides the
      :flag:`Keep Proof Equalities` flag for those inductive types.
      :attr:`Template polymorphic <universes(template)>` inductive types are
      implicitly added to this table when defined.
      Use the :cmd:`Add` and :cmd:`Remove` commands to update this set manually.

.. tacn:: simplify_eq {? @induction_arg }

   Examines a hypothesis that has the form :n:`@term__1 = @term__2`.  If the terms are
   structurally different, the tactic does a :tacn:`discriminate`.  Otherwise, it does
   an :tacn:`injection` to simplify the equality, if possible.  If :n:`induction_arg`
   is not provided, the tactic examines the goal, which must be in the form
   :n:`@term__1 <> @term__2`.

   See the description of :token:`induction_arg` in :tacn:`injection` for an
   explanation of the parameters.

   .. tacn:: esimplify_eq {? @induction_arg }

      Works the same as :tacn:`simplify_eq` but if the type of :n:`@one_term` or the
      type of the hypothesis referred to by :n:`@natural` has uninstantiated
      parameters, these parameters are left as existential variables.

.. tacn:: inversion {| @ident | @natural } {? as @or_and_intropattern } {? in {+ @ident } }
          inversion {| @ident | @natural } using @one_term {? in {+ @ident } }
   :name: inversion; _

   .. comment: the other inversion* tactics don't support the using clause,
      but they should be able to, if desired.  It wouldn't make sense for
      inversion_sigma.
      See https://github.com/coq/coq/pull/14179#discussion_r642193096

   For a hypothesis whose type is a (co)inductively defined
   proposition, the tactic introduces a goal for each constructor
   of the proposition that isn't self-contradictory.  Each such goal
   includes the hypotheses needed to deduce the proposition.
   :gdef:`(Co)inductively defined propositions <inductively defined proposition>`
   are those defined with the :cmd:`Inductive` or :cmd:`CoInductive` commands whose
   contructors yield a `Prop`, as in this :ref:`example <inversion-intropattern-ex>`.


   :n:`@ident`
     The name of the hypothesis to invert.
     If :n:`@ident` does not denote a hypothesis in the local context but
     refers to a hypothesis quantified in the goal, then the latter is
     first introduced in the local context using :n:`intros until @ident`.

   :n:`@natural`
     Equivalent to :n:`intros until @natural; inversion @ident`
     where :n:`@ident` is the identifier for the last introduced hypothesis.

   :n:`{? in {+ @ident } }`
     When :n:`{+ @ident}` are identifiers in the local context, this does
     a :tacn:`generalize` :n:`{+ @ident}` as the initial step of `inversion`.

   :n:`as @or_and_intropattern`
     Provides names for the variables introduced in each new subgoal.  The
     :token:`or_and_intropattern` must have one :n:`{* @intropattern }`
     for each constructor of the (co)inductive predicate, given in the order
     in which the constructors are defined.
     If there are not enough names, Coq picks fresh names.

     If an equation splits into several
     equations (because ``inversion`` applies ``injection`` on the equalities it
     generates), the corresponding :n:`@intropattern` should be in the form
     :n:`[ {* @intropattern } ]` (or the equivalent :n:`{*, ( @simple_intropattern ) }`),
     with the number of entries equal to the number
     of subequalities obtained from splitting the original equation.
     Example :ref:`here <inversion-intropattern-ex>`.

   .. note::
      The ``inversion … as`` variant of
      ``inversion`` generally behaves in a slightly more expected way than
      ``inversion`` (no artificial duplication of some hypotheses referring to
      other hypotheses). To take advantage of these improvements, it is enough to use
      ``inversion … as []``, letting Coq choose fresh names.

   .. note::
      As ``inversion`` proofs may be large, we recommend
      creating and using lemmas whenever the same instance needs to be
      inverted several times. See :ref:`derive-inversion`.

   .. note::
      Part of the behavior of the :tacn:`inversion` tactic is to generate
      equalities between expressions that appeared in the hypothesis that is
      being processed. By default, no equalities are generated if they
      relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort
      :g:`Prop`). This behavior can be turned off by using the
      :flag:`Keep Proof Equalities` setting.

.. _inversion-intropattern-ex:

   .. example:: :tacn:`inversion` with :n:`as @or_and_intropattern`

      .. coqtop:: reset all

         Inductive contains0 : list nat -> Prop :=
         | in_hd : forall l, contains0 (0 :: l)
         | in_tl : forall l b, contains0 l -> contains0 (b :: l).

      .. coqtop:: in

         Goal forall l:list nat, contains0 (1 :: l) -> contains0 l.

      .. coqtop:: all

         intros l H.
         inversion H as [ | l' p Hl' [Heqp Heql'] ].

   .. tacn:: inversion_clear {| @ident | @natural } {? as @or_and_intropattern } {? in {+ @ident } }

      Does an :tacn:`inversion` and then erases the hypothesis that was used for
      the inversion.

   .. tacn:: simple inversion {| @ident | @natural } {? as @or_and_intropattern } {? in {+ @ident } }

      A very simple inversion tactic that derives all the necessary
      equalities but does not simplify the constraints as :tacn:`inversion` does.

   .. tacn:: dependent inversion {| @ident | @natural } {? as @or_and_intropattern } {? with @one_term }

      For use when the inverted hypothesis appears in the current goal.
      Does an :tacn:`inversion` and then substitutes the name of the hypothesis
      where the corresponding term appears in the goal.

   .. tacn:: dependent inversion_clear {| @ident | @natural } {? as @or_and_intropattern } {? with @one_term }

      Does a :tacn:`dependent inversion` and then erases the hypothesis that was used for
      the dependent inversion.

   .. tacn:: dependent simple inversion {| @ident | @natural } {? as @or_and_intropattern } {? with @one_term }
      :undocumented:

.. tacn:: inversion_sigma {? @ident {? as @simple_intropattern } }

   Turns equalities of dependent pairs (e.g.,
   :g:`existT P x p = existT P y q`, frequently left over by :tacn:`inversion` on
   a dependent type family) into pairs of equalities (e.g., a hypothesis
   :g:`H : x = y` and a hypothesis of type :g:`rew H in p = q`); these
   hypotheses can subsequently be simplified using :tacn:`subst`, without ever
   invoking any kind of axiom asserting uniqueness of identity proofs. If you
   want to explicitly specify the hypothesis to be inverted, you can pass it as
   an argument to :tacn:`inversion_sigma`. This tactic also works for
   :g:`sig`, :g:`sigT2`, :g:`sig2`, :g:`ex`, and :g:`ex2` and there are similar :g:`eq_sig`
   :g:`***_rect` induction lemmas.


   .. exn:: Type of @ident is not an equality of recognized Σ types: expected one of sig sig2 sigT sigT2 sigT2 ex or ex2 but got @term

      When applied to a hypothesis, :tacn:`inversion_sigma` can only handle equalities of the
      listed sigma types.

   .. exn:: @ident is not an equality of Σ types

      When applied to a hypothesis, :tacn:`inversion_sigma` can only be called on hypotheses that
      are equalities using :g:`Coq.Logic.Init.eq`.

.. example:: Non-dependent inversion

   Let us consider the relation :g:`Le` over natural numbers:

   .. coqtop:: reset in

      Inductive Le : nat -> nat -> Set :=
      | LeO : forall n:nat, Le 0 n
      | LeS : forall n m:nat, Le n m -> Le (S n) (S m).


   Let us consider the following goal:

   .. coqtop:: none

      Section Section.
      Variable P : nat -> nat -> Prop.
      Variable Q : forall n m:nat, Le n m -> Prop.
      Goal forall n m, Le (S n) m -> P n m.

   .. coqtop:: out

      intros.

   To prove the goal, we may need to reason by cases on :g:`H` and to derive
   that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that
   :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only
   possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert
   the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le`
   is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`.

   .. coqtop:: all

      inversion_clear H.

   Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the
   hypothesis :g:`(Le n m0)` has been added to the context.

   Sometimes it is interesting to have the equality :g:`m = (S m0)` in the
   context to use it after. In that case we can use :tacn:`inversion` that does
   not clear the equalities:

   .. coqtop:: none restart

      intros.

   .. coqtop:: all

      inversion H.

.. example:: Dependent inversion

   Let us consider the following goal:

   .. coqtop:: none

      Abort.
      Goal forall n m (H:Le (S n) m), Q (S n) m H.

   .. coqtop:: out

      intros.

   As :g:`H` occurs in the goal, we may want to reason by cases on its
   structure and so, we would like inversion tactics to substitute :g:`H` by
   the corresponding @term in constructor form. Neither :tacn:`inversion` nor
   :tacn:`inversion_clear` do such a substitution. To have such a behavior we
   use the dependent inversion tactics:

   .. coqtop:: all

      dependent inversion_clear H.

   Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`.

.. example:: Using :tacn:`inversion_sigma`

   Let us consider the following inductive type of
   length-indexed lists, and a lemma about inverting equality of cons:

   .. coqtop:: reset all

      Require Import Coq.Logic.Eqdep_dec.

      Inductive vec A : nat -> Type :=
      | nil : vec A O
      | cons {n} (x : A) (xs : vec A n) : vec A (S n).

      Lemma invert_cons : forall A n x xs y ys,
               @cons A n x xs = @cons A n y ys
               -> xs = ys.

      Proof.
      intros A n x xs y ys H.

   After performing inversion, we are left with an equality of existTs:

   .. coqtop:: all

      inversion H.

   We can turn this equality into a usable form with inversion_sigma:

   .. coqtop:: all

      inversion_sigma.

   To finish cleaning up the proof, we will need to use the fact that
   that all proofs of n = n for n a nat are eq_refl:

   .. coqtop:: all

      let H := match goal with H : n = n |- _ => H end in
      pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H.
      simpl in *.

   Finally, we can finish the proof:

   .. coqtop:: all

      assumption.
      Qed.

.. seealso:: :tacn:`functional inversion`

Helper tactics
~~~~~~~~~~~~~~

.. tacn:: decide equality

   Solves a goal of the form :g:`forall x y : R, {x = y} + {~ x = y}`,
   where :g:`R` is an inductive type such that its constructors do not take
   proofs or functions as arguments, nor objects in dependent types. It
   solves goals of the form :g:`{x = y} + {~ x = y}` as well.

.. tacn:: compare @one_term__1 @one_term__2

   Compares two :n:`@one_term`\s of an
   inductive datatype. If :g:`G` is the current goal, it leaves the
   sub-goals :n:`@one_term__1 = @one_term__2 -> G` and :n:`~ @one_term__1 = @one_term__2 -> G`.
   The type of the :n:`@one_term`\s must satisfy the same restrictions as in the
   tactic :tacn:`decide equality`.

.. tacn:: dependent rewrite {? {| -> | <- } } @one_term {? in @ident }

   If :n:`@ident` has type
   :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each
   term of the equality has a sigma type :g:`{ a:A & (B a)}`) this tactic
   rewrites :g:`a` into :g:`a'` and :g:`b` into :g:`b'` in the current goal.
   This tactic works even if :g:`B` is also a sigma type. This kind of
   equalities between dependent pairs may be derived by the
   :tacn:`injection` and :tacn:`inversion` tactics.

   :n:`{? {| -> | <- } }`
     By default, the equality is applied from left to right.  Specify `<-` to
     apply the equality from right to left.

.. _proofschemes-induction-principles:

Generation of induction principles with ``Scheme``
--------------------------------------------------------

.. cmd:: Scheme {? @ident := } @scheme_kind {* with {? @ident := } @scheme_kind }

   .. insertprodn scheme_kind sort_family scheme_type

   .. prodn::
      scheme_kind ::= @scheme_type for @reference Sort @sort_family
      scheme_type ::= Induction
      | Minimality
      | Elimination
      | Case
      sort_family ::= Prop
      | SProp
      | Set
      | Type

   Generates :term:`induction principles <induction principle>` with given
   :n:`scheme_type`\s and :n:`scheme_sort`\s for an inductive type. In the case
   where the inductive definition is a mutual inductive definition, the
   :n:`with` clause is used to generate a mutually recursive inductive scheme
   for each clause of the mutual inductive type.

   :n:`@ident`
      The name of the scheme. If not provided, the name will be determined
      automatically from the :n:`@scheme_type` and :n:`@sort_family`.

   The following :n:`@scheme_type`\s generate induction principles with
   given properties:

   =================== =========== ===========
    :n:`@scheme_type`   Recursive   Dependent
   =================== =========== ===========
    :n:`Induction`         Yes         Yes
    :n:`Minimality`        Yes         No
    :n:`Elimination`       No          Yes
    :n:`Case`              No          No
   =================== =========== ===========

   See examples of the :n:`@scheme_type`\s :ref:`here <scheme_example>`.

.. cmd:: Scheme {? Boolean } Equality for @reference
   :name: Scheme Equality; Scheme Boolean Equality

   Tries to generate a Boolean equality for :n:`@reference`. If
   :n:`Boolean` is not specified, the command also tries to generate
   a proof of the decidability of propositional equality over
   :n:`@reference`.
   If :token:`reference` involves independent constants or other
   inductive types, we recommend defining their equality first.

.. example:: Induction scheme for tree and forest

   Currently the automatically-generated :term:`induction principles <induction principle>`
   such as `odd_ind` are not useful for mutually-inductive types such as `odd` and `even`.
   You can define a mutual induction principle for tree and forest in sort ``Set`` with
   the :cmd:`Scheme` command:

    .. coqtop:: reset none

       Axiom A : Set.
       Axiom B : Set.

    .. coqtop:: in

     Inductive tree : Set :=
     | node : A -> forest -> tree
     with forest : Set :=
     | leaf : B -> forest
     | cons : tree -> forest -> forest.

    .. coqtop:: all

     Scheme tree_forest_rec := Induction for tree Sort Set
       with forest_tree_rec := Induction for forest Sort Set.

  You may now look at the type of tree_forest_rec:

  .. coqtop:: all

    Check tree_forest_rec.

  This principle involves two different predicates for trees and forests;
  it also has three premises each one corresponding to a constructor of
  one of the inductive definitions.

  The principle `forest_tree_rec` shares exactly the same premises, only
  the conclusion now refers to the property of forests.

.. example:: Predicates odd and even on naturals

  Let odd and even be inductively defined as:

   .. coqtop:: in

      Inductive odd : nat -> Prop :=
      | oddS : forall n : nat, even n -> odd (S n)
      with even : nat -> Prop :=
      | evenO : even 0
      | evenS : forall n : nat, odd n -> even (S n).

  The following command generates a powerful elimination principle:

   .. coqtop:: all

    Scheme odd_even := Minimality for odd Sort Prop
    with even_odd := Minimality for even Sort Prop.

  The type of odd_even for instance will be:

  .. coqtop:: all

    Check odd_even.

  The type of `even_odd` shares the same premises but the conclusion is
  `forall n : nat, even n -> P0 n`.

.. _scheme_example:

   .. example:: `Scheme` commands with various :n:`@scheme_type`\s

      Let us demonstrate the difference between the Scheme commands.

      .. coqtop:: all

         Unset Elimination Schemes.

         Inductive Nat :=
         | z : Nat
         | s : Nat -> Nat.

         (* dependent, recursive *)
         Scheme Induction for Nat Sort Set.
         About Nat_rec.

         (* non-dependent, recursive *)
         Scheme Minimality for Nat Sort Set.
         About Nat_rec_nodep.

         (* dependent, non-recursive *)
         Scheme Elimination for Nat Sort Set.
         About Nat_case.

         (* non-dependent, non-recursive *)
         Scheme Case for Nat Sort Set.
         About Nat_case_nodep.

Automatic declaration of schemes
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

.. flag:: Elimination Schemes

   This :term:`flag` enables automatic declaration of induction principles when defining a new
   inductive type.  Defaults to on.

.. flag:: Nonrecursive Elimination Schemes

   This :term:`flag` enables automatic declaration of induction
   principles for types declared with the :cmd:`Variant` and
   :cmd:`Record` commands.  Defaults to off.

.. flag:: Case Analysis Schemes

   This :term:`flag` governs the generation of case analysis lemmas for inductive types,
   i.e. corresponding to the pattern matching term alone and without fixpoint.

.. flag:: Boolean Equality Schemes
          Decidable Equality Schemes

   These :term:`flags <flag>` control the automatic declaration of those Boolean equalities (see
   the second variant of ``Scheme``).

.. warning::

   You have to be careful with these flags since Coq may now reject well-defined
   inductive types because it cannot compute a Boolean equality for them.

.. flag:: Rewriting Schemes

   This :term:`flag` governs generation of equality-related schemes such as congruence.

Combined Scheme
~~~~~~~~~~~~~~~

.. cmd:: Combined Scheme @ident__def from {+, @ident }

   Combines induction principles generated
   by the :cmd:`Scheme` command.
   Each :n:`@ident` is a different inductive principle that must  belong
   to the same package of mutual inductive principle definitions.
   This command generates :n:`@ident__def` as the conjunction of the
   principles: it is built from the common premises of the principles
   and concluded by the conjunction of their conclusions.
   In the case where all the inductive principles used are in sort
   ``Prop``, the propositional conjunction ``and`` is used, otherwise
   the simple product ``prod`` is used instead.

.. example::

  We can define the induction principles for trees and forests using:

  .. coqtop:: all

    Scheme tree_forest_ind := Induction for tree Sort Prop
    with forest_tree_ind := Induction for forest Sort Prop.

  Then we can build the combined induction principle which gives the
  conjunction of the conclusions of each individual principle:

  .. coqtop:: all

    Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind.

  The type of tree_forest_mutind will be:

  .. coqtop:: all

    Check tree_forest_mutind.

.. example::

   We can also combine schemes at sort ``Type``:

  .. coqtop:: all

     Scheme tree_forest_rect := Induction for tree Sort Type
     with forest_tree_rect := Induction for forest Sort Type.

  .. coqtop:: all

     Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect.

  .. coqtop:: all

     Check tree_forest_mutrect.

.. seealso:: :ref:`functional-scheme`

.. _derive-inversion:

Generation of inversion principles with ``Derive`` ``Inversion``
-----------------------------------------------------------------

.. cmd:: Derive Inversion @ident with @one_term {? Sort @sort_family }

   Generates an inversion lemma for the
   :tacn:`inversion` tactic.  :token:`ident` is the name
   of the generated lemma.  :token:`one_term` should be in the form
   :token:`qualid` or :n:`(forall {+ @binder }, @qualid @term)` where
   :token:`qualid` is the name of an inductive
   predicate and :n:`{+ @binder }` binds the variables occurring in the term
   :token:`term`. The lemma is generated for the sort
   :token:`sort_family` corresponding to :token:`one_term`.
   Applying the lemma is equivalent to inverting the instance with the
   :tacn:`inversion` tactic.

.. cmd:: Derive Inversion_clear @ident with @one_term {? Sort @sort_family }

   When applied, it is equivalent to having inverted the instance with the
   tactic inversion replaced by the tactic `inversion_clear`.

.. cmd:: Derive Dependent Inversion @ident with @one_term Sort @sort_family

   When applied, it is equivalent to having inverted the instance with
   the tactic `dependent inversion`.

.. cmd:: Derive Dependent Inversion_clear @ident with @one_term Sort @sort_family

   When applied, it is equivalent to having inverted the instance
   with the tactic `dependent inversion_clear`.

.. example::

  Consider the relation `Le` over natural numbers and the following
  parameter ``P``:

  .. coqtop:: all

    Inductive Le : nat -> nat -> Set :=
    | LeO : forall n:nat, Le 0 n
    | LeS : forall n m:nat, Le n m -> Le (S n) (S m).

    Parameter P : nat -> nat -> Prop.

  To generate the inversion lemma for the instance :g:`(Le (S n) m)` and the
  sort :g:`Prop`, we do:

  .. coqtop:: all

    Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop.
    Check leminv.

  Then we can use the proven inversion lemma:

  .. the original LaTeX did not have any Coq code to setup the goal

  .. coqtop:: none

    Goal forall (n m : nat) (H : Le (S n) m), P n m.
    intros.

  .. coqtop:: all

    Show.

    inversion H using leminv.

.. _dependent-induction-examples:

Examples of :tacn:`dependent destruction` / :tacn:`dependent induction`
-----------------------------------------------------------------------

The tactics :tacn:`dependent induction` and :tacn:`dependent destruction` are another
solution for inverting inductive predicate instances and potentially
doing induction at the same time. It is based on the ``BasicElim`` tactic
of Conor McBride which works by abstracting each argument of an
inductive instance by a variable and constraining it by equalities
afterwards. This way, the usual induction and destruct tactics can be
applied to the abstracted instance and after simplification of the
equalities we get the expected goals.

The abstracting tactic is called generalize_eqs and it takes as
argument a hypothesis to generalize. It uses the JMeq datatype
defined in Coq.Logic.JMeq, hence we need to require it before. For
example, revisiting the first example of the inversion documentation:

.. coqtop:: in reset

   Require Import Coq.Logic.JMeq.

   Inductive Le : nat -> nat -> Set :=
        | LeO : forall n:nat, Le 0 n
        | LeS : forall n m:nat, Le n m -> Le (S n) (S m).

   Parameter P : nat -> nat -> Prop.

   Goal forall n m:nat, Le (S n) m -> P n m.

   intros n m H.

.. coqtop:: all

   generalize_eqs H.

The index ``S n`` gets abstracted by a variable here, but a corresponding
equality is added under the abstract instance so that no information
is actually lost. The goal is now almost amenable to do induction or
case analysis. One should indeed first move ``n`` into the goal to
strengthen it before doing induction, or ``n`` will be fixed in the
inductive hypotheses (this does not matter for case analysis). As a
rule of thumb, all the variables that appear inside constructors in
the indices of the hypothesis should be generalized. This is exactly
what the ``generalize_eqs_vars`` variant does:

.. coqtop:: all abort

   generalize_eqs_vars H.
   induction H.

As the hypothesis itself did not appear in the goal, we did not need
to use an heterogeneous equality to relate the new hypothesis to the
old one (which just disappeared here). However, the tactic works just
as well in this case, e.g.:

.. coqtop:: none

   Require Import Coq.Program.Equality.

.. coqtop:: in

   Parameter Q : forall (n m : nat), Le n m -> Prop.
   Goal forall n m (p : Le (S n) m), Q (S n) m p.

.. coqtop:: all

   intros n m p.
   generalize_eqs_vars p.

One drawback of this approach is that in the branches one will have to
substitute the equalities back into the instance to get the right
assumptions. Sometimes injection of constructors will also be needed
to recover the needed equalities. Also, some subgoals should be
directly solved because of inconsistent contexts arising from the
constraints on indexes. The nice thing is that we can make a tactic
based on discriminate, injection and variants of substitution to
automatically do such simplifications (which may involve the axiom K).
This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality``
does. For example, we might simplify the previous goals considerably:

.. coqtop:: all abort

   induction p ; simplify_dep_elim.

The higher-order tactic ``do_depind`` defined in ``Coq.Program.Equality``
takes a tactic and combines the building blocks we have seen with it:
generalizing by equalities calling the given tactic with the
generalized induction hypothesis as argument and cleaning the subgoals
with respect to equalities. Its most important instantiations
are :tacn:`dependent induction` and :tacn:`dependent destruction` that do induction or
simply case analysis on the generalized hypothesis. For example we can
redo what we've done manually with dependent destruction:

.. coqtop:: in

   Lemma ex : forall n m:nat, Le (S n) m -> P n m.

.. coqtop:: in

   intros n m H.

.. coqtop:: all abort

   dependent destruction H.

This gives essentially the same result as inversion. Now if the
destructed hypothesis actually appeared in the goal, the tactic would
still be able to invert it, contrary to dependent inversion. Consider
the following example on vectors:

.. coqtop:: in

   Set Implicit Arguments.

.. coqtop:: in

   Parameter A : Set.

.. coqtop:: in

   Inductive vector : nat -> Type :=
            | vnil : vector 0
            | vcons : A -> forall n, vector n -> vector (S n).

.. coqtop:: in

   Goal forall n, forall v : vector (S n),
            exists v' : vector n, exists a : A, v = vcons a v'.

.. coqtop:: in

   intros n v.

.. coqtop:: all

   dependent destruction v.

In this case, the ``v`` variable can be replaced in the goal by the
generalized hypothesis only when it has a type of the form ``vector (S n)``,
that is only in the second case of the destruct. The first one is
dismissed because ``S n <> 0``.


A larger example
~~~~~~~~~~~~~~~~

Let's see how the technique works with induction on inductive
predicates on a real example. We will develop an example application
to the theory of simply-typed lambda-calculus formalized in a
dependently-typed style:

.. coqtop:: in reset

   Inductive type : Type :=
            | base : type
            | arrow : type -> type -> type.

.. coqtop:: in

   Notation " t --> t' " := (arrow t t') (at level 20, t' at next level).

.. coqtop:: in

   Inductive ctx : Type :=
            | empty : ctx
            | snoc : ctx -> type -> ctx.

.. coqtop:: in

   Notation " G , tau " := (snoc G tau) (at level 20, tau at next level).

.. coqtop:: in

   Fixpoint conc (G D : ctx) : ctx :=
            match D with
            | empty => G
            | snoc D' x => snoc (conc G D') x
            end.

.. coqtop:: in

   Notation " G ; D " := (conc G D) (at level 20).

.. coqtop:: in

   Inductive term : ctx -> type -> Type :=
            | ax : forall G tau, term (G, tau) tau
            | weak : forall G tau,
                       term G tau -> forall tau', term (G, tau') tau
            | abs : forall G tau tau',
                      term (G , tau) tau' -> term G (tau --> tau')
            | app : forall G tau tau',
                      term G (tau --> tau') -> term G tau -> term G tau'.

We have defined types and contexts which are snoc-lists of types. We
also have a ``conc`` operation that concatenates two contexts. The ``term``
datatype represents in fact the possible typing derivations of the
calculus, which are isomorphic to the well-typed terms, hence the
name. A term is either an application of:


+ the axiom rule to type a reference to the first variable in a
  context
+ the weakening rule to type an object in a larger context
+ the abstraction or lambda rule to type a function
+ the application to type an application of a function to an argument


Once we have this datatype we want to do proofs on it, like weakening:

.. coqtop:: in abort

   Lemma weakening : forall G D tau, term (G ; D) tau ->
                     forall tau', term (G , tau' ; D) tau.

The problem here is that we can't just use induction on the typing
derivation because it will forget about the ``G ; D`` constraint appearing
in the instance. A solution would be to rewrite the goal as:

.. coqtop:: in abort

   Lemma weakening' : forall G' tau, term G' tau ->
                      forall G D, (G ; D) = G' ->
                      forall tau', term (G, tau' ; D) tau.

With this proper separation of the index from the instance and the
right induction loading (putting ``G`` and ``D`` after the inducted-on
hypothesis), the proof will go through, but it is a very tedious
process. One is also forced to make a wrapper lemma to get back the
more natural statement. The :tacn:`dependent induction` tactic alleviates this
trouble by doing all of this plumbing of generalizing and substituting
back automatically. Indeed we can simply write:

.. coqtop:: in

   Require Import Coq.Program.Tactics.
   Require Import Coq.Program.Equality.

.. coqtop:: in

   Lemma weakening : forall G D tau, term (G ; D) tau ->
                     forall tau', term (G , tau' ; D) tau.

.. coqtop:: in

   Proof with simpl in * ; simpl_depind ; auto.

.. coqtop:: in

   intros G D tau H. dependent induction H generalizing G D ; intros.

This call to :tacn:`dependent induction` has an additional arguments which is
a list of variables appearing in the instance that should be
generalized in the goal, so that they can vary in the induction
hypotheses. By default, all variables appearing inside constructors
(except in a parameter position) of the instantiated hypothesis will
be generalized automatically but one can always give the list
explicitly.

.. coqtop:: all

   Show.

The ``simpl_depind`` tactic includes an automatic tactic that tries to
simplify equalities appearing at the beginning of induction
hypotheses, generally using trivial applications of ``reflexivity``. In
cases where the equality is not between constructor forms though, one
must help the automation by giving some arguments, using the
``specialize`` tactic for example.

.. coqtop:: in

   destruct D... apply weak; apply ax. apply ax.

.. coqtop:: in

   destruct D...

.. coqtop:: all

   Show.

.. coqtop:: all

   specialize (IHterm G0 empty eq_refl).

Once the induction hypothesis has been narrowed to the right equality,
it can be used directly.

.. coqtop:: all

   apply weak, IHterm.

Now concluding this subgoal is easy.

.. coqtop:: in

   constructor; apply IHterm; reflexivity.