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

Defines one or more inductive types and its constructors. Rocq generates induction principles depending on the universe that the inductive type belongs to.

The induction principles are named ident_rect, ident_ind, ident_rec and ident_sind, which respectively correspond to on Type, Prop, Set and SProp. Their types expresses structural induction/recursion principles over objects of type ident. These constants are generated when possible (for instance ident_rect may be impossible to derive when ident 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 in Prop.

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 as destruct on such inductives.

Note that explicit declarations through Scheme are not affected by this flag.

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

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

When record syntax is used, this command also supports the projections(primitive) attribute. Also, in the record syntax, if given, the as 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_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 induction principles currently generated for such types are not useful. Use the Scheme command to generate useful induction principles. See Mutually defined inductive types.

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. For this reason, the parameters must be strictly the same for each inductive type. See Parameterized inductive types.

Constructor idents can come with binders, in which case the actual type of the constructor is forall 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 the bypass_check(positivity) attribute (see Controlling Typing Flags).

Error The conclusion of type is not valid; it must be built from ident.¶: The conclusion of the type of the constructors must be the inductive type ident being defined (or ident applied to arguments in the case of indexed inductive types — cf. next section).

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

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.

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 binders 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 non-uniform 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.

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:

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.

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? := termfixannot::={ struct ident }|{ wf one_term ident }|{ measure one_term ident? one_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.

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.

Top-level 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 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 program, bypass_check(universes), and bypass_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 the Fixpoint definition always terminates. The point of the {struct ident} annotation (see fixannot) 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 the program attribute does not support the wf or measure clauses of fixannot. 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 Rocq enters proof mode. This can be used to define a term incrementally, in particular by relying on the refine tactic. In this case, the proof should be terminated with Defined 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 when n equals O we return m, and when n 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 from match 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 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".

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)

Aside: Observe that plus n 0 is reducible but plus 0 n is not, the reverse of Nat.add, for which 0 + n is reducible and n + 0 is not.

Goal forall n:nat, plus n 0 = plus 0 n.: 1 goal ============================ forall n : nat, plus n 0 = plus 0 n
intros; simpl. (* plus 0 n not reducible *): 1 goal n : nat ============================ n = plus 0 n

Abort.

Goal forall n:nat, n + 0 = 0 + n.: 1 goal ============================ forall n : nat, n + 0 = 0 + n
intros; simpl. (* n + 0 not reducible *): 1 goal n : nat ============================ n + 0 = n

Abort.

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 function mod2 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:

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

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

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 well-typed 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 non-uniform parameters). Let $q_1 , …, q_r$, with $0≤ r≤ m$, be a (possibly) partial instantiation of the recursively uniform parameters of $Γ_P$. We have:

Ind-Family: \[\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 l-1})_{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 l-1}$);

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 Ind-Const and App, then it is typable using the rule Ind-Family. Conversely, the extended theory is not stronger than the theory without Ind-Family. 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}$ well-formed implies that $\ind{p}{Γ_{I'}}{Γ_{C'}}$ is well-formed 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 template-polymorphic 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 the universes(polymorphic) attribute) it will prevail over automatic template polymorphism.

Warning Automatically declaring ident as template polymorphic.¶

Warning auto-template can be used (it is off by default) to find which types are implicitly declared template polymorphic by Auto 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 the universes(polymorphic) attribute is used.

Error Ill-formed 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 the Auto Template Polymorphism flag is on.

In practice, the rule Ind-Family is used by Rocq 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 non-singleton 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 side-condition about allowed elimination sorts in the rule Ind-Family 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 “sort-polymorphism 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 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_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 rocq-runtime.plugins.extraction ... 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.

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