1.3 The Vernacular
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.
sentence |
::= |
declaration |
|
| |
definition |
|
| |
statement |
|
| |
inductive |
|
| |
fixpoint |
|
| |
statement proof |
|
|
|
params |
::= |
typed_idents ; ... ; typed_idents |
|
|
|
declaration |
::= |
Axiom ident : term . |
|
| |
declaration_keyword params . |
|
|
|
declaration_keyword |
::= |
Parameter | Parameters |
|
| |
Variable | Variables |
|
| |
Hypothesis | Hypotheses |
|
|
|
definition |
::= |
Definition ident [: term] := term . |
|
| |
Local ident [: term] := term . |
|
|
|
inductive |
::= |
[Mutual] Inductive ind_body with ... with ind_body
. |
|
| |
[Mutual] CoInductive ind_body with ... with ind_body
. |
|
|
|
ind_body |
::= |
ident [[ params ]] : term
:=
[constructor | ... | constructor] |
|
|
|
constructor |
::= |
ident : term |
|
|
|
fixpoint |
::= |
Fixpoint fix_body with ... with fix_body
. |
|
| |
CoFixpoint cofix_body with ... with cofix_body
. |
|
|
|
statement |
::= |
Theorem ident : term . |
|
| |
Lemma ident : term . |
|
| |
Definition ident : term . |
|
|
|
proof |
::= |
Proof . ... Qed . |
|
| |
Proof . ... Defined . |
Figure 1.2: Syntax of sentences
The different kinds of command are described hereafter. They all suppose
that the terms occurring in the sentences are well-typed.
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 iff 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:
-
Clash with previous constant ident
Variants:
-
Parameter ident : term.
Is equivalent to Axiom ident : term
- Parameter ident , ... , ident : term ; ... ; ident , ... , ident : term .
Links the term's to the names comprising the lists ident , ... , ident : term ; ... ; ident , ... , ident : term.
Remark: It is possible to replace Parameter by
Parameters when more than one parameter are given.
Variable ident : term.
This command links term to the name ident in the context of the
current section (see 2.5 for a description of the section
mechanism). The name ident will be unknown when the current
section will be closed. One says that the variable is discharged. Using the Variable command out of any section is
equivalent to Axiom.
Error messages:
-
Clash with previous constant ident
Variants:
-
Variable ident , ... , ident:term ; ... ; ident , ... , ident:term .
Links term to the
names comprising the list ident , ... , ident:term ; ... ; ident , ... , ident:term
- Hypothesis ident , ... , ident : term ; ... ; ident , ... , ident : term .
Hypothsis is a synonymous of Variable
Remark: It is possible to replace Variable by
Variables and Hypothesis by Hypotheses
when more than one variable or one hypothesis are given.
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 since they allow 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
d-conversion (see section
4.3). A defined object is accepted by the system iff the
defining term is well-typed 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.4.
Definition ident := term.
This command binds the value term to the name ident in the
environment, provided that term is well-typed.
Error messages:
-
Clash with previous constant ident
Variants:
-
Definition ident : term1 := term2. It
checks that the type of term2 is definitionally equal to
term1, and registers ident as being of type term1,
and bound to value term2.
Error messages:
-
In environment ...the term: term2 does not have type
term1.
Actually, it has type term3.
See also: sections 5.2.4, 5.2.5, 7.5.5
Local ident := term.
This command binds the value term to the name ident in the
environment of the current section. The name ident will be unknown
when the current section will be closed and all occurrences of
ident in persistent objects (such as theorems) defined within the
section will be replaced by term. One can say that the Local
definition is a kind of macro.
Error messages:
-
Clash with previous constant ident
Variants:
-
Local ident : term1 := term2.
See also: 2.5 (section mechanism), 5.2.4,
5.2.5 (opaque/transparent constants), 7.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 co-inductive types.
Simple inductive types
The definition of a simple inductive type has the following form:
Inductive ident : sort := |
|
ident1 |
: |
type1 |
| |
... |
|
|
| |
identn |
: |
typen |
|
The name ident is the name of the inductively defined type and
sort is the universes where it lives.
The names ident1, ..., identn
are the names of its constructors and type1, ...,
typen 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,
ident1, ..., identn 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 := O : nat | S : nat -> nat.
nat_ind is defined
nat_rec is defined
nat_rect is defined
nat 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
: (P:(nat->Prop))(P O)->((n:nat)(P n)->(P (S n)))->(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 to prove some universal property of natural numbers ((n:nat)(P n)) by induction on n. Recall that (n:nat)(P n)
is Gallina's syntax for the universal quantification "
n:nat· P(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).
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 : (n:nat)(even n)->(even (S (S n))).
even_ind is defined
even 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
: (P:(nat->Prop))
(P O)
->((n:nat)(even n)->(P n)->(P (S (S n))))
->(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
- Type of Constructor not well-formed
Variants:
-
Inductive ident [ params ] : term :=
ident1:term1 | ... | identn:termn.
Allows
to define parameterized inductive types.
For instance, one can define
parameterized lists as:
Coq < Inductive list [X:Set] : Set :=
Coq < Nil : (list X) | Cons : X->(list X)->(list X).
Notice that, in the type of Nil and Cons, we write (list X) and not just list.
The constants Nil and
Cons will have respectively types:
Coq < Check Nil.
Nil
: (X:Set)(list X)
and
Coq < Check Cons.
Cons
: (X:Set)X->(list X)->(list X)
Types of destructors will be also quantified with (X:Set).
- Inductive sort ident :=
ident1:term1 | ... | identn:termn.
with sort being one of Prop, Type, Set is
equivalent to
Inductive ident : sort :=
ident1:term1 | ... | identn:termn.
- Inductive sort ident [ params ]:=
ident1:term1 | ... | identn:termn.
Same as before but with parameters.
See also: sections 4.5, 7.7.1
Mutually inductive types
The definition of a block of mutually inductive types has the form:
Inductive ident1 : type1 := |
|
ident11 |
: |
type11 |
| |
... |
|
|
| |
identn11 |
: |
typen11 |
|
with |
... |
with identm : typem := |
|
ident1m |
: |
type1m |
| |
... |
| |
identnmm |
: |
typenmm. |
|
Remark: The word Mutual can be optionally
inserted in front of Inductive.
It has the same semantics as the above Inductive definition for
each ident1, ..., identm. All names ident1, ...,
identm and ident11, ..., identnmm are
simultaneously added to the environment. Then
well-typing of constructors can be checked. Each one of the
ident1, ..., identm 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 extented syntax is:
Inductive ident1 [params ] : type1 :=
ident11 : type11
| ..
| identn11 : typen11
with
..
with identm [params ] : typem :=
ident1m : type1m
| ..
| identnmm : typenmm.
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 := 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
: (P:(tree->Set))((a:A; f:forest)(P (node a f)))->(t:tree)(P t)
Coq < Check forest_rec.
forest_rec
: (P:(forest->Set))
((b:B)(P (leaf b)))
->((t:tree; f:forest)(P f)->(P (cons t f)))
->(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
Coq < tree [A,B:Set] : Set := node : A -> (forest A B) -> (tree A B)
Coq < with forest [A,B:Set] : Set := 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: 2.5
Co-inductive types
The objects of an inductive type are well-founded with respect to the
constructors of the type. In other words, such objects contain only a
finite number constructors. Co-inductive types arise from
relaxing this condition, and admitting types whose objects contain an
infinity of constructors. Infinite objects are introduced by a
non-ending (but effective) process of construction, defined in terms
of the constructors of the type.
An example of a co-inductive 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 Set Stream := 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
co-inductive type, since such principles only make sense for inductive
ones. For co-inductive 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]Cases x of (Seq a s) => a end.
hd is defined
Coq < Definition tl := [x:Stream]Cases x of (Seq a s) => s end.
tl is defined
Definition of co-inductive predicates and blocks of mutually
co-inductive definitions are also allowed. An example of a
co-inductive predicate is the extensional equality on streams:
Coq < CoInductive EqSt : Stream->Stream->Prop :=
Coq < eqst : (s1,s2:Stream)
Coq < (hd s1)=(hd s2)->
Coq < (EqSt (tl s1) (tl s2))->(EqSt s1 s2).
EqSt is defined
In order to prove the extensionally equality of two streams s1 and
s2 we have to construct and infinite proof of equality, that is,
an infinite object of type (EqSt s1 s2). We will see
how to introduce infinite objects in section 1.3.4.
1.3.4 Definition of recursive functions
Fixpoint ident [ ident1 : type1 ] :
type0 := term0
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 one argument ident1 of type
term1 such that (ident ident1) has type type0 and is
equivalent to the expression term0. The type of the ident is
consequently (ident1 : type1)type0 and the value is
equivalent to [ident1 : type1]term0. The argument
ident1 (of type type1) is called the recursive
variable of ident. Its type should be an inductive definition.
To be accepted, a Fixpoint definition has to satisfy some
syntactical constraints on this recursive variable. They are needed to
ensure that the Fixpoint definition always terminates. For
instance, one can define the addition function as :
Coq < Fixpoint add [n:nat] : nat->nat
Coq < := [m:nat]Cases n of O => m | (S p) => (S (add p m)) end.
add is recursively defined
The Cases 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 Cases 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 Cases
n of.
Variants:
-
Fixpoint ident [ params ] : type0 :=
term0.
It declares a list of identifiers with their type
usable in the type type0 and the definition body term0
and the last identifier in params is the recursion variable.
- Fixpoint ident1 [ params1 ] :
type1 := term1
with ...
with identm [ paramsm ] : typem :=
typem
Allows to define simultaneously ident1, ...,
identm.
Example: The following definition is not correct and generates an
error message:
Coq < Fixpoint wrongplus [n:nat] : nat->nat
Coq < := [m:nat]Cases m of O => n | (S p) => (S (wrongplus n p)) end.
Error during interpretation of command:
Fixpoint wrongplus [n:nat] : nat->nat
:= [m:nat]Cases m of O => n | (S p) => (S (wrongplus n p)) end.
Error: Recursive call applied to an illegal term
The recursive definition wrongplus :=
[n,m:nat]Cases m of
O => n
| (S p) => (S (wrongplus n p))
end is not well-formed
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] : nat
Coq < := Cases m of O => n | (S p) => (S (plus n p)) end.
The ordinary match operation on natural numbers can be mimicked in the
following way.
Coq < Fixpoint nat_match [C:Set;f0:C;fS:nat->C->C;n:nat] : C
Coq < := Cases n of O => f0 | (S p) => (fS p (nat_match C f0 fS p)) 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 < := Cases n of
Coq < O => O
Coq < | (S p) => Cases p of O => (S O) | (S q) => (mod2 q) 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
recursive variable (whose 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.
Example: The size of trees and forests can be defined the following way:
Coq < Fixpoint tree_size [t:tree] : nat :=
Coq < Cases t of (node a f) => (S (forest_size f)) end
Coq < with forest_size [f:forest] : nat :=
Coq < Cases f of (leaf b) => (S O)
Coq < | (cons t f') => (plus (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 7.15.
CoFixpoint ident :
type0 := term0.
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:
Coq < CoInductive Set Stream := Seq : nat->Stream->Stream.
Coq < Definition hd := [x:Stream]Cases x of (Seq a s) => a end.
Coq < Definition tl := [x:Stream]Cases x of (Seq a s) => s end.
Coq < CoFixpoint from : nat->Stream := [n:nat](Seq n (from (S n))).
from is corecursively defined
Oppositely to recursive ones, there is no decreasing argument in a
co-recursive 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
co-recursive 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 : (nat->bool)->Stream->Stream :=
Coq < [p:nat->bool]
Coq < [s:Stream]
Coq < if (p (hd s)) then (Seq (hd s) (filter p (tl s)))
Coq < else (filter p (tl s)).
Notice that the definition contains an unguarded recursive
call of filter on the else branch of the test.
The elimination of co-recursive 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 expression. Isolate, 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 O).
= (CoFix from{from : nat->Stream := [n:nat](Seq n (from (S n)))}
O)
: Stream
Coq < Eval Compute in (hd (from O)).
= O
: nat
Coq < Eval Compute in (tl (from O)).
= (CoFix from{from : nat->Stream := [n:nat](Seq n (from (S n)))}
(S O))
: Stream
As in the Fixpoint command (cf. section 1.3.4), it
is possible to introduce a block of mutually dependent methods. The
general syntax for this case is:
CoFixpoint ident1 :type1 := term1
with
...
with identm : typem := termm
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 6.
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.
Same as Theorem except
that if this statement is in a section then the name ident will be unknown
when the current section (see 2.5) will be closed. All
proofs of persistent objects (such as theorems) referring to ident
within the section will be replaced by the proof of ident.
- Definition ident : type.
Allow to define a term of type type using the proof editing mode. It
behaves as Theorem except the defined term will be transparent (see
5.2.5, 7.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
7. Besides tactics, there are commands to manage the proof
editing mode. They are described in chapter 6. When
the proof is completed it should be validated and put in the
environment using the keyword Qed.
Error message:
-
Clash with previous constant ident
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 is mandatory to validate a proof.
Variants:
-
Proof . ...Defined .
Same as Proof . ...Qed . but it is
intended to surround a definition built using the proof-editing mode.
- 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.