\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Functional induction

Note

The functional induction (FunInd) plugin is legacy functionality. For new code and new projects, we recommend Equations, a more powerful plugin that provides most of FunInd's features. It can be installed through the Coq Platform. Refer to the Equations documentation to learn more. FunInd is not deprecated and not planned for removal yet because porting code from FunInd to Equations can be difficult (due to differences in the generated induction principles).

Note

The tactics described in this chapter require the Stdlib library.

## Advanced recursive functions

The following command is available when the `FunInd` library has been loaded via `From Stdlib Require Import FunInd`:

Command Function fix_definition with fix_definition*

  This command is a generalization of `Fixpoint`. It is a wrapper for several ways of defining a function and other useful related objects, namely: an induction principle that reflects the recursive structure of the function (see `functional induction`) and its fixpoint equality. This defines a function similar to those defined by `Fixpoint`. As in `Fixpoint`, the decreasing argument must be given (unless the function is not recursive), but it might not necessarily be structurally decreasing. Use the `fixannot` clause to name the decreasing argument and to describe which kind of decreasing criteria to use to ensure termination of recursive calls.

  `Function` also supports the `with` clause to create mutually recursive definitions, however this feature is limited to structurally recursive functions (i.e. when `fixannot` is a `struct` clause).

  See `functional induction` and `Functional Scheme` for how to use the induction principle to reason easily about the function.

  The form of the `fixannot` clause determines which definition mechanism `Function` uses. (Note that references to `ident` below refer to the name of the function being defined.):

  - If `fixannot` is not specified, `Function` defines the nonrecursive function `ident` as if it was declared with `Definition`. In addition, the following are defined:

    > - `ident``_rect`, `ident``_rec` and `ident``_ind`, which reflect the pattern matching structure of `term` (see `Inductive`);

    > - The inductive `R_ident` corresponding to the graph of `ident` (silently);

    > - `ident``_complete` and `ident``_correct` which are inversion information linking the function and its graph.

  - If `{ struct ... }` is specified, `Function` defines the structural recursive function `ident` as if it was declared with `Fixpoint`. In addition, the following are defined:

    > - The same objects as above;

    > - The fixpoint equation of `ident`: `ident``_equation`.

  - If `{ measure ... }` or `{ wf ... }` are specified, `Function` defines a recursive function by well-founded recursion. The module `Recdef` of the standard library must be loaded for this feature.

    > - `{measure one_term1 ident? one_term2? }`: where `ident` is the decreasing argument and `one_term1` is a function from the type of `ident` to `nat` for which the decreasing argument decreases (for the `lt` order on `nat`) for each recursive call of the function. The parameters of the function are bound in `one_term1`.

    > - `{wf one_term ident }`: where `ident` is the decreasing argument and `one_term` is an ordering relation on the type of `ident` (i.e. of type `T`\(_{\sf ident}\) → `T`\(_{\sf ident}\) → `Prop`) for which the decreasing argument decreases for each recursive call of the function. The order must be well-founded. The parameters of the function are bound in `one_term`.

    If the clause is `measure` or `wf`, the user is left with some proof obligations that will be used to define the function. These proofs are: proofs that each recursive call is actually decreasing with respect to the given criteria, and (if the criteria is `wf`) a proof that the ordering relation is well-founded. Once proof obligations are discharged, the following objects are defined:

    > - The same objects as with the `struct` clause;

    > - The lemma `ident``_tcc` which collects all proof obligations in one property;

    > - The lemmas `ident``_terminate` and `ident``_F` which will be inlined during extraction of `ident`.

    The way this recursive function is defined is the subject of several papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other hand.

Note

To obtain the right principle, it is better to put rigid parameters of the function as first arguments. For example it is better to define plus like this:

From Stdlib Require Import FunInd.
  Toplevel input, characters 27-33: > From Stdlib Require Import FunInd. > ^^^^^^ Error: Cannot find a physical path bound to logical path FunInd with prefix Stdlib.

Function plus (m n : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus m p) end.
  Toplevel input, characters 0-8: > Function plus (m n : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus m p) end. > ^^^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

than like this:

From Stdlib Require Import FunInd.
  Toplevel input, characters 27-33: > From Stdlib Require Import FunInd. > ^^^^^^ Error: Cannot find a physical path bound to logical path FunInd with prefix Stdlib.

Function plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus p m) end.
  Toplevel input, characters 0-8: > Function plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus p m) end. > ^^^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

Limitations

`term` must be built as a pure pattern matching tree (`match … with`) with applications only at the end of each branch.

`Function` does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of `wrong` in the body of `wrong`:

From Stdlib Require List.
  Toplevel input, characters 20-24: > From Stdlib Require List. > ^^^^ Error: Cannot find a physical path bound to logical path List with prefix Stdlib.
Import List.ListNotations.
  Toplevel input, characters 7-25: > Import List.ListNotations. > ^^^^^^^^^^^^^^^^^^ Error: Cannot find module List.ListNotations

Function wrong (C:nat) : nat := List.hd 0 (List.map wrong (C::nil)).
  Toplevel input, characters 0-8: > Function wrong (C:nat) : nat := List.hd 0 (List.map wrong (C::nil)). > ^^^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

For now, dependent cases are not treated for non-structurally terminating functions.

Error The recursive argument must be specified.

Error No argument name ident.

Error Cannot use mutual definition with well-founded recursion or measure.

Warning Cannot define graph for ident.

  The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident raised a typing error. Only `ident` is defined; the induction scheme will not be generated. This error happens generally when:

  - the definition uses pattern matching on dependent types, which `Function` cannot deal with yet.

  - the definition is not a pattern matching tree as explained above.

Warning Cannot define principle(s) for ident.

  The generation of the graph relation (`R_ident`) succeeded but the induction principle could not be built. Only `ident` is defined. Please report.

Warning Cannot build functional inversion principle.

  `functional inversion` will not be available for the function.

## Tactics

Tactic functional induction term using one_term_with_bindings? as simple_intropattern?

  Performs case analysis and induction following the definition of a function `qualid`, which must be fully applied to its arguments as part of `term`. It uses a principle generated by `Function` or `Functional Scheme`. Note that this tactic is only available after a `From Stdlib Require Import FunInd`. See the `Function` command.

  `using one_term`

    Specifies the induction principle (aka elimination scheme).

  `with bindings`

    Specifies the arguments of the induction principle.

  `as simple_intropattern`

    Provides names for the introduced variables.

  Example

  From Stdlib Require Import FunInd.
    Toplevel input, characters 27-33: > From Stdlib Require Import FunInd. > ^^^^^^ Error: Cannot find a physical path bound to logical path FunInd with prefix Stdlib.
  Functional Scheme minus_ind := Induction for minus Sort Prop.
    Toplevel input, characters 0-10: > Functional Scheme minus_ind := Induction for minus Sort Prop. > ^^^^^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
  Check minus_ind.
    Toplevel input, characters 6-15: > Check minus_ind. > ^^^^^^^^^ Error: The reference minus_ind was not found in the current environment.
  Lemma le_minus (n m:nat) : n - m <= n.
    1 goal n, m : nat ============================ n - m <= n
  functional induction (minus n m) using minus_ind; simpl; auto.
    Toplevel input, characters 33-38: > functional induction (minus n m) using minus_ind; simpl; auto. > ^^^^^ Error: Syntax error: [ltac_use_default] expected after [tactic] (in [tactic_command]).
  Qed.
    Toplevel input, characters 0-4: > Qed. > ^^^^ Error: (in proof le_minus): Attempt to save an incomplete proof (there are remaining open goals).

  Note

  `functional induction (f x1 x2 x3)` is actually a wrapper for `induction x1, x2, x3, (f x1 x2 x3) using qualid` followed by a cleaning phase, where `qualid` is the induction principle registered for `f` (by the `Function` or `Functional Scheme` command) corresponding to the sort of the goal. Therefore `functional induction` may fail if the induction scheme `qualid` is not defined.

  Note

  There is a difference between obtaining an induction scheme for a function by using `Function` and by using `Functional Scheme` after a normal definition using `Fixpoint` or `Definition`.

  Error Cannot find induction information on qualid.
  Error Not the right number of induction arguments.

Tactic soft functional induction one_term+ using one_term_with_bindings? as simple_intropattern?

Tactic functional inversion ident​natural qualid?

  Performs inversion on hypothesis `ident` of the form `qualid term+ = term` or `term = qualid term+` when `qualid` is defined using `Function`. Note that this tactic is only available after a `From Stdlib Require Import FunInd`.

  `natural`

    Does the same thing as `intros until natural` followed by `functional inversion ident` where `ident` is the identifier for the last introduced hypothesis.

  `qualid`

    If the hypothesis `ident` (or `natural`) has a type of the form `qualid1 termi+ = qualid2 termj+` where `qualid1` and `qualid2` are valid candidates to functional inversion, this variant allows choosing which `qualid` is inverted.

  Error Hypothesis ident must contain at least one Function.
  Error Cannot find inversion information for hypothesis ident.

    This error may be raised when some inversion lemma failed to be generated by Function.

## Generation of induction principles with `Functional` `Scheme`

Command Functional Scheme func_scheme_def with func_scheme_def*
  func_scheme_def`::=`ident := Induction for qualid Sort sort_quality_or_set``

  An experimental high-level tool that automatically generates induction principles corresponding to functions that may be mutually recursive. The command generates an induction principle named `ident` for each given function named `qualid`. The `qualid`s must be given in the same order as when they were defined.

  Note the command must be made available via `From Stdlib` `Require Import` `FunInd`.

Warning

There is a difference between induction schemes generated by the command `Functional Scheme` and these generated by the `Function`. Indeed, `Function` generally produces smaller principles that are closer to how a user would implement them. See Advanced recursive functions for details.

Example

Induction scheme for div2.

We define the function div2 as follows:

From Stdlib Require Import FunInd.
  Toplevel input, characters 27-33: > From Stdlib Require Import FunInd. > ^^^^^^ Error: Cannot find a physical path bound to logical path FunInd with prefix Stdlib.
From Stdlib Require Import Arith.
  Toplevel input, characters 27-32: > From Stdlib Require Import Arith. > ^^^^^ Error: Cannot find a physical path bound to logical path Arith with prefix Stdlib.
Fixpoint div2 (n:nat) : nat := match n with | O => 0 | S O => 0 | S (S n') => S (div2 n') end.
  div2 is defined div2 is recursively defined (guarded on 1st argument)

The definition of a principle of induction corresponding to the recursive structure of `div2` is defined by the command:

Functional Scheme div2_ind := Induction for div2 Sort Prop.
  Toplevel input, characters 27-29: > Functional Scheme div2_ind := Induction for div2 Sort Prop. > ^^ Error: Syntax error: [ltac_use_default] expected after [tactic] (in [tactic_command]).

You may now look at the type of div2_ind:

Check div2_ind.
  Toplevel input, characters 6-14: > Check div2_ind. > ^^^^^^^^ Error: The reference div2_ind was not found in the current environment. Did you mean sig2_ind?

We can now prove the following lemma using this principle:

Lemma div2_le' : forall n:nat, div2 n <= n.
  Toplevel input, characters 0-43: > Lemma div2_le' : forall n:nat, div2 n <= n. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.
intro n.
  Toplevel input, characters 0-7: > intro n. > ^^^^^^^ Error: No product even after head-reduction.
pattern n, (div2 n).
  1 goal n, m : nat ============================ (fun n0 _ : nat => n0 - m <= n0) n (div2 n)
apply div2_ind; intros.
  Toplevel input, characters 6-14: > apply div2_ind; intros. > ^^^^^^^^ Error: The variable div2_ind was not found in the current environment.
auto with arith.
  Toplevel input, characters 0-15: > auto with arith. > ^^^^^^^^^^^^^^^ Error: No such Hint database: arith.
auto with arith.
  Toplevel input, characters 0-15: > auto with arith. > ^^^^^^^^^^^^^^^ Error: No such Hint database: arith.
simpl; auto with arith.
  Toplevel input, characters 7-22: > simpl; auto with arith. > ^^^^^^^^^^^^^^^ Error: No such Hint database: arith.
Qed.
  Toplevel input, characters 0-4: > Qed. > ^^^^ Error: (in proof le_minus): Attempt to save an incomplete proof (there are remaining open goals).

We can use directly the functional induction (`functional induction`) tactic instead of the pattern/apply trick:

Reset div2_le'.
Lemma div2_le : forall n:nat, div2 n <= n.
  Toplevel input, characters 0-42: > Lemma div2_le : forall n:nat, div2 n <= n. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.
intro n.
  Toplevel input, characters 0-7: > intro n. > ^^^^^^^ Error: No product even after head-reduction.
functional induction (div2 n).
  Toplevel input, characters 0-10: > functional induction (div2 n). > ^^^^^^^^^^ Error: The reference functional was not found in the current environment.
auto with arith.
  Toplevel input, characters 0-15: > auto with arith. > ^^^^^^^^^^^^^^^ Error: No such Hint database: arith.
auto with arith.
  Toplevel input, characters 0-15: > auto with arith. > ^^^^^^^^^^^^^^^ Error: No such Hint database: arith.
auto with arith.
  Toplevel input, characters 0-15: > auto with arith. > ^^^^^^^^^^^^^^^ Error: No such Hint database: arith.
Qed.
  Toplevel input, characters 0-4: > Qed. > ^^^^ Error: (in proof le_minus): Attempt to save an incomplete proof (there are remaining open goals).

Example

Induction scheme for tree_size.

We define trees by the following mutual inductive type:

Axiom A : Set.
  A is declared
Inductive tree : Set := node : A -> forest -> tree with forest : Set := | empty : forest | cons : tree -> forest -> forest.
  tree, forest are defined tree_rect is defined tree_ind is defined tree_rec is defined tree_sind is defined forest_rect is defined forest_ind is defined forest_rec is defined forest_sind is defined

We define the function tree_size that computes the size of a tree or a forest. Note that we use `Function` which generally produces better principles.

From Stdlib Require Import FunInd.
  Toplevel input, characters 27-33: > From Stdlib Require Import FunInd. > ^^^^^^ Error: Cannot find a physical path bound to logical path FunInd with prefix Stdlib.
Function tree_size (t:tree) : nat := match t with | node A f => S (forest_size f) end with forest_size (f:forest) : nat := match f with | empty => 0 | cons t f' => (tree_size t + forest_size f') end.
  Toplevel input, characters 0-8: > Function tree_size (t:tree) : nat := match t with | node A f => S (forest_size f) end with forest_size (f:forest) : nat := match f with | empty => 0 | cons t f' => (tree_size t + forest_size f') end. > ^^^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

Notice that the induction principles `tree_size_ind` and `forest_size_ind` generated by `Function` are not mutual.

Check tree_size_ind.
  Toplevel input, characters 6-19: > Check tree_size_ind. > ^^^^^^^^^^^^^ Error: The reference tree_size_ind was not found in the current environment. Did you mean tree_sind?

Mutual induction principles following the recursive structure of `tree_size` and `forest_size` can be generated by the following command:

Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop with forest_size_ind2 := Induction for forest_size Sort Prop.
  Toplevel input, characters 0-10: > Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop with forest_size_ind2 := Induction for forest_size Sort Prop. > ^^^^^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

You may now look at the type of `tree_size_ind2`:

Check tree_size_ind2.
  Toplevel input, characters 6-20: > Check tree_size_ind2. > ^^^^^^^^^^^^^^ Error: The reference tree_size_ind2 was not found in the current environment.

Command Functional Case func_scheme_def
Command Generate graph for qualid

  Internal debugging commands.

## Flags

Flag Functional Induction Rewrite Dependent

  Makes FunInd use dependent `subst` instead of `simple subst`. On by default.

Flag Function_raw_tcc

  When Function is using a well-founded relation, this flag (when set) prevents the post-processing of the tcc (type checking conditions) generated for termination. (The post-processing is basically conjunction splitting + auto.) Off by default.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF