Chapter 1 The Gallina specification language
This chapter describes Gallina, the specification language of Coq.
It allows to develop mathematical theories and to prove specifications
of programs. The theories are built from axioms, hypotheses,
parameters, lemmas, theorems and definitions of constants, functions,
predicates and sets. The syntax of logical objects involved in
theories is described in section 1.2. The language of
commands, called The Vernacular is described in section
1.3.
In Coq, logical objects are typed to ensure their logical
correctness. The rules implemented by the typing algorithm are described in
chapter 4.
About the grammars in the manual
Grammars are presented in BackusNaur form (BNF). Terminal symbols are
set in typewriter font. In addition, there are special
notations for regular expressions.
An expression enclosed in square brackets [...] means at
most one occurrence of this expression (this corresponds to an
optional component).
The notation ``entry sep ... sep entry'' stands for a non empty
sequence of expressions parsed by entry and
separated by the literal ``sep''^{1}.
Similarly, the notation ``entry ... entry'' stands for a non
empty sequence of expressions parsed by the ``entry'' entry,
without any separator between.
At the end, the notation ``[entry sep ... sep entry]'' stands for a
possibly empty sequence of expressions parsed by the ``entry'' entry,
separated by the literal ``sep''.
1.1 Lexical conventions
Blanks
Space, newline and horizontal tabulation are considered as blanks.
Blanks are ignored but they separate tokens.
Comments
Comments in Coq are enclosed between (* and *), and can be nested. They can contain any
character. However, string literals must be correctly closed. Comments
are treated as blanks.
Identifiers and access identifiers
Identifiers, written ident, are sequences of letters, digits,
_
and '
, that do not start with a digit or '
.
That is, they are recognized by the following lexical class:
first_letter 
::= 
a..z  A..Z  _ 
subsequent_letter 
::= 
a..z  A..Z  0..9
 _  ' 
ident 
::= 
first_letter [subsequent_letter...subsequent_letter] 
All characters are meaningful. In particular, identifiers are casesensitive.
Access identifiers, written access_ident, are identifiers prefixed
by .
(dot) without blank. They are used in the syntax of qualified
identifiers.
Natural numbers and integers
Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign.
digit 
::= 
0..9 
num 
::= 
digit...digit 
integer 
::= 
[]num 
Strings
Strings are delimited by "
(double quote), and enclose a
sequence of any characters different from "
or the sequence
""
to denote the double quote character. In grammars, the
entry for quoted strings is string.
Keywords
The following identifiers are reserved keywords, and cannot be
employed otherwise:
_ 
as 
at 
cofix 
else 
end 
exists 
exists2 
fix 
for 
forall 
fun 
if 
IF 
in 
let 
match 
mod 
Prop 
return 
Set 
then 
Type 
using 
where 
with 
Special tokens
The following sequences of characters are special tokens:
! 
% 
& 
&& 
( 
() 
) 
* 
+ 
++ 
, 
 
> 
. 
.( 
.. 
/ 
/\ 
: 
:: 
:< 
:= 
:> 
; 
< 
< 
<> 
<: 
<= 
<> 
= 
=> 
=_D 
> 
>> 
>= 
? 
?= 
@ 
[ 
\/ 
] 
^ 
{ 
 
 
 
} 
~ 
Lexical ambiguities are resolved according to the ``longest match''
rule: when a sequence of non alphanumerical characters can be decomposed
into several different ways, then the first token is the longest
possible one (among all tokens defined at this moment), and so on.
1.2.1 Syntax of terms
Figures 1.1 and 1.2 describe the basic
set of terms which form the Calculus of Inductive Constructions
(also called pCic). The formal presentation of pCic is given in
chapter 4. Extensions of this syntax are given in chapter
2. How to customize the syntax is described in
chapter 11.
term 
::= 
forall binderlist , term 

(1.2.8) 

 
fun binderlist => term 

(1.2.7) 

 
fix fix_bodies 

(1.2.14) 

 
cofix cofix_bodies 

(1.2.14) 

 
let ident_with_params := term
in term 

(1.2.12) 

 
let fix fix_body in term 

(1.2.14) 

 
let cofix cofix_body
in term 

(1.2.14) 

 
let ( [name , ... , name] ) [dep_ret_type]
:= term
in term 

(1.2.13, 2.2.1) 

 
if term [dep_ret_type] then term
else term 

(1.2.13, 2.2.1) 

 
term : term 

(1.2.10) 

 
term > term 

(1.2.8) 

 
term arg ... arg 

(1.2.9) 

 
@ qualid [term ... term] 

(2.6.7) 

 
term % ident 

(11.2.2) 

 
match match_item , ... , match_item
[return_type] with 




[[] equation  ...  equation] end 

(1.2.13) 

 
qualid 

(1.2.3) 

 
sort 

(1.2.5) 

 
num 

(1.2.4) 

 
_ 

(1.2.11) 





arg 
::= 
term 



 
( ident := term ) 

(2.6.7) 





binderlist 
::= 
name ... name [: term] 

1.2.6 

 
binder binderlet ... binderlet 







binder 
::= 
name 

1.2.6 

 
( name ... name : term ) 







binderlet 
::= 
binder 

1.2.6 

 
( name [: term] := term ) 







name 
::= 
ident 



 
_ 







qualid 
::= 
ident 



 
qualid access_ident 







sort 
::= 
Prop  Set  Type 

Figure 1.1: Syntax of terms
ident_with_params 
::= 
ident [binderlet ... binderlet] [: term] 



fix_bodies 
::= 
fix_body 

 
fix_body with fix_body with ... with fix_body
for ident 
cofix_bodies 
::= 
cofix_body 

 
cofix_body with cofix_body with ... with cofix_body
for ident 



fix_body 
::= 
ident binderlet ... binderlet [annotation] [: term]
:= term 
cofix_body 
::= 
ident_with_params := term 



annotation 
::= 
{ struct ident } 



match_item 
::= 
term [as name]
[in term] 



dep_ret_type 
::= 
[as name] return_type 



return_type 
::= 
return term 



equation 
::= 
pattern , ... , pattern => term 



pattern 
::= 
qualid pattern ... pattern 

 
pattern as ident 

 
pattern % ident 

 
qualid 

 
_ 

 
num 

 
( pattern , ... , pattern ) 
Figure 1.2: Syntax of terms (continued)
Coq terms are typed. Coq types are recognized by the same
syntactic class as term. We denote by type the semantic subclass
of types inside the syntactic class term.
1.2.3 Qualified identifiers and simple identifiers
Qualified identifiers (qualid) denote global constants
(definitions, lemmas, theorems, remarks or facts), global
variables (parameters or axioms), inductive
types or constructors of inductive types.
Simple identifiers (or shortly ident) are a
syntactic subset of qualified identifiers. Identifiers may also
denote local variables, what qualified identifiers do not.
Numerals have no definite semantics in the calculus. They are mere
notations that can be bound to objects through the notation mechanism
(see chapter 11 for details). Initially, numerals are
bound to Peano's representation of natural numbers
(see 3.1.3).
Note: negative integers are not at the same level as num, for this
would make precedence unnatural.
There are three sorts Set, Prop and Type.

Prop is the universe of logical propositions.
The logical propositions themselves are typing the proofs.
We denote propositions by form. This constitutes a semantic
subclass of the syntactic class term.
 Set is is the universe of program
types or specifications.
The specifications themselves are typing the programs.
We denote specifications by specif. This constitutes a semantic
subclass of the syntactic class term.
 Type is the type of Set and Prop
More on sorts can be found in section 4.1.1.
Various constructions introduce variables which scope is some of its
subexpressions. There is a uniform syntax for this. A binder may be
an (unqualified) identifier: the name to use to refer to this
variable. If the variable is not to be used, its name can be _. When its type cannot be synthesized by the system, it can be
specified with notation ( ident : type ). There is a notation for several variables sharing the same type:
( ident_{1}...ident_{n} : type ).
Some constructions allow ``letbinders'', that is either a binder as
defined above, or a variable with a value. The notation is ( ident := term ). Only one variable can be
introduced at the same time. It is also possible to give the type of
the variable before the symbol :=.
The last kind of binders is the ``binder list''. It is either a list
of letbinders (the first one not being a variable with value), or
ident_{1}...ident_{n} : type if all variables
share the same type.
Coq terms are typed. Coq types are recognized by the same
syntactic class as term. We denote by type the semantic subclass
of types inside the syntactic class term.
1.2.7 Abstractions
The expression ``fun ident : type=> term''
denotes the abstraction of the variable ident of type
type, over the term term. Put in another way, it is function of
formal parameter ident of type type returning term.
Keyword fun is followed by a ``binder list'', so any of the
binders of Section 1.2.6 apply. Internally, abstractions are
only over one variable. Multiple variable binders are an iteration of
the single variable abstraction: notation fun ident_{1} ... ident_{n} : type => term stands for fun ident_{1} : type => ... fun ident_{n} : type => term.
Variables with a value expand to a local definition (see
Section 1.2.12).
The expression ``forall ident : type , term''
denotes the product of the variable ident of type type,
over the term term. As for abstractions, forall is followed
by a binder list, and it is represented by an iteration of single
variable products.
Non dependent product types have a special notation ``A >
B'' stands for ``forall _:A, B''. This is to stress
on the fact that non dependent product types are usual functional types.
1.2.9 Applications
The expression term_{0} term_{1} denotes the application of
term term_{0} to term_{1}.
The expression term_{0} term_{1} ... term_{n}
denotes the application of the term term_{0} to the arguments
term_{1} ... then term_{n}. It is equivalent to ...
( term_{0} term_{1} ) ... term_{n} :
associativity is to the left.
When using implicit arguments mechanism, implicit positions can be
forced a value with notation ( ident := term ) or ( num := term ). See Section 2.6.7 for
details.
The expression ``term : type'' is a type cast
expression. It enforces the type of term to be type.
1.2.11 Inferable subterms
Since there are redundancies, a term can be typechecked without
giving it in totality. Subterms that are left to guess by the
typechecker are replaced by ``_''.
1.2.12 Local definitions (letin)
let ident := term_{1} in term_{2} denotes
the local binding of term_{1} to the variable ident in
term_{2}.
There is a syntactic sugar for local definition of functions: let ident binder_{1} ...binder_{n} := term_{1}
in term_{2} stands for let ident := fun
binder_{1} ...binder_{n} in term_{2}.
1.2.13 Definition by case analysis
This paragraph only shows simple variants of case analysis. See
Section 2.2.1 and Chapter 15 for
explanations of the general form.
Objects of inductive types can be destructurated by a caseanalysis
construction, also called patternmatching in functional languages. In
its simple form, a case analysis expression is used to analyze the
structure of an inductive objects (upon which constructor it is
built).
The expression match term_{0} return_type with
pattern_{1} => term_{1}  ... 
pattern_{n} => term_{n} end, denotes a patternmatching over the term term_{0} (expected to be of an
inductive type I). term_{1}...term_{n} are called branches. In
a simple pattern qualid ident ... ident, the qualified identifier
qualid is intended to
be a constructor. There should be a branch for every constructor of
I.
The return_type is used to compute the resulting type of the whole
match expression and the type of the branches. Most of the time,
when this type is the same as the types of all the term_{i}, the
annotation is not needed^{2}. This
annotation has to be given when the resulting type of the whole match depends on the actual term_{0} matched.
There are specific notations for case analysis on types with one or
two constructors: if / then / else and
let (...) := ...in....
See also: section 2.2.1 for details and examples.
See also: Section 2.2.1 for details and examples.
1.2.14 Recursive functions
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 ith component of a block of functions
defined by mutual wellfounded recursion. It is the local counterpart
of the Fixpoint command. See Section 1.3.4 for more
details. When n=1, the for ident_{i} is omitted.
The expression ``cofix ident_{1} binder_{1} :
type_{1} with ... with ident_{n} binder_{n} : type_{n} for ident_{i}'' denotes the ith component of
a block of terms defined by a mutual guarded corecursion. It is the
local counterpart of the CoFixpoint command. See
Section 1.3.4 for more details. When n=1, the for ident_{i} is omitted.
The association of a single fixpoint and a local
definition have a special syntax: ``let fix f ... := ... in ...'' stands for ``let f :=
fix f ... := ... in ...''. The same
applies for cofixpoints.
1.3 The Vernacular
sentence 
::= 
declaration 

 
definition 

 
inductive 

 
fixpoint 

 
statement [proof] 



declaration 
::= 
declaration_keyword assums . 



declaration_keyword 
::= 
Axiom  Conjecture 

 
Parameter  Parameters 

 
Variable  Variables 

 
Hypothesis  Hypotheses 



assums 
::= 
ident ... ident : term 

 
binder ... binder 



definition 
::= 
Definition ident_with_params := term . 

 
Let ident_with_params := term . 



inductive 
::= 
Inductive ind_body with ... with ind_body . 

 
CoInductive ind_body with ... with ind_body . 



ind_body 
::= 
ident [binderlet ... binderlet] : term := 


[[] ident_with_params  ...  ident_with_params] 



fixpoint 
::= 
Fixpoint fix_body with ... with fix_body . 

 
CoFixpoint cofix_body with ... with cofix_body . 



statement 
::= 
statement_keyword ident [binderlet ... binderlet] : term . 



statement_keyword 
::= 
Theorem  Lemma  Definition 



proof 
::= 
Proof . ... Qed . 

 
Proof . ... Defined . 

 
Proof . ... Admitted . 
Figure 1.3: Syntax of sentences
Figure 1.3 describes The Vernacular which is the
language of commands of Gallina. A sentence of the vernacular
language, like in many natural languages, begins with a capital letter
and ends with a dot.
The different kinds of command are described hereafter. They all suppose
that the terms occurring in the sentences are welltyped.
1.3.1 Declarations
The declaration mechanism allows the user to specify his own basic
objects. Declared objects play the role of axioms or parameters in
mathematics. A declared object is an ident associated to a term. A
declaration is accepted by Coq if and only if this term is a
correct type in the current context of the declaration and ident was
not previously defined in the same module. This term is considered
to be the type, or specification, of the ident.
Axiom ident :term .
This command links term to the name ident as its specification
in the global context. The fact asserted by term is thus assumed as
a postulate.
Error messages: 
ident already exists
Variants: 
Parameter ident :term.
Is equivalent to Axiom ident : term
 Parameter ident_{1}...ident_{n} :term.
Adds n parameters with specification term
 Parameter ( ident_{1,1}...ident_{1,k1} : term_{1} ) ... ( ident_{n,1}...ident_{n,kn} : term_{n} ).
Adds n blocks of parameters with different specifications.
 Conjecture ident :term.
Is equivalent to Axiom ident : term.
Remark: It is possible to replace Parameter by
Parameters.
Variable ident :term.
This command links term to the name ident in the context of the
current section (see Section 2.3 for a description of the section
mechanism). When the current section is closed, name ident will be
unknown and every object using this variable will be explicitly
parameterized (the variable is discharged). Using the Variable command out of any section is equivalent to Axiom.
Error messages: 
ident already exists
Variants: 
Variable ident_{1}...ident_{n} :term.
Links term to names ident_{1}...ident_{n}.
 Variable ( ident_{1,1}...ident_{1,k1} : term_{1} ) ... ( ident_{n,1}...ident_{n,kn} : term_{n} ).
Adds n blocks of variables with different specifications.
 Hypothesis ident :term.
Hypothesis is a synonymous of Variable
Remark: It is possible to replace Variable by
Variables and Hypothesis by Hypotheses.
It is advised to use the keywords Axiom
and Hypothesis
for logical postulates (i.e. when the assertion term is of sort
Prop
), and to use the keywords Parameter
and
Variable
in other cases (corresponding to the declaration of an
abstract mathematical entity).
1.3.2 Definitions
Definitions differ from declarations in allowing to give a name to a
term whereas declarations were just giving a type to a name. That is
to say that the name of a defined object can be replaced at any time
by its definition. This replacement is called
deltaconversion (see
Section 4.3). A defined object is accepted by the system if
and only if the defining term is welltyped in the current context of
the definition. Then the type of the name is the type of term. The
defined name is called a constant and one says
that the constant is added to the
environment.
A formal presentation of constants and environments is given in
Section 4.2.
Definition ident := term.
This command binds the value term to the name ident in the
environment, provided that term is welltyped.
Error messages: 
ident already exists
Variants: 
Definition ident :term_{1} := term_{2}.
It checks that the type of term_{2} is definitionally equal to
term_{1}, and registers ident as being of type term_{1},
and bound to value term_{2}.
 Definition ident binder_{1}...binder_{n}
:term_{1} := term_{2}.
This is equivalent to
Definition ident : forall binder_{1}...binder_{n}, term_{1} := fun binder_{1}...binder_{n} => term_{2} .
Error messages: 
In environment ... the term: term_{2} does not have type
term_{1}.
Actually, it has type term_{3}.
See also: Sections 6.2.4, 6.2.5, 8.5.5
Let ident := term.
This command binds the value term to the name ident in the
environment of the current section. The name ident disappears
when the current section is eventually closed, and, all
persistent objects (such as theorems) defined within the
section and depending on ident are prefixed by the local definition
let ident := term in.
Error messages: 
ident already exists
Variants: 
Let ident : term_{1} := term_{2}.
See also: Sections 2.3 (section mechanism), 6.2.4,
6.2.5 (opaque/transparent constants), 8.5.5
1.3.3 Inductive definitions
We gradually explain simple inductive types, simple
annotated inductive types, simple parametric inductive types,
mutually inductive types. We explain also coinductive types.
Simple inductive types
The definition of a simple inductive type has the following form:
Inductive ident : sort := 

ident_{1} 
: 
type_{1} 
 
... 


 
ident_{n} 
: 
type_{n} 

The name ident is the name of the inductively defined type and
sort is the universes where it lives.
The names ident_{1}, ..., ident_{n}
are the names of its constructors and type_{1}, ...,
type_{n} their respective types. The types of the constructors have
to satisfy a positivity condition (see Section 4.5.3)
for ident. This condition ensures the soundness of the inductive
definition. If this is the case, the constants ident,
ident_{1}, ..., ident_{n} are added to the environment with
their respective types. Accordingly to the universe where
the inductive type lives (e.g. its type sort), Coq provides a
number of destructors for ident. Destructors are named
ident_ind, ident_rec or ident_rect which
respectively correspond to elimination principles on Prop, Set and Type. The type of the destructors expresses structural
induction/recursion principles over objects of ident. We give below
two examples of the use of the Inductive definitions.
The set of natural numbers is defined as:
Coq < Inductive nat : Set :=
Coq <  O : nat
Coq <  S : nat > nat.
nat is defined
nat_rect is defined
nat_ind is defined
nat_rec is defined
The type nat is defined as the least Set
containing O and closed by the S constructor. The constants nat,
O and S are added to the environment.
Now let us have a look at the elimination principles. They are three :
nat_ind, nat_rec and nat_rect. The type of nat_ind is:
Coq < 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 to prove some universal property of natural numbers (forall n:nat, P n) by induction on n.
The types of nat_rec and nat_rect are similar, except
that they pertain to (P:nat>Set) and (P:nat>Type)
respectively . They correspond to primitive induction principles
(allowing dependent types) respectively over sorts Set
and
Type
. The constant ident_ind is always provided,
whereas ident_rec and ident_rect can be impossible
to derive (for example, when ident is a proposition).
Variants: 
Coq < Inductive nat : Set := O  S (_:nat).
In the case where inductive types have no annotations (next section
gives an example of such annotations), the positivity condition
implies that a constructor can be defined by only giving the type of
its arguments.
Simple annotated inductive types
In an annotated 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.
As an example of annotated inductive types, let us define the
even predicate:
Coq < Inductive even : nat > Prop :=
Coq <  even_0 : even O
Coq <  even_SS : forall n:nat, even n > even (S (S n)).
even is defined
even_ind 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:
Coq < 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 it asserts that the natural numbers
satisfying the predicate even are exactly the 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 indeed analogous to the structural
induction principle we got for nat.
Error messages: 
Non strictly positive occurrence of ident in type
 The conclusion of type is not valid; it must be
built from ident
Parameterized inductive types
Inductive types may be parameterized. Parameters differ from inductive
type annotations in the fact that recursive invokations of inductive
types must always be done with the same values of parameters as its
specification.
The general scheme is:
Inductive ident binder_{1}...binder_{k} : term :=
ident_{1}: term_{1}  ...  ident_{n}: term_{n}
.
A typical example is the definition of polymorphic lists:
Coq < Inductive list (A:Set) : Set :=
Coq <  nil : list A
Coq <  cons : A > list A > list A.
Note that in the type of nil and cons, we write (list A) and not just list.
The constants nil and
cons will have respectively types:
Coq < Check nil.
nil
: forall A : Set, list A
Coq < Check cons.
cons
: forall A : Set, A > list A > list A
Types of destructors are also quantified with (A:Set).
Variants: 
Coq < Inductive list (A:Set) : Set := nil  cons (_:A) (_:list A).
This is an alternative definition of lists where we specify the
arguments of the constructors rather than their full type.
Error messages: 
The numth argument of ident must be ident' in type
See also: Sections 4.5 and 4.
Mutually defined inductive types
The definition of a block of mutually inductive types has the form:
Inductive ident_{1} : type_{1} := 

ident_{1}^{1} 
: 
type_{1}^{1} 
 
... 


 
ident_{n1}^{1} 
: 
type_{n1}^{1} 

with 
... 
with ident_{m} : type_{m} := 

ident_{1}^{m} 
: 
type_{1}^{m} 
 
... 
 
ident_{nm}^{m} 
: 
type_{nm}^{m}. 

It has the same semantics as the above Inductive
definition for each ident_{1}, ..., ident_{m}. All names
ident_{1}, ..., ident_{m} and ident_{1}^{1}, ...,
ident_{nm}^{m} are simultaneously added to the environment. Then
welltyping of constructors can be checked. Each one of the
ident_{1}, ..., ident_{m} can be used on its own.
It is also possible to parameterize these inductive definitions.
However, parameters correspond to a local
context in which the whole set of inductive declarations is done. For
this reason, the parameters must be strictly the same for each
inductive types The extended syntax is:
Inductive ident_{1} params : type_{1} :=
ident_{1}^{1} : type_{1}^{1}
 ..
 ident_{n1}^{1} : type_{n1}^{1}
with
..
with ident_{m} params : type_{m} :=
ident_{1}^{m} : type_{1}^{m}
 ..
 ident_{nm}^{m} : type_{nm}^{m}.
Example: The typical example of a mutual inductive data type is the one for
trees and forests. We assume given two types A and B as variables.
It can be declared the following way.
Coq < Variables A B : Set.
Coq < Inductive tree : Set :=
Coq < node : A > forest > tree
Coq < with forest : Set :=
Coq <  leaf : B > forest
Coq <  cons : tree > forest > forest.
This declaration generates automatically six induction
principles. They are respectively
called tree_rec, tree_ind, tree_rect, forest_rec, forest_ind, forest_rect. These ones are not the most general ones but are
just the induction principles corresponding to each inductive part
seen as a single inductive definition.
To illustrate this point on our example, we give the types of tree_rec and forest_rec.
Coq < Check tree_rec.
tree_rec
: forall P : tree > Set,
(forall (a : A) (f : forest), P (node a f)) > forall t : tree, P t
Coq < 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 f1 : forest, P f1
Assume we want to parameterize our mutual inductive definitions with
the two type variables A and B, the declaration should be done the
following way:
Coq < Inductive tree (A B:Set) : Set :=
Coq < node : A > forest A B > tree A B
Coq < with forest (A B:Set) : Set :=
Coq <  leaf : B > forest A B
Coq <  cons : tree A B > forest A B > forest A B.
Assume we define an inductive definition inside a section. 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: Section 2.3
Coinductive types
The objects of an inductive type are wellfounded with respect to the
constructors of the type. In other words, such objects contain only a
finite number constructors. Coinductive types arise from
relaxing this condition, and admitting types whose objects contain an
infinity of constructors. Infinite objects are introduced by a
nonending (but effective) process of construction, defined in terms
of the constructors of the type.
An example of a coinductive type is the type of infinite sequences of
natural numbers, usually called streams. It can be introduced in Coq
using the CoInductive command:
Coq < CoInductive Stream : Set :=
Coq < Seq : nat > Stream > Stream.
Stream is defined
The syntax of this command is the same as the command Inductive
(cf. Section 1.3.3). Notice that no
principle of induction is derived from the definition of a
coinductive type, since such principles only make sense for inductive
ones. For coinductive ones, the only elimination principle is case
analysis. For example, the usual destructors on streams
hd:Stream>nat and tl:Str>Str can be defined as
follows:
Coq < Definition hd (x:Stream) := let (a,s) := x in a.
hd is defined
Coq < Definition tl (x:Stream) := let (a,s) := x in s.
tl is defined
Definition of coinductive predicates and blocks of mutually
coinductive definitions are also allowed. An example of a
coinductive predicate is the extensional equality on streams:
Coq < CoInductive EqSt : Stream > Stream > Prop :=
Coq < eqst :
Coq < forall s1 s2:Stream,
Coq < hd s1 = hd s2 > EqSt (tl s1) (tl s2) > EqSt s1 s2.
EqSt is defined
In order to prove the extensionally equality of two streams s_{1} and
s_{2} we have to construct and infinite proof of equality, that is,
an infinite object of type (EqSt s_{1} s_{2}). We will see
how to introduce infinite objects in Section 1.3.4.
1.3.4 Definition of recursive functions
Fixpoint ident params {struct
ident_{0} } : type_{0} := term_{0}
This command allows to define inductive objects using a fixed point
construction. The meaning of this declaration is to define ident
a recursive function with arguments specified by
binder_{1}...binder_{n} such that ident applied to
arguments corresponding to these binders has type type_{0}, and is
equivalent to the expression term_{0}. The type of the ident is
consequently forall params , type_{0}
and the value is equivalent to fun params => term_{0}.
To be accepted, a Fixpoint definition has to satisfy some
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 is to let the user tell the system which argument decreases
along the recursive calls. This annotation may be left implicit for
fixpoints with one argument. For instance, one can define the addition
function as :
Coq < Fixpoint add (n m:nat) {struct n} : nat :=
Coq < match n with
Coq <  O => m
Coq <  S p => S (add p m)
Coq < end.
add is recursively defined
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 detail in Section 4.5.4. 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:
Coq < Fixpoint wrongplus (n m:nat) {struct n} : nat :=
Coq < match m with
Coq <  O => n
Coq <  S p => S (wrongplus n p)
Coq < end.
Coq < Coq < Error:
Recursive definition of wrongplus is illformed.
In environment
n : nat
m : nat
p : nat
Recursive call to wrongplus has principal argument equal to
"n"
instead of a subterm of n
because the declared decreasing argument n actually does not
decrease in the recursive call. The function computing the addition
over the second argument should rather be written:
Coq < Fixpoint plus (n m:nat) {struct m} : nat :=
Coq < match m with
Coq <  O => n
Coq <  S p => S (plus n p)
Coq < end.
The ordinary match operation on natural numbers can be mimicked in the
following way.
Coq < Fixpoint nat_match
Coq < (C:Set) (f0:C) (fS:nat > C > C) (n:nat) {struct n} : C :=
Coq < match n with
Coq <  O => f0
Coq <  S p => fS p (nat_match C f0 fS p)
Coq < end.
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.
Coq < Fixpoint mod2 (n:nat) : nat :=
Coq < match n with
Coq <  O => O
Coq <  S p => match p with
Coq <  O => S O
Coq <  S q => mod2 q
Coq < end
Coq < end.
In order to keep the strong normalisation 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.
The Fixpoint construction enjoys also the with extension
to define functions over mutually defined inductive types or more
generally any mutually recursive definitions.
Variants: 
Fixpoint ident_{1} params_{1} :type_{1} := term_{1}
with ...
with ident_{m} params_{m} :type_{m} := type_{m}
Allows to define simultaneously ident_{1}, ...,
ident_{m}.
Example: The size of trees and forests can be defined the following way:
Coq < Fixpoint tree_size (t:tree) : nat :=
Coq < match t with
Coq <  node a f => S (forest_size f)
Coq < end
Coq < with forest_size (f:forest) : nat :=
Coq < match f with
Coq <  leaf b => 1
Coq <  cons t f' => (tree_size t + forest_size f')
Coq < end.
A generic command Scheme is useful to build automatically various
mutual induction principles. It is described in Section 8.13.
CoFixpoint ident : type_{0} := term_{0}.
The CoFixpoint command introduces a method for constructing an
infinite object of a coinductive type. For example, the stream
containing all natural numbers can be introduced applying the
following method to the number O (see
Section 1.3.3 for the definition of Stream,
hd and tl):
Coq < CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
from is corecursively defined
Oppositely to recursive ones, there is no decreasing argument in a
corecursive definition. To be admissible, a method of construction
must provide at least one extra constructor of the infinite object for
each iteration. A syntactical guard condition is imposed on
corecursive definitions in order to ensure this: each recursive call
in the definition must be protected by at least one constructor, and
only by constructors. That is the case in the former definition, where
the single recursive call of from is guarded by an
application of Seq. On the contrary, the following recursive
function does not satisfy the guard condition:
Coq < CoFixpoint filter (p:nat > bool) (s:Stream) : Stream :=
Coq < if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
Coq < Coq < Error:
Recursive definition of filter is illformed.
In environment
filter : (nat > bool) > Stream > Stream
p : nat > bool
s : Stream
unguarded recursive call in "filter p (tl s)"
The elimination of corecursive definition is done lazily, i.e. the
definition is expanded only when it occurs at the head of an
application which is the argument of a case analysis expression. In
any other context, it is considered as a canonical expression which is
completely evaluated. We can test this using the command
Eval, which computes the normal forms of a term:
Coq < Eval compute in (from 0).
= (cofix from (n : nat) : Stream := Seq n (from (S n))) 0
: Stream
Coq < Eval compute in (hd (from 0)).
= 0
: nat
Coq < Eval compute in (tl (from 0)).
= (cofix from (n : nat) : Stream := Seq n (from (S n))) 1
: Stream
Variants: 
CoFixpoint ident_{1} params :type_{1} :=
term_{1}
As for most constructions, arguments of cofixpoints
expressions can be introduced before the := sign.
 CoFixpoint ident_{1} :type_{1} := term_{1}
with
...
with ident_{m} : type_{m} := term_{m}
As in the Fixpoint command (cf. Section 1.3.4), it
is possible to introduce a block of mutually dependent methods.
1.3.5 Statement and proofs
A statement claims a goal of which the proof is then interactively done
using tactics. More on the proof editing mode, statements and proofs can be
found in chapter 7.
Theorem ident : type.
This command binds type to the name ident in the
environment, provided that a proof of type is next given.
After a statement, Coq needs a proof.
Variants: 
Lemma ident : type.
It is a synonymous of Theorem
 Remark ident : type.
It is a synonymous of Theorem
 Fact ident : type.
It is a synonymous of Theorem
 Definition ident : type.
Allow to define a term of type type using the proof editing mode. It
behaves as Theorem but is intended for the interactive
definition of expression which computational behaviour will be used by
further commands.
See also: 6.2.5 and 8.5.5.
Proof . ...Qed .
A proof starts by the keyword Proof. Then Coq enters the
proof editing mode until the proof is completed. The proof editing
mode essentially contains tactics that are described in chapter
8. Besides tactics, there are commands to manage the proof
editing mode. They are described in chapter 7. When
the proof is completed it should be validated and put in the
environment using the keyword Qed.
Error message: 
ident already exists
Remarks: 
Several statements can be simultaneously opened.
 Not only other statements but any vernacular command can be given
within the proof editing mode. In this case, the command is
understood as if it would have been given before the statements still to be
proved.
 Proof is recommended but can currently be omitted. On the
opposite, Qed (or Defined, see below) is mandatory to validate a proof.
 Proofs ended by Qed are declared opaque (see 6.2.4)
and cannot be unfolded by conversion tactics (see 8.5).
To be able to unfold a proof, you should end the proof by Defined
(see below).
Variants: 
Proof . ...Defined .
Same as Proof . ...Qed . but the proof is
then declared transparent (see 6.2.5), which means it
can be unfolded in conversion tactics (see 8.5).
 Proof . ...Save.
Same as Proof . ...Qed .
 Goal type...Save ident
Same as Lemma ident: type...Save.
This is intended to be used in the interactive mode. Conversely to named
lemmas, anonymous goals cannot be nested.
 Proof. ...Admitted.
Turns the current conjecture into an axiom and exits editing of
current proof.
 1
 This is similar to the
expression ``entry { sep entry }'' in
standard BNF, or ``entry ( sep entry )*'' in
the syntax of regular expressions.
 2
 except if no equation is given, to
match the term in an empty type, e.g. the type False