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

Inductive types and recursive functions

The Inductive command allows defining types by cases on the form of the inhabitants of the type. These constructors can recursively have arguments in the type being defined. In contrast, in types defined by the Variant command, such recursive references are not permitted. Inductive types include natural numbers, lists and well-founded trees. Inhabitants of inductive types can recursively nest only a finite number of constructors. So, they are well-founded. This distinguishes them from CoInductive types, such as streams, whose constructors can be infinitely nested. In Rocq, Variant types thus correspond to the common subset of inductive and coinductive types that are non-recursive.

Due to the recursive structure of inductive types, functions on inductive types generally must be defined recursively using the fix expression (see term_fix) or the Fixpoint command.

Inductive types

Command Inductive inductive_definition with inductive_definition*

Command Inductive record_definition with record_definition*

inductive_definition::=ident cumul_univ_decl? binder* | binder*? : type? := |? constructor+|? decl_notations?constructor::=#[ attribute+, ]* ident binder* of term99+&? of_type_inst?

Constructor idents can come with binders, in which case the actual type of the constructor is forall binder*, type, where type is its result type. For inductive types without indices, this result type can be omitted and is inferred from the declaration.

of term99+&? of T1 & ... & Tn is syntactic sugar for anonymous binders (_ : T1) ... (_ : Tn).

Constructor arguments can be declared using three alternative syntaxes.

Example: Constructor argument syntaxes

The following declarations use a full constructor type, anonymous binders, and of, respectively, to describe pairs of booleans.

Inductive bool_pair_type : Type := | pair_type : bool -> bool -> bool_pair_type.: bool_pair_type is defined bool_pair_type_rect is defined bool_pair_type_ind is defined bool_pair_type_rec is defined bool_pair_type_sind is defined
Inductive bool_pair_binders : Type := | pair_binders (_ : bool) (_ : bool).: bool_pair_binders is defined bool_pair_binders_rect is defined bool_pair_binders_ind is defined bool_pair_binders_rec is defined bool_pair_binders_sind is defined
Inductive bool_pair_of : Type := | pair_of of bool & bool.: bool_pair_of is defined bool_pair_of_rect is defined bool_pair_of_ind is defined bool_pair_of_rec is defined bool_pair_of_sind is defined

Mutually inductive types can be defined by including multiple inductive_definitions. The idents are simultaneously added to the global environment before the types of constructors are checked. Each ident can be used independently thereafter. However, the automatically generated induction principles do not provide induction hypotheses for the other mutually defined types. Use the Scheme command to generate mutual induction principles. See Mutually defined inductive types.

Example: Mutually inductive predicates

The following predicates characterize even and odd natural numbers. Each refers to the other, so they are declared together using with.

Inductive even : nat -> Prop := | even_zero : even 0 | even_succ : forall n, odd n -> even (S n) with odd : nat -> Prop := | odd_succ : forall n, even n -> odd (S n).: even, odd are defined even_ind is defined even_sind is defined odd_ind is defined odd_sind is defined

If the entire inductive definition is parameterized with binders, those inductive parameters correspond to a local context in which the entire set of inductive declarations is interpreted. Within a mutual declaration, all inductive types must have the same parameter binders, with the same names and types in the same order. See Parameterized inductive types.

| binder*?: The | separates uniform and non-uniform parameters. See Uniform Inductive Parameters for more details.

The Inductive command supports the universes(polymorphic), universes(template), universes(cumulative), universes(collapse_sort_variables), bypass_check(universes), bypass_check(positivity), private(matching) and schemes attributes.

When record syntax ({ ... }) is used, projections(primitive) is also supported, while private(matching) and the bypass_check attributes are not supported. In record syntax, the optional as ident part specifies the name to use for inhabitants of the record in the type of projections.

Automatic Prop lowering

When an inductive type is declared without an explicit sort, it is put in the smallest sort which permits large elimination, that is, elimination into Set or Type (excluding SProp from the inferred sorts). For empty and singleton types this means they are declared in Prop. An empty type has no constructors; a singleton type has one constructor whose arguments, if any, are proofs.

Example: Inferring sorts

Neither declaration below specifies a sort. The first has one constructor without arguments, so Rocq declares it in Prop. The second stores an element of A : Type, so inferred_box A belongs to Type.

Inductive inferred_singleton := inferred_singleton_intro.: inferred_singleton is defined inferred_singleton_rect is defined inferred_singleton_ind is defined inferred_singleton_rec is defined inferred_singleton_sind is defined
Inductive inferred_box (A : Type) := | inferred_box_intro : A -> inferred_box A.: inferred_box is defined inferred_box_rect is defined inferred_box_ind is defined inferred_box_rec is defined inferred_box_sind is defined

Check inferred_singleton.: inferred_singleton : Prop
Check inferred_box Type.: inferred_box Type : Type

Positivity Condition

To be accepted, an inductive type must satisfy the strict positivity condition. See Positivity Condition for the exact condition, including for mutual and nested inductive types. Informally, the inductive type being defined must not occur to the left of an arrow within an argument type, even under another arrow. It may occur to the right of an arrow whose domain does not contain that type.

Error Non strictly positive occurrence of ident in type.: An occurrence of the inductive type in a constructor argument violates the strict positivity condition. Positivity checking can be disabled using the Positivity Checking flag or the bypass_check(positivity) attribute (see Controlling Typing Flags).

Example: An inductive type in the domain of a function argument

The constructor below takes a function whose input has type negative, the type being defined. This occurrence is to the left of an arrow in the constructor argument type negative -> nat, so it is rejected.

Fail Inductive negative : Type := | negative_intro : (negative -> nat) -> negative.: The command has indeed failed with message: Non strictly positive occurrence of "negative" in "(negative -> nat) -> negative".

Example: Two arrows do not restore strict positivity

Nesting double_negative -> nat in another function domain does not make the recursive occurrence strictly positive. The type being defined still occurs to the left of an arrow within the constructor argument type, so Rocq rejects the following definition as well:

Fail Inductive double_negative : Type := | double_negative_intro : ((double_negative -> nat) -> nat) -> double_negative.: The command has indeed failed with message: Non strictly positive occurrence of "double_negative" in "((double_negative -> nat) -> nat) -> double_negative".

Constructor conclusions must also satisfy a separate requirement: they must return the inductive type being defined.

Error The conclusion of type is not valid; it must be built from ident.

The conclusion of each constructor type must be the inductive type ident being defined, applied to its parameters and indices when present.

Example: A constructor with an invalid conclusion

The constructor below returns nat instead of the type invalid_conclusion being defined, so Rocq rejects the declaration.

Fail Inductive invalid_conclusion : Type := | invalid_conclusion_intro : nat.: The command has indeed failed with message: In environment invalid_conclusion : Univ Unable to unify "nat" with "invalid_conclusion".

Eliminators

By default, Rocq automatically generates eliminators, also known as induction principles, for an inductive type, depending on the sort to which it belongs and the sorts into which it can be eliminated.

The induction principles are named ident_rect, ident_ind, ident_rec and ident_sind, corresponding respectively to elimination into Type, Prop, Set and SProp. Their types express structural induction or recursion over objects of type ident. These constants are generated when permitted by the elimination restrictions. For instance, ident_rect may not be generated when ident is a proposition.

Example: Generated eliminators

The eliminators bool_ind and bool_rect each require cases for true and false. Their predicates take values in Prop and Type, respectively.

Check bool_ind.: bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
Check bool_rect.: bool_rect : forall P : bool -> Type, P true -> P false -> forall b : bool, P b

Variants of these eliminators as well as other schemes can be generated with the Scheme command. See also Automatic declaration of schemes for the flags and attribute controlling the automatic generation of these schemes.

Flag Dependent Proposition Eliminators

This flag controls whether automatically generated induction principles for inductive types explicitly declared in Prop are dependent. It defaults to off: the result type does not depend on the proof being eliminated. When the flag is on, the result type may depend on that proof. For example, when eliminating p : P, a dependent principle can establish Q p, whereas a non-dependent principle establishes a result whose type does not depend on p. The flag does not relax the restrictions on the sorts into which the inductive type can be eliminated.

Example: Non-dependent and dependent principles

The two propositions below have the same form, but the generated principles differ. In plain_proof_ind, P is a proposition. In dependent_proof_ind, P is a predicate on proofs of dependent_proof.

Unset Dependent Proposition Eliminators.
Inductive plain_proof : Prop := plain_intro.: plain_proof is defined plain_proof_rect is defined plain_proof_ind is defined plain_proof_rec is defined plain_proof_sind is defined

Check plain_proof_ind.: plain_proof_ind : forall P : Prop, P -> plain_proof -> P

Set Dependent Proposition Eliminators.
Inductive dependent_proof : Prop := dependent_intro.: dependent_proof is defined dependent_proof_rect is defined dependent_proof_ind is defined dependent_proof_rec is defined dependent_proof_sind is defined

Check dependent_proof_ind.: dependent_proof_ind : forall P : dependent_proof -> Prop, P dependent_intro -> forall d : dependent_proof, P d

Unset Dependent Proposition Eliminators.

The flag is consulted when the inductive type is declared; changing it does not alter principles already generated. Types automatically lowered to Prop already receive dependent principles, even when the flag is off. For other sorts, generated principles are also dependent whenever the inductive type permits dependent elimination. Some records using Primitive Projections do not permit it.

With Scheme, dependent induction corresponds to Induction and non-dependent induction to Minimality in scheme_type. Explicit declarations through this command are not affected by the flag. The flag can also affect the names automatically chosen for variables introduced by tactics such as destruct.

Examples of inductive types and eliminators

The following sections show examples of simple inductive types, simple indexed inductive types, parameterized inductive types, mutually defined inductive types and nested inductive types.

Simple inductive types

A simple inductive type belongs to a universe that is a simple sort.

Example

The set of natural numbers is defined as:

Inductive nat : Set := | O : nat | S : nat -> nat.: nat is defined nat_rect is defined nat_ind is defined nat_rec is defined nat_sind is defined

The type nat is defined as the least Set containing O and closed by the S constructor. The names nat, O and S are added to the global environment.

This definition generates four induction principles: nat_rect, nat_ind, nat_rec and nat_sind. The type of nat_ind is:

Check nat_ind.: nat_ind : forall P : nat -> Prop, P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

This is the well known structural induction principle over natural numbers, i.e. the second-order form of Peano’s induction principle. It allows proving universal properties of natural numbers (forall n:nat, P n) by induction on n.

The types of nat_rect, nat_rec and nat_sind are similar, except that they apply to, respectively, (P:nat->Type), (P:nat->Set) and (P:nat->SProp). They correspond to primitive induction principles (allowing dependent types) respectively over sorts Type, Set and SProp.

In the case where inductive types don't have indices (the next section gives an example of indices), a constructor can be defined by giving the type of its arguments alone.

Example

Reset nat.

Inductive nat : Set := O | S (_:nat).: nat is defined nat_rect is defined nat_ind is defined nat_rec is defined nat_sind is defined

Simple indexed inductive types

An indexed inductive definition has arguments called indices, whose instantiations may differ between constructor conclusions. Its type is an arity of the form forall x1 : T1, ... forall xn : Tn, s, where s is a sort.

Example: The Collatz predicate

The following predicate describes natural numbers that reach 1 after finitely many Collatz steps: an even number is divided by 2, and an odd number is multiplied by 3 and increased by 1.

Import Nat.
Inductive even : nat -> Prop := | even_zero : even 0 | even_succ : forall n, odd n -> even (S n) with odd : nat -> Prop := | odd_succ : forall n, even n -> odd (S n).: even, odd are defined even_ind is defined even_sind is defined odd_ind is defined odd_sind is defined

Inductive collatz : nat -> Prop := | collatz_root : collatz 1 | collatz_even n : even n -> collatz (n / 2) -> collatz n | collatz_odd n : odd n -> collatz (3 * n + 1) -> collatz n.: collatz is defined collatz_ind is defined collatz_sind is defined

The natural number n is an index of collatz. The constructor collatz_root establishes collatz 1. The other constructors establish collatz n from the corresponding parity condition and a proof of collatz at the next step. Thus, constructor conclusions can instantiate the index with a fixed value such as 1 or a constructor-bound variable such as n. Recursive occurrences can use a different index, here n / 2 or 3 * n + 1.

Check collatz_ind.: collatz_ind : forall P : nat -> Prop, P 1 -> (forall n : nat, even n -> collatz (n / 2) -> P (n / 2) -> P n) -> (forall n : nat, odd n -> collatz (3 * n + 1) -> P (3 * n + 1) -> P n) -> forall n : nat, collatz n -> P n

The principle collatz_ind establishes that a predicate P : nat -> Prop holds for every natural number satisfying collatz. It requires a proof of P 1 and two step cases. The even case assumes even n, collatz (n / 2), and the induction hypothesis P (n / 2), and must prove P n. Similarly, the odd case assumes odd n, collatz (3 * n + 1), and P (3 * n + 1), and must prove P n. Induction follows the structure of the proof of collatz n, even though the next step need not be a smaller natural number.

Parameterized inductive types

In the previous example, constructor conclusions instantiate the index with 1 or the constructor-bound variable n. Parameters, in contrast, are binders shared by all constructors. Every constructor conclusion uses the parameters bound by the declaration as their instantiations.

Parameters need not have the same instantiation in recursive occurrences within constructor arguments. A parameter is uniform when it has the same instantiation in all recursive occurrences as in the constructor conclusions; otherwise, it is non-uniform. The distinction is determined by how the parameter is used in the definition.

An inductive definition can use indices in place of parameters, but this can affect its sort and elimination principles. Constructors must then quantify explicitly over the arguments that were parameters; this quantification can impose higher universe requirements. The induction predicate is quantified over the indices, whereas a uniform parameter is fixed before the induction predicate is introduced.

Uniform parameters

In every constructor conclusion, the inductive type must be applied to the parameters bound by the declaration. In recursive occurrences of the inductive type within constructor arguments, uniform parameters must be instantiated with the same values as in the constructor conclusion.

Example

A typical example is the definition of polymorphic lists:

Inductive list (A:Set) : Set := | nil : list A | cons : A -> list A -> list A.: list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined

In the type of nil and cons, we write "list A" and not just "list". The constructors nil and cons have these types:

Check nil.: nil : forall A : Set, list A
Check cons.: cons : forall A : Set, A -> list A -> list A

Observe that the induction principles are also quantified with (A:Set), for example:

Check list_ind.: list_ind : forall (A : Set) (P : list A -> Prop), P (nil A) -> (forall (a : A) (l : list A), P l -> P (cons A a l)) -> forall l : list A, P l

Once again, the names of the constructor arguments and the type of the conclusion can be omitted:

Reset list.

Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).: list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined

Non-uniform parameters

In constructor conclusions, a non-uniform parameter must be instantiated with the parameter bound by the declaration. In recursive occurrences within constructor arguments, it may be instantiated with a different term. The induction principle must therefore allow its predicate to vary with that parameter, whereas a uniform parameter is fixed throughout induction.

Example: A non-uniform parameter in recursive occurrences

In the power list type plist, the constructor pcons takes a recursive argument of type plist (A * A) and returns plist A. Thus, A is a non-uniform parameter: it is instantiated with A * A in the recursive argument and with A in the constructor conclusion.

Inductive plist (A : Set) : Set := | pnil : plist A | pcons : A -> plist (A * A) -> plist A.: plist is defined plist_rect is defined plist_ind is defined plist_rec is defined plist_sind is defined

Unlike list_ind, whose predicate concerns lists over one fixed type A, plist_ind takes a predicate over all element types in Set. Its recursive premise uses that predicate at A * A.

Check plist_ind.: plist_ind : forall P : forall A : Set, plist A -> Prop, (forall A : Set, P A (pnil A)) -> (forall (A : Set) (a : A) (p : plist (A * A)), P (A * A)%type p -> P A (pcons A a p)) -> forall (A : Set) (p : plist A), P A p

Example: Invalid parameter instantiation in constructor conclusions

Even a non-uniform parameter must be instantiated with the parameter bound by the declaration in each constructor conclusion. The following declaration is rejected because its constructors return listw (A * A) instead of listw A:

Fail Inductive listw (A : Set) : Set := | nilw : listw (A * A) | consw : A -> listw (A * A) -> listw (A * A).: The command has indeed failed with message: In environment listw : Set -> Set A : Set Unable to unify "listw (A * A)%type" with "listw A".

The separator | specifies which parameters are abstracted during constructor checking. Parameters before it are uniform by construction and are omitted from recursive occurrences within the declaration. Parameters after it are supplied explicitly and may be used uniformly or non-uniformly. Outside the declaration, the inductive type takes both groups as arguments.

Example: Using | in parameters

A parameter after | can still be uniform, as A is here:

Inductive explicit_list | (A : Type) : Type := | explicit_nil : explicit_list A | explicit_cons : A -> explicit_list A -> explicit_list A.: explicit_list is defined explicit_list_rect is defined explicit_list_ind is defined explicit_list_rec is defined explicit_list_sind is defined

Check explicit_list_ind.: explicit_list_ind : forall (A : Type) (P : explicit_list A -> Prop), P (explicit_nil A) -> (forall (a : A) (e : explicit_list A), P e -> P (explicit_cons A a e)) -> forall e : explicit_list A, P e

As in list_ind, A is fixed before the induction predicate is introduced.

However, placing A before | prevents the non-uniform instantiation used in plist: during constructor checking, uniform_plist takes no explicit parameter, so applying it to A * A is rejected.

Fail Inductive uniform_plist (A : Set) | : Set := | uniform_pnil : uniform_plist | uniform_pcons : A -> uniform_plist (A * A)%type -> uniform_plist.: The command has indeed failed with message: Illegal application (Non-functional construction): The expression "uniform_plist" of type "Set" cannot be applied to the term "(A * A)%type" : "Set"

Flag Uniform Inductive Parameters

This flag determines the implicit position of | when the declaration does not contain an explicit separator. It defaults to off, corresponding to placing | before all parameters. When on, it corresponds to placing | after all parameters.

When the flag is on, all parameters are abstracted during constructor checking and are uniform by construction. They are therefore omitted from recursive occurrences within the declaration. When the flag is off, parameters are supplied explicitly, as in list A and plist (A * A) above, and may be used uniformly or non-uniformly.

Example: Declaring uniform parameters implicitly

With the flag on, A is fixed throughout the declaration, so the recursive occurrence is written list3 rather than list3 A.

Set Uniform Inductive Parameters.
Inductive list3 (A : Set) : Set := | nil3 : list3 | cons3 : A -> list3 -> list3.: list3 is defined list3_rect is defined list3_ind is defined list3_rec is defined list3_sind is defined
Unset Uniform Inductive Parameters.

This is equivalent to declaring the type in a section with A in the context (see Sections):

Section list3.
Context (A : Set).: A is declared
Inductive list3 : Set := | nil3 : list3 | cons3 : A -> list3 -> list3.: list3 is defined list3_rect is defined list3_ind is defined list3_rec is defined list3_sind is defined
End list3.

An explicit | overrides the flag. Only the parameters before the separator are abstracted during constructor checking; those after it are supplied explicitly and may be used uniformly or non-uniformly.

Example: Explicit non-uniform parameters with the flag on

Placing | before A allows it to be non-uniform even with the flag on. As in plist, the recursive argument instantiates A with A * A.

Set Uniform Inductive Parameters.
Inductive explicit_plist | (A : Set) : Set := | explicit_pnil : explicit_plist A | explicit_pcons : A -> explicit_plist (A * A) -> explicit_plist A.: explicit_plist is defined explicit_plist_rect is defined explicit_plist_ind is defined explicit_plist_rec is defined explicit_plist_sind is defined
Unset Uniform Inductive Parameters.

Mutually defined inductive types

The automatically generated induction principles do not provide induction hypotheses for the other mutually defined types. Use the Scheme command to generate mutual induction principles.

Example: Mutually defined inductive types

A typical example of mutually inductive data types is trees and forests. We assume two types A and B that are given as variables. The types can be declared like this:

Parameters A B : Set.: A is declared B is declared
Inductive tree : Set := node : A -> forest -> tree with forest : Set := | leaf : B -> 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

This declaration automatically generates eight induction principles. They are not the most general principles, but they correspond to each inductive part seen as a single inductive definition.

To illustrate this point on our example, here are the types of tree_rec and forest_rec.

Check tree_rec.: tree_rec : forall P : tree -> Set, (forall (a : A) (f : forest), P (node a f)) -> forall t : tree, P t
Check forest_rec.: forest_rec : forall P : forest -> Set, (forall b : B, P (leaf b)) -> (forall (t : tree) (f : forest), P f -> P (cons t f)) -> forall f : forest, P f

Assume we want to parameterize our mutual inductive definitions with the two type variables A and B, the declaration should be done as follows:

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

Assume we define an inductive definition inside a section (cf. Sections). When the section is closed, the variables declared in the section and occurring free in the declaration are added as parameters to the inductive definition.

Nested inductive types

An occurrence of an inductive type in a constructor argument is called nested when it appears as an argument to another inductive type. By extension, an inductive type with nested recursive occurrences is itself called nested. Such occurrences can be accepted if they satisfy the nested positivity condition.

To generate induction hypotheses for nested recursive arguments, Rocq uses an All predicate and its associated theorem registered for the type used for nesting. The predicate expresses that the induction predicate holds for each recursive subterm contained in the nested argument. Without these registered definitions, the generated eliminator has no induction hypothesis for that argument.

For an inductive type, these definitions can be generated and registered with Scheme All before declaring the nested inductive type. See Eliminators for Nested Inductive Types for details on generating and registering them.

Example: Rose trees

A rose tree has leaves labeled with elements of A and nodes containing lists of child trees. In the argument type list (RoseTree A), the recursive occurrence RoseTree A is nested in list. Informally, this is permitted because the element type is a strictly positive uniform parameter of list.

Scheme All for list.: list_all is defined list_all_rect is defined list_all_ind is defined list_all_rec is defined list_all_sind is defined list_all_forall is defined
Inductive RoseTree A : Type := | RTleaf (a : A) : RoseTree A | RTnode (l : list (RoseTree A)) : RoseTree A.: RoseTree is defined RoseTree_rect is defined RoseTree_ind is defined RoseTree_rec is defined RoseTree_sind is defined

The generated principle uses list_all to express the induction hypotheses for the child trees:

Check RoseTree_ind.: RoseTree_ind : forall (A : Type) (P : RoseTree A -> Prop), (forall a : A, P (RTleaf A a)) -> (forall l : list (RoseTree A), list_all (RoseTree A) P l -> P (RTnode A l)) -> forall r : RoseTree A, P r

For a predicate P : RoseTree A -> Prop, the RTnode case requires list_all (RoseTree A) P l, expressing that P holds for every tree in l, to establish P (RTnode A l). The definition of list_all has a case for the empty list and a case requiring P for the head and list_all (RoseTree A) P for the tail:

Print list_all.: Inductive list_all@{α ; u u0} (A : Type) (PA : A -> Univ@{α ; _}) : list A -> Type := nil_all : list_all A PA nil | cons_all : forall a : A, PA a -> forall l : list A, list_all A PA l -> list_all A PA (a :: l). Arguments list_all A%_type_scope PA%_function_scope l%_list_scope Arguments nil_all A%_type_scope PA%_function_scope Arguments cons_all A%_type_scope PA%_function_scope a _ l%_list_scope _

Writing Recursive Functions using Fixpoints

Rocq provides primitive support for defining recursive functions over inductive types using fixpoints. The recommended way to declare such functions is the top-level Fixpoint command. Recursive functions can also be written directly within a term using a fix expression, which is the construction to which Fixpoint declarations are elaborated.

The following subsections describe these two forms and their use. Rocq only accepts terminating recursive functions to preserve consistency. Termination checking is performed by the guard condition.

Top-level recursive functions

The Fixpoint command declares functions defined by structural recursion over inductive types.

Command Fixpoint fix_definition with fix_definition*

fix_definition::=ident_decl binder* fixannot? : type? := term? decl_notations?fixannot::={ struct ident }|{ wf one_term ident }|{ measure one_term ident? one_term? }

Allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define ident as a recursive function with arguments specified by the binders such that ident applied to arguments corresponding to these binders has type type, and is equivalent to the expression term. The type of ident is consequently forall binder*, type and its value is equivalent to fun binder* => term.

This command accepts the same attributes as Definition. The bypass_check(guard) attribute disables termination checking for this definition.

With the program attribute, Fixpoint also supports well-founded recursion: wf specifies a well-founded relation on an argument, while measure specifies a measure that must decrease at recursive calls. Program generates obligations to prove the decrease and well-foundedness of the relation. These annotations are not supported without program. See Program Fixpoint for their syntax, defaults, and examples.

The {struct ident} annotation (see fixannot) selects the structural argument, also called the decreasing argument. Definitions must satisfy the guard condition for that argument. A fixpoint is unfolded only when the structural argument is instantiated with a term starting with a constructor.

If the {struct ident} annotation is omitted, Rocq tries arguments from left to right until it finds one that satisfies the guard condition. If no argument satisfies it, the definition is rejected. Specifying the structural argument explicitly can therefore significantly speed up type checking of large mutual fixpoints.

Example: Minimum of two natural numbers

The following function computes the minimum of two natural numbers. It matches both arguments: if both are successors, it adds one to the minimum of their predecessors; otherwise, it returns zero. The structural argument is inferred to be n.

Fixpoint min_left (n m : nat) : nat := match n with | 0 => 0 | S p => match m with | 0 => 0 | S q => S (min_left p q) end end.: min_left is defined min_left is recursively defined (guarded on 1st argument)

The function unfolds when its first argument starts with a constructor. For 0, it reduces to 0, even when m is a variable:

Goal forall m : nat, min_left 0 m = 0.: 1 goal ============================ forall m : nat, min_left 0 m = 0
Proof.
reflexivity.: No more goals.
Qed.

For S p, it reduces to the inner match on m. This match returns 0 when m is 0, and S (min_left p q) when m is S q:

Goal forall p m : nat, min_left (S p) m = match m with | 0 => 0 | S q => S (min_left p q) end.: 1 goal ============================ forall p m : nat, min_left (S p) m = match m with | 0 => 0 | S q => S (min_left p q) end
Proof.
reflexivity.: No more goals.
Qed.

Example: Inferring or selecting the structural argument

In this addition function, the recursive call leaves n unchanged and decreases m. Rocq therefore selects m as the structural argument:

Fixpoint plus_second (n m : nat) : nat := match m with | 0 => n | S p => S (plus_second n p) end.: plus_second is defined plus_second is recursively defined (guarded on 2nd argument)

Explicitly selecting n prevents this choice. Since only m decreases, the following definition is rejected. Selecting m instead would allow this definition.

Fail Fixpoint wrongplus (n m : nat) {struct n} : nat := match m with | 0 => n | S p => S (wrongplus n p) end.: The command has indeed failed with message: Recursive definition of wrongplus is ill-formed. In environment wrongplus : nat -> nat -> nat n : nat m : nat p : nat Recursive call to wrongplus has principal argument equal to "n" instead of a subterm of "n". Recursive definition is: "fun n m : nat => match m with | 0 => n | S p => S (wrongplus n p) end".

When no argument decreases, inference cannot find a structural argument, and the definition is rejected:

Fail Fixpoint unchanged (n : nat) : nat := unchanged n.: The command has indeed failed with message: Recursive definition of unchanged is ill-formed. In environment unchanged : nat -> nat n : nat Recursive call to unchanged has principal argument equal to "n" instead of a subterm of "n". Recursive definition is: "fun n : nat => unchanged n".

Some fixpoints satisfy the guard condition for more than one argument. The choice affects reduction, since a fixpoint unfolds only when its structural argument starts with a constructor. An explicit annotation is needed to select an argument other than the first one accepted by Rocq.

Example: Choosing another structural argument

In min_left, the recursive call decreases both n and m. The same body can therefore use m as its structural argument.

Fixpoint min_right (n m : nat) {struct m} : nat := match n with | 0 => 0 | S p => match m with | 0 => 0 | S q => S (min_right p q) end end.: min_right is defined min_right is recursively defined (guarded on 2nd argument)

Both functions compute the same minimum, but m now controls unfolding. Unlike min_left 0 m in the previous example, min_right 0 m cannot unfold while m is a variable. Its value can still be shown to be zero by case analysis on m:

Goal forall m : nat, min_right 0 m = 0.: 1 goal ============================ forall m : nat, min_right 0 m = 0
Proof.
Fail reflexivity.: The command has indeed failed with message: In environment m : nat Unable to unify "0" with "min_right 0 m".
destruct m; reflexivity.: No more goals.
Qed.

Conversely, min_right unfolds when m starts with a constructor, even when n is a variable, whereas min_left does not:

Goal forall n : nat, min_right n 0 = match n with 0 => 0 | S _ => 0 end.: 1 goal ============================ forall n : nat, min_right n 0 = match n with | 0 | _ => 0 end
Proof.
reflexivity.: No more goals.
Qed.

The with clause enables users to declare mutually recursive functions. In particular, it can be used to declare functions over mutually defined inductive types.

Example: Mutual fixpoints

For the mutually defined types tree and forest, the size functions call each other when traversing their recursive arguments:

Fixpoint 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 | leaf b => 1 | 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)

If term is omitted, type is required and Rocq enters proof mode. This allows the body to be constructed incrementally using tactics. Moreover, the refine attribute allows specific parts of the body to be constructed in proof mode by replacing them with _. Closing the definition with Defined keeps the resulting constant transparent, allowing the function to unfold and compute. Closing it with Qed instead makes it opaque.

Example: Constructing a fixpoint in proof mode

The following definition doubles a natural number. Case analysis creates a goal for each constructor, and exact supplies the corresponding branch of the body. The successor branch makes a recursive call on the predecessor p.

Fixpoint double (n : nat) : nat.: 1 goal double : nat -> nat n : nat ============================ nat
Proof.
destruct n as [|p].: 2 goals double : nat -> nat ============================ nat goal 2 is: nat
- exact 0.: 1 goal double : nat -> nat ============================ nat This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. 1 goal goal 1 is: nat
- exact (S (S (double p))).: 1 goal double : nat -> nat p : nat ============================ nat No more goals.
Defined.

Compute double 3.: = 6 : nat

#[refine] Fixpoint double' (n : nat) : nat := match n with | 0 => 0 | S p => _ end.: 1 goal double' : nat -> nat n, p : nat ============================ nat
Proof.
exact (S (S (double' p))).: No more goals.
Defined.

Compute double' 3.: = 6 : nat

Primitive fix construction

Rocq provides primitive fixpoints through the fix term constructor, to which top-level Fixpoint declarations are elaborated.

term_fix::=let fix fix_decl in term|fix fix_decl with fix_decl+ for ident?fix_decl::=ident binder* fixannot? : type? := term

The expression "fix ident₁ binder₁ : type₁ := term₁ with … with ident_n binder_n : type_n := term_n for ident_i" denotes the $i$-th component of a block of functions defined by mutual structural recursion. It is the local counterpart of the Fixpoint command. When $n=1$, the "for ident_i" clause is omitted.

A local definition of a single recursive function has a special syntax: let fix ident binder* := term in stands for let ident := fix ident binder* := term in. The same abbreviation is available for cofixpoints.

The fix and let fix expressions support only the struct form of fixannot. The wf and measure forms are supported by commands such as Fixpoint with the program attribute and Function.

The {struct ident} annotation selects the structural argument as for Fixpoint; it can also be omitted to let Rocq infer that argument. Local fixpoints satisfy the same guard condition as top-level definitions.

Warning

Unfolding definitions containing local fixpoints can duplicate those fixpoints in proof terms and cause repeated type and guard checking. Local fixpoints are commonly used in functional programming to write tail-recursive functions. Unfolding such definitions during Rocq proofs can drastically increase the size of the proof term and make it much longer to type-check, as each occurrence of the fixpoint must be type-checked and checked for termination. Defining the helper as a separate top-level Fixpoint allows it to remain a constant when the enclosing definition is unfolded, avoiding repeated guard checking unless the helper itself is unfolded.

Example: Tail-recursive list reversal with a local fixpoint

The function rev uses a local helper aux to accumulate the reversed list. The structural argument is the remaining input list; the accumulator grows with each recursive call.

Local Open Scope list_scope.
Definition rev {T : Type} (l : list T) : list T := let fix aux (p acc : list T) {struct p} : list T := match p with | nil => acc | x :: p => aux p (x :: acc) end in aux l nil.: rev is defined

In the following proof, cbn unfolds rev on both sides of the equality and performs the first recursive call, adding n + 0 and n to the respective accumulators. Since the remaining list l is a variable, aux cannot reduce further and remains exposed in the goal:

Goal forall n l, rev ((n + 0) :: l) = rev (n :: l).: 1 goal ============================ forall (n : nat) (l : list nat), rev (n + 0 :: l) = rev (n :: l)
Proof.
intros n l.: 1 goal n : nat l : list nat ============================ rev (n + 0 :: l) = rev (n :: l)

cbn.: 1 goal n : nat l : list nat ============================ (fix aux (p acc : list nat) {struct p} : list nat := match p with | nil => acc | x :: p0 => aux p0 (x :: acc) end) l (n + 0 :: nil) = (fix aux (p acc : list nat) {struct p} : list nat := match p with | nil => acc | x :: p0 => aux p0 (x :: acc) end) l (n :: nil)

rewrite <- plus_n_O.: 1 goal n : nat l : list nat ============================ (fix aux (p acc : list nat) {struct p} : list nat := match p with | nil => acc | x :: p0 => aux p0 (x :: acc) end) l (n :: nil) = (fix aux (p acc : list nat) {struct p} : list nat := match p with | nil => acc | x :: p0 => aux p0 (x :: acc) end) l (n :: nil)
reflexivity.: No more goals.

Show Proof.: (fun (n : nat) (l : list nat) => eq_ind n (fun n0 : nat => (fix aux (p acc : list nat) {struct p} : list nat := match p with | nil => acc | x :: p0 => aux p0 (x :: acc) end) l (n0 :: nil) = (fix aux (p acc : list nat) {struct p} : list nat := match p with | nil => acc | x :: p0 => aux p0 (x :: acc) end) l (n :: nil)) eq_refl (n + 0) (plus_n_O n) : rev (n + 0 :: l) = rev (n :: l))

Qed.

The proof term produced by reflexivity contains the exposed fixpoint. Type-checking this term therefore type-checks aux and checks its guard condition twice, even though it was already checked when rev was defined.

In contrast, if we define rev' with a real auxiliary function, the fixpoint does not unfold when simplifying the goal with cbn, thus producing a much smaller proof term and avoiding type-checking and checking termination of rev_acc twice more.

Local Open Scope list_scope.
Fixpoint rev_acc {T : Type} (p acc : list T) {struct p} : list T := match p with | nil => acc | x :: p => rev_acc p (x :: acc) end.: rev_acc is defined rev_acc is recursively defined (guarded on 2nd argument)
Definition rev' {T : Type} (l : list T) : list T := rev_acc l nil.: rev' is defined

Goal forall n l, rev' ((n + 0) :: l) = rev' (n :: l).: 1 goal ============================ forall (n : nat) (l : list nat), rev' (n + 0 :: l) = rev' (n :: l)
Proof.
intros n l.: 1 goal n : nat l : list nat ============================ rev' (n + 0 :: l) = rev' (n :: l)

cbn.: 1 goal n : nat l : list nat ============================ rev_acc l (n + 0 :: nil) = rev_acc l (n :: nil)

rewrite <- plus_n_O.: 1 goal n : nat l : list nat ============================ rev_acc l (n :: nil) = rev_acc l (n :: nil)
reflexivity.: No more goals.

Show Proof.: (fun (n : nat) (l : list nat) => eq_ind n (fun n0 : nat => rev_acc l (n0 :: nil) = rev_acc l (n :: nil)) eq_refl (n + 0) (plus_n_O n) : rev' (n + 0 :: l) = rev' (n :: l))

Qed.

The Guard Condition

Rocq checks termination of fixpoints using a guard condition: a syntactic check triggered every time a fixpoint is type-checked. It can also be tested earlier in proof mode using the Guarded command.

The guard condition ensures that each recursive call is performed on a strict subterm of the structural argument, and hence, that the function terminates. Pattern-matching on the structural argument or one of its subterms introduces variables for strictly smaller recursive constructor arguments, on which recursive calls are allowed.

The guard condition consists of a minimal guard and several mostly independent extensions, described below:

Checking fixpoints up to reduction
Propagating subterm information through beta-iota cuts
An advanced subterm analysis that traverses fixpoints and pattern-matching

Guard checking can be disabled with Guard Checking or the bypass_check(guard) attribute. Disabling it risks breaking consistency and subject reduction, so it should be used with caution.

Example: Disabling guard checking breaks consistency

With guard checking disabled, Rocq accepts the following fixpoint even though its recursive call uses the unchanged argument n. The function does not terminate, and its declared return type allows us to prove False by applying it to 0.

#[bypass_check(guard)] Fixpoint loop (n : nat) : False := loop n.: loop is defined loop is recursively defined (guarded on 1st argument)
Unset Guard Checking.
Fixpoint loop' (n : nat) : False := loop' n.: loop' is defined loop' is recursively defined (guarded on 1st argument)
Goal False.: 1 goal ============================ False
Proof.
exact (loop 0).: No more goals.
Qed.

Re-enabling guard checking does not recheck previously accepted definitions: loop remains in the environment. It is therefore possible to reason about a function whose termination is not established by the guard condition.

Example: Using a previously accepted definition

Set Guard Checking.
Goal forall n, loop n = loop n.: 1 goal ============================ forall n : nat, loop n = loop n
Proof.
reflexivity.: No more goals.
Qed.

However, locally disabling and then re-enabling the guard condition is not stable under reduction. Unfolding a definition exposes its body, which must satisfy the current guard condition when the resulting term is type-checked. A definition accepted with weaker checks may therefore be rejected after unfolding.

Example: Unfolding a definition accepted without guard checking

Unfolding loop inserts its fixpoint into the proof term. Checking the guard condition of this proof term rejects the fixpoint, since guard checking has been re-enabled.

Goal forall n, loop n = loop n.: 1 goal ============================ forall n : nat, loop n = loop n
Proof.

unfold loop.: 1 goal ============================ forall n : nat, (fix loop (n0 : nat) : False := loop n0) n = (fix loop (n0 : nat) : False := loop n0) n

reflexivity.: No more goals.

Fail Qed.: The command has indeed failed with message: Recursive definition of loop is ill-formed. In environment n : nat loop : nat -> False n0 : nat Recursive call to loop has principal argument equal to "n0" instead of a subterm of "n0". Recursive definition is: "fun n : nat => loop n".

Although reflexivity leaves no goals, the resulting proof term contains the body of loop, which does not satisfy the guard condition. The proof term is therefore rejected by Qed with the current flags:

Show Proof.: ((fun n : nat => eq_refl) : forall n : nat, loop n = loop n)

Abort.

Minimal Guard Condition

The minimal guard condition requires the structural argument of every recursive call to be a strict subterm of the current function's structural argument. A strict subterm is a smaller part obtained by exposing recursive constructor arguments through pattern-matching or primitive projections, possibly in several steps. A large, or non-strict, subterm is either a strict subterm or the structural argument itself. The guard checker tracks these subterm relationships when analyzing the fixpoint body.

Under the minimal guard condition, the recursive call's structural argument must reduce to a variable or a primitive projection recognized as a strict subterm of the current function's structural argument.

Pattern-matching the structural argument or one of its strict subterms introduces variables for recursive constructor arguments. These variables are recognized as strict subterms of the structural argument. Matching a term not recognized as a subterm of the structural argument does not give its constructor arguments this relationship to the structural argument.

Example: An eliminator for natural numbers

The eliminator of nat is recursively defined by matching the structural argument n as S p. The variable p is a strict subterm of n, so the recursive call on p is accepted.

Fixpoint nat_elim (P : nat -> Type) (P0 : P 0) (PS : forall n, P n -> P (S n)) (n : nat) {struct n} : P n := match n as m return P m with | 0 => P0 | S p => PS p (nat_elim P P0 PS p) end.: nat_elim is defined nat_elim is recursively defined (guarded on 4th argument)

Matching a strict subterm of the structural argument exposes further strict subterms of that same structural argument. Recursive calls can therefore use subterms exposed by successive pattern matches.

Example: Recursion on a subterm exposed by successive matches

The function mod2 computes the remainder modulo two by matching its argument twice before making a recursive call:

Fixpoint mod2 (n : nat) : nat := match n with | 0 => 0 | S p => match p with | 0 => 1 | S q => mod2 q end end.: mod2 is defined mod2 is recursively defined (guarded on 1st argument)

The first match exposes p as a strict subterm of n. The second exposes q as a strict subterm of p, and hence of n. The recursive call mod2 q is therefore accepted.

In a mutual fixpoint, each recursive call must pass a strict subterm of the caller's structural argument as the called function's structural argument. Recursive constructor arguments of any inductive type in the mutual block can be recognized as strict subterms of the caller's structural argument.

Example: Structural decrease in mutual fixpoints

In the mutual fixpoint example, matching t as node a f exposes f as a strict subterm of t, so tree_size may call forest_size f. Likewise, matching f as cons t f' exposes both t and f' as strict subterms of f, allowing the calls tree_size t and forest_size f'. In each call, the smaller part is passed as the structural argument of the called function.

Example: Recursive call on a subterm exposed by weak-head reduction

In the following function, recursion is performed upon (fun x => x) p rather than p itself. Recursive calls are checked after weak-head reduction, which reduces this expression to p, a strict subterm of the structural argument n.

Fixpoint rid (n : nat) : nat := match n with | 0 => 0 | S p => S (rid ((fun x => x) p)) end.: rid is defined rid is recursively defined (guarded on 1st argument)

Traversing Subterm Analysis

The guard condition features an advanced subterm analysis that traverses fixpoints and pattern-matching to determine whether the term recursion is performed upon is strictly smaller than the structural argument. This analysis traverses the definitions of the terms recursion is performed upon.

A match is a (strict) subterm provided every branch is a (strict) subterm, introducing the recursive arguments using the subterm specification of the term that is matched, as for checking termination.

An application of a mutual fixpoint fix is a (strict) subterm provided the fixpoint that is focussed returns an inductive type and its body is a (strict) subterm. The body of the focussed fixpoint is analyzed using the subterm specification of the instantiation of the structural argument, and with recursive calls to the focussed fixpoint treated as strict subterms. Calls to the other fixpoints in the mutual block are not considered subterms.

Example: Recursive call on a computed subterm

In the following function, recursion is performed upon z - y, which does not reduce to a variable while z is a variable.

Fixpoint foo x y {struct x} : nat := match x with | 0 => 0 | S z => foo (z - y) y end.: foo is defined foo is recursively defined (guarded on 1st argument)

This function is accepted thanks to traversing subterm analysis, which unfolds Nat.sub and traverses its definition to establish that z - y is strictly smaller than the structural argument x.

Print Nat.sub.: Nat.sub = fix sub (n m : nat) {struct n} : nat := match n with | 0 => n | S k => match m with | 0 => n | S l => sub k l end end : nat -> nat -> nat Arguments Nat.sub (n m)%_nat_scope

Subtraction z - y returns z unchanged when z or y is zero. Otherwise, recursion is performed upon the predecessor of z. Since z is already a strict subterm of x, the unchanged result is strictly smaller than x. The recursive result is also recognized as strictly smaller. All branches of the match are strictly smaller; hence, so are the match, the result of the fixpoint, and z - y.

However, constructors cannot be subterms. This restriction is tied to the reduction rule for fixpoints, which unfolds them whenever their structural argument starts with a constructor. Allowing recursive calls on reconstructed constructors could produce infinitely many unfoldings even on open terms, breaking strong normalization.

Example: Constructors are not Subterms

Rebuilding a term with constructors does not preserve its subterm information. The following identity function returns 0 or S p instead of the variable n being matched:

Definition id (n : nat) := match n with | 0 => 0 | S p => S p end.: id is defined

Although id n is propositionally equal to n, it is not equal to it by definition, and the subterm analysis cannot recognize it as a subterm. Matching its result therefore does not introduce a variable known to be smaller than the structural argument, and the following recursive call is rejected because id n is not recognized as a subterm of n:

Fail Fixpoint zero (n : nat) : nat := match (id n) with | 0 => 0 | S n => zero n end.: The command has indeed failed with message: Recursive definition of zero is ill-formed. In environment zero : nat -> nat n : nat n0 : nat Recursive call to zero has principal argument equal to "n0" instead of a subterm of "n". Recursive definition is: "fun n : nat => match id n with | 0 => 0 | S n0 => zero n0 end".

The same restriction applies when the recursive argument is itself the result of id. Although matching n exposes p as a strict subterm, reconstructing p through id p loses that information:

Fail Fixpoint zero_id (n : nat) : nat := match n with | 0 => 0 | S p => zero_id (id p) end.: The command has indeed failed with message: Recursive definition of zero_id is ill-formed. In environment zero_id : nat -> nat n : nat p : nat Recursive call to zero_id has principal argument equal to "id p" instead of "p". Recursive definition is: "fun n : nat => match n with | 0 => 0 | S p => zero_id (id p) end".

Returning the variable n in both branches preserves its subterm information, as in Nat.sub in the computed-subterm example above. The analysis can then recognize id' n as a subterm of n. In the successor branch of the outer match, recursion is performed upon the strictly smaller variable introduced by that match:

Definition id' (n : nat) := match n with | 0 => n | S p => n end.: id' is defined
Fixpoint zero (n : nat) : nat := match (id' n) with | 0 => 0 | S n => zero n end.: zero is defined zero is recursively defined (guarded on 1st argument)

Theory of inductive definitions

Formally, we can represent any inductive definition as $\ind{p}{Γ_I}{Γ_C}$ where:

$Γ_I$ determines the names and types of inductive types;
$Γ_C$ determines the names and types of constructors of these inductive types;
$p$ determines the number of parameters of these inductive types.

These inductive definitions, together with global assumptions and global definitions, then form the global environment. Additionally, for any $p$ there always exists $Γ_P =[a_1 :A_1 ;~…;~a_p :A_p ]$ such that each $T$ in $(t:T)∈Γ_I \cup Γ_C$ can be written as: $∀Γ_P , T'$ where $Γ_P$ is called the context of parameters. Furthermore, we must have that each $T$ in $(t:T)∈Γ_I$ can be written as: $∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S$ where $Γ_{\mathit{Arr}(t)}$ is called the Arity of the inductive type $t$ and $S$ is called the sort of the inductive type $t$ (not to be confused with $\Sort$ which is the set of sorts).

Example

The declaration for parameterized lists is:

\[\begin{split}\ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} \Nil & : & ∀ A:\Set,~\List~A \\ \cons & : & ∀ A:\Set,~A→ \List~A→ \List~A \end{array} \right]}\end{split}\]

which corresponds to the result of the Rocq declaration:

Inductive list (A:Set) : Set := | nil : list A | cons : A -> list A -> list A.: list is defined list_rect is defined list_ind is defined list_rec is defined list_sind is defined

Example

The declaration for a mutual inductive definition of tree and forest is:

\[\begin{split}\ind{0}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} {\left[\begin{array}{rcl} \node &:& \forest → \tree\\ \emptyf &:& \forest\\ \consf &:& \tree → \forest → \forest\\ \end{array}\right]}\end{split}\]

which corresponds to the result of the Rocq declaration:

Inductive tree : Set := | node : forest -> tree with forest : Set := | emptyf : forest | consf : 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

Example

The declaration for a mutual inductive definition of even and odd is:

\[\begin{split}\ind{0}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ \evenS &:& ∀ n,~\odd~n → \even~(\nS~n)\\ \oddS &:& ∀ n,~\even~n → \odd~(\nS~n) \end{array}\right]}\end{split}\]

which corresponds to the result of the Rocq declaration:

Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) with odd : nat -> Prop := | odd_S : forall n, even n -> odd (S n).: even, odd are defined even_ind is defined even_sind is defined odd_ind is defined odd_sind is defined

Types of inductive objects

We have to give the type of constants in a global environment $E$ which contains an inductive definition.

Ind: \[\frac{% \WFE{Γ}% \hspace{3em}% \ind{p}{Γ_I}{Γ_C} ∈ E% \hspace{3em}% (a:A)∈Γ_I% }{% E[Γ] ⊢ a : A% }\]

Constr: \[\frac{% \WFE{Γ}% \hspace{3em}% \ind{p}{Γ_I}{Γ_C} ∈ E% \hspace{3em}% (c:C)∈Γ_C% }{% E[Γ] ⊢ c : C% }\]

Example

Provided that our global environment $E$ contains inductive definitions we showed before, these two inference rules above enable us to conclude that:

\[\begin{split}\begin{array}{l} E[Γ] ⊢ \even : \nat→\Prop\\ E[Γ] ⊢ \odd : \nat→\Prop\\ E[Γ] ⊢ \evenO : \even~\nO\\ E[Γ] ⊢ \evenS : ∀ n:\nat,~\odd~n → \even~(\nS~n)\\ E[Γ] ⊢ \oddS : ∀ n:\nat,~\even~n → \odd~(\nS~n) \end{array}\end{split}\]

Well-formed inductive definitions

We cannot accept any inductive definition because some of them lead to inconsistent systems. We restrict ourselves to definitions which satisfy a syntactic criterion of positivity. Before giving the formal rules, we need a few definitions:

Arity of a given sort

A type $T$ is an arity of sort $s$ if it converts to the sort $s$ or to a product $∀ x:T,~U$ with $U$ an arity of sort $s$.

Example

$A→\Set$ is an arity of sort $\Set$. $∀ A:\Prop,~A→ \Prop$ is an arity of sort $\Prop$.

Arity

A type $T$ is an arity if there is a $s∈ \Sort$ such that $T$ is an arity of sort $s$.

Example

$A→ \Set$ and $∀ A:\Prop,~A→ \Prop$ are arities.

Type of constructor

We say that $T$ is a type of constructor of $I$ in one of the following two cases:

$T$ is $(I~t_1 … t_q )$
$T$ is $∀ x:U,~T'$ where $T'$ is also a type of constructor of $I$

Example

$\nat$ and $\nat→\nat$ are types of constructor of $\nat$. $∀ A:\Type,~\List~A$ and $∀ A:\Type,~A→\List~A→\List~A$ are types of constructor of $\List$.

Positivity Condition

The type of constructor $T$ will be said to satisfy the positivity condition for a set of constants $X_1 … X_k$ in the following cases:

$T=(X_j~t_1 … t_q )$ for some $j$ and no $X_1 … X_k$ occur free in any $t_i$
$T=∀ x:U,~V$ and $X_1 … X_k$ occur only strictly positively in $U$ and the type $V$ satisfies the positivity condition for $X_1 … X_k$.

Strict positivity

The constants $X_1 … X_k$ occur strictly positively in $T$ in the following cases:

no $X_1 … X_k$ occur in $T$
$T$ converts to $(X_j~t_1 … t_q )$ for some $j$ and no $X_1 … X_k$ occur in any of $t_i$
$T$ converts to $∀ x:U,~V$ and $X_1 … X_k$ occur strictly positively in type $V$ but none of them occur in $U$
$T$ converts to $(I~a_1 … a_r~t_1 … t_s )$ where $I$ is the name of an inductive definition of the form

\[\ind{r}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_r :P_r ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_r :P_r ,~C_n}\]

(in particular, it is not mutually defined and it has $r$ parameters) and no $X_1 … X_k$ occur in any of the $t_i$ nor in any of the $a_j$ for $m < j ≤ r$ where $m ≤ r$ is the number of recursively uniform parameters, and the (instantiated) types of constructor $\subst{C_i}{p_j}{a_j}_{j=1… m}$ of $I$ satisfy the nested positivity condition for $X_1 … X_k$

Nested Positivity

If $I$ is a non-mutual inductive type with $r$ parameters, then, the type of constructor $T$ of $I$ satisfies the nested positivity condition for a set of constants $X_1 … X_k$ in the following cases:

$T=(I~b_1 … b_r~u_1 … u_s)$ and no $X_1 … X_k$ occur in any $u_i$ nor in any of the $b_j$ for $m < j ≤ r$ where $m ≤ r$ is the number of recursively uniform parameters
$T=∀ x:U,~V$ and $X_1 … X_k$ occur only strictly positively in $U$ and the type $V$ satisfies the nested positivity condition for $X_1 … X_k$

Example

For instance, if one considers the following variant of a tree type branching over the natural numbers:

Inductive nattree (A:Type) : Type := | leaf : nattree A | natnode : A -> (nat -> nattree A) -> nattree A.: nattree is defined nattree_rect is defined nattree_ind is defined nattree_rec is defined nattree_sind is defined

Then every instantiated constructor of nattree A satisfies the nested positivity condition for nattree:

Type nattree A of constructor leaf satisfies the positivity condition for nattree because nattree does not appear in any (real) arguments of the type of that constructor (primarily because nattree does not have any (real) arguments) ... (bullet 1)
Type A → (nat → nattree A) → nattree A of constructor natnode satisfies the positivity condition for nattree because:
- nattree occurs only strictly positively in A ... (bullet 1)
- nattree occurs only strictly positively in nat → nattree A ... (bullet 3 + 2)
- nattree satisfies the positivity condition for nattree A ... (bullet 1)

Correctness rules

We shall now describe the rules allowing the introduction of a new inductive definition.

Let $E$ be a global environment and $Γ_P$, $Γ_I$, $Γ_C$ be contexts such that $Γ_I$ is $[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]$, and $Γ_C$ is $[c_1:∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n ]$. Then

W-Ind: \[\frac{% \WFE{Γ_P}% \hspace{3em}% (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n}% }{% \WF{E;~\ind{l}{Γ_I}{Γ_C}}{}% }\]

provided that the following side conditions hold:

$k>0$ and all of $I_j$ and $c_i$ are distinct names for $j=1… k$ and $i=1… n$,

$l$ is the size of $Γ_P$ which is called the context of parameters,

for $j=1… k$ we have that $A_j$ is an arity of sort $s_j$ and $I_j ∉ E$,

for $i=1… n$ we have that $C_i$ is a type of constructor of $I_{q_i}$ which satisfies the positivity condition for $I_1 … I_k$ and $c_i ∉ E$.

Additionally, for $j=1… k$ the following universe constraints must be satisfied, or $s_j$ must be an impredicative sort (SProp, Prop, or if -impredicative-set was used Set) and the jth inductive may not be eliminated to larger sorts:

for each (non parameter) constructor argument, the universe of its type must be smaller than $s_j$
if -indices-matter or Indices Matter was used, for each index the universe of its type must be smaller than $s_j$. When neither -indices-matter nor Indices Matter is used, inductives whose indices would contribute universe constraints are printed by Print Assumptions.
if there are 2 or more constructors, Set must be smaller than $s_j$
unless the inductive is a primitive record, and unless Definitional UIP was used, if there is 1 constructor, Prop must be smaller than $s_j$ (essentially this means $s_j$ must not be SProp)

Example

It is well known that the existential quantifier can be encoded as an inductive definition. The following declaration introduces the second-order existential quantifier $∃ X.P(X)$.

Inductive exProp (P:Prop->Prop) : Prop := | exP_intro : forall X:Prop, P X -> exProp P.: exProp is defined exProp_ind is defined exProp_sind is defined

The same definition on $\Set$ is not allowed and fails:

Fail Inductive exSet (P:Set->Prop) : Set := exS_intro : forall X:Set, P X -> exSet P.: The command has indeed failed with message: Universe inconsistency. Cannot enforce Set+1 <= Set.

It is possible to declare the same inductive definition in the universe $\Type$. The exType inductive definition has type $(\Type(i)→\Prop)→\Type(j)$ with the constraint that the parameter $X$ of $\kw{exT}_{\kw{intro}}$ has type $\Type(k)$ with $k<j$ and $k≤ i$.

Inductive exType (P:Type->Prop) : Type := exT_intro : forall X:Type, P X -> exType P.: exType is defined exType_rect is defined exType_ind is defined exType_rec is defined exType_sind is defined

Example: Negative occurrence (first example)

The following inductive definition is rejected because it does not satisfy the positivity condition:

Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I.: The command has indeed failed with message: Non strictly positive occurrence of "I" in "(I -> False) -> I".

If we were to accept such definition, we could derive a contradiction from it (we can test this by disabling the Positivity Checking flag):

#[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.: I is defined

Definition I_not_I : I -> ~ I := fun i => match i with not_I_I not_I => not_I end.: I_not_I is defined

Lemma contradiction : False.: 1 goal ============================ False
Proof.
enough (I /\ ~ I) as [] by contradiction.: 1 goal ============================ I /\ ~ I
split.: 2 goals ============================ I goal 2 is: ~ I
- apply not_I_I.: 1 goal ============================ I 1 goal ============================ I -> False
intro.: 1 goal H : I ============================ False
now apply I_not_I.: This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. 1 goal goal 1 is: ~ I
- intro.: 1 goal ============================ ~ I 1 goal H : I ============================ False
now apply I_not_I.: No more goals.
Qed.

Example: Negative occurrence (second example)

Here is another example of an inductive definition which is rejected because it does not satify the positivity condition:

Fail Inductive Lam := lam (_ : Lam -> Lam).: The command has indeed failed with message: Non strictly positive occurrence of "Lam" in "(Lam -> Lam) -> Lam".

Again, if we were to accept it, we could derive a contradiction (this time through a non-terminating recursive function):

#[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam).: Lam is defined

Fixpoint infinite_loop l : False := match l with lam x => infinite_loop (x l) end.: infinite_loop is defined infinite_loop is recursively defined (guarded on 1st argument)
Check infinite_loop (lam (@id Lam)) : False.: infinite_loop (lam (id (A:=Lam))) : False : False

Example: Non strictly positive occurrence

It is less obvious why inductive type definitions with occurences that are positive but not strictly positive are harmful. We will see that in presence of an impredicative type they are unsound:

Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.: The command has indeed failed with message: Non strictly positive occurrence of "A" in "((A -> Prop) -> Prop) -> A".

If we were to accept this definition we could derive a contradiction by creating an injective function from $A → \Prop$ to $A$.

This function is defined by composing the injective constructor of the type $A$ with the function $λx. λz. z = x$ injecting any type $T$ into $T → \Prop$.

#[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.: A is defined

Definition f (x: A -> Prop): A := introA (fun z => z = x).: f is defined

Lemma f_inj: forall x y, f x = f y -> x = y.: 1 goal ============================ forall x y : A -> Prop, f x = f y -> x = y
Proof.
unfold f; intros ? ? H; injection H.: 1 goal x, y : A -> Prop H : introA (fun z : A -> Prop => z = x) = introA (fun z : A -> Prop => z = y) ============================ (fun z : A -> Prop => z = x) = (fun z : A -> Prop => z = y) -> x = y
set (F := fun z => z = y); intro HF.: 1 goal x, y : A -> Prop H : introA (fun z : A -> Prop => z = x) = introA (fun z : A -> Prop => z = y) F := fun z : A -> Prop => z = y : (A -> Prop) -> Prop HF : (fun z : A -> Prop => z = x) = F ============================ x = y
symmetry; replace (y = x) with (F y).: 2 goals x, y : A -> Prop H : introA (fun z : A -> Prop => z = x) = introA (fun z : A -> Prop => z = y) F := fun z : A -> Prop => z = y : (A -> Prop) -> Prop HF : (fun z : A -> Prop => z = x) = F ============================ F y goal 2 is: F y = (y = x)
+ unfold F; reflexivity.: 1 goal x, y : A -> Prop H : introA (fun z : A -> Prop => z = x) = introA (fun z : A -> Prop => z = y) F := fun z : A -> Prop => z = y : (A -> Prop) -> Prop HF : (fun z : A -> Prop => z = x) = F ============================ F y This subproof is complete, but there are some unfocused goals. Focus next goal with bullet +. 1 goal goal 1 is: F y = (y = x)
+ rewrite <- HF; reflexivity.: 1 goal x, y : A -> Prop H : introA (fun z : A -> Prop => z = x) = introA (fun z : A -> Prop => z = y) F := fun z : A -> Prop => z = y : (A -> Prop) -> Prop HF : (fun z : A -> Prop => z = x) = F ============================ F y = (y = x) No more goals.
Qed.

The type $A → \Prop$ can be understood as the powerset of the type $A$. To derive a contradiction from the injective function $f$ we use Cantor's classic diagonal argument.

Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x.: d is defined
Definition fd: A := f d.: fd is defined

Lemma cantor: (d fd) <-> ~(d fd).: 1 goal ============================ d fd <-> ~ d fd
Proof.
split.: 2 goals ============================ d fd -> ~ d fd goal 2 is: ~ d fd -> d fd
+ intros [s [H1 H2]]; unfold fd in H1.: 1 goal ============================ d fd -> ~ d fd 1 goal s : A -> Prop H1 : f d = f s H2 : ~ s fd ============================ ~ d fd
replace d with s.: 2 goals s : A -> Prop H1 : f d = f s H2 : ~ s fd ============================ ~ s fd goal 2 is: s = d
* assumption.: 1 goal s : A -> Prop H1 : f d = f s H2 : ~ s fd ============================ ~ s fd This subproof is complete, but there are some unfocused goals. Focus next goal with bullet *. 2 goals goal 1 is: s = d goal 2 is: ~ d fd -> d fd
* apply f_inj; congruence.: 1 goal s : A -> Prop H1 : f d = f s H2 : ~ s fd ============================ s = d This subproof is complete, but there are some unfocused goals. Focus next goal with bullet +. 1 goal goal 1 is: ~ d fd -> d fd
+ intro; exists d; tauto.: 1 goal ============================ ~ d fd -> d fd No more goals.
Qed.
Lemma bad: False.: 1 goal ============================ False
Proof.
pose cantor; tauto.: No more goals.
Qed.

This derivation was first presented by Thierry Coquand and Christine Paulin in [CP90].

Destructors

The specification of inductive definitions with arities and constructors is quite natural. But we still have to say how to use an object in an inductive type.

This problem is rather delicate. There are actually several different ways to do that. Some of them are logically equivalent but not always equivalent from the computational point of view or from the user point of view.

From the computational point of view, we want to be able to define a function whose domain is an inductively defined type by using a combination of case analysis over the possible constructors of the object and recursion.

Because we need to keep a consistent theory and also we prefer to keep a strongly normalizing reduction, we cannot accept any sort of recursion (even terminating). So the basic idea is to restrict ourselves to primitive recursive functions and functionals.

For instance, assuming a parameter $A:\Set$ exists in the local context, we want to build a function $\length$ of type $\List~A → \nat$ which computes the length of the list, such that $(\length~(\Nil~A)) = \nO$ and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$. We want these equalities to be recognized implicitly and taken into account in the conversion rule.

From the logical point of view, we have built a type family by giving a set of constructors. We want to capture the fact that we do not have any other way to build an object in this type. So when trying to prove a property about an object $m$ in an inductive type it is enough to enumerate all the cases where $m$ starts with a different constructor.

In case the inductive definition is effectively a recursive one, we want to capture the extra property that we have built the smallest fixed point of this recursive equation. This says that we are only manipulating finite objects. This analysis provides induction principles. For instance, in order to prove $∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l))$ it is enough to prove:

$(\kw{has}\_\kw{length}~A~(\Nil~A)~(\length~(\Nil~A)))$
$∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →$ $(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\length~(\cons~A~a~l)))$

which given the conversion equalities satisfied by $\length$ is the same as proving:

$(\kw{has}\_\kw{length}~A~(\Nil~A)~\nO)$
$∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →$ $(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\nS~(\length~l)))$

One conceptually simple way to do that, following the basic scheme proposed by Martin-Löf in his Intuitionistic Type Theory, is to introduce for each inductive definition an elimination operator. At the logical level it is a proof of the usual induction principle and at the computational level it implements a generic operator for doing primitive recursion over the structure.

But this operator is rather tedious to implement and use. We choose to factorize the operator for primitive recursion into two more primitive operations as was first suggested by Th. Coquand in [Coq92]. One is the definition by pattern matching. The second one is a definition by guarded fixpoints.

The match ... with ... end construction

The basic idea of this operator is that we have an object $m$ in an inductive type $I$ and we want to prove a property which possibly depends on $m$. For this, it is enough to prove the property for $m = (c_i~u_1 … u_{p_i} )$ for each constructor of $I$. The Rocq term for this proof will be written:

\[\Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend\]

In this expression, if $m$ eventually happens to evaluate to $(c_i~u_1 … u_{p_i})$ then the expression will behave as specified in its $i$-th branch and it will reduce to $f_i$ where the $x_{i1} …x_{ip_i}$ are replaced by the $u_1 … u_{p_i}$ according to the ι-reduction.

Actually, for type checking a $\Match…\with…\kwend$ expression we also need to know the predicate $P$ to be proved by case analysis. In the general case where $I$ is an inductively defined $n$-ary relation, $P$ is a predicate over $n+1$ arguments: the $n$ first ones correspond to the arguments of $I$ (parameters excluded), and the last one corresponds to object $m$. Rocq can sometimes infer this predicate but sometimes not. The concrete syntax for describing this predicate uses the $\as…\In…\return$ construction. For instance, let us assume that $I$ is an unary predicate with one parameter and one argument. The predicate is made explicit using the syntax:

\[\Match~m~\as~x~\In~I~\_~a~\return~P~\with~ (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend\]

The $\as$ part can be omitted if either the result type does not depend on $m$ (non-dependent elimination) or $m$ is a variable (in this case, $m$ can occur in $P$ where it is considered a bound variable). The $\In$ part can be omitted if the result type does not depend on the arguments of $I$. Note that the arguments of $I$ corresponding to parameters must be $\_$, because the result type is not generalized to all possible values of the parameters. The other arguments of $I$ (sometimes called indices in the literature) have to be variables ($a$ above) and these variables can occur in $P$. The expression after $\In$ must be seen as an inductive type pattern. Notice that expansion of implicit arguments and notations apply to this pattern. For the purpose of presenting the inference rules, we use a more compact notation:

\[\case(m,(λ a x . P), λ x_{11} ... x_{1p_1} . f_1~| … |~λ x_{n1} ...x_{np_n} . f_n )\]

Allowed elimination sorts. An important question for building the typing rule for $\Match$ is what can be the type of $λ a x . P$ with respect to the type of $m$. If $m:I$ and $I:A$ and $λ a x . P : B$ then by $[I:A|B]$ we mean that one can use $λ a x . P$ with $m$ in the above match-construct.

Notations. The $[I:A|B]$ is defined as the smallest relation satisfying the following rules: We write $[I|B]$ for $[I:A|B]$ where $A$ is the type of $I$.

The case of inductive types in sorts $\Set$ or $\Type$ is simple. There is no restriction on the sort of the predicate to be eliminated.

Prod: \[\frac{% [(I~x):A′|B′]% }{% [I:∀ x:A,~A′|∀ x:A,~B′]% }\]

Set & Type: \[\frac{% s_1 ∈ \{\Set,\Type(j)\}% \hspace{3em}% s_2 ∈ \Sort% }{% [I:s_1 |I→ s_2 ]% }\]

The case of Inductive definitions of sort $\Prop$ is a bit more complicated, because of our interpretation of this sort. The only harmless allowed eliminations, are the ones when predicate $P$ is also of sort $\Prop$ or is of the morally smaller sort $\SProp$.

Prop: \[\frac{% s ∈ \{\SProp,\Prop\}% }{% [I:\Prop|I→s]% }\]

$\Prop$ is the type of logical propositions, the proofs of properties $P$ in $\Prop$ could not be used for computation and are consequently ignored by the extraction mechanism. Assume $A$ and $B$ are two propositions, and the logical disjunction $A ∨ B$ is defined inductively by:

Example

Inductive or (A B:Prop) : Prop := or_introl : A -> or A B | or_intror : B -> or A B.: or is defined or_ind is defined or_sind is defined

The following definition which computes a boolean value by case over the proof of or A B is not accepted:

Example

Fail Definition choice (A B: Prop) (x:or A B) := match x with or_introl _ _ a => true | or_intror _ _ b => false end.: The command has indeed failed with message: Incorrect elimination of "x" in the inductive type "or": the return type has sort "Set" while it should be SProp or Prop. Elimination of an inductive object of sort Prop is not allowed on a predicate in sort "Set" because proofs can be eliminated only to build proofs.

From the computational point of view, the structure of the proof of (or A B) in this term is needed for computing the boolean value.

In general, if $I$ has type $\Prop$ then $P$ cannot have type $I→\Set$, because it will mean to build an informative proof of type $(P~m)$ doing a case analysis over a non-computational object that will disappear in the extracted program. But the other way is safe with respect to our interpretation we can have $I$ a computational object and $P$ a non-computational one, it just corresponds to proving a logical property of a computational object.

In the same spirit, elimination on $P$ of type $I→\Type$ cannot be allowed because it trivially implies the elimination on $P$ of type $I→ \Set$ by cumulativity. It also implies that there are two proofs of the same property which are provably different, contradicting the proof-irrelevance property which is sometimes a useful axiom:

Example

Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.: proof_irrelevance is declared

The elimination of an inductive type of sort $\Prop$ on a predicate $P$ of type $I→ \Type$ leads to a paradox when applied to impredicative inductive definition like the second-order existential quantifier exProp defined above, because it gives access to the two projections on this type.

Empty and singleton elimination. There are special inductive definitions in $\Prop$ for which more eliminations are allowed.

Prop-extended: \[\frac{% I~\kw{is an empty or singleton definition}% \hspace{3em}% s ∈ \Sort% }{% [I:\Prop|I→ s]% }\]

A singleton definition has only one constructor and all the arguments of this constructor have type $\Prop$. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort $s$ is legal. Typical examples are the conjunction of non-informative propositions and the equality. If there is a hypothesis $h:a=b$ in the local context, it can be used for rewriting not only in logical propositions but also in any type.

Example

Print eq_rec.: eq_rec = fun (A : Type) (x : A) (P : A -> Set) (eq_refl : P x) (a : A) (e : x = a) => match e in _ = a0 return P a0 with | Logic.eq_refl => eq_refl end : forall [A : Type] (x : A) (P : A -> Set), P x -> forall a : A, x = a -> P a Arguments eq_rec [A]%_type_scope x P%_function_scope eq_refl y e (where some original arguments have been renamed)
Require Extraction.: [Loading ML file rocq-runtime.plugins.extraction ... done]
Extraction eq_rec.: (** val eq_rec : 'a1 -> 'a2 -> 'a1 -> 'a2 **) let eq_rec _ eq_refl _ = eq_refl

An empty definition has no constructors, in that case also, elimination on any sort is allowed.

Inductive types in $\SProp$ must have no constructors (i.e. be empty) to be eliminated to produce relevant values.

Note that thanks to proof irrelevance elimination functions can be produced for other types, for instance the elimination for a unit type is the identity.

Type of branches. Let $c$ be a term of type $C$, we assume $C$ is a type of constructor for an inductive type $I$. Let $P$ be a term that represents the property to be proved. We assume $r$ is the number of parameters and $s$ is the number of arguments.

We define a new type $\{c:C\}^P$ which represents the type of the branch corresponding to the $c:C$ constructor.

\[\begin{split}\begin{array}{ll} \{c:(I~q_1\ldots q_r\ t_1 \ldots t_s)\}^P &\equiv (P~t_1\ldots ~t_s~c) \\ \{c:∀ x:T,~C\}^P &\equiv ∀ x:T,~\{(c~x):C\}^P \end{array}\end{split}\]

We write $\{c\}^P$ for $\{c:C\}^P$ with $C$ the type of $c$.

Example

The following term in concrete syntax:

match t as l return P' with
| nil _ => t1
| cons _ hd tl => t2
end

can be represented in abstract syntax as

\[\case(t,P,f_1 | f_2 )\]

where

\begin{eqnarray*} P & = & λ l.~P^\prime\\ f_1 & = & t_1\\ f_2 & = & λ (hd:\nat).~λ (tl:\List~\nat).~t_2 \end{eqnarray*}

According to the definition:

\[\{(\Nil~\nat)\}^P ≡ \{(\Nil~\nat) : (\List~\nat)\}^P ≡ (P~(\Nil~\nat))\]

\[\begin{split}\begin{array}{rl} \{(\cons~\nat)\}^P & ≡\{(\cons~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ & ≡∀ n:\nat,~\{(\cons~\nat~n) : (\List~\nat→\List~\nat)\}^P \\ & ≡∀ n:\nat,~∀ l:\List~\nat,~\{(\cons~\nat~n~l) : (\List~\nat)\}^P \\ & ≡∀ n:\nat,~∀ l:\List~\nat,~(P~(\cons~\nat~n~l)). \end{array}\end{split}\]

Given some $P$ then $\{(\Nil~\nat)\}^P$ represents the expected type of $f_1$, and $\{(\cons~\nat)\}^P$ represents the expected type of $f_2$.

Typing rule. Our very general destructor for inductive definitions has the following typing rule

match: \[\begin{split}\frac{% \begin{array}{l}% \hspace{3em}% E[Γ] ⊢ c : (I~q_1 … q_r~t_1 … t_s ) \\% \hspace{3em}% E[Γ] ⊢ P : B \\% \hspace{3em}% [(I~q_1 … q_r)|B] \\% \hspace{3em}% (E[Γ] ⊢ f_i : \{(c_{p_i}~q_1 … q_r)\}^P)_{i=1… l}% \hspace{3em}% \end{array}% }{% E[Γ] ⊢ \case(c,P,f_1 |… |f_l ) : (P~t_1 … t_s~c)% }\end{split}\]

provided $I$ is an inductive type in a definition $\ind{r}{Γ_I}{Γ_C}$ with $Γ_C = [c_1 :C_1 ;~…;~c_n :C_n ]$ and $c_{p_1} … c_{p_l}$ are the only constructors of $I$.

Example

Below is a typing rule for the term shown in the previous example:

list example: \[\begin{split}\frac{% \begin{array}{l}% \hspace{3em}% E[Γ] ⊢ t : (\List ~\nat) \\% \hspace{3em}% E[Γ] ⊢ P : B \\% \hspace{3em}% [(\List ~\nat)|B] \\% \hspace{3em}% E[Γ] ⊢ f_1 : \{(\Nil ~\nat)\}^P \\% \hspace{3em}% E[Γ] ⊢ f_2 : \{(\cons ~\nat)\}^P% \hspace{3em}% \end{array}% }{% E[Γ] ⊢ \case(t,P,f_1 |f_2 ) : (P~t)% }\end{split}\]

Definition of ι-reduction. We still have to define the ι-reduction in the general case.

An ι-redex is a term of the following form:

\[\case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l )\]

with $c_{p_i}$ the $i$-th constructor of the inductive type $I$ with $r$ parameters.

The ι-contraction of this term is $(f_i~a_1 … a_m )$ leading to the general reduction rule:

\[\case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) \triangleright_ι (f_i~a_1 … a_m )\]

Fixpoint definitions

The second operator for elimination is fixpoint definition. This fixpoint may involve several mutually recursive definitions. The basic concrete syntax for a recursive set of mutually recursive declarations is (with $Γ_i$ contexts):

\[\fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n\]

The terms are obtained by projections from this set of declarations and are written

\[\fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n~\for~f_i\]

In the inference rules, we represent such a term by

\[\Fix~f_i\{f_1 :A_1':=t_1' … f_n :A_n':=t_n'\}\]

with $t_i'$ (resp. $A_i'$) representing the term $t_i$ abstracted (resp. generalized) with respect to the bindings in the context $Γ_i$, namely $t_i'=λ Γ_i . t_i$ and $A_i'=∀ Γ_i , A_i$.

Typing rule

The typing rule is the expected one for a fixpoint.

Fix: \[\frac{% (E[Γ] ⊢ A_i : s_i )_{i=1… n}% \hspace{3em}% (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n}% }{% E[Γ] ⊢ \Fix~f_i\{f_1 :A_1 :=t_1 … f_n :A_n :=t_n \} : A_i% }\]

Any fixpoint definition cannot be accepted because non-normalizing terms allow proofs of absurdity. The basic scheme of recursion that should be allowed is the one needed for defining primitive recursive functionals. In that case the fixpoint enjoys a special syntactic restriction, namely one of the arguments belongs to an inductive type, the function starts with a case analysis and recursive calls are done on variables coming from patterns and representing subterms. For instance in the case of natural numbers, a proof of the induction principle of type

\[∀ P:\nat→\Prop,~(P~\nO)→(∀ n:\nat,~(P~n)→(P~(\nS~n)))→ ∀ n:\nat,~(P~n)\]

can be represented by the term:

\[\begin{split}\begin{array}{l} λ P:\nat→\Prop.~λ f:(P~\nO).~λ g:(∀ n:\nat,~(P~n)→(P~(\nS~n))).\\ \Fix~h\{h:∀ n:\nat,~(P~n):=λ n:\nat.~\case(n,P,f | λp:\nat.~(g~p~(h~p)))\} \end{array}\end{split}\]

Before accepting a fixpoint definition as being correctly typed, we check that the definition is “guarded”. A precise analysis of this notion can be found in [Gimenez94]. The first stage is to precise on which argument the fixpoint will be decreasing. The type of this argument should be an inductive type. For doing this, the syntax of fixpoints is extended and becomes

\[\Fix~f_i\{f_1/k_1 :A_1:=t_1 … f_n/k_n :A_n:=t_n\}\]

where $k_i$ are positive integers. Each $k_i$ represents the index of parameter of $f_i$, on which $f_i$ is decreasing. Each $A_i$ should be a type (reducible to a term) starting with at least $k_i$ products $∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'$ and $B_{k_i}$ an inductive type.

Now in the definition $t_i$, if $f_j$ occurs then it should be applied to at least $k_j$ arguments and the $k_j$-th argument should be syntactically recognized as structurally smaller than $y_{k_i}$.

The definition of being structurally smaller is a bit technical. One needs first to define the notion of recursive arguments of a constructor. For an inductive definition $\ind{r}{Γ_I}{Γ_C}$, if the type of a constructor $c$ has the form $∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_m :T_m,~(I_j~p_1 … p_r~t_1 … t_s )$, then the recursive arguments will correspond to $T_i$ in which one of the $I_l$ occurs.

The main rules for being structurally smaller are the following. Given a variable $y$ of an inductively defined type in a declaration $\ind{r}{Γ_I}{Γ_C}$ where $Γ_I$ is $[I_1 :A_1 ;~…;~I_k :A_k]$, and $Γ_C$ is $[c_1 :C_1 ;~…;~c_n :C_n ]$, the terms structurally smaller than $y$ are:

$(t~u)$ and $λ x:U .~t$ when $t$ is structurally smaller than $y$.
$\case(c,P,f_1 … f_n)$ when each $f_i$ is structurally smaller than $y$. If $c$ is $y$ or is structurally smaller than $y$, its type is an inductive type $I_p$ part of the inductive definition corresponding to $y$. Each $f_i$ corresponds to a type of constructor $C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_m :B_m ,~(I_p~p_1 … p_r~t_1 … t_s )$ and can consequently be written $λ y_1 :B_1' .~… λ y_m :B_m'.~g_i$. ($B_i'$ is obtained from $B_i$ by substituting parameters for variables) the variables $y_j$ occurring in $g_i$ corresponding to recursive arguments $B_i$ (the ones in which one of the $I_l$ occurs) are structurally smaller than $y$.

The following definitions are correct, we enter them using the Fixpoint command and show the internal representation.

Example

Fixpoint plus (n m:nat) {struct n} : nat := match n with | O => m | S p => S (plus p m) end.: plus is defined plus is recursively defined (guarded on 1st argument)
Print plus.: plus = fix plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus p m) end : nat -> nat -> nat Arguments plus (n m)%_nat_scope
Fixpoint lgth (A:Set) (l:list A) {struct l} : nat := match l with | nil _ => O | cons _ a l' => S (lgth A l') end.: lgth is defined lgth is recursively defined (guarded on 2nd argument)
Print lgth.: lgth = fix lgth (A : Set) (l : list A) {struct l} : nat := match l with | nil _ => 0 | cons _ _ l' => S (lgth A l') end : forall A : Set, list A -> nat Arguments lgth A%_type_scope l
Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f) with sizef (f:forest) : nat := match f with | emptyf => O | consf t f => plus (sizet t) (sizef f) end.: sizet is defined sizef is defined sizet, sizef are recursively defined (guarded respectively on 1st, 1st arguments)
Print sizet.: sizet = fix sizet (t : tree) : nat := let (f) := t in S (sizef f) with sizef (f : forest) : nat := match f with | emptyf => 0 | consf t f0 => plus (sizet t) (sizef f0) end for sizet : tree -> nat Arguments sizet t

Reduction rule

Let $F$ be the set of declarations: $f_1 /k_1 :A_1 :=t_1 …f_n /k_n :A_n:=t_n$. The reduction for fixpoints is:

\[(\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i}\]

when the structural argument $a_{k_i}$ starts with a constructor. This last restriction is needed in order to keep strong normalization and corresponds to the reduction for primitive recursive operators. The following reductions are now possible:

\begin{eqnarray*} \plus~(\nS~(\nS~\nO))~(\nS~\nO)~& \trii & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ & \trii & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ & \trii & \nS~(\nS~(\nS~\nO))\\ \end{eqnarray*}

Mutual induction

The principles of mutual induction can be automatically generated using the Scheme command described in Section Generation of induction principles with Scheme.