4.5 Inductive Definitions

A (possibly mutual) inductive definition is specified by giving the names and the type of the inductive sets or families to be defined and the names and types of the constructors of the inductive predicates. An inductive declaration in the environment can consequently be represented with two contexts (one for inductive definitions, one for constructors).

Stating the rules for inductive definitions in their general form needs quite tedious definitions. We shall try to give a concrete understanding of the rules by precising them on running examples. We take as examples the type of natural numbers, the type of parameterized lists over a type A, the relation which state that a list has some given length and the mutual inductive definition of trees and forests.

4.5.1 Representing an inductive definition

Inductive definitions without parameters

As for constants, inductive definitions can be defined in a non-empty context.
We write Ind(G)(G_I:=G_C ) an inductive definition valid in a context G, a context of definitions G_I and a context of constructors G_C.

Examples.

The inductive declaration for the type of natural numbers will be:

Ind

()(

nat

Set

nat

)

In a context with a variable A:Set, the lists of elements in A is represented by:

Ind

(A:

Set

)(

List

Set

nil

List

cons

: A Ž

List

)

Assuming G_I is [I₁:A₁;...;I_k:A_k], and G_C is [c₁:C₁;...;c_n:C_n], the general typing rules are:

(I_j:A_j) Î E

(c_i:C_i{I_j/I_j}

j=1... k

)Î E

Inductive definitions with parameters

We have to slightly complicate the representation above in order to handle the delicate problem of parameters. Let us explain that on the example of List. As they were defined above, the type List can only be used in an environment where we have a variable A:Set. Generally one want to consider lists of elements in different types. For constants this is easily done by abstracting the value over the parameter. In the case of inductive definitions we have to handle the abstraction over several objects.

One possible way to do that would be to define the type List inductively as being an inductive family of type SetŽSet:

Ind

()(

List

Set

nil

:(A:

Set

)(

List

A),

cons

: (A:

Set

)A Ž (

List

A) Ž (

List

A) )

There are drawbacks to this point of view. The information which says that (List nat) is an inductively defined Set has been lost. In the system, we keep track in the syntax of the context of parameters. The idea of these parameters is that they can be instantiated and still we have an inductive definition for which we know the specification.

Formally the representation of an inductive declaration will be Ind(G)[G_P](G_I:=G_C ) for an inductive definition valid in a context G with parameters G_P, a context of definitions G_I and a context of constructors G_C. The occurrences of the variables of G_P in the contexts G_I and G_C are bound.

The definition Ind(G)[G_P]( G_I:=G_C ) will be well-formed exactly when Ind(G,G_P)( G_I:=G_C ) is. If G_P is [p₁:P₁;...;p_r:P_r], an object in Ind(G)[G_P](G_I:=G_C ) applied to q₁,...,q_r will behave as the corresponding object of Ind(G)(G_I{(p_i/q_i)_i=1..r}:=G_C{(p_i/q_i)_i=1..r} ).

Examples

The declaration for parameterized lists is:

Ind

()[A:

Set

](

List

Set

nil

List

cons

: A Ž

List

)

The declaration for the length of lists is:

Ind

()[A:

Set

](

Length

List

A)Ž

nat

Prop

Lnil

Length

(

nil

Lcons

:(a:A)(l:(

List

A))(n:

nat

)(

Length

l n)Ž (

Length

(

cons

A a l) (

n)) )

The declaration for a mutual inductive definition of forests and trees is:

Ind

([])(

tree

Set

forest

Set

node

forest

tree

emptyf

forest

consf

tree

forest

)

These representations are the ones obtained as the result of the Coq declaration:

Coq < Inductive Set nat := O : nat | S : nat -> nat.

Coq < Inductive list [A : Set] : Set :=
Coq < nil : (list A) | cons : A -> (list A) -> (list A).

Coq < Inductive Length [A:Set] : (list A) -> nat -> Prop :=
Coq < Lnil : (Length A (nil A) O)
Coq < | Lcons : (a:A)(l:(list A))(n:nat)
Coq < (Length A l n)->(Length A (cons A a l) (S n)).

Coq < Mutual Inductive tree : Set := node : forest -> tree
Coq < with forest : Set := emptyf : forest | consf : tree -> forest -> forest.

The inductive declaration in Coq is slightly different from the one we described theoretically. The difference is that in the type of constructors the inductive definition is explicitly applied to the parameters variables. The Coq type-checker verifies that all parameters are applied in the correct manner in each recursive call. In particular, the following definition will not be accepted because there is an occurrence of List which is not applied to the parameter variable:

Coq < Inductive list [A : Set] : Set :=
Coq < nil : (list A) | cons : A -> (list A->A) -> (list A).
Error during interpretation of command:
Inductive list [A : Set] : Set :=
nil : (list A) | cons : A -> (list A->A) -> (list A).
Error: Bad application to parameters in (A:Set)A->(list A->A)->(list A)

4.5.2 Types of inductive objects

We have to give the type of constants in an environment E which contains an inductive declaration.

Ind-Const

Assuming G_P is [p₁:P₁;...;p_r:P_r], G_I is [I₁:A₁;...;I_k:A_k], and G_C is [c₁:C₁;...;c_n:C_n],

(I_j:(p₁:P₁)...(p_r:P_r)A_j) Î E

(c_i:(p₁:P₁)...(p_r:P_r)C_i{I_j/(I_j p₁... p_r)}

j=1... k

)Î E

Example.

We have (List:Set Ž Set), (cons:(A:Set)AŽ(List A)Ž (List A)),
(Length:(A:Set)(List A)ŽnatŽProp), tree:Set and forest:Set.

From now on, we write List_A instead of (List A) and Length_A for (Length A).

4.5.3 Well-formed inductive definitions

We cannot accept any inductive declaration 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:

Definitions

A type T is an arity of sort sif it is the sort s or a product (x:T)U with U an arity of sort s. (For instance AŽ Set or (A:Prop)AŽ Prop are arities of sort respectively Set and Prop).

A type of constructor of Iis either a term (I t₁... t_n) or (x:T)C with C a type of constructor of I. It will be said to satisfy the positivity condition with respect to a constant X if X does not occur in t_i and occurs only strictly positively in each domain of product T.

The constant X occurs strictly positively in (X t₁ ... t_n) if it does not occur in t_i and occurs strictly positively in (x:T)U if it does not occur in T and occurs strictly positively in U.

Example

For instance X occurs strictly positively in AŽ X but not in X Ž A or (X Ž A)Ž A or X*A or ( list X) assuming the notion of product and lists were already defined. In the last two cases it is easy to define an equivalent (possibly mutual inductive) definition which enjoys the positivity condition.

Correctness rules.

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

W-Ind

Let E be an environment and G,G_P,G_I,G_C are contexts such that G_I is [I₁:A₁;...;I_k:A_k] and G_C is [c₁:C₁;...;c_n:C_n].

(E;

Ind	(G)[G_P](G_I:=G_C )

)[G]

providing the following side conditions hold:

k>0, I_j, c_i are different names for j=1... k and i=1... n,
for j=1... k we have A_j is an arity of sort s_j and I_j Ď G Č E,
for i=1... n we have C_i is a type of constructor of I_{p_i} which satisfies the positivity condition for I₁ ... I_k and c_i Ď G Č 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 impredicative sorts (Prop or Set) but may generate constraints between universes.

4.5.4 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 normalising 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 context, we want to build a function length of type List_AŽ nat which computes the length of the list, so such that (length nil) = O and (length (cons A a l)) = (S (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 (P m) for m in an inductive definition 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)(Length_A l (length l)) it is enough to prove:

(Length_A nil (length nil)) and

(a:A)(l:List_A)(Length_A l (length l)) Ž (Length_A (cons A a l) (length (cons A a l))).

which given the conversion equalities satisfied by length is the same as proving: (Length_A nil O) and (a:A)(l:List_A)(Length_A l (length l)) Ž (Length_A (cons A a l) (S (length l))).

One conceptually simple way to do that, following the basic scheme proposed by Martin-Lof 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 [20]. One is the definition by case analysis. The second one is a definition by guarded fixpoints.

The `Cases...of ...end` construction.

The basic idea of this destructor operation is that we have an object m in an inductive type I and we want to prove a property (P m) which in general depends on m. For this, it is enough to prove the property for m = (c_i u₁... u_{p_i}) for each constructor of I.

This proof will be denoted by a generic term:

Cases

of

(c₁ x₁₁ ... x_1p₁)

=>

f₁ ...(c_n x_n1 | ... | x_{np_n})

=>

f_n

end

In this expression, if m is a term built from a constructor (c_i u₁... u_{p_i}) then the expression will behave as it is specified with i-th branch and will reduce to f_i where the x_i1...x_{ip_i} are replaced by the u₁... u_p according to the i-reduction.

This is the basic idea which is generalized to the case where I is an inductively defined n-ary relation (in which case the property P to be proved will be a n+1-ary relation).

Non-dependent elimination.

When defining a function by case analysis, we build an object of type I Ž C and the minimality principle on an inductively defined logical predicate of type A Ž Prop is often used to prove a property (x:A)(I x)Ž (C x). This is a particular case of the dependent principle that we stated before with a predicate which does not depend explicitly on the object in the inductive definition.

For instance, a function testing whether a list is empty can be defined as:

[l:

List_A

]

<[H:

List_A

]

bool

Cases

of

nil

=>

true

| (

cons

a m)

=>

false

end

Remark. In the system Coq the expression above, can be written without mentioning the dummy abstraction: <bool>Cases l of nil => true | (cons a m) => false end

Allowed elimination sorts.

An important question for building the typing rule for Case is what can be the type of P with respect to the type of the inductive definitions.

Remembering that the elimination builds an object in (P m) from an object in m in type I it is clear that we cannot allow any combination.

For instance we cannot in general have I has type Prop and P has 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.

Also if I is in one of the sorts {Prop, Set}, one cannot in general allow an elimination over a bigger sort such as Type. But this operation is safe whenever I is a small inductive type, which means that all the types of constructors of I are small with the following definition:
(I t₁... t_s) is a small type of constructor and (x:T)C is a small type of constructor if C is and if T has type Prop or Set.

We call this particular elimination which gives the possibility to compute a type by induction on the structure of a term, a strong elimination.

We define now a relation [I:A|B] between an inductive definition I of type A, an arity B which says that an object in the inductive definition I can be eliminated for proving a property P of type B.

The [I:A|B] is defined as the smallest relation satisfying the following rules:

Prod

[I:(x:A)A'|(x:A)B']

Prop

[I:

Prop

|IŽ

Prop

]

[I:

Prop

|IŽ

Set

]

Set

[I:

Set

|IŽ s]

[I:

Set

|IŽ s]

Type

[I:

Type

(i)|IŽ s]

Notations.

We write [I|B] for [I:A|B] where A is the type of I.

Singleton elimination

A singleton definition has always an informative content, even if it is a proposition.

A singleton definition has only one constructor and all the argument of this constructor are non informative. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on sort s is legal. Typical examples are the conjunction of non-informative propositions and the equality. In that case, the term eq_rec which was defined as an axiom, is now a term of the calculus.

Coq < Print eq_rec.
eq_rec =
[A:Set]
[x:A][P:A->Set][f:(P x)][y:A][e:x=y]Cases e of refl_equal => f end
: (A:Set)(x:A)(P:A->Set)(P x)->(y:A)x=y->(P y)

Coq < Extraction eq_rec.
eq_rec ==> [A:Set][_:A][P:Set][f:P][_:A]f
: (A:Set)A->(P:Set)P->A->P

Type of branches.

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

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

{c:(I_i p₁... p_r t₁ ... t_p)}^P

ş (P t₁... t_p c)

{c:(x: T)C}^P

ş (x:T)

{(c x):C}^P

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

Examples.

For List_A the type of P will be List_AŽ s for s Î {Prop,Set,Type(i)}.
{(cons A)}^P ş (a:A)(l:List_A)(P (cons A a l)).

For Length_A, the type of P will be (l:List_A)(n:nat)(Length_A l n)Ž Prop and the expression {(Lcons A)}^P is defined as:
(a:A)(l:List_A)(n:nat)(h:(Length_A l n))(P (cons A a l) (S n) (Lcons A a l n l)).
If P does not depend on its third argument, we find the more natural expression:
(a:A)(l:List_A)(n:nat)(Length_A l n)Ž(P (cons A a l) (S n)).

Typing rule.

Our very general destructor for inductive definition enjoys the following typing rule (we write Cases c of [x₁₁:T₁₁]...[x_1p₁:T_1p₁]f₁... [x_n1:T_n1]...[x_{np_n}:T_{np_n}f_n end for Cases m of (c₁ x₁₁ ... x_1p₁) => f₁ ... (c_n x_n1 | ... | x_{np_n}) => f_n end):

Case

E[G]

Cases

of

f₁... f_l

end

: (P t₁... t_s c)

provided I is an inductive type in a declaration Ind(D)[G_P](G_I:=G_C ) with |G_P| = r, G_C = [c₁:C₁;...;c_n:C_n] and c_p₁... c_{p_l} are the only constructors of I.

Example.

For List and Length the typing rules for the Case expression are (writing just t:M instead of E[G] |- t : M, the environment and context being the same in all the judgments).

Cases

of

f₁ f₂

end

:(P l)

Cases

of

f₁ f₂

end

:(P L N H)

Definition of i-reduction.

We still have to define the i-reduction in the general case.

A i-redex is a term of the following form:

Cases

(c_{p_i} q₁... q_r a₁... a_m)

of

f₁... f_l

end

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

The i-contraction of this term is (f_i a₁... a_m) leading to the general reduction rule:

Cases

(c_{p_i} q₁... q_r a₁... a_m)

of

f₁... f_n

end

(f_i a₁... a_m)

4.5.5 Fixpoint definitions

The second operator for elimination is fixpoint definition. This fixpoint may involve several mutually recursive definitions. The basic syntax for a recursive set of declarations is

Fix {f₁:A₁:=t₁ ... f_n:A_n:=t_n}

The terms are obtained by projections from this set of declarations and are written Fix f_i{f₁:A₁:=t₁ ... f_n:A_n:=t_n}

Typing rule

The typing rule is the expected one for a fixpoint.

Fix

E[G] |- Fix f_i{f₁:A₁:=t₁ ... f_n:A_n:=t_n} : A_i

Any fixpoint definition cannot be accepted because non-normalizing terms will lead to 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 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

)Ž((n:

nat

)(P n)Ž(P (

n)))Ž(n:

nat

)(P n)

can be represented by the term:

[P:

nat

Prop

][f:(P

)][g:(n:

nat

)(P n)Ž(P (

n))]

Fix

h{h:(n:

nat

)(P n):=[n:

nat

]

Cases

of

f [p:

nat

](g p (h p))

end

}

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 [46].

The first stage is to precise on which argument the fixpoint will be decreasing. The type of this argument should be an inductive definition.

For doing this the syntax of fixpoints is extended and becomes

Fix f_i{f₁/k₁:A₁:=t₁ ... f_n/k_n:A_n:=t_n}

where k_i are positive integers. Each A_i should be a type (reducible to a term) starting with at least k_i products (y₁:B₁)... (y_{k_i}:B_{k_i}) A'_i and B_{k_i} being an instance of an inductive definition.

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(G)[G_P](G_I:=G_C ), the type of a constructor c have the form (p₁:P₁)...(p_r:P_r)(x₁:T₁)... (x_r:T_r)(I_j p₁... p_r t₁... t_s) 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 type an inductive definition in a declaration Ind(G)[G_P](G_I:=G_C ) where G_I is [I₁:A₁;...;I_k:A_k], and G_C is [c₁:C₁;...;c_n:C_n]. The terms structurally smaller than y are:

(t u), [x:u]t when t is structurally smaller than y .
Cases c of f₁... f_n end when each f_i is structurally smaller than y.
If c is y or is structurally smaller than y, its type is an inductive definition I_p part of the inductive declaration corresponding to y. Each f_i corresponds to a type of constructor C_q ş (y₁:B₁)... (y_k:B_k)(I a₁... a_k) and can consequently be written [y₁:B'₁]... [y_k:B'_k]g_i. (B'_i is obtained from B_i by substituting parameters 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 as described in section 1.3.4 and show the internal representation.

Coq < Fixpoint plus [n:nat] : nat -> nat :=
Coq < [m:nat]Case n of m [p:nat](S (plus p m)) end.
plus is recursively defined

Coq < Print plus.
plus =
Fix plus{plus [n:nat] : nat->nat :=
 [m:nat]Cases n of
 O => m
 | (S p) => (S (plus p m))
 end}
 : nat->nat->nat

Coq < Fixpoint lgth [A:Set;l:(list A)] : nat :=
Coq < Case l of O [a:A][l':(list A)](S (lgth A l')) end.
lgth is recursively defined

Coq < Print lgth.
lgth =
Fix lgth{lgth [A:(Set);l:(list A)] : nat :=
 Cases l of
 nil => O
 | (cons _ l') => (S (lgth A l'))
 end}
 : (A:Set)(list A)->nat

Coq < Fixpoint sizet [t:tree] : nat
Coq < := Case t of [f:forest](S (sizef f)) end
Coq < with sizef [f:forest] : nat
Coq < := Case f of O [t:tree][f:forest](plus (sizet t) (sizef f)) end.
sizet, sizef are recursively defined

Coq < Print sizet.
sizet =
Fix sizet{sizet [t:tree] : nat :=
 Cases t of (node f) => (S (sizef f)) end
 with
 sizef [f:forest] : nat :=
 Cases f of
 emptyf => O
 | (consf t f0) => (plus (sizet t) (sizef f0))
 end}
 : tree->nat

Reduction rule

Let F be the set of declarations: f₁/k₁:A₁:=t₁ ... f_n/k_n:A_n:=t_n. The reduction for fixpoints is:

(

Fix

f_i{F} a₁...a_{k_i}) |>

t_i{(f_k/

Fix

f_k{F})

k=1... n

}

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.

We can illustrate this behavior on examples.

Coq < Goal (n,m:nat)(plus (S n) m)=(S (plus n m)).
1 subgoal

 ============================
 (n,m:nat)(plus (S n) m)=(S (plus n m))

Coq < Reflexivity.
Subtree proved!

Coq < Abort.
Current goal aborted

Coq < Goal (f:forest)(sizet (node f))=(S (sizef f)).
1 subgoal

 ============================
 (f:forest)(sizet (node f))=(S (sizef f))

Coq < Reflexivity.
Subtree proved!

Coq < Abort.
Current goal aborted

But assuming the definition of a son function from tree to forest:

Coq < Definition sont : tree -> forest := [t]Case t of [f]f end.
sont is defined

The following is not a conversion but can be proved after a case analysis.

Coq < Goal (t:tree)(sizet t)=(S (sizef (sont t))).
1 subgoal

 ============================
 (t:tree)(sizet t)=(S (sizef (sont t)))

Coq < (* this one fails *)
Coq < Reflexivity.
Error during interpretation of command:
Reflexivity.
Error: Impossible to unify S with sizet

Coq < Destruct t.
1 subgoal

 t : tree
 ============================
 (f:forest)(sizet (node f))=(S (sizef (sont (node f))))

Coq < Reflexivity.
Subtree proved!

The `Match ...with ...end` expression

The Match operator which was a primitive notion in older presentations of the Calculus of Inductive Constructions is now just a macro definition which generates the good combination of Case and Fix operators in order to generate an operator for primitive recursive definitions. It always considers an inductive definition as a single inductive definition.

The following examples illustrates this feature.

Coq < Definition nat_pr : (C:Set)C->(nat->C->C)->nat->C
Coq < :=[C,x,g,n]Match n with x g end.
nat_pr is defined

Coq < Print nat_pr.
nat_pr =
[C:Set]
[x:C]
 [g:nat->C->C]
 [n:nat]
 (Fix F{F [n0:nat] : C :=
 Cases n0 of
 O => x
 | (S n1) => (g n1 (F n1))
 end} n)
 : (C:Set)C->(nat->C->C)->nat->C

Coq < Definition forest_pr
Coq < : (C:Set)C->(tree->forest->C->C)->forest->C
Coq < := [C,x,g,n]Match n with x g end.
forest_pr is defined

The principles of mutual induction can be automatically generated using the Scheme command described in section 7.15.

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.0.3.4.html at 8/10/98