\[\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

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 (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:

Require Import FunInd.
[Loading ML file extraction_plugin.cmxs (using legacy method) ... done] [Loading ML file funind_plugin.cmxs (using legacy method) ... 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 0-70: > Function wrong (C:nat) : nat := List.hd 0 (List.map wrong (C::nil)). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Recursive definition of wrong is ill-formed. In environment wrong : nat -> nat C : nat l := [C]%list : list 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 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 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

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 goal n, m : nat ============================ n - m <= n
functional induction (minus n m) using minus_ind; simpl; auto.
No more goals.
Qed.

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

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 qualids must be given in the same order as when they were defined.

Note the command must be made available via 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:

Require Import FunInd.
Require Import Arith.
[Loading ML file ring_plugin.cmxs (using legacy method) ... 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 goal ============================ forall n : nat, div2 n <= n
intro n.
1 goal n : nat ============================ div2 n <= n
pattern n, (div2 n).
1 goal n : nat ============================ (fun n0 n1 : nat => n1 <= n0) n (div2 n)
apply div2_ind; intros.
3 goals n, n0 : nat e : n0 = 0 ============================ 0 <= 0 goal 2 is: 0 <= 1 goal 3 is: S (div2 n') <= S (S n')
auto with arith.
2 goals n, n0, n1 : nat e : n0 = S n1 e0 : n1 = 0 ============================ 0 <= 1 goal 2 is: S (div2 n') <= S (S n')
auto with arith.
1 goal 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 goals.
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 goal ============================ forall n : nat, div2 n <= n
intro n.
1 goal n : nat ============================ div2 n <= n
functional induction (div2 n).
3 goals ============================ 0 <= 0 goal 2 is: 0 <= 1 goal 3 is: S (div2 n') <= S (S n')
auto with arith.
2 goals ============================ 0 <= 1 goal 2 is: S (div2 n') <= S (S n')
auto with arith.
1 goal n' : nat IHn0 : div2 n' <= n' ============================ S (div2 n') <= S (S n')
auto with arith.
No more goals.
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)