The Gallina specification language¶
This chapter describes Gallina, the specification language of Coq. It allows developing 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 Terms. The language of commands, called The Vernacular is described in Section The Vernacular.
In Coq, logical objects are typed to ensure their logical correctness. The rules implemented by the typing algorithm are described in Chapter Calculus of Inductive Constructions.
About the grammars in the manual¶
Grammars are presented in BackusNaur form (BNF). Terminal symbols are
set in black 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
”.
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 ∣ _ ∣ unicodeletter subsequent_letter ::= a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ' ∣ unicodeletter ∣ unicodeidpart ident ::=
first_letter
[subsequent_letter
…subsequent_letter
] access_ident ::= .ident
All characters are meaningful. In particular, identifiers are casesensitive. The entry
unicodeletter
nonexhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letterlike symbols, hyphens, nonbreaking space, … The entryunicodeidpart
nonexhaustively includes symbols for prime letters and subscripts.Access identifiers, written
access_ident
, are identifiers prefixed by.
(dot) without blank. They are used in the syntax of qualified identifiers. Numerals
Numerals are sequences of digits with a potential fractional part and exponent. Integers are numerals without fractional nor exponent part and optionally preceded by a minus sign. Underscores
_
can be used as comments in numerals.digit ::= 0..9 num ::=
digit
…digit
integer ::= []num
dot ::= . exp ::= e  E sign ::= +   numeral ::=num
[dot
num
][exp
[sign
]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 isstring
.  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 return SProp Prop Set Type then 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.
Terms¶
Syntax of terms¶
The following grammars describe the basic syntax of the terms of the Calculus of Inductive Constructions (also called Cic). The formal presentation of Cic is given in Chapter Calculus of Inductive Constructions. Extensions of this syntax are given in Chapter Extensions of Gallina. How to customize the syntax is described in Chapter Syntax extensions and interpretation scopes.
term ::= forallbinders
,term
funbinders
=>term
fixfix_bodies
cofixcofix_bodies
letident
[binders
] [:term
] :=term
interm
let fixfix_body
interm
let cofixcofix_body
interm
let ( [name
, … ,name
] ) [dep_ret_type
] :=term
interm
let 'pattern
[interm
] :=term
[return_type
] interm
ifterm
[dep_ret_type
] thenterm
elseterm
term
:term
term
<:term
term
:>term
>term
term
arg
…arg
@qualid
[term
…term
]term
%ident
matchmatch_item
, … ,match_item
[return_type
] with [[]equation
 … equation
] endqualid
sort
num
_ (term
) arg ::=term
(ident
:=term
) binders ::=binder
…binder
binder ::=name
(name
…name
:term
) (name
[:term
] :=term
) 'pattern
name ::=ident
 _ qualid ::=ident
qualid
access_ident
sort ::= SProp  Prop  Set  Type fix_bodies ::=fix_body
fix_body
withfix_body
with … withfix_body
forident
cofix_bodies ::=cofix_body
cofix_body
withcofix_body
with … withcofix_body
forident
fix_body ::=ident
binders
[annotation
] [:term
] :=term
cofix_body ::=ident
[binders
] [:term
] :=term
annotation ::= { structident
} match_item ::=term
[asname
] [inqualid
[pattern
…pattern
]] dep_ret_type ::= [asname
]return_type
return_type ::= returnterm
equation ::=mult_pattern
 … mult_pattern
=>term
mult_pattern ::=pattern
, … ,pattern
pattern ::=qualid
pattern
…pattern
@qualid
pattern
…pattern
pattern
asident
pattern
%ident
qualid
_num
(or_pattern
, … ,or_pattern
) or_pattern ::=pattern
 … pattern
Types¶
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
.
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,
while qualified identifiers do not.
Numerals¶
Numerals have no definite semantics in the calculus. They are mere notations that can be bound to objects through the notation mechanism (see Chapter Syntax extensions and interpretation scopes for details). Initially, numerals are bound to Peano’s representation of natural numbers (see Datatypes).
Note
Negative integers are not at the same level as num
, for this
would make precedence unnatural.
Sorts¶
There are four sorts SProp
, Prop
, Set
and Type
.
SProp
is the universe of definitionally irrelevant propositions (also called strict propositions).Prop
is the universe of logical propositions. The logical propositions themselves are typing the proofs. We denote propositions byform
. This constitutes a semantic subclass of the syntactic classterm
.Set
is the universe of program types or specifications. The specifications themselves are typing the programs. We denote specifications byspecif
. This constitutes a semantic subclass of the syntactic classterm
.Type
is the type of sorts.
More on sorts can be found in Section Sorts.
Binders¶
Various constructions such as fun
, forall
, fix
and cofix
bind variables. A binding is represented by an identifier. If the binding
variable is not used in the expression, the identifier can be replaced by the
symbol _
. When the type of a bound variable cannot be synthesized by the
system, it can be specified with the notation (ident : type)
. There is also
a notation for a sequence of binding variables sharing the same type:
(ident+ : type)
. A
binder can also be any pattern prefixed by a quote, e.g. '(x,y)
.
Some constructions allow the binding of a variable to value. This is
called a “letbinder”. The entry binder
of the grammar accepts
either an assumption binder as defined above or a letbinder. The notation in
the latter case is (ident := term)
. In a letbinder, only one
variable can be introduced at the same time. It is also possible to give
the type of the variable as follows:
(ident : type := term)
.
Lists of binder
are allowed. In the case of fun
and forall
,
it is intended that at least one binder of the list is an assumption otherwise
fun and forall gets identical. Moreover, parentheses can be omitted in
the case of a single sequence of bindings sharing the same type (e.g.:
fun (x y z : A) => t
can be shortened in fun x y z : A => t
).
Abstractions¶
The expression fun ident : type => term
defines the
abstraction of the variable ident
, of type type
, over the term
term
. It denotes a function of the variable ident
that evaluates to
the expression term
(e.g. fun x : A => x
denotes the identity
function on type A
). The keyword fun
can be followed by several
binders as given in Section Binders. Functions over
several variables are equivalent to an iteration of onevariable
functions. For instance the expression
“fun ident
\(_{1}\) … ident
\(_{n}\)
: type
=> term
”
denotes the same function as “ fun ident
\(_{1}\) : type
=> …
fun ident
\(_{n}\) : type
=> term
”. If
a letbinder occurs in
the list of binders, it is expanded to a letin definition (see
Section Letin definitions).
Products¶
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 products
over several variables are equivalent to an iteration of onevariable
products. Note that term
is intended to be a type.
If the variable ident
occurs in term
, the product is called
dependent product. The intention behind a dependent product
forall x : A, B
is twofold. It denotes either
the universal quantification of the variable x
of type A
in the proposition B
or the functional dependent product from
A
to B
(a construction usually written
\(\Pi_{x:A}.B\) in set theory).
Non dependent product types have a special notation: A > B
stands for
forall _ : A, B
. The non dependent product is used both to denote
the propositional implication and function types.
Applications¶
The expression term
\(_0\) term
\(_1\) denotes the
application of 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.
The notation (ident := term)
for arguments is used for making
explicit the value of implicit arguments (see
Section Explicit applications).
Type cast¶
The expression term : type
is a type cast expression. It enforces
the type of term
to be type
.
term <: type
locally sets up the virtual machine for checking that
term
has type type
.
term <<: type
uses native compilation for checking that term
has type type
.
Inferable subterms¶
Expressions often contain redundant pieces of information. Subterms that can be
automatically inferred by Coq can be replaced by the symbol _
and Coq will
guess the missing piece of information.
Letin definitions¶
let ident := term in term’
denotes the local binding of term
to the variable
ident
in term
’. There is a syntactic sugar for letin
definition of functions: let ident binder+ := term in term’
stands for let ident := fun binder+ => term in term’
.
Definition by case analysis¶
Objects of inductive types can be destructured by a caseanalysis construction called pattern matching expression. A pattern matching expression is used to analyze the structure of an inductive object and to apply specific treatments accordingly.
This paragraph describes the basic form of pattern matching. See
Section Multiple and nested pattern matching and Chapter Extended pattern matching for the description
of the general form. The basic form of pattern matching is characterized
by a single match_item
expression, a mult_pattern
restricted to a
single pattern
and pattern
restricted to the form
qualid ident*
.
The expression match "term
\(_0\) return_type
with
pattern
\(_1\) => term
\(_1\) \(\) … \(\)
pattern
\(_n\) => term
\(_n\) end" denotes a
pattern matching over the term term
\(_0\) (expected to be
of an inductive type \(I\)). The terms term
\(_1\)…term
\(_n\) are the branches of the pattern matching
expression. Each of pattern
\(_i\) has a form qualid
ident
where qualid
must denote a constructor. There should be
exactly one branch for every constructor of \(I\).
The return_type
expresses the type returned by the whole match
expression. There are several cases. In the non dependent case, all
branches have the same type, and the return_type
is the common type of
branches. In this case, return_type
can usually be omitted as it can be
inferred from the type of the branches [2].
In the dependent case, there are three subcases. In the first subcase,
the type in each branch may depend on the exact value being matched in
the branch. In this case, the whole pattern matching itself depends on
the term being matched. This dependency of the term being matched in the
return type is expressed with an “as ident
” clause where ident
is dependent in the return type. For instance, in the following example:
 Inductive bool : Type := true : bool  false : bool.
 bool is defined bool_rect is defined bool_ind is defined bool_rec is defined
 Inductive eq (A:Type) (x:A) : A > Prop := eq_refl : eq A x x.
 eq is defined eq_rect is defined eq_ind is defined eq_rec is defined
 Inductive or (A:Prop) (B:Prop) : Prop :=  or_introl : A > or A B  or_intror : B > or A B.
 or is defined or_ind is defined
 Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b as x return or (eq bool x true) (eq bool x false) with  true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true)  false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) end.
 bool_case is defined
the branches have respective types "or (eq bool true true) (eq bool true false)
"
and "or (eq bool false true) (eq bool false false)
" while the whole
pattern matching expression has type "or (eq bool b true) (eq bool b false)
",
the identifier b
being used to represent the dependency.
Note
When the term being matched is a variable, the as
clause can be
omitted and the term being matched can serve itself as binding name in
the return type. For instance, the following alternative definition is
accepted and has the same meaning as the previous one.
 Reset bool_case.
 Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b return or (eq bool b true) (eq bool b false) with  true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true)  false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) end.
 bool_case is defined
The second subcase is only relevant for annotated inductive types such
as the equality predicate (see Section Equality),
the order predicate on natural numbers or the type of lists of a given
length (see Section Matching objects of dependent types). In this configuration, the
type of each branch can depend on the type dependencies specific to the
branch and the whole pattern matching expression has a type determined
by the specific dependencies in the type of the term being matched. This
dependency of the return type in the annotations of the inductive type
is expressed using a “in
\(I\) _ … _
pattern
\(_1\) …
pattern
\(_n\)” clause, where
 \(I\) is the inductive type of the term being matched;
 the
_
are matching the parameters of the inductive type: the return type is not dependent on them.  the
pattern
\(_i\) are matching the annotations of the inductive type: the return type is dependent on them  in the basic case which we describe below, each
pattern
\(_i\) is a nameident
\(_i\); see Patterns in in for the general case
For instance, in the following example:
 Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with  eq_refl _ _ => eq_refl A x end.
 eq_sym is defined
the type of the branch is eq A x x
because the third argument of
eq
is x
in the type of the pattern eq_refl
. On the contrary, the
type of the whole pattern matching expression has type eq A y x
because the
third argument of eq is y in the type of H. This dependency of the case analysis
in the third argument of eq
is expressed by the identifier z
in the
return type.
Finally, the third subcase is a combination of the first and second
subcase. In particular, it only applies to pattern matching on terms in
a type with annotations. For this third subcase, both the clauses as
and
in
are available.
There are specific notations for case analysis on types with one or two
constructors: if … then … else …
and let (…,…) := … in …
(see
Sections Patternmatching on boolean values: the if expression and Irrefutable patterns: the destructuring let variants).
Recursive functions¶
The expression “fix
ident
\(_1\) binder
\(_1\) :
type
\(_1\) :=
term
\(_1\) with … with
ident
\(_n\) binder
\(_n\) : type
\(_n\)
:=
term
\(_n\) for
ident
\(_i\)” denotes the
\(i\)th component of a block of functions defined by mutual structural
recursion. It is the local counterpart of the Fixpoint
command. When
\(n=1\), the “for
ident
\(_i\)” clause is omitted.
The expression “cofix
ident
\(_1\) binder
\(_1\) :
type
\(_1\) with … with
ident
\(_n\) binder
\(_n\)
: type
\(_n\) for
ident
\(_i\)” denotes the
\(i\)th component of a block of terms defined by a mutual guarded
corecursion. It is the local counterpart of the CoFixpoint
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 binders := term in
stands for
let ident := fix ident binders := term in
. The same applies for cofixpoints.
The Vernacular¶
decoratedsentence ::= [decoration
…decoration
]sentence
sentence ::=assumption
definition
inductive
fixpoint
assertion
proof
assumption ::=assumption_keyword
assums
. assumption_keyword ::= Axiom  Conjecture Parameter  Parameters Variable  Variables Hypothesis  Hypotheses assums ::=ident
…ident
:term
(ident
…ident
:term
) … (ident
…ident
:term
) definition ::= [Local] Definitionident
[binders
] [:term
] :=term
. Letident
[binders
] [:term
] :=term
. inductive ::= Inductiveind_body
with … withind_body
. CoInductiveind_body
with … withind_body
. ind_body ::=ident
[binders
] :term
:= [[]ident
[binders
] [:term
]  … ident
[binders
] [:term
]] fixpoint ::= Fixpointfix_body
with … withfix_body
. CoFixpointcofix_body
with … withcofix_body
. assertion ::=assertion_keyword
ident
[binders
] :term
. assertion_keyword ::= Theorem  Lemma Remark  Fact Corollary  Property  Proposition Definition  Example proof ::= Proof . … Qed . Proof . … Defined . Proof . … Admitted . decoration ::= #[attributes
] attributes ::= [attribute
, … ,attribute
] attribute ::=ident
ident
=string
ident
(attributes
)
This grammar 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.
Sentences may be decorated with socalled attributes, which are described in the corresponding section (Attributes).
The different kinds of command are described hereafter. They all suppose that the terms occurring in the sentences are welltyped.
Assumptions¶
Assumptions extend the environment with axioms, parameters, hypotheses
or variables. An assumption binds an ident
to a type
. It is accepted
by Coq if and only if this type
is a correct type in the environment
preexisting the declaration and if ident
was not previously defined in
the same module. This type
is considered to be the type (or
specification, or statement) assumed by ident
and we say that ident
has type type
.

Command
Parameter ident : type
¶ This command links
type
to the nameident
as its specification in the global context. The fact asserted bytype
is thus assumed as a postulate.
Variant
Local Parameter ( ident+ : type )+
¶ Such parameters are never made accessible through their unqualified name by
Import
and its variants. You have to explicitly give their fully qualified name to refer to them.

Variant
Local? Parameters ( ident+ : type )+
¶ 
Variant
Local? Axiom ( ident+ : type )+
¶ 
Variant
Local? Axioms ( ident+ : type )+
¶ 
Variant
Local? Conjecture ( ident+ : type )+
¶ 
Variant
Local? Conjectures ( ident+ : type )+
¶ These variants are synonyms of
Local? Parameter ( ident+ : type )+
.

Variant
Variable ( ident+ : type )+
¶ 
Variant
Variables ( ident+ : type )+
¶ 
Variant
Hypothesis ( ident+ : type )+
¶ 
Variant
Hypotheses ( ident+ : type )+
¶ Outside of any section, these variants are synonyms of
Local Parameter ( ident+ : type )+
. For their meaning inside a section, seeVariable
in Section mechanism.
Warning
ident is declared as a local axiom [localdeclaration,scope]
¶ Warning generated when using
Variable
instead ofLocal Parameter
.

Warning

Variant
Note
It is advised to use the commands Axiom
, Conjecture
and
Hypothesis
(and their plural forms) for logical postulates (i.e. when
the assertion type
is of sort Prop
), and to use the commands
Parameter
and Variable
(and their plural forms) in other cases
(corresponding to the declaration of an abstract mathematical entity).
See also
Section Section mechanism.
Definitions¶
Definitions extend the environment with associations of names to terms. A definition can be seen as a way to give a meaning to a name or as a way to abbreviate a term. In any case, the name can later be replaced at any time by its definition.
The operation of unfolding a name into its definition is called \(\delta\)conversion (see Section δreduction). A definition is accepted by the system if and only if the defined term is welltyped in the current context of the definition and if the name is not already used. The name defined by the definition is called a constant and the term it refers to is its body. A definition has a type which is the type of its body.
A formal presentation of constants and environments is given in Section Typing rules.

Command
Definition ident := term
¶ This command binds
term
to the nameident
in the environment, provided thatterm
is welltyped.
Variant
Definition ident : type := term
This variant checks that the type of
term
is definitionally equal totype
, and registersident
as being of typetype
, and bound to valueterm
.

Variant
Definition ident binders : type? := term
This is equivalent to
Definition ident : forall binders, type := fun binders => term
.

Variant
Local Definition ident binders? : type? := term
¶ Such definitions are never made accessible through their unqualified name by
Import
and its variants. You have to explicitly give their fully qualified name to refer to them.

Variant
Let ident := term
¶ Outside of any section, this variant is a synonym of
Local Definition ident := term
. For its meaning inside a section, seeLet
in Section mechanism.
Warning
ident is declared as a local definition [localdeclaration,scope]
¶ Warning generated when using
Let
instead ofLocal Definition
.

Warning

Variant
See also
Section Section mechanism, commands Opaque
,
Transparent
, and tactic unfold
.
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¶

Command
Inductive ident : sort? := ? ident : type  ident : type*
¶ This command defines a simple inductive type and its constructors. The first
ident
is the name of the inductively defined type andsort
is the universe where it lives. The nextident
s are the names of its constructors andtype
their respective types. Depending on the universe where the inductive typeident
lives (e.g. its typesort
), Coq provides a number of destructors. Destructors are namedident
_sind
,:token:ident
_ind
,ident
_rec
orident
_rect
which respectively correspond to elimination principles onSProp
,Prop
,Set
andType
. The type of the destructors expresses structural induction/recursion principles over objects of typeident
. The constantident
_ind
is always provided, whereasident
_rec
andident
_rect
can be impossible to derive (for example, whenident
is a proposition).
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.

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 (orident
applied to arguments in the case of annotated inductive types — cf. next section).
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
The type nat is defined as the least
Set
containingO
and closed by theS
constructor. The namesnat
,O
andS
are added to the environment.Now let us have a look at the elimination principles. They are three of them:
nat_ind
,nat_rec
andnat_rect
. The type ofnat_ind
is: Check nat_ind.
 nat_ind : forall P : nat > Prop, P O > (forall n : nat, P n > P (S n)) > forall n : nat, P n
This is the well known structural induction principle over natural numbers, i.e. the secondorder form of Peano’s induction principle. It allows proving some universal property of natural numbers (
forall n:nat, P n
) by induction onn
.The types of
nat_rec
andnat_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 sortsSet
andType
.
Variant
Inductive ident : sort? := ? ident binders? : type?*
Constructors
ident
s can come withbinders
in which case, the actual type of the constructor isforall binders, type
.In the case where inductive types have no annotations (next section gives an example of such annotations), a constructor can be defined by only giving the type of its arguments.
Example
 Reset nat.
 Inductive nat : Set := O  S (_:nat).
 nat is defined nat_rect is defined nat_ind is defined nat_rec is defined

Error
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.
Example
As an example of annotated 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
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 it 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 indeed analogous to the
structural induction principle we got for nat
.
Parameterized inductive types¶

Variant
Inductive ident binders : type? := ? ident : type  ident : type*
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 annotation, we use a context of parameters which arebinders
shared by all the constructors of the definition.Parameters differ from inductive type annotations in the fact that the conclusion of each type of constructor invoke the inductive type with the same values of parameters as 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
In the type of
nil
andcons
, we write(list A)
and not justlist
. The constructorsnil
andcons
will have respectively types: Check nil.
 nil : forall A : Set, list A
 Check cons.
 cons : forall A : Set, A > list A > list A
Types of destructors are also quantified with
(A:Set)
.Once again, it is possible to specify only the type of the arguments of the constructors, and to omit the type of the conclusion:
 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
Note
It is possible in the type of a constructor, to invoke recursively 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
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
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: Last occurrence of "listw" must have "A" as 1st argument in "listw (A * A)%type".
because the conclusion of the type of constructors should be
listw A
in both cases.A parameterized inductive definition can be defined using annotations 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 option 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
This behavior is essentially equivalent to starting a new section and using
Context
to give the uniform parameters, like so (cf. Section mechanism): 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
 End list3.
See also
Section Inductive Definitions and the induction
tactic.
Variants¶

Command
Variant ident binders : type? := ? ident : type  ident : type*
¶ The
Variant
command is identical to theInductive
command, except that it disallows recursive definition of types (for instance, lists cannot be defined usingVariant
). No induction scheme is generated for this variant, unless optionNonrecursive Elimination Schemes
is on.
Mutually defined inductive types¶

Variant
Inductive ident : type? := ? ident : type* with ? ident : type?**
This variant allows defining a block of mutually inductive types. It has the same semantics as the above
Inductive
definition for eachident
. Allident
are simultaneously added to the environment. Then welltyping of constructors can be checked. Each one of theident
can be used on its own.
Variant
Inductive ident binders : type? := ? ident : type* with ? ident binders : type?**
In this variant, the inductive definitions are parameterized with
binders
. 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.

Variant
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.
 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 forest_rect is defined forest_ind is defined forest_rec is defined
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
.
 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) (f0 : forest), P f0 > P (cons t f0)) > 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:
Assume we define an inductive definition inside a section (cf. Section mechanism). When the section is closed, the variables declared in the section and occurring free in the declaration are added as parameters to the inductive definition.
See also
A generic command Scheme
is useful to build automatically various
mutual induction principles.
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 of 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.

Command
CoInductive ident binders : type? := ? ident : type  ident : type*
¶ This command introduces a coinductive type. The syntax of the command is the same as the command
Inductive
. No principle of induction is derived from the definition of a coinductive type, since such principles only make sense for inductive types. For coinductive types, the only elimination principle is case analysis.
Example
An example of a coinductive type is the type of infinite sequences of natural numbers, usually called streams.
 CoInductive Stream : Set := Seq : nat > Stream > Stream.
 Stream is defined
The usual destructors on streams hd:Stream>nat
and tl:Str>Str
can be defined as follows:
 Definition hd (x:Stream) := let (a,s) := x in a.
 hd is defined
 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.
Example
An example of a coinductive predicate is the extensional equality on streams:
 CoInductive EqSt : Stream > Stream > Prop := eqst : forall s1 s2:Stream, hd s1 = hd s2 > EqSt (tl s1) (tl s2) > EqSt s1 s2.
 EqSt is defined
In order to prove the extensional equality of two streams s1
and s2
we have to construct an infinite proof of equality, that is, an infinite
object of type (EqSt s1 s2)
. We will see how to introduce infinite
objects in Section Definitions of recursive objects in coinductive types.
Caveat¶
The ability to define coinductive types by constructors, hereafter called positive coinductive types, is known to break subject reduction. The story is a bit long: this is due to dependent patternmatching which implies propositional ηequality, which itself would require full ηconversion for subject reduction to hold, but full ηconversion is not acceptable as it would make typechecking undecidable.
Since the introduction of primitive records in Coq 8.5, an alternative presentation is available, called negative coinductive types. This consists in defining a coinductive type as a primitive record type through its projections. Such a technique is akin to the copattern style that can be found in e.g. Agda, and preserves subject reduction.
The above example can be rewritten in the following way.
 Reset Stream.
 Set Primitive Projections.
 CoInductive Stream : Set := Seq { hd : nat; tl : Stream }.
 Stream is defined hd is defined tl is defined
 CoInductive EqSt (s1 s2: Stream) : Prop := eqst { eqst_hd : hd s1 = hd s2; eqst_tl : EqSt (tl s1) (tl s2); }.
 EqSt is defined eqst_hd is defined eqst_tl is defined
Some properties that hold over positive streams are lost when going to the negative presentation, typically when they imply equality over streams. For instance, propositional ηequality is lost when going to the negative presentation. It is nonetheless logically consistent to recover it through an axiom.
 Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s).
 Stream_eta is declared
More generally, as in the case of positive coinductive types, it is consistent to further identify extensional equality of coinductive types with propositional equality:
 Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 > s1 = s2.
 Stream_ext is declared
As of Coq 8.9, it is now advised to use negative coinductive types rather than their positive counterparts.
See also
Primitive Projections for more information about negative records and primitive projections.
Definition of recursive functions¶
Definition of functions by recursion over inductive objects¶
This section describes the primitive form of definition by recursion over
inductive objects. See the Function
command for more advanced
constructions.

Command
Fixpoint ident binders {struct ident}? : type? := term
¶ This command allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define
ident
a recursive function with arguments specified by thebinders
such thatident
applied to arguments corresponding to thesebinders
has typetype
, and is equivalent to the expressionterm
. The type ofident
is consequentlyforall binders, type
and its value is equivalent tofun binders => term
.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 theFixpoint
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.The
{struct ident}
annotation may be left implicit, in this case the system tries successively arguments from left to right until it finds one that satisfies the decreasing condition.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 (decreasing on 1st argument)
The match operator matches a value (here
n
) with the various constructors of its (inductive) type. The remaining arguments give the respective values to be returned, as functions of the parameters of the corresponding constructor. Thus here whenn
equalsO
we returnm
, and whenn
equals(S p)
we return(S (add p m))
.The match operator is formally described in Section The match ... with ... end construction. The system recognizes that in the inductive call
(add p m)
the first argument actually decreases because it is a pattern variable coming frommatch n with
.Example
The following definition is not correct and generates an error message:
 Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := match m with  O => n  S p => S (wrongplus n p) end.
 The command has indeed failed with message: Recursive definition of wrongplus is illformed. In environment wrongplus : nat > nat > nat n : nat m : nat p : nat Recursive call to wrongplus has principal argument equal to "n" instead of a subterm of "n". Recursive definition is: "fun n m : nat => match m with  0 => n  S p => S (wrongplus n p) end".
because the declared decreasing argument
n
does not actually decrease in the recursive call. The function computing the addition over the second argument should rather be written: Fixpoint plus (n m:nat) {struct m} : nat := match m with  O => n  S p => S (plus n p) end.
 plus is defined plus is recursively defined (decreasing on 2nd argument)
Example
The recursive call may not only be on direct subterms of the recursive variable
n
but also on a deeper subterm and we can directly write the functionmod2
which gives the remainder modulo 2 of a natural number. Fixpoint mod2 (n:nat) : nat := match n with  O => O  S p => match p with  O => S O  S q => mod2 q end end.
 mod2 is defined mod2 is recursively defined (decreasing on 1st argument)

Variant
Fixpoint ident binders {struct ident}? : type? := term with ident binders : type? := term*
This variant allows defining simultaneously several mutual fixpoints. It is especially useful when defining functions over mutually defined inductive types.
Example
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 (decreasing respectively on 1st, 1st arguments)
Definitions of recursive objects in coinductive types¶

Command
CoFixpoint ident binders? : type? := term
¶ This 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 Coinductive types for the definition ofStream
,hd
andtl
): CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
 from is defined 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 ofSeq
. On the contrary, the following recursive function does not satisfy the guard condition: Fail CoFixpoint filter (p:nat > bool) (s:Stream) : Stream := if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
 The command has indeed failed with message: 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)". Recursive definition is: "fun (p : nat > bool) (s : Stream) => if p (hd s) then { hd := hd s; tl := filter p (tl s) } else 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: Eval compute in (from 0).
 = (cofix from (n : nat) : Stream := { hd := n; tl := from (S n) }) 0 : Stream
 Eval compute in (hd (from 0)).
 = 0 : nat
 Eval compute in (tl (from 0)).
 = (cofix from (n : nat) : Stream := { hd := n; tl := from (S n) }) 1 : Stream
Assertions and proofs¶
An assertion states a proposition (or a type) of which the proof (or an inhabitant of the type) is interactively built using tactics. The interactive proof mode is described in Chapter Proof handling and the tactics in Chapter Tactics. The basic assertion command is:

Command
Theorem ident binders? : type
¶ After the statement is asserted, Coq needs a proof. Once a proof of
type
under the assumptions represented bybinders
is given and validated, the proof is generalized into a proof offorall binders, type
and the theorem is bound to the nameident
in the environment.
Error
ident already exists.
¶ The name you provided is already defined. You have then to choose another name.

Error
Nested proofs are not allowed unless you turn option Nested Proofs Allowed on.
¶ You are asserting a new statement while already being in proof editing mode. This feature, called nested proofs, is disabled by default. To activate it, turn option
Nested Proofs Allowed
on.

Error

Variant
Theorem ident binders? : type with ident binders? : type*
This command is useful for theorems that are proved by simultaneous induction over a mutually inductive assumption, or that assert mutually dependent statements in some mutual coinductive type. It is equivalent to
Fixpoint
orCoFixpoint
but using tactics to build the proof of the statements (or the body of the specification, depending on the point of view). The inductive or coinductive types on which the induction or coinduction has to be done is assumed to be non ambiguous and is guessed by the system.Like in a
Fixpoint
orCoFixpoint
definition, the induction hypotheses have to be used on structurally smaller arguments (for aFixpoint
) or be guarded by a constructor (for aCoFixpoint
). The verification that recursive proof arguments are correct is done only at the time of registering the lemma in the environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the commandGuarded
.The command can be used also with
Lemma
,Remark
, etc. instead ofTheorem
.

Variant
Definition ident binders? : type
This allows defining a term of type
type
using the proof editing mode. It behaves asTheorem
but is intended to be used in conjunction withDefined
in order to define a constant of which the computational behavior is relevant.The command can be used also with
Example
instead ofDefinition
.See also

Variant
Let ident binders? : type
Like
Definition ident binders? : type
except that the definition is turned into a letin definition generalized over the declarations depending on it after closing the current section.

Variant
Fixpoint ident binders : type with ident binders : type*
This generalizes the syntax of
Fixpoint
so that one or more bodies can be defined interactively using the proof editing mode (when a body is omitted, its type is mandatory in the syntax). When the block of proofs is completed, it is intended to be ended byDefined
.

Variant
CoFixpoint ident binders? : type with ident binders? : type*
This generalizes the syntax of
CoFixpoint
so that one or more bodies can be defined interactively using the proof editing mode.
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 Tactics. Besides tactics, there
are commands to manage the proof editing mode. They are described in Chapter
Proof handling.
When the proof is completed it should be validated and put in the environment
using the keyword Qed
.
Note
 Several statements can be simultaneously asserted provided option
Nested Proofs Allowed
was turned on.  Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the statements still to be proved. Nonetheless, this practice is discouraged and may stop working in future versions.
 Proofs ended by
Qed
are declared opaque. Their content cannot be unfolded (see Performing computations), thus realizing some form of proofirrelevance. To be able to unfold a proof, the proof should be ended byDefined
. Proof
is recommended but can currently be omitted. On the opposite side,Qed
(orDefined
) is mandatory to validate a proof. One can also use
Admitted
in place ofQed
to turn the current asserted statement into an axiom and exit the proof editing mode.
Attributes¶
Any vernacular command can be decorated with a list of attributes, enclosed
between #[
(hash and opening square bracket) and ]
(closing square bracket)
and separated by commas ,
. Multiple spaceseparated blocks may be provided.
Each attribute has a name (an identifier) and may have a value.
A value is either a string
(in which case it is specified with an equal =
sign),
or a list of attributes, enclosed within brackets.
Some attributes are specific to a command, and so are described with that command. Currently, the following attributes are recognized by a variety of commands:
universes(monomorphic)
,universes(polymorphic)
 Equivalent to the
Monomorphic
andPolymorphic
flags (see Polymorphic Universes). program
 Takes no value, equivalent to the
Program
flag (see Program). global
,local
 Take no value, equivalent to the
Global
andLocal
flags (see Controlling the locality of commands). deprecated
Takes as value the optional attributes
since
andnote
; both have a string value.This attribute can trigger the following warnings:
Example
 From Coq Require Program.
 [Loading ML file extraction_plugin.cmxs ... done]
 #[program] Definition one : nat := S _.
 one has typechecked, generating 1 obligation Solving obligations automatically... 1 obligation remaining Obligation 1 of one: nat.
 Next Obligation.
 1 subgoal ============================ nat
 exact O.
 No more subgoals.
 Defined.
 one_obligation_1 is defined No more obligations remaining one is defined
 #[deprecated(since="8.9.0", note="Use idtac instead.")] Ltac foo := idtac.
 foo is defined
 Goal True.
 1 subgoal ============================ True
 Proof.
 now foo.
 Toplevel input, characters 47: > now foo. > ^^^ Warning: Tactic foo is deprecated since 8.9.0. Use idtac instead. [deprecatedtactic,deprecated] No more subgoals.
 Abort.
[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 the inductive type is empty in which case there is no equation that can be used to infer the return type. 