1
\chapter{The \gallina{} specification language
2
\label{Gallina}\index{Gallina}}
4
This chapter describes \gallina, the specification language of {\Coq}.
5
It allows to develop mathematical theories and to prove specifications
6
of programs. The theories are built from axioms, hypotheses,
7
parameters, lemmas, theorems and definitions of constants, functions,
8
predicates and sets. The syntax of logical objects involved in
9
theories is described in section \ref{term}. The language of
10
commands, called {\em The Vernacular} is described in section
13
In {\Coq}, logical objects are typed to ensure their logical
14
correctness. The rules implemented by the typing algorithm are described in
17
\subsection*{About the grammars in the manual
18
\label{BNF-syntax}\index{BNF metasyntax}}
20
Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
21
set in {\tt typewriter font}. In addition, there are special
22
notations for regular expressions.
24
An expression enclosed in square brackets \zeroone{\ldots} means at
25
most one occurrence of this expression (this corresponds to an
28
The notation ``\nelist{\entry}{sep}'' stands for a non empty
29
sequence of expressions parsed by {\entry} and
30
separated by the literal ``{\tt sep}''\footnote{This is similar to the
31
expression ``{\entry} $\{$ {\tt sep} {\entry} $\}$'' in
32
standard BNF, or ``{\entry} $($ {\tt sep} {\entry} $)$*'' in
33
the syntax of regular expressions.}.
35
Similarly, the notation ``\nelist{\entry}{}'' stands for a non
36
empty sequence of expressions parsed by the ``{\entry}'' entry,
37
without any separator between.
39
At the end, the notation ``\sequence{\entry}{\tt sep}'' stands for a
40
possibly empty sequence of expressions parsed by the ``{\entry}'' entry,
41
separated by the literal ``{\tt sep}''.
43
\section{Lexical conventions
44
\label{lexical}\index{Lexical conventions}}
47
Space, newline and horizontal tabulation are considered as blanks.
48
Blanks are ignored but they separate tokens.
52
Comments in {\Coq} are enclosed between {\tt (*} and {\tt
53
*)}\index{Comments}, and can be nested. They can contain any
54
character. However, string literals must be correctly closed. Comments
55
are treated as blanks.
57
\paragraph{Identifiers and access identifiers}
59
Identifiers, written {\ident}, are sequences of letters, digits,
60
\verb!_! and \verb!'!, that do not start with a digit or \verb!'!.
61
That is, they are recognized by the following lexical class:
66
{\firstletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt \_}
67
$\mid$ {\tt unicode-letter}
69
{\subsequentletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt 0..9}
70
$\mid$ {\tt \_} % $\mid$ {\tt \$}
72
$\mid$ {\tt unicode-letter}
73
$\mid$ {\tt unicode-id-part} \\
74
{\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}
77
All characters are meaningful. In particular, identifiers are
78
case-sensitive. The entry {\tt unicode-letter} non-exhaustively
79
includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian,
80
Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical
81
letter-like symbols, hyphens, non-breaking space, {\ldots} The entry
82
{\tt unicode-id-part} non-exhaustively includes symbols for prime
83
letters and subscripts.
85
Access identifiers, written {\accessident}, are identifiers prefixed
86
by \verb!.! (dot) without blank. They are used in the syntax of qualified
89
\paragraph{Natural numbers and integers}
90
Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign.
93
\index{integer@{\integer}}
95
\begin{tabular}{r@{\quad::=\quad}l}
96
{\digit} & {\tt 0..9} \\
97
{\num} & \nelistwithoutblank{\digit}{} \\
98
{\integer} & \zeroone{\tt -}{\num} \\
104
\index{string@{\qstring}}
105
Strings are delimited by \verb!"! (double quote), and enclose a
106
sequence of any characters different from \verb!"! or the sequence
107
\verb!""! to denote the double quote character. In grammars, the
108
entry for quoted strings is {\qstring}.
111
The following identifiers are reserved keywords, and cannot be
114
\begin{tabular}{llllll}
149
\paragraph{Special tokens}
150
The following sequences of characters are special tokens:
152
\begin{tabular}{lllllll}
211
Lexical ambiguities are resolved according to the ``longest match''
212
rule: when a sequence of non alphanumerical characters can be decomposed
213
into several different ways, then the first token is the longest
214
possible one (among all tokens defined at this moment), and so on.
216
\section{Terms \label{term}\index{Terms}}
218
\subsection{Syntax of terms}
220
Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic
221
set of terms which form the {\em Calculus of Inductive Constructions}
222
(also called \CIC). The formal presentation of {\CIC} is given in
223
chapter \ref{Cic}. Extensions of this syntax are given in chapter
224
\ref{Gallina-extension}. How to customize the syntax is described in
225
chapter \ref{Addoc-syntax}.
229
\begin{tabular}{lcl@{\qquad}r}
231
{\tt forall} {\binderlist} {\tt ,} {\term} &(\ref{products})\\
232
& $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
233
& $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\
234
& $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\
235
& $|$ & {\tt let} {\idparams} {\tt :=} {\term}
236
{\tt in} {\term} &(\ref{let-in})\\
237
& $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\
238
& $|$ & {\tt let cofix} {\cofixpointbody}
239
{\tt in} {\term} &(\ref{fixpoints})\\
240
& $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem}
242
{\tt in} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
243
& $|$ & {\tt if} {\term} \zeroone{\ifitem} {\tt then} {\term}
244
{\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
245
& $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
246
& $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
247
& $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\
248
& $|$ & {\tt @} {\qualid} \sequence{\term}{}
249
&(\ref{Implicits-explicitation})\\
250
& $|$ & {\term} {\tt \%} {\ident} &(\ref{scopechange})\\
251
& $|$ & {\tt match} \nelist{\caseitem}{\tt ,}
252
\zeroone{\returntype} {\tt with} &\\
253
&& ~~~\zeroone{\zeroone{\tt |} \nelist{\eqn}{|}} {\tt end}
254
&(\ref{caseanalysis})\\
255
& $|$ & {\qualid} &(\ref{qualid})\\
256
& $|$ & {\sort} &(\ref{Gallina-sorts})\\
257
& $|$ & {\num} &(\ref{numerals})\\
258
& $|$ & {\_} &(\ref{hole})\\
260
{\termarg} & ::= & {\term} &\\
261
& $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )}
262
&(\ref{Implicits-explicitation})\\
263
%% & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )}
264
%% &(\ref{Implicits-explicitation})\\
266
{\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\
267
& $|$ & {\binder} \nelist{\binderlet}{} &\\
269
{\binder} & ::= & {\name} & \ref{Binders} \\
270
& $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\
272
{\binderlet} & ::= & {\binder} & \ref{Binders} \\
273
& $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
275
{\name} & ::= & {\ident} &\\
278
{\qualid} & ::= & {\ident} & \\
279
& $|$ & {\qualid} {\accessident} &\\
281
{\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} &
284
\caption{Syntax of terms}
295
{\idparams} & ::= & {\ident} \sequence{\binderlet}{} {\typecstr} \\
297
{\fixpointbodies} & ::= &
299
& $|$ & {\fixpointbody} {\tt with} \nelist{\fixpointbody}{{\tt with}}
300
{\tt for} {\ident} \\
301
{\cofixpointbodies} & ::= &
303
& $|$ & {\cofixpointbody} {\tt with} \nelist{\cofixpointbody}{{\tt with}}
304
{\tt for} {\ident} \\
306
{\fixpointbody} & ::= &
307
{\ident} \nelist{\binderlet}{} \zeroone{\annotation} {\typecstr}
309
{\cofixpointbody} & ::= & {\idparams} {\tt :=} {\term} \\
311
{\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\
313
{\caseitem} & ::= & {\term} \zeroone{{\tt as} \name}
314
\zeroone{{\tt in} \term} \\
316
{\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\
318
{\returntype} & ::= & {\tt return} {\term} \\
320
{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\
322
{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\
324
{\pattern} & ::= & {\qualid} \nelist{\pattern}{} \\
325
& $|$ & {\pattern} {\tt as} {\ident} \\
326
& $|$ & {\pattern} {\tt \%} {\ident} \\
330
& $|$ & {\tt (} \nelist{\orpattern}{,} {\tt )} \\
332
{\orpattern} & ::= & \nelist{\pattern}{\tt |}\\
335
\caption{Syntax of terms (continued)}
336
\label{term-syntax-aux}
344
{\Coq} terms are typed. {\Coq} types are recognized by the same
345
syntactic class as {\term}. We denote by {\type} the semantic subclass
346
of types inside the syntactic class {\term}.
350
\subsection{Qualified identifiers and simple identifiers
354
{\em Qualified identifiers} ({\qualid}) denote {\em global constants}
355
(definitions, lemmas, theorems, remarks or facts), {\em global
356
variables} (parameters or axioms), {\em inductive
357
types} or {\em constructors of inductive types}.
358
{\em Simple identifiers} (or shortly {\ident}) are a
359
syntactic subset of qualified identifiers. Identifiers may also
360
denote local {\em variables}, what qualified identifiers do not.
365
Numerals have no definite semantics in the calculus. They are mere
366
notations that can be bound to objects through the notation mechanism
367
(see chapter~\ref{Addoc-syntax} for details). Initially, numerals are
368
bound to Peano's representation of natural numbers
371
Note: negative integers are not at the same level as {\num}, for this
372
would make precedence unnatural.
380
\label{Gallina-sorts}}
382
There are three sorts \Set, \Prop\ and \Type.
384
\item \Prop\ is the universe of {\em logical propositions}.
385
The logical propositions themselves are typing the proofs.
386
We denote propositions by {\form}. This constitutes a semantic
387
subclass of the syntactic class {\term}.
389
\item \Set\ is is the universe of {\em program
390
types} or {\em specifications}.
391
The specifications themselves are typing the programs.
392
We denote specifications by {\specif}. This constitutes a semantic
393
subclass of the syntactic class {\term}.
394
\index{specif@{\specif}}
395
\item {\Type} is the type of {\Set} and {\Prop}
397
\noindent More on sorts can be found in section \ref{Sorts}.
401
{\Coq} terms are typed. {\Coq} types are recognized by the same
402
syntactic class as {\term}. We denote by {\type} the semantic subclass
403
of types inside the syntactic class {\term}.
410
Various constructions such as {\tt fun}, {\tt forall}, {\tt fix} and
411
{\tt cofix} {\em bind} variables. A binding is represented by an
412
identifier. If the binding variable is not used in the expression, the
413
identifier can be replaced by the symbol {\tt \_}. When the type of a
414
bound variable cannot be synthesized by the system, it can be
415
specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt
416
)}. There is also a notation for a sequence of binding variables
417
sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt
418
:}\,{\type}\,{\tt )}.
420
Some constructions allow the binding of a variable to value. This is
421
called a ``let-binder''. The entry {\binderlet} of the grammar accepts
422
either a binder as defined above or a let-binder. The notation in the
423
latter case is {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )}. In a
424
let-binder, only one variable can be introduced at the same
425
time. It is also possible to give the type of the variable as follows:
426
{\tt (}\,{\ident}\,{\tt :}\,{\term}\,{\tt :=}\,{\term}\,{\tt )}.
428
Lists of {\binderlet} are allowed. In the case of {\tt fun} and {\tt
429
forall}, the first binder of the list cannot be a let-binder, but
430
parentheses can be omitted in the case of a single sequence of
431
bindings sharing the same type (e.g.: {\tt fun~(x~y~z~:~A)~=>~t} can
432
be shortened in {\tt fun~x~y~z~:~A~=>~t}).
434
\subsection{Abstractions
436
\index{abstractions}}
438
The expression ``{\tt fun} {\ident} {\tt :} {\type} {\tt =>}~{\term}''
439
defines the {\em abstraction} of the variable {\ident}, of type
440
{\type}, over the term {\term}. It denotes a function of the variable
441
{\ident} that evaluates to the expression {\term} (e.g. {\tt fun x:$A$
442
=> x} denotes the identity function on type $A$).
443
% The variable {\ident} is called the {\em parameter} of the function
444
% (we sometimes say the {\em formal parameter}).
445
The keyword {\tt fun} can be followed by several binders as given in
446
Section~\ref{Binders}. Functions over several variables are
447
equivalent to an iteration of one-variable functions. For instance the
448
expression ``{\tt fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt
449
:}~\type~{\tt =>}~{\term}'' denotes the same function as ``{\tt
450
fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt =>}~{\ldots}~{\tt
451
fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}''. If a let-binder
452
occurs in the list of binders, it is expanded to a local definition
453
(see Section~\ref{let-in}).
459
The expression ``{\tt forall}~{\ident}~{\tt :}~{\type}{\tt
460
,}~{\term}'' denotes the {\em product} of the variable {\ident} of
461
type {\type}, over the term {\term}. As for abstractions, {\tt forall}
462
is followed by a binder list, and products over several variables are
463
equivalent to an iteration of one-variable products.
464
Note that {\term} is intended to be a type.
466
If the variable {\ident} occurs in {\term}, the product is called {\em
467
dependent product}. The intention behind a dependent product {\tt
468
forall}~$x$~{\tt :}~{$A$}{\tt ,}~{$B$} is twofold. It denotes either
469
the universal quantification of the variable $x$ of type $A$ in the
470
proposition $B$ or the functional dependent product from $A$ to $B$ (a
471
construction usually written $\Pi_{x:A}.B$ in set theory).
473
Non dependent product types have a special notation: ``$A$ {\tt ->}
474
$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The non dependent
475
product is used both to denote the propositional implication and
478
\subsection{Applications
480
\index{applications}}
482
The expression \term$_0$ \term$_1$ denotes the application of
483
\term$_0$ to \term$_1$.
485
The expression {\tt }\term$_0$ \term$_1$ ... \term$_n${\tt}
486
denotes the application of the term \term$_0$ to the arguments
487
\term$_1$ ... then \term$_n$. It is equivalent to {\tt (} {\ldots}
488
{\tt (} {\term$_0$} {\term$_1$} {\tt )} {\ldots} {\tt )} {\term$_n$} {\tt }:
489
associativity is to the left.
491
The notation {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )} for
492
arguments is used for making explicit the value of implicit arguments
493
(see Section~\ref{Implicits-explicitation}).
495
\subsection{Type cast
499
The expression ``{\term}~{\tt :}~{\type}'' is a type cast
500
expression. It enforces the type of {\term} to be {\type}.
502
\subsection{Inferable subterms
506
Expressions often contain redundant pieces of information. Subterms that
507
can be automatically inferred by {\Coq} can be replaced by the
508
symbol ``\_'' and {\Coq} will guess the missing piece of information.
510
\subsection{Local definitions (let-in)
512
\index{Local definitions}
516
{\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes
517
the local binding of \term$_1$ to the variable $\ident$ in
519
There is a syntactic sugar for local definition of functions: {\tt
520
let} {\ident} {\binder$_1$} \ldots {\binder$_n$} {\tt :=} {\term$_1$}
521
{\tt in} {\term$_2$} stands for {\tt let} {\ident} {\tt := fun}
522
{\binder$_1$} \ldots {\binder$_n$} {\tt =>} {\term$_2$} {\tt in}
525
\subsection{Definition by case analysis
527
\index{match@{\tt match\ldots with\ldots end}}}
529
Objects of inductive types can be destructurated by a case-analysis
530
construction called {\em pattern-matching} expression. A
531
pattern-matching expression is used to analyze the structure of an
532
inductive objects and to apply specific treatments accordingly.
534
This paragraph describes the basic form of pattern-matching. See
535
Section~\ref{Mult-match} and Chapter~\ref{Mult-match-full} for the
536
description of the general form. The basic form of pattern-matching is
537
characterized by a single {\caseitem} expression, a {\multpattern}
538
restricted to a single {\pattern} and {\pattern} restricted to the
539
form {\qualid} \nelist{\ident}{}.
541
The expression {\tt match} {\term$_0$} {\returntype} {\tt with}
542
{\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$}
543
{\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em
544
pattern-matching} over the term {\term$_0$} (expected to be of an
545
inductive type $I$). The terms {\term$_1$}\ldots{\term$_n$} are the
546
{\em branches} of the pattern-matching expression. Each of
547
{\pattern$_i$} has a form \qualid~\nelist{\ident}{} where {\qualid}
548
must denote a constructor. There should be exactly one branch for
549
every constructor of $I$.
551
The {\returntype} expresses the type returned by the whole {\tt match}
552
expression. There are several cases. In the {\em non dependent} case,
553
all branches have the same type, and the {\returntype} is the common
554
type of branches. In this case, {\returntype} can usually be omitted
555
as it can be inferred from the type of the branches\footnote{Except if
556
the inductive type is empty in which case there is no equation to help
557
to infer the return type.}.
559
In the {\em dependent} case, there are three subcases. In the first
560
subcase, the type in each branch may depend on the exact value being
561
matched in the branch. In this case, the whole pattern-matching itself
562
depends on the term being matched. This dependency of the term being
563
matched in the return type is expressed with an ``{\tt as {\ident}}''
564
clause where {\ident} is dependent in the return type.
565
For instance, in the following example:
567
Inductive bool : Type := true : bool | false : bool.
568
Inductive eq (A:Type) (x:A) : A -> Prop := refl_equal : eq A x x.
569
Inductive or (A:Prop) (B:Prop) : Prop :=
570
| or_introl : A -> or A B
571
| or_intror : B -> or A B.
572
Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
573
:= match b as x return or (eq bool x true) (eq bool x false) with
574
| true => or_introl (eq bool true true) (eq bool true false)
575
(refl_equal bool true)
576
| false => or_intror (eq bool false true) (eq bool false false)
577
(refl_equal bool false)
580
the branches have respective types {\tt or (eq bool true true) (eq
581
bool true false)} and {\tt or (eq bool false true) (eq bool false
582
false)} while the whole pattern-matching expression has type {\tt or
583
(eq bool b true) (eq bool b false)}, the identifier {\tt x} being used
584
to represent the dependency. Remark that when the term being matched
585
is a variable, the {\tt as} clause can be omitted and the term being
586
matched can serve itself as binding name in the return type. For
587
instance, the following alternative definition is accepted and has the
588
same meaning as the previous one.
590
Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
591
:= match b return or (eq bool b true) (eq bool b false) with
592
| true => or_introl (eq bool true true) (eq bool true false)
593
(refl_equal bool true)
594
| false => or_intror (eq bool false true) (eq bool false false)
595
(refl_equal bool false)
599
The second subcase is only relevant for annotated inductive types such
600
as the equality predicate (see section~\ref{Equality}), the order
601
predicate on natural numbers (see section~\ref{le}) or the type of
602
lists of a given length (see section~\ref{listn}). In this configuration,
603
the type of each branch can depend on the type dependencies specific
604
to the branch and the whole pattern-matching expression has a type
605
determined by the specific dependencies in the type of the term being
606
matched. This dependency of the return type in the annotations of the
607
inductive type is expressed using a {\tt
608
``in~I~\_~$\ldots$~\_~\ident$_1$~$\ldots$~\ident$_n$}'' clause, where
610
\item $I$ is the inductive type of the term being matched;
612
\item the names \ident$_i$'s correspond to the arguments of the
613
inductive type that carry the annotations: the return type is dependent
616
\item the {\_}'s denote the family parameters of the inductive type:
617
the return type is not dependent on them.
620
For instance, in the following example:
622
Definition sym_equal (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
623
match H in eq _ _ z return eq A z x with
624
| refl_equal => refl_equal A x
627
the type of the branch has type {\tt eq~A~x~x} because the third
628
argument of {\tt eq} is {\tt x} in the type of the pattern {\tt
629
refl\_equal}. On the contrary, the type of the whole pattern-matching
630
expression has type {\tt eq~A~y~x} because the third argument of {\tt
631
eq} is {\tt y} in the type of {\tt H}. This dependency of the case
632
analysis in the third argument of {\tt eq} is expressed by the
633
identifier {\tt z} in the return type.
635
Finally, the third subcase is a combination of the first and second
636
subcase. In particular, it only applies to pattern-matching on terms
637
in a type with annotations. For this third subcase, both
638
the clauses {\tt as} and {\tt in} are available.
640
There are specific notations for case analysis on types with one or
641
two constructors: ``{\tt if {\ldots} then {\ldots} else {\ldots}}''
642
and ``{\tt let (}\nelist{\ldots}{,}{\tt ) := } {\ldots} {\tt in}
643
{\ldots}'' (see Sections~\ref{if-then-else} and~\ref{Letin}).
645
%\SeeAlso Section~\ref{Mult-match} for convenient extensions of pattern-matching.
647
\subsection{Recursive functions
649
\index{fix@{fix \ident$_i$\{\dots\}}}}
651
The expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$}
652
\texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$
653
\binder$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for}
654
{\ident$_i$}'' denotes the $i$\nth component of a block of functions
655
defined by mutual well-founded recursion. It is the local counterpart
656
of the {\tt Fixpoint} command. See Section~\ref{Fixpoint} for more
657
details. When $n=1$, the ``{\tt for}~{\ident$_i$}'' clause is omitted.
659
The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :}
660
{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binder$_n$ {\tt
661
:} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$\nth component of
662
a block of terms defined by a mutual guarded co-recursion. It is the
663
local counterpart of the {\tt CoFixpoint} command. See
664
Section~\ref{CoFixpoint} for more details. When $n=1$, the ``{\tt
665
for}~{\ident$_i$}'' clause is omitted.
667
The association of a single fixpoint and a local
668
definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
669
:=}~{\ldots}~{\tt in}~{\ldots}'' stands for ``{\tt let}~$f$~{\tt :=
670
fix}~$f$~\ldots~{\tt :=}~{\ldots}~{\tt in}~{\ldots}''. The same
671
applies for co-fixpoints.
674
\section{The Vernacular
680
{\sentence} & ::= & {\declaration} \\
681
& $|$ & {\definition} \\
682
& $|$ & {\inductive} \\
683
& $|$ & {\fixpoint} \\
684
& $|$ & {\statement} \zeroone{\proof} \\
687
{\declaration} & ::= & {\declarationkeyword} {\assums} {\tt .} \\
689
{\declarationkeyword} & ::= & {\tt Axiom} $|$ {\tt Conjecture} \\
690
& $|$ & {\tt Parameter} $|$ {\tt Parameters} \\
691
& $|$ & {\tt Variable} $|$ {\tt Variables} \\
692
& $|$ & {\tt Hypothesis} $|$ {\tt Hypotheses}\\
694
{\assums} & ::= & \nelist{\ident}{} {\tt :} {\term} \\
695
& $|$ & \nelist{\binder}{} \\
698
{\definition} & ::= &
699
{\tt Definition} {\idparams} {\tt :=} {\term} {\tt .} \\
700
& $|$ & {\tt Let} {\idparams} {\tt :=} {\term} {\tt .} \\
704
{\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
705
& $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
707
{\inductivebody} & ::= &
708
{\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\
709
&& ~~~\zeroone{\zeroone{\tt |} \nelist{\idparams}{|}} \\
710
& & \\ %% TODO: where ...
712
{\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\
713
& $|$ & {\tt CoFixpoint} \nelist{\cofixpointbody}{with} {\tt .} \\
717
{\statkwd} {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt .} \\
719
{\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} $|$ {\tt Definition} \\
721
{\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\
722
& $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\
723
& $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}
726
\caption{Syntax of sentences}
727
\label{sentences-syntax}
730
Figure \ref{sentences-syntax} describes {\em The Vernacular} which is the
731
language of commands of \gallina. A sentence of the vernacular
732
language, like in many natural languages, begins with a capital letter
735
The different kinds of command are described hereafter. They all suppose
736
that the terms occurring in the sentences are well-typed.
739
%% Axioms and Parameters
741
\subsection{Declarations
743
\label{Declarations}}
745
The declaration mechanism allows the user to specify his own basic
746
objects. Declared objects play the role of axioms or parameters in
747
mathematics. A declared object is an {\ident} associated to a \term. A
748
declaration is accepted by {\Coq} if and only if this {\term} is a
749
correct type in the current context of the declaration and \ident\ was
750
not previously defined in the same module. This {\term} is considered
751
to be the type, or specification, of the \ident.
753
\subsubsection{{\tt Axiom {\ident} :{\term} .}
755
\comindex{Parameter}\comindex{Parameters}
756
\comindex{Conjecture}
759
This command links {\term} to the name {\ident} as its specification
760
in the global context. The fact asserted by {\term} is thus assumed as
764
\item \errindex{{\ident} already exists}
768
\item {\tt Parameter {\ident} :{\term}.} \\
769
Is equivalent to {\tt Axiom {\ident} : {\term}}
771
\item {\tt Parameter {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
772
Adds $n$ parameters with specification {\term}
776
(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
777
\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
778
{\term$_n$} {\tt )}.}\\
779
Adds $n$ blocks of parameters with different specifications.
781
\item {\tt Conjecture {\ident} :{\term}.}\\
782
Is equivalent to {\tt Axiom {\ident} : {\term}}.
785
\noindent {\bf Remark: } It is possible to replace {\tt Parameter} by
789
\subsubsection{{\tt Variable {\ident} :{\term}}.
792
\comindex{Hypothesis}
793
\comindex{Hypotheses}}
795
This command links {\term} to the name {\ident} in the context of the
796
current section (see Section~\ref{Section} for a description of the section
797
mechanism). When the current section is closed, name {\ident} will be
798
unknown and every object using this variable will be explicitly
799
parametrized (the variable is {\em discharged}). Using the {\tt
800
Variable} command out of any section is equivalent to {\tt Axiom}.
803
\item \errindex{{\ident} already exists}
807
\item {\tt Variable {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
808
Links {\term} to names {\ident$_1$}\ldots{\ident$_n$}.
811
(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
812
\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
813
{\term$_n$} {\tt )}.}\\
814
Adds $n$ blocks of variables with different specifications.
815
\item {\tt Hypothesis {\ident} {\tt :}{\term}.} \\
816
\texttt{Hypothesis} is a synonymous of \texttt{Variable}
819
\noindent {\bf Remark: } It is possible to replace {\tt Variable} by
820
{\tt Variables} and {\tt Hypothesis} by {\tt Hypotheses}.
822
It is advised to use the keywords \verb:Axiom: and \verb:Hypothesis:
823
for logical postulates (i.e. when the assertion {\term} is of sort
824
\verb:Prop:), and to use the keywords \verb:Parameter: and
825
\verb:Variable: in other cases (corresponding to the declaration of an
826
abstract mathematical entity).
831
\subsection{Definitions
833
\label{Simpl-definitions}}
835
Definitions differ from declarations in allowing to give a name to a
836
term whereas declarations were just giving a type to a name. That is
837
to say that the name of a defined object can be replaced at any time
838
by its definition. This replacement is called
839
$\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see
840
Section~\ref{delta}). A defined object is accepted by the system if
841
and only if the defining term is well-typed in the current context of
842
the definition. Then the type of the name is the type of term. The
843
defined name is called a {\em constant}\index{Constant} and one says
844
that {\it the constant is added to the
845
environment}\index{Environment}.
847
A formal presentation of constants and environments is given in
848
Section~\ref{Typed-terms}.
850
\subsubsection{\tt Definition {\ident} := {\term}.
851
\comindex{Definition}}
853
This command binds the value {\term} to the name {\ident} in the
854
environment, provided that {\term} is well-typed.
857
\item \errindex{{\ident} already exists}
861
\item {\tt Definition {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
862
It checks that the type of {\term$_2$} is definitionally equal to
863
{\term$_1$}, and registers {\ident} as being of type {\term$_1$},
864
and bound to value {\term$_2$}.
865
\item {\tt Definition {\ident} {\binder$_1$}\ldots{\binder$_n$}
866
{\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
867
This is equivalent to \\
868
{\tt Definition\,{\ident}\,{\tt :\,forall}\,%
869
{\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
870
{\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
873
\item {\tt Example {\ident} := {\term}.}\\
874
{\tt Example {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
875
{\tt Example {\ident} {\binder$_1$}\ldots{\binder$_n$}
876
{\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
878
These are synonyms of the {\tt Definition} forms.
882
\item \errindex{Error: The term ``{\term}'' has type "{\type}" while it is expected to have type ``{\type}''}
885
\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
887
\subsubsection{\tt Let {\ident} := {\term}.
890
This command binds the value {\term} to the name {\ident} in the
891
environment of the current section. The name {\ident} disappears
892
when the current section is eventually closed, and, all
893
persistent objects (such as theorems) defined within the
894
section and depending on {\ident} are prefixed by the local definition
895
{\tt let {\ident} := {\term} in}.
898
\item \errindex{{\ident} already exists}
902
\item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.}
905
\SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque},
906
\ref{Transparent} (opaque/transparent constants), \ref{unfold}
911
\subsection{Inductive definitions
912
\index{Inductive definitions}
913
\label{gal_Inductive_Definitions}
917
We gradually explain simple inductive types, simple
918
annotated inductive types, simple parametric inductive types,
919
mutually inductive types. We explain also co-inductive types.
921
\subsubsection{Simple inductive types}
923
The definition of a simple inductive type has the following form:
928
Inductive {\ident} : {\sort} := \\
929
\begin{tabular}{clcl}
930
& {\ident$_1$} &:& {\type$_1$} \\
932
| & {\ident$_n$} &:& {\type$_n$}
938
The name {\ident} is the name of the inductively defined type and
939
{\sort} is the universes where it lives.
940
The names {\ident$_1$}, {\ldots}, {\ident$_n$}
941
are the names of its constructors and {\type$_1$}, {\ldots},
942
{\type$_n$} their respective types. The types of the constructors have
943
to satisfy a {\em positivity condition} (see Section~\ref{Positivity})
944
for {\ident}. This condition ensures the soundness of the inductive
945
definition. If this is the case, the constants {\ident},
946
{\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with
947
their respective types. Accordingly to the universe where
948
the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a
949
number of destructors for {\ident}. Destructors are named
950
{\ident}{\tt\_ind}, {\ident}{\tt \_rec} or {\ident}{\tt \_rect} which
951
respectively correspond to elimination principles on {\tt Prop}, {\tt
952
Set} and {\tt Type}. The type of the destructors expresses structural
953
induction/recursion principles over objects of {\ident}. We give below
954
two examples of the use of the {\tt Inductive} definitions.
956
The set of natural numbers is defined as:
958
Inductive nat : Set :=
963
The type {\tt nat} is defined as the least \verb:Set: containing {\tt
964
O} and closed by the {\tt S} constructor. The constants {\tt nat},
965
{\tt O} and {\tt S} are added to the environment.
967
Now let us have a look at the elimination principles. They are three
969
{\tt nat\_ind}, {\tt nat\_rec} and {\tt nat\_rect}. The type of {\tt
975
This is the well known structural induction principle over natural
976
numbers, i.e. the second-order form of Peano's induction principle.
977
It allows to prove some universal property of natural numbers ({\tt
978
forall n:nat, P n}) by induction on {\tt n}.
980
The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except
981
that they pertain to {\tt (P:nat->Set)} and {\tt (P:nat->Type)}
982
respectively . They correspond to primitive induction principles
983
(allowing dependent types) respectively over sorts \verb:Set: and
984
\verb:Type:. The constant {\ident}{\tt \_ind} is always provided,
985
whereas {\ident}{\tt \_rec} and {\ident}{\tt \_rect} can be impossible
986
to derive (for example, when {\ident} is a proposition).
994
Inductive nat : Set := O | S (_:nat).
996
In the case where inductive types have no annotations (next section
997
gives an example of such annotations),
998
%the positivity condition implies that
999
a constructor can be defined by only giving the type of
1003
\subsubsection{Simple annotated inductive types}
1005
In an annotated inductive types, the universe where the inductive
1006
type is defined is no longer a simple sort, but what is called an
1007
arity, which is a type whose conclusion is a sort.
1009
As an example of annotated inductive types, let us define the
1013
Inductive even : nat -> Prop :=
1015
| even_SS : forall n:nat, even n -> even (S (S n)).
1018
The type {\tt nat->Prop} means that {\tt even} is a unary predicate
1019
(inductively defined) over natural numbers. The type of its two
1020
constructors are the defining clauses of the predicate {\tt even}. The
1021
type of {\tt even\_ind} is:
1027
From a mathematical point of view it asserts that the natural numbers
1028
satisfying the predicate {\tt even} are exactly in the smallest set of
1029
naturals satisfying the clauses {\tt even\_0} or {\tt even\_SS}. This
1030
is why, when we want to prove any predicate {\tt P} over elements of
1031
{\tt even}, it is enough to prove it for {\tt O} and to prove that if
1032
any natural number {\tt n} satisfies {\tt P} its double successor {\tt
1033
(S (S n))} satisfies also {\tt P}. This is indeed analogous to the
1034
structural induction principle we got for {\tt nat}.
1037
\item \errindex{Non strictly positive occurrence of {\ident} in {\type}}
1038
\item \errindex{The conclusion of {\type} is not valid; it must be
1039
built from {\ident}}
1042
\subsubsection{Parametrized inductive types}
1043
In the previous example, each constructor introduces a
1044
different instance of the predicate {\tt even}. In some cases,
1045
all the constructors introduces the same generic instance of the
1046
inductive definition, in which case, instead of an annotation, we use
1047
a context of parameters which are binders shared by all the
1048
constructors of the definition.
1050
% Inductive types may be parameterized. Parameters differ from inductive
1051
% type annotations in the fact that recursive invokations of inductive
1052
% types must always be done with the same values of parameters as its
1055
The general scheme is:
1057
{\tt Inductive} {\ident} {\binder$_1$}\ldots{\binder$_k$} : {\term} :=
1058
{\ident$_1$}: {\term$_1$} | {\ldots} | {\ident$_n$}: \term$_n$
1061
Parameters differ from inductive type annotations in the fact that the
1062
conclusion of each type of constructor {\term$_i$} invoke the inductive
1063
type with the same values of parameters as its specification.
1067
A typical example is the definition of polymorphic lists:
1068
\begin{coq_example*}
1069
Inductive list (A:Set) : Set :=
1071
| cons : A -> list A -> list A.
1074
Note that in the type of {\tt nil} and {\tt cons}, we write {\tt
1075
(list A)} and not just {\tt list}.\\ The constants {\tt nil} and
1076
{\tt cons} will have respectively types:
1083
Types of destructors are also quantified with {\tt (A:Set)}.
1090
\begin{coq_example*}
1091
Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
1093
This is an alternative definition of lists where we specify the
1094
arguments of the constructors rather than their full type.
1098
\item \errindex{The {\num}th argument of {\ident} must be {\ident'} in
1102
\paragraph{New from \Coq{} V8.1} The condition on parameters for
1103
inductive definitions has been relaxed since \Coq{} V8.1. It is now
1104
possible in the type of a constructor, to invoke recursively the
1105
inductive definition on an argument which is not the parameter itself.
1109
Inductive list2 (A:Set) : Set :=
1111
| cons2 : A -> list2 (A*A) -> list2 A.
1116
that can also be written by specifying only the type of the arguments:
1117
\begin{coq_example*}
1118
Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
1120
But the following definition will give an error:
1122
Inductive listw (A:Set) : Set :=
1123
| nilw : listw (A*A)
1124
| consw : A -> listw (A*A) -> listw (A*A).
1126
Because the conclusion of the type of constructors should be {\tt
1127
listw A} in both cases.
1129
A parametrized inductive definition can be defined using
1130
annotations instead of parameters but it will sometimes give a
1131
different (bigger) sort for the inductive definition and will produce
1132
a less convenient rule for case elimination.
1134
\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{Tac-induction}.
1137
\subsubsection{Mutually defined inductive types
1138
\comindex{Mutual Inductive}
1139
\label{Mutual-Inductive}}
1141
The definition of a block of mutually inductive types has the form:
1146
Inductive {\ident$_1$} : {\type$_1$} := \\
1147
\begin{tabular}{clcl}
1148
& {\ident$_1^1$} &:& {\type$_1^1$} \\
1150
| & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$}
1154
with {\ident$_m$} : {\type$_m$} := \\
1155
\begin{tabular}{clcl}
1156
& {\ident$_1^m$} &:& {\type$_1^m$} \\
1158
| & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}.
1164
\noindent It has the same semantics as the above {\tt Inductive}
1165
definition for each \ident$_1$, {\ldots}, \ident$_m$. All names
1166
\ident$_1$, {\ldots}, \ident$_m$ and \ident$_1^1$, \dots,
1167
\ident$_{n_m}^m$ are simultaneously added to the environment. Then
1168
well-typing of constructors can be checked. Each one of the
1169
\ident$_1$, {\ldots}, \ident$_m$ can be used on its own.
1171
It is also possible to parametrize these inductive definitions.
1172
However, parameters correspond to a local
1173
context in which the whole set of inductive declarations is done. For
1174
this reason, the parameters must be strictly the same for each
1175
inductive types The extended syntax is:
1180
Inductive {\ident$_1$} {\params} : {\type$_1$} := \\
1181
\begin{tabular}{clcl}
1182
& {\ident$_1^1$} &:& {\type$_1^1$} \\
1184
| & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$}
1188
with {\ident$_m$} {\params} : {\type$_m$} := \\
1189
\begin{tabular}{clcl}
1190
& {\ident$_1^m$} &:& {\type$_1^m$} \\
1192
| & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}.
1199
The typical example of a mutual inductive data type is the one for
1200
trees and forests. We assume given two types $A$ and $B$ as variables.
1201
It can be declared the following way.
1206
\begin{coq_example*}
1207
Variables A B : Set.
1208
Inductive tree : Set :=
1209
node : A -> forest -> tree
1210
with forest : Set :=
1211
| leaf : B -> forest
1212
| cons : tree -> forest -> forest.
1215
This declaration generates automatically six induction
1216
principles. They are respectively
1217
called {\tt tree\_rec}, {\tt tree\_ind}, {\tt
1218
tree\_rect}, {\tt forest\_rec}, {\tt forest\_ind}, {\tt
1219
forest\_rect}. These ones are not the most general ones but are
1220
just the induction principles corresponding to each inductive part
1221
seen as a single inductive definition.
1223
To illustrate this point on our example, we give the types of {\tt
1224
tree\_rec} and {\tt forest\_rec}.
1231
Assume we want to parametrize our mutual inductive definitions with
1232
the two type variables $A$ and $B$, the declaration should be done the
1238
\begin{coq_example*}
1239
Inductive tree (A B:Set) : Set :=
1240
node : A -> forest A B -> tree A B
1241
with forest (A B:Set) : Set :=
1242
| leaf : B -> forest A B
1243
| cons : tree A B -> forest A B -> forest A B.
1246
Assume we define an inductive definition inside a section. When the
1247
section is closed, the variables declared in the section and occurring
1248
free in the declaration are added as parameters to the inductive
1251
\SeeAlso Section~\ref{Section}
1253
\subsubsection{Co-inductive types
1254
\label{CoInductiveTypes}
1255
\comindex{CoInductive}}
1257
The objects of an inductive type are well-founded with respect to the
1258
constructors of the type. In other words, such objects contain only a
1259
{\it finite} number of constructors. Co-inductive types arise from
1260
relaxing this condition, and admitting types whose objects contain an
1261
infinity of constructors. Infinite objects are introduced by a
1262
non-ending (but effective) process of construction, defined in terms
1263
of the constructors of the type.
1265
An example of a co-inductive type is the type of infinite sequences of
1266
natural numbers, usually called streams. It can be introduced in \Coq\
1267
using the \texttt{CoInductive} command:
1269
CoInductive Stream : Set :=
1270
Seq : nat -> Stream -> Stream.
1273
The syntax of this command is the same as the command \texttt{Inductive}
1274
(cf. Section~\ref{gal_Inductive_Definitions}). Notice that no
1275
principle of induction is derived from the definition of a
1276
co-inductive type, since such principles only make sense for inductive
1277
ones. For co-inductive ones, the only elimination principle is case
1278
analysis. For example, the usual destructors on streams
1279
\texttt{hd:Stream->nat} and \texttt{tl:Str->Str} can be defined as
1282
Definition hd (x:Stream) := let (a,s) := x in a.
1283
Definition tl (x:Stream) := let (a,s) := x in s.
1286
Definition of co-inductive predicates and blocks of mutually
1287
co-inductive definitions are also allowed. An example of a
1288
co-inductive predicate is the extensional equality on streams:
1291
CoInductive EqSt : Stream -> Stream -> Prop :=
1293
forall s1 s2:Stream,
1294
hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
1297
In order to prove the extensionally equality of two streams $s_1$ and
1298
$s_2$ we have to construct an infinite proof of equality, that is,
1299
an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see
1300
how to introduce infinite objects in Section~\ref{CoFixpoint}.
1305
\subsection{Definition of recursive functions}
1307
\subsubsection{Definition of functions by recursion over inductive objects}
1309
This section describes the primitive form of definition by recursion
1310
over inductive objects. See Section~\ref{Function} for more advanced
1311
constructions. The command:
1313
\texttt{Fixpoint {\ident} {\params} {\tt \{struct}
1314
\ident$_0$ {\tt \}} : type$_0$ := \term$_0$
1315
\comindex{Fixpoint}\label{Fixpoint}}
1317
allows to define functions by pattern-matching over inductive objects
1318
using a fixed point construction.
1319
The meaning of this declaration is to define {\it ident} a recursive
1320
function with arguments specified by the binders in {\params} such
1321
that {\it ident} applied to arguments corresponding to these binders
1322
has type \type$_0$, and is equivalent to the expression \term$_0$. The
1323
type of the {\ident} is consequently {\tt forall {\params} {\tt,}
1324
\type$_0$} and the value is equivalent to {\tt fun {\params} {\tt
1327
To be accepted, a {\tt Fixpoint} definition has to satisfy some
1328
syntactical constraints on a special argument called the decreasing
1329
argument. They are needed to ensure that the {\tt Fixpoint} definition
1330
always terminates. The point of the {\tt \{struct \ident {\tt \}}}
1331
annotation is to let the user tell the system which argument decreases
1332
along the recursive calls. This annotation may be left implicit for
1333
fixpoints where only one argument has an inductive type. For instance,
1334
one can define the addition function as :
1337
Fixpoint add (n m:nat) {struct n} : nat :=
1340
| S p => S (add p m)
1344
The {\tt match} operator matches a value (here \verb:n:) with the
1345
various constructors of its (inductive) type. The remaining arguments
1346
give the respective values to be returned, as functions of the
1347
parameters of the corresponding constructor. Thus here when \verb:n:
1348
equals \verb:O: we return \verb:m:, and when \verb:n: equals
1349
\verb:(S p): we return \verb:(S (add p m)):.
1351
The {\tt match} operator is formally described
1352
in detail in Section~\ref{Caseexpr}. The system recognizes that in
1353
the inductive call {\tt (add p m)} the first argument actually
1354
decreases because it is a {\em pattern variable} coming from {\tt match
1357
\Example The following definition is not correct and generates an
1361
Set Printing Depth 50.
1362
(********** The following is not correct and should produce **********)
1363
(********* Error: Recursive call to wrongplus ... **********)
1366
Fixpoint wrongplus (n m:nat) {struct n} : nat :=
1369
| S p => S (wrongplus n p)
1373
because the declared decreasing argument {\tt n} actually does not
1374
decrease in the recursive call. The function computing the addition
1375
over the second argument should rather be written:
1377
\begin{coq_example*}
1378
Fixpoint plus (n m:nat) {struct m} : nat :=
1381
| S p => S (plus n p)
1385
The ordinary match operation on natural numbers can be mimicked in the
1387
\begin{coq_example*}
1389
(C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C :=
1392
| S p => fS p (nat_match C f0 fS p)
1395
The recursive call may not only be on direct subterms of the recursive
1396
variable {\tt n} but also on a deeper subterm and we can directly
1397
write the function {\tt mod2} which gives the remainder modulo 2 of a
1399
\begin{coq_example*}
1400
Fixpoint mod2 (n:nat) : nat :=
1403
| S p => match p with
1409
In order to keep the strong normalization property, the fixed point
1410
reduction will only be performed when the argument in position of the
1411
decreasing argument (which type should be in an inductive definition)
1412
starts with a constructor.
1414
The {\tt Fixpoint} construction enjoys also the {\tt with} extension
1415
to define functions over mutually defined inductive types or more
1416
generally any mutually recursive definitions.
1419
\item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\
1421
with {\ident$_m$} {\params$_m$} :{\type$_m$} := {\type$_m$}}\\
1422
Allows to define simultaneously {\ident$_1$}, {\ldots},
1427
The size of trees and forests can be defined the following way:
1430
Variables A B : Set.
1431
Inductive tree : Set :=
1432
node : A -> forest -> tree
1433
with forest : Set :=
1434
| leaf : B -> forest
1435
| cons : tree -> forest -> forest.
1437
\begin{coq_example*}
1438
Fixpoint tree_size (t:tree) : nat :=
1440
| node a f => S (forest_size f)
1442
with forest_size (f:forest) : nat :=
1445
| cons t f' => (tree_size t + forest_size f')
1448
A generic command {\tt Scheme} is useful to build automatically various
1449
mutual induction principles. It is described in Section~\ref{Scheme}.
1451
\subsubsection{Definition of recursive objects in co-inductive types}
1455
\texttt{CoFixpoint {\ident} : \type$_0$ := \term$_0$}
1456
\comindex{CoFixpoint}\label{CoFixpoint}
1458
introduces a method for constructing an infinite object of a
1459
coinduc\-tive type. For example, the stream containing all natural
1460
numbers can be introduced applying the following method to the number
1461
\texttt{O} (see Section~\ref{CoInductiveTypes} for the definition of
1462
{\tt Stream}, {\tt hd} and {\tt tl}):
1465
CoInductive Stream : Set :=
1466
Seq : nat -> Stream -> Stream.
1467
Definition hd (x:Stream) := match x with
1470
Definition tl (x:Stream) := match x with
1475
CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
1478
Oppositely to recursive ones, there is no decreasing argument in a
1479
co-recursive definition. To be admissible, a method of construction
1480
must provide at least one extra constructor of the infinite object for
1481
each iteration. A syntactical guard condition is imposed on
1482
co-recursive definitions in order to ensure this: each recursive call
1483
in the definition must be protected by at least one constructor, and
1484
only by constructors. That is the case in the former definition, where
1485
the single recursive call of \texttt{from} is guarded by an
1486
application of \texttt{Seq}. On the contrary, the following recursive
1487
function does not satisfy the guard condition:
1490
Set Printing Depth 50.
1491
(********** The following is not correct and should produce **********)
1492
(***************** Error: Unguarded recursive call *******************)
1495
CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
1496
if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
1499
The elimination of co-recursive definition is done lazily, i.e. the
1500
definition is expanded only when it occurs at the head of an
1501
application which is the argument of a case analysis expression. In
1502
any other context, it is considered as a canonical expression which is
1503
completely evaluated. We can test this using the command
1504
\texttt{Eval}, which computes the normal forms of a term:
1507
Eval compute in (from 0).
1508
Eval compute in (hd (from 0)).
1509
Eval compute in (tl (from 0)).
1513
\item{\tt CoFixpoint {\ident$_1$} {\params} :{\type$_1$} :=
1514
{\term$_1$}}\\ As for most constructions, arguments of co-fixpoints
1515
expressions can be introduced before the {\tt :=} sign.
1516
\item{\tt CoFixpoint {\ident$_1$} :{\type$_1$} := {\term$_1$}\\
1518
\mbox{}\hspace{0.1cm} $\ldots$ \\
1519
with {\ident$_m$} : {\type$_m$} := {\term$_m$}}\\
1520
As in the \texttt{Fixpoint} command (cf. Section~\ref{Fixpoint}), it
1521
is possible to introduce a block of mutually dependent methods.
1525
%% Theorems & Lemmas
1527
\subsection{Statement and proofs}
1529
A statement claims a goal of which the proof is then interactively done
1530
using tactics. More on the proof editing mode, statements and proofs can be
1531
found in chapter \ref{Proof-handling}.
1533
\subsubsection{\tt Theorem {\ident} : {\type}.
1539
This command binds {\type} to the name {\ident} in the
1540
environment, provided that a proof of {\type} is next given.
1542
After a statement, {\Coq} needs a proof.
1545
\item {\tt Lemma {\ident} : {\type}.}\\
1546
{\tt Remark {\ident} : {\type}.}\\
1547
{\tt Fact {\ident} : {\type}.}\\
1548
{\tt Corollary {\ident} : {\type}.}\\
1549
{\tt Proposition {\ident} : {\type}.}\\
1550
\comindex{Proposition}
1551
\comindex{Corollary}
1552
All these commands are synonymous of \texttt{Theorem}
1553
% Same as {\tt Theorem} except
1554
% that if this statement is in one or more levels of sections then the
1555
% name {\ident} will be accessible only prefixed by the sections names
1556
% when the sections (see \ref{Section} and \ref{LongNames}) will be
1558
% %All proofs of persistent objects (such as theorems) referring to {\ident}
1559
% %within the section will be replaced by the proof of {\ident}.
1560
% Same as {\tt Remark} except
1561
% that the innermost section name is dropped from the full name.
1562
\item {\tt Definition {\ident} : {\type}.} \\
1563
Allow to define a term of type {\type} using the proof editing mode. It
1564
behaves as {\tt Theorem} but is intended for the interactive
1565
definition of expression which computational behavior will be used by
1566
further commands. \SeeAlso~\ref{Transparent} and \ref{unfold}.
1569
\subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}
1575
\comindex{Admitted}}
1577
A proof starts by the keyword {\tt Proof}. Then {\Coq} enters the
1578
proof editing mode until the proof is completed. The proof editing
1579
mode essentially contains tactics that are described in chapter
1580
\ref{Tactics}. Besides tactics, there are commands to manage the proof
1581
editing mode. They are described in chapter \ref{Proof-handling}. When
1582
the proof is completed it should be validated and put in the
1583
environment using the keyword {\tt Qed}.
1588
\item \errindex{{\ident} already exists}
1592
\item Several statements can be simultaneously opened.
1593
\item Not only other statements but any vernacular command can be given
1594
within the proof editing mode. In this case, the command is
1595
understood as if it would have been given before the statements still to be
1597
\item {\tt Proof} is recommended but can currently be omitted. On the
1598
opposite, {\tt Qed} (or {\tt Defined}, see below) is mandatory to validate a proof.
1599
\item Proofs ended by {\tt Qed} are declared opaque (see \ref{Opaque})
1600
and cannot be unfolded by conversion tactics (see \ref{Conversion-tactics}).
1601
To be able to unfold a proof, you should end the proof by {\tt Defined}
1606
\item {\tt Proof} {\tt .} \dots {\tt Defined} {\tt .}\\
1607
Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} but the proof is
1608
then declared transparent (see \ref{Transparent}), which means it
1609
can be unfolded in conversion tactics (see \ref{Conversion-tactics}).
1610
\item {\tt Proof} {\tt .} \dots {\tt Save.}\\
1611
Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}
1612
\item {\tt Goal} \type \dots {\tt Save} \ident \\
1613
Same as {\tt Lemma} \ident {\tt :} \type \dots {\tt Save.}
1614
This is intended to be used in the interactive mode. Conversely to named
1615
lemmas, anonymous goals cannot be nested.
1616
\item {\tt Proof.} \dots {\tt Admitted.}\\
1617
Turns the current conjecture into an axiom and exits editing of
1623
% TeX-master: "Reference-Manual"
1626
% $Id: RefMan-gal.tex 9614 2007-02-07 18:43:42Z herbelin $
added
removed
refman/RefMan-gal.tex
