Functional induction¶
Advanced recursive functions¶
The following command is available when the FunInd
library has been loaded via 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 (seefunctional induction
) and its fixpoint equality. This defines a function similar to those defined byFixpoint
. As inFixpoint
, the decreasing argument must be given (unless the function is not recursive), but it might not necessarily be structurally decreasing. Use thefixannot
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 thewith
clause to create mutually recursive definitions, however this feature is limited to structurally recursive functions (i.e. whenfixannot
is astruct
clause).See
functional induction
andFunctional Scheme
for how to use the induction principle to reason easily about the function.The form of the
fixannot
clause determines which definition mechanismFunction
uses. (Note that references toident
below refer to the name of the function being defined.):If
fixannot
is not specified,Function
defines the nonrecursive functionident
as if it was declared withDefinition
. In addition, the following are defined:If
{ struct ... }
is specified,Function
defines the structural recursive functionident
as if it was declared withFixpoint
. In addition, the following are defined:If
{ measure ... }
or{ wf ... }
are specified,Function
defines a recursive function by wellfounded recursion. The moduleRecdef
of the standard library must be loaded for this feature.{measure one_term_{1} ident? one_term_{2}? }
: whereident
is the decreasing argument andone_term_{1}
is a function from the type ofident
tonat
for which the decreasing argument decreases (for thelt
order onnat
) for each recursive call of the function. The parameters of the function are bound inone_term_{1}
.{wf one_term ident }
: whereident
is the decreasing argument andone_term
is an ordering relation on the type ofident
(i.e. of typeT
\(_{\sf ident}\) →T
\(_{\sf ident}\) →Prop
) for which the decreasing argument decreases for each recursive call of the function. The order must be wellfounded. The parameters of the function are bound inone_term
.
If the clause is
measure
orwf
, 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 iswf
) a proof that the ordering relation is wellfounded. Once proof obligations are discharged, the following objects are defined: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:
 Require Import FunInd.
 [Loading ML file extraction_plugin.cmxs ... done] [Loading ML file recdef_plugin.cmxs ... done]
 Function plus (m n : nat) {struct n} : nat := match n with  0 => m  S p => S (plus m p) end.
 plus is defined plus is recursively defined (guarded on 2nd argument) plus_equation is defined plus_rect is defined plus_ind is defined plus_rec is defined R_plus_correct is defined R_plus_complete is defined
than like this:
 Require Import FunInd.
 Function plus (n m : nat) {struct n} : nat := match n with  0 => m  S p => S (plus p m) end.
 plus is defined plus is recursively defined (guarded on 1st argument) plus_equation is defined plus_rect is defined plus_ind is defined plus_rec is defined R_plus_correct is defined R_plus_complete is defined
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
:
 Require List.
 Import List.ListNotations.
 Function wrong (C:nat) : nat := List.hd 0 (List.map wrong (C::nil)).
 Toplevel input, characters 070: > Function wrong (C:nat) : nat := List.hd 0 (List.map wrong (C::nil)). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Recursive definition of wrong is illformed. In environment wrong : nat > nat C : nat Recursive call to wrong has principal argument equal to "C" instead of a subterm of "C". Recursive definition is: "fun C : nat => List.hd 0 (List.map wrong [C])".
For now, dependent cases are not treated for non structurally terminating functions.

Error
The recursive argument must be specified.
¶

Error
Cannot use mutual definition with wellfounded 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. Onlyident
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. Onlyident
is defined. Please report.

Warning
Cannot build functional inversion principle.
¶ functional inversion
will not be available for the function.
Tactics¶

Tactic
functional induction (qualid term+)
¶ The tactic functional induction performs case analysis and induction following the definition of a function. It makes use of a principle generated by
Function
orFunctional Scheme
. Note that this tactic is only available after aRequire Import FunInd
.Example
 Require Import FunInd.
 Functional Scheme minus_ind := Induction for minus Sort Prop.
 sub_equation is defined minus_ind is defined
 Check minus_ind.
 minus_ind : forall P : nat > nat > nat > Prop, (forall n m : nat, n = 0 > P 0 m n) > (forall n m k : nat, n = S k > m = 0 > P (S k) 0 n) > (forall n m k : nat, n = S k > forall l : nat, m = S l > P k l (k  l) > P (S k) (S l) (k  l)) > forall n m : nat, P n m (n  m)
 Lemma le_minus (n m:nat) : n  m <= n.
 1 subgoal n, m : nat ============================ n  m <= n
 functional induction (minus n m) using minus_ind; simpl; auto.
 No more subgoals.
 Qed.
Note
(qualid term+)
must be a correct full application ofqualid
. In particular, the rules for implicit arguments are the same as usual. For example use@qualid
if you want to write implicit arguments explicitly.Note
functional induction (f x1 x2 x3)
is actually a wrapper forinduction x1, x2, x3, (f x1 x2 x3) using qualid
followed by a cleaning phase, wherequalid
is the induction principle registered forf
(by theFunction
orFunctional Scheme
command) corresponding to the sort of the goal. Thereforefunctional induction
may fail if the induction schemequalid
is not defined.Note
There is a difference between obtaining an induction scheme for a function by using
Function
and by usingFunctional Scheme
after a normal definition usingFixpoint
orDefinition
.
Error
Not the right number of induction arguments.
¶

Variant
functional induction (qualid term+) as simple_intropattern using term with bindings_list
Similarly to
induction
andelim
, this allows giving explicitly the name of the introduced variables, the induction principle, and the values of dependent premises of the elimination scheme, including predicates for mutual induction whenqualid
is part of a mutually recursive definition.

Tactic
functional inversion ident
¶ functional inversion
is a tactic that performs inversion on hypothesisident
of the formqualid term+ = term
orterm = qualid term+
wherequalid
must have been defined usingFunction
. Note that this tactic is only available after aRequire Import FunInd
.
Error
Cannot find inversion information for hypothesis ident.
¶ This error may be raised when some inversion lemma failed to be generated by Function.

Variant
functional inversion num
This does the same thing as
intros until num
followed byfunctional inversion ident
whereident
is the identifier for the last introduced hypothesis.

Variant
functional inversion ident qualid

Variant
functional inversion num qualid
If the hypothesis
ident
(ornum
) has a type of the formqualid_{1} term_{i}+ = qualid_{2} term_{j}+
wherequalid_{1}
andqualid_{2}
are valid candidates to functional inversion, this variant allows choosing whichqualid
is inverted.

Error
Generation of induction principles with Functional
Scheme
¶

Command
Functional Scheme ident_{0} := Induction for ident' Sort sort with ident_{i} := Induction for ident_{i}' Sort sort*
¶ This command is a highlevel experimental tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. First, it must be made available via
Require Import FunInd
. Eachident_{i}
is a different mutually defined function name (the names must be in the same order as when they were defined). This command generates the induction principle for eachident_{i}
, following the recursive structure and case analyses of the corresponding functionident_{i}'
.
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:
 Require Import FunInd.
 Require Import Arith.
 [Loading ML file newring_plugin.cmxs ... done]
 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.
 div2_equation is defined div2_ind is defined
You may now look at the type of div2_ind:
 Check div2_ind.
 div2_ind : forall P : nat > nat > Prop, (forall n : nat, n = 0 > P 0 0) > (forall n n0 : nat, n = S n0 > n0 = 0 > P 1 0) > (forall n n0 : nat, n = S n0 > forall n' : nat, n0 = S n' > P n' (div2 n') > P (S (S n')) (S (div2 n'))) > forall n : nat, P n (div2 n)
We can now prove the following lemma using this principle:
 Lemma div2_le' : forall n:nat, div2 n <= n.
 1 subgoal ============================ forall n : nat, div2 n <= n
 intro n.
 1 subgoal n : nat ============================ div2 n <= n
 pattern n, (div2 n).
 1 subgoal n : nat ============================ (fun n0 n1 : nat => n1 <= n0) n (div2 n)
 apply div2_ind; intros.
 3 subgoals n, n0 : nat e : n0 = 0 ============================ 0 <= 0 subgoal 2 is: 0 <= 1 subgoal 3 is: S (div2 n') <= S (S n')
 auto with arith.
 2 subgoals n, n0, n1 : nat e : n0 = S n1 e0 : n1 = 0 ============================ 0 <= 1 subgoal 2 is: S (div2 n') <= S (S n')
 auto with arith.
 1 subgoal n, n0, n1 : nat e : n0 = S n1 n' : nat e0 : n1 = S n' H : div2 n' <= n' ============================ S (div2 n') <= S (S n')
 simpl; auto with arith.
 No more subgoals.
 Qed.
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.
 1 subgoal ============================ forall n : nat, div2 n <= n
 intro n.
 1 subgoal n : nat ============================ div2 n <= n
 functional induction (div2 n).
 3 subgoals ============================ 0 <= 0 subgoal 2 is: 0 <= 1 subgoal 3 is: S (div2 n') <= S (S n')
 auto with arith.
 2 subgoals ============================ 0 <= 1 subgoal 2 is: S (div2 n') <= S (S n')
 auto with arith.
 1 subgoal n' : nat IHn0 : div2 n' <= n' ============================ S (div2 n') <= S (S n')
 auto with arith.
 No more subgoals.
 Qed.
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.
 Require Import FunInd.
 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.
 tree_size is defined forest_size is defined tree_size, forest_size are recursively defined (guarded respectively on 1st, 1st arguments) tree_size_equation is defined tree_size_rect is defined tree_size_ind is defined tree_size_rec is defined forest_size_equation is defined forest_size_rect is defined forest_size_ind is defined forest_size_rec is defined R_tree_size_correct is defined R_forest_size_correct is defined R_tree_size_complete is defined R_forest_size_complete is defined
Notice that the induction principles tree_size_ind
and forest_size_ind
generated by Function
are not mutual.
 Check tree_size_ind.
 tree_size_ind : forall P : tree > nat > Prop, (forall (t : tree) (A : A) (f : forest), t = node A f > P (node A f) (S (forest_size f))) > forall t : tree, P t (tree_size t)
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.
 tree_size_ind2 is defined forest_size_ind2 is defined
You may now look at the type of tree_size_ind2
:
 Check tree_size_ind2.
 tree_size_ind2 : forall (P : tree > nat > Prop) (P0 : forest > nat > Prop), (forall (t : tree) (A : A) (f : forest), t = node A f > P0 f (forest_size f) > P (node A f) (S (forest_size f))) > (forall f0 : forest, f0 = empty > P0 empty 0) > (forall (f1 : forest) (t : tree) (f' : forest), f1 = cons t f' > P t (tree_size t) > P0 f' (forest_size f') > P0 (cons t f') (tree_size t + forest_size f')) > forall t : tree, P t (tree_size t)