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 wellfounded trees. Inhabitants of inductive types can
recursively nest only a finite number of constructors. So, they are
wellfounded. This distinguishes them from CoInductive
types,
such as streams, whose constructors can be infinitely nested. In Coq,
Variant
types thus correspond to the common subset of inductive
and coinductive types that are nonrecursive.
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_type_inst?Defines one or more inductive types and its constructors. Coq generates induction principles depending on the universe that the inductive type belongs to.
The induction principles are named
ident
_rect
,ident
_ind
,ident
_rec
andident
_sind
, which respectively correspond to onType
,Prop
,Set
andSProp
. Their types expresses structural induction/recursion principles over objects of typeident
. These constants are generated when possible (for instanceident
_rect
may be impossible to derive whenident
is a proposition). Flag Dependent Proposition Eliminators¶
The inductive principles express dependent elimination when the inductive type allows it (always true when not using
Primitive Projections
), except by default when the inductive is explicitly declared inProp
.Explicitly
Prop
inductive types declared when this flag is enabled also automatically declare dependent inductive principles. Name generation may also change when using tactics such asdestruct
on such inductives.Note that explicit declarations through
Scheme
are not affected by this flag.
 binder*?
The

separates uniform and non uniform parameters. SeeUniform Inductive Parameters
.
The
Inductive
command supports theuniverses(polymorphic)
,universes(template)
,universes(cumulative)
,bypass_check(positivity)
,bypass_check(universes)
andprivate(matching)
attributes.When record syntax is used, this command also supports the
projections(primitive)
attribute. Also, in the record syntax, if given, theas ident
part specifies the name to use for inhabitants of the record in the type of projections.Mutually inductive types can be defined by including multiple
inductive_definition
s. Theident
s are simultaneously added to the global environment before the types of constructors are checked. Eachident
can be used independently thereafter. However, the induction principles currently generated for such types are not useful. Use theScheme
command to generate useful induction principles. See Mutually defined inductive types.If the entire inductive definition is parameterized with
binder
s, those inductive parameters correspond to a local context in which the entire set of inductive declarations is interpreted. For this reason, the parameters must be strictly the same for each inductive type. See Parameterized inductive types.Constructor
ident
s can come withbinder
s, in which case the actual type of the constructor isforall binder*, type
. Error Non strictly positive occurrence of ident in type.¶
The types of the constructors have to satisfy a positivity condition (see Section Positivity Condition). This condition ensures the soundness of the inductive definition. Positivity checking can be disabled using the
Positivity Checking
flag or thebypass_check(positivity)
attribute (see Controlling Typing Flags).
The following subsections show examples of simple inductive types, simple indexed inductive types, simple parametric inductive types, mutually inductive types and private (matching) 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 secondorder 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
Automatic Prop lowering¶
When an inductive is declared without an explicit sort, it is put in the
smallest sort which permits large elimination (excluding
SProp
). For empty and singleton
types this means they are declared in Prop
.
 Flag Automatic Proposition Inductives¶
By default the above behaviour is extended to empty and singleton inductives explicitly declared in
Type
(but not those in explicit universes usingType@{u}
, or inType
through an auxiliary definition such asDefinition typ := Type.
).Disabling this flag prevents inductives with an explicit non
Prop
type from being lowered toProp
. This will become the default in a future version. UseDependent Proposition Eliminators
to declare the inductive type inProp
while preserving compatibility.Depending on universe minimization they may then be declared in
Set
or in a floating universe level, see alsoUniverse Minimization ToSet
.
 Warning Automatically putting ident in Prop even though it was declared with Type.¶
This warning is produced when
Automatic Proposition Inductives
is enabled and resulted in an inductive type being lowered toProp
.
Simple indexed inductive types¶
In indexed inductive types, the universe where the inductive type
is defined is no longer a simple sort
, but what is called an arity,
which is a type whose conclusion is a sort
.
Example
As an example of indexed inductive types, let us define the
even
predicate:
 Inductive even : nat > Prop :=  even_0 : even O  even_SS : forall n:nat, even n > even (S (S n)).
 even is defined even_ind is defined even_sind is defined
The type nat>Prop
means that even
is a unary predicate (inductively
defined) over natural numbers. The type of its two constructors are the
defining clauses of the predicate even
. The type of even_ind
is:
 Check even_ind.
 even_ind : forall P : nat > Prop, P O > (forall n : nat, even n > P n > P (S (S n))) > forall n : nat, even n > P n
From a mathematical point of view, this asserts that the natural numbers satisfying
the predicate even
are exactly in the smallest set of naturals satisfying the
clauses even_0
or even_SS
. This is why, when we want to prove any
predicate P
over elements of even
, it is enough to prove it for O
and to prove that if any natural number n
satisfies P
its double
successor (S (S n))
satisfies also P
. This is analogous to the
structural induction principle we got for nat
.
Parameterized inductive types¶
In the previous example, each constructor introduces a different
instance of the predicate even
. In some cases, all the constructors
introduce the same generic instance of the inductive definition, in
which case, instead of an index, we use a context of parameters
which are binder
s shared by all the constructors of the definition.
Parameters differ from inductive type indices in that the conclusion of each type of constructor invokes the inductive type with the same parameter values of its specification.
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
Note
The constructor type can recursively invoke the inductive definition on an argument which is not the parameter itself.
One can define :
 Inductive list2 (A:Set) : Set :=  nil2 : list2 A  cons2 : A > list2 (A*A) > list2 A.
 list2 is defined list2_rect is defined list2_ind is defined list2_rec is defined list2_sind is defined
that can also be written by specifying only the type of the arguments:
 Inductive list2 (A:Set) : Set :=  nil2  cons2 (_:A) (_:list2 (A*A)).
 list2 is defined list2_rect is defined list2_ind is defined list2_rec is defined list2_sind is defined
But the following definition will give an error:
 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".
because the conclusion of the type of constructors should be
listw A
in both cases.A parameterized inductive definition can be defined using indices instead of parameters but it will sometimes give a different (bigger) sort for the inductive definition and will produce a less convenient rule for case elimination.
 Flag Uniform Inductive Parameters¶
When this flag is set (it is off by default), inductive definitions are abstracted over their parameters before type checking constructors, allowing to write:
 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
This behavior is essentially equivalent to starting a new section and using
Context
to give the uniform parameters, like so (cf. 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.
For finer control, you can use a

between the uniform and the nonuniform parameters: Inductive Acc {A:Type} (R:A>A>Prop)  (x:A) : Prop := Acc_in : (forall y, R y x > Acc y) > Acc x.
 Acc is defined Acc_rect is defined Acc_ind is defined Acc_rec is defined Acc_sind is defined
The flag can then be seen as deciding whether the

is at the beginning (when the flag is unset) or at the end (when it is set) of the parameters when not explicitly given.
See also
Section Theory of inductive definitions and the induction
tactic.
Mutually defined inductive types¶
The induction principles currently generated for mutually defined types are not
useful. Use the Scheme
command to generate a useful induction principle.
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:
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.
See also
A generic command Scheme
is useful to build automatically various
mutual induction principles.
Recursive functions: fix¶
term_fix::=
let fix fix_decl in term

fix fix_decl with fix_decl+ for ident?
fix_decl::=
ident binder* fixannot? : type? := term
fixannot::=
{ struct ident }

{ wf one_term ident }

{ measure one_term ident? one_term? }
The expression "fix ident_{1} binder_{1} : type_{1} := term_{1} 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.
The association of a single fixpoint and a local definition have a special
syntax: let fix ident binder* := term in
stands for
let ident := fix ident binder* := term in
. The same applies for cofixpoints.
Some options of fixannot
are only supported in specific constructs. fix
and let fix
only support the struct
option, while wf
and measure
are only supported in
commands such as Fixpoint
(with the program
attribute) and Function
.
Toplevel recursive functions¶
This section describes the primitive form of definition by recursion over
inductive objects. See the Function
command for more advanced
constructions.
 Command Fixpoint fix_definition with fix_definition*¶
 fix_definition
::=
ident_decl binder* fixannot? : type? := term? decl_notations?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 thebinder
s such thatident
applied to arguments corresponding to thesebinder
s has typetype
, and is equivalent to the expressionterm
. The type ofident
is consequentlyforall binder*, type
and its value is equivalent tofun binder* => term
.This command accepts the
program
,bypass_check(universes)
, andbypass_check(guard)
attributes.To be accepted, a
Fixpoint
definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They are needed to ensure that theFixpoint
definition always terminates. The point of the{struct ident}
annotation (seefixannot
) is to let the user tell the system which argument decreases along the recursive calls.The
{struct ident}
annotation may be left implicit, in which case the system successively tries arguments from left to right until it finds one that satisfies the decreasing condition.Fixpoint
without theprogram
attribute does not support thewf
ormeasure
clauses offixannot
. See Program Fixpoint.The
with
clause allows simultaneously defining several mutual fixpoints. It is especially useful when defining functions over mutually defined inductive types. Example: Mutual Fixpoints.If
term
is omitted,type
is required and Coq enters proof mode. This can be used to define a term incrementally, in particular by relying on therefine
tactic. In this case, the proof should be terminated withDefined
in order to define a constant for which the computational behavior is relevant. See Entering and exiting proof mode.This command accepts the
using
attribute.Note
Some fixpoints may have several arguments that fit as decreasing arguments, and this choice influences the reduction of the fixpoint. Hence an explicit annotation must be used if the leftmost decreasing argument is not the desired one. Writing explicit annotations can also speed up type checking of large mutual fixpoints.
In order to keep the strong normalization property, the fixed point reduction will only be performed when the argument in position of the decreasing argument (which type should be in an inductive definition) starts with a constructor.
Example
One can define the addition function as :
 Fixpoint add (n m:nat) {struct n} : nat := match n with  O => m  S p => S (add p m) end.
 add is defined add is recursively defined (guarded on 1st argument)
The match operator matches a value (here
n
) with the various constructors of its (inductive) type. The remaining arguments give the respective values to be returned, as functions of the parameters of the corresponding constructor. Thus here whenn
equalsO
we returnm
, and whenn
equals(S p)
we return(S (add p m))
.The match operator is formally described in Section The match ... with ... end construction. The system recognizes that in the inductive call
(add p m)
the first argument actually decreases because it is a pattern variable coming frommatch n with
.Example
The following definition is not correct and generates an error message:
 Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := match m with  O => n  S p => S (wrongplus n p) end.
 The command has indeed failed with message: Recursive definition of wrongplus is illformed. 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".
because the declared decreasing argument
n
does not actually decrease in the recursive call. The function computing the addition over the second argument should rather be written: Fixpoint plus (n m:nat) {struct m} : nat := match m with  O => n  S p => S (plus n p) end.
 plus is defined plus is recursively defined (guarded on 2nd argument)
Example
The recursive call may not only be on direct subterms of the recursive variable
n
but also on a deeper subterm and we can directly write the functionmod2
which gives the remainder modulo 2 of a natural number. Fixpoint mod2 (n:nat) : nat := match n with  O => O  S p => match p with  O => S O  S q => mod2 q end end.
 mod2 is defined mod2 is recursively defined (guarded on 1st argument)
Example: Mutual fixpoints
The size of trees and forests can be defined the following way:
 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)
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:
which corresponds to the result of the Coq 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:
which corresponds to the result of the Coq 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:
which corresponds to the result of the Coq 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:
Wellformed 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 nonmutual 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 constructorleaf
satisfies the positivity condition fornattree
becausenattree
does not appear in any (real) arguments of the type of that constructor (primarily becausenattree
does not have any (real) arguments) ... (bullet 1)Type
A → (nat → nattree A) → nattree A
of constructornatnode
satisfies the positivity condition fornattree
because:nattree
occurs only strictly positively inA
... (bullet 1)nattree
occurs only strictly positively innat → nattree A
... (bullet 3 + 2)nattree
satisfies the positivity condition fornattree 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
 WInd
 \[\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\).
One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative sorts \(\SProp\) and \(\Prop\) but may fail to define inductive type on sort \(\Set\) and generate constraints between universes for inductive types in the Type hierarchy.
Example
It is well known that the existential quantifier can be encoded as an inductive definition. The following declaration introduces the secondorder 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 nonterminating 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].
Template polymorphism¶
Inductive types can be made polymorphic over the universes introduced by their parameters in \(\Type\), if the minimal inferred sort of the inductive declarations either mention some of those parameter universes or is computed to be \(\Prop\) or \(\Set\).
If \(A\) is an arity of some sort and \(s\) is a sort, we write \(A_{/s}\) for the arity obtained from \(A\) by replacing its sort with \(s\). Especially, if \(A\) is welltyped in some global environment and local context, then \(A_{/s}\) is typable by typability of all products in the Calculus of Inductive Constructions. The following typing rule is added to the theory.
Let \(\ind{p}{Γ_I}{Γ_C}\) be an inductive definition. Let \(Γ_P = [p_1 :P_1 ;~…;~p_p :P_p ]\) be its context of parameters, \(Γ_I = [I_1:∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k ]\) its context of definitions and \(Γ_C = [c_1 :∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n]\) its context of constructors, with \(c_i\) a constructor of \(I_{q_i}\). Let \(m ≤ p\) be the length of the longest prefix of parameters such that the \(m\) first arguments of all occurrences of all \(I_j\) in all \(C_k\) (even the occurrences in the hypotheses of \(C_k\)) are exactly applied to \(p_1 … p_m\) (\(m\) is the number of recursively uniform parameters and the \(p−m\) remaining parameters are the recursively nonuniform parameters). Let \(q_1 , …, q_r\), with \(0≤ r≤ m\), be a (possibly) partial instantiation of the recursively uniform parameters of \(Γ_P\). We have:
 IndFamily
 \[\begin{split}\frac{% \left\{\begin{array}{l}% \hspace{3em}% \ind{p}{Γ_I}{Γ_C} \in E\\% \hspace{3em}% (E[] ⊢ q_l : P'_l)_{l=1\ldots r}\\% \hspace{3em}% (E[] ⊢ P'_l ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l1})_{l=1\ldots r}\\% \hspace{3em}% 1 \leq j \leq k% \hspace{3em}% \end{array}% \hspace{3em}% \right.% }{% E[] ⊢ I_j~q_1 … q_r :∀ [p_{r+1} :P_{r+1} ;~…;~p_p :P_p], (A_j)_{/s_j}% }\end{split}\]
provided that the following side conditions hold:
\(Γ_{P′}\) is the context obtained from \(Γ_P\) by replacing each \(P_l\) that is an arity with \(P_l'\) for \(1≤ l ≤ r\) (notice that \(P_l\) arity implies \(P_l'\) arity since \(E[] ⊢ P_l' ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l1}\));
there are sorts \(s_i\), for \(1 ≤ i ≤ k\) such that, for \(Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]\) we have \((E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}\) ;
the sorts \(s_i\) are all introduced by the inductive declaration and have no universe constraints beside being greater than or equal to \(\Prop\), and such that all eliminations, to \(\Prop\), \(\Set\) and \(\Type(j)\), are allowed (see Section Destructors).
Notice that if \(I_j~q_1 … q_r\) is typable using the rules IndConst and App, then it is typable using the rule IndFamily. Conversely, the extended theory is not stronger than the theory without IndFamily. We get an equiconsistency result by mapping each \(\ind{p}{Γ_I}{Γ_C}\) occurring into a given derivation into as many different inductive types and constructors as the number of different (partial) replacements of sorts, needed for this derivation, in the parameters that are arities (this is possible because \(\ind{p}{Γ_I}{Γ_C}\) wellformed implies that \(\ind{p}{Γ_{I'}}{Γ_{C'}}\) is wellformed and has the same allowed eliminations, where \(Γ_{I′}\) is defined as above and \(Γ_{C′} = [c_1 :∀ Γ_{P′} ,C_1 ;~…;~c_n :∀ Γ_{P′} ,C_n ]\)). That is, the changes in the types of each partial instance \(q_1 … q_r\) can be characterized by the ordered sets of arity sorts among the types of parameters, and to each signature is associated a new inductive definition with fresh names. Conversion is preserved as any (partial) instance \(I_j~q_1 … q_r\) or \(C_i~q_1 … q_r\) is mapped to the names chosen in the specific instance of \(\ind{p}{Γ_I}{Γ_C}\).
Warning
The restriction that sorts are introduced by the inductive declaration prevents inductive types declared in sections to be templatepolymorphic on universes introduced previously in the section: they cannot parameterize over the universes introduced with section variables that become parameters at section closing time, as these may be shared with other definitions from the same section which can impose constraints on them.
 Flag Auto Template Polymorphism¶
This flag, enabled by default, makes every inductive type declared at level \(\Type\) (without an explicit universe instance or hiding it behind a definition) template polymorphic if possible.
This can be prevented using the
universes(template=no)
attribute.Template polymorphism and full universe polymorphism (see Chapter Polymorphic Universes) are incompatible, so if the latter is enabled (through the
Universe Polymorphism
flag or theuniverses(polymorphic)
attribute) it will prevail over automatic template polymorphism.
 Warning Automatically declaring ident as template polymorphic.¶
Warning
autotemplate
can be used (it is off by default) to find which types are implicitly declared template polymorphic byAuto Template Polymorphism
.An inductive type can be forced to be template polymorphic using the
universes(template)
attribute: in this case, the warning is not emitted.
 Attribute universes(template= yesno?)¶
This boolean attribute can be used to explicitly declare an inductive type as template polymorphic, whether the
Auto Template Polymorphism
flag is on or off. Error template and polymorphism not compatible¶
This attribute cannot be used in a full universe polymorphic context, i.e. if the
Universe Polymorphism
flag is on or if theuniverses(polymorphic)
attribute is used.
 Error Illformed template inductive declaration: not polymorphic on any universe.¶
The attribute was used but the inductive definition does not satisfy the criterion to be template polymorphic.
When
universes(template=no)
is used, it will prevent an inductive type to be template polymorphic, even if theAuto Template Polymorphism
flag is on.
In practice, the rule IndFamily is used by Coq only when there is only one inductive type in the inductive definition and it is declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over the parameters whose type is an arity of sort in the Type hierarchy. The sorts \(s_j\) are chosen canonically so that each \(s_j\) is minimal with respect to the hierarchy \(\Prop ⊂ \Set_p ⊂ \Type\) where \(\Set_p\) is predicative \(\Set\). More precisely, an empty or small singleton inductive definition (i.e. an inductive definition of which all inductive types are singleton – see Section Destructors) is set in \(\Prop\), a small nonsingleton inductive type is set in \(\Set\) (even in case \(\Set\) is impredicative – see The Calculus of Inductive Constructions with impredicative Set), and otherwise in the Type hierarchy.
Note that the sidecondition about allowed elimination sorts in the rule IndFamily avoids to recompute the allowed elimination sorts at each instance of a pattern matching (see Section Destructors). As an example, let us consider the following definition:
Example
 Inductive option (A:Type) : Type :=  None : option A  Some : A > option A.
 option is defined option_rect is defined option_ind is defined option_rec is defined option_sind is defined
As the definition is set in the Type hierarchy, it is used
polymorphically over its parameters whose types are arities of a sort
in the Type hierarchy. Here, the parameter \(A\) has this property, hence,
if option
is applied to a type in \(\Set\), the result is in \(\Set\). Note that
if option
is applied to a type in \(\Prop\), then, the result is not set in
\(\Prop\) but in \(\Set\) still. This is because option
is not a singleton type
(see Section Destructors) and it would lose the elimination to \(\Set\) and \(\Type\)
if set in \(\Prop\).
Example
 Check (fun A:Set => option A).
 fun A : Set => option A : Set > Set
 Check (fun A:Prop => option A).
 fun A : Prop => option A : Prop > Set
Here is another example.
Example
 Inductive prod (A B:Type) : Type := pair : A > B > prod A B.
 prod is defined prod_rect is defined prod_ind is defined prod_rec is defined prod_sind is defined
As prod
is a singleton type, it will be in \(\Prop\) if applied twice to
propositions, in \(\Set\) if applied twice to at least one type in \(\Set\) and
none in \(\Type\), and in \(\Type\) otherwise. In all cases, the three kind of
eliminations schemes are allowed.
Example
 Check (fun A:Set => prod A).
 fun A : Set => prod A : Set > Type > Type
 Check (fun A:Prop => prod A A).
 fun A : Prop => prod A A : Prop > Prop
 Check (fun (A:Prop) (B:Set) => prod A B).
 fun (A : Prop) (B : Set) => prod A B : Prop > Set > Set
 Check (fun (A:Type) (B:Prop) => prod A B).
 fun (A : Type) (B : Prop) => prod A B : Type > Prop > Type
Note
Template polymorphism used to be called “sortpolymorphism of inductive types” before universe polymorphism (see Chapter Polymorphic Universes) was introduced.
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 MartinLö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 in this version of Coq 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 Coq term for this proof will be written:
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\). Coq 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:
The \(\as\) part can be omitted if either the result type does not depend on \(m\) (nondependent 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:
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:AB]\) we mean that one can use \(λ a x . P\) with \(m\) in the above matchconstruct.
Notations. The \([I:AB]\) is defined as the smallest relation satisfying the following rules: We write \([IB]\) for \([I:AB]\) 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:\PropI→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 noncomputational 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 noncomputational 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 proofirrelevance 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 secondorder 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.
 Propextended
 \[\frac{% I~\kw{is an empty or singleton definition}% \hspace{3em}% s ∈ \Sort% }{% [I:\PropI→ 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 noninformative 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_rect x P : 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 f y e (where some original arguments have been renamed)
 Require Extraction.
 [Loading ML file extraction_plugin.cmxs (using legacy method) ... done]
 Extraction eq_rec.
 (** val eq_rec : 'a1 > 'a2 > 'a1 > 'a2 **) let eq_rec _ f _ = f
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.
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
where
According to the definition:
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:
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:
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):
The terms are obtained by projections from this set of declarations and are written
In the inference rules, we represent such a term by
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 nonnormalizing 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
can be represented by the term:
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
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:
when \(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:
Mutual induction
The principles of mutual induction can be automatically generated using the Scheme command described in Section Generation of induction principles with Scheme.