From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 doc/refman/RefMan-gal.tex | 1696 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 1696 insertions(+)
 create mode 100644 doc/refman/RefMan-gal.tex

(limited to 'doc/refman/RefMan-gal.tex')

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
new file mode 100644
index 00000000..d1489591
--- /dev/null
+++ b/doc/refman/RefMan-gal.tex
@@ -0,0 +1,1696 @@
+\chapter{The \gallina{} specification language
+\label{Gallina}\index{Gallina}}
+\label{BNF-syntax} % Used referred to as a chapter label
+
+This chapter describes \gallina, the specification language of {\Coq}.
+It allows to develop mathematical theories and to prove specifications
+of programs.  The theories are built from axioms, hypotheses,
+parameters, lemmas, theorems and definitions of constants, functions,
+predicates and sets. The syntax of logical objects involved in
+theories is described in Section~\ref{term}. The language of
+commands, called {\em The Vernacular} is described in section
+\ref{Vernacular}.
+
+In {\Coq}, logical objects are typed to ensure their logical
+correctness. The rules implemented by the typing algorithm are described in
+Chapter \ref{Cic}.
+
+\subsection*{About the grammars in the manual
+\index{BNF metasyntax}}
+
+Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
+set in {\tt typewriter font}.  In addition, there are special
+notations for regular expressions.
+
+An expression enclosed in square brackets \zeroone{\ldots} means at
+most one occurrence of this expression (this corresponds to an
+optional component).
+
+The notation ``\nelist{\entry}{sep}'' stands for a non empty
+sequence of expressions parsed by {\entry} and
+separated by the literal ``{\tt sep}''\footnote{This is similar to the
+expression ``{\entry} $\{$ {\tt sep} {\entry} $\}$'' in
+standard BNF, or ``{\entry}~{$($} {\tt sep} {\entry} {$)$*}'' in
+the syntax of regular expressions.}.
+
+Similarly, the notation ``\nelist{\entry}{}'' stands for a non
+empty sequence of expressions parsed by the ``{\entry}'' entry,
+without any separator between.
+
+At the end, the notation ``\sequence{\entry}{\tt sep}'' stands for a
+possibly empty sequence of expressions parsed by the ``{\entry}'' entry,
+separated by the literal ``{\tt sep}''.
+
+\section{Lexical conventions
+\label{lexical}\index{Lexical conventions}}
+
+\paragraph{Blanks}
+Space, newline and horizontal tabulation are considered as blanks.
+Blanks are ignored but they separate tokens.
+
+\paragraph{Comments}
+
+Comments in {\Coq} are enclosed between {\tt (*} and {\tt
+  *)}\index{Comments}, and can be nested. They can contain any
+character. However, string literals must be correctly closed. Comments
+are treated as blanks.
+
+\paragraph{Identifiers and access identifiers}
+
+Identifiers, written {\ident}, are sequences of letters, digits,
+\verb!_! and \verb!'!, that do not start with a digit or \verb!'!.
+That is, they are recognized by the following lexical class:
+
+\index{ident@\ident}
+\begin{center}
+\begin{tabular}{rcl} 
+{\firstletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt \_}
+$\mid$ {\tt unicode-letter}  
+\\
+{\subsequentletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt 0..9}
+$\mid$ {\tt \_} % $\mid$ {\tt \$}
+$\mid$ {\tt '} 
+$\mid$ {\tt unicode-letter}  
+$\mid$ {\tt unicode-id-part} \\
+{\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}
+\end{tabular}
+\end{center}
+All characters are meaningful. In particular, identifiers are
+case-sensitive.  The entry {\tt unicode-letter} non-exhaustively
+includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian,
+Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical
+letter-like symbols, hyphens, non-breaking space, {\ldots} The entry
+{\tt unicode-id-part} non-exhaustively includes symbols for prime
+letters and subscripts.
+
+Access identifiers, written {\accessident}, are identifiers prefixed
+by \verb!.! (dot) without blank. They are used in the syntax of qualified
+identifiers.
+
+\paragraph{Natural numbers and integers}
+Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign.
+
+\index{num@{\num}}
+\index{integer@{\integer}}
+\begin{center}
+\begin{tabular}{r@{\quad::=\quad}l}
+{\digit} & {\tt 0..9} \\
+{\num} & \nelistwithoutblank{\digit}{} \\
+{\integer} & \zeroone{\tt -}{\num} \\
+\end{tabular}
+\end{center}
+
+\paragraph[Strings]{Strings\label{strings}
+\index{string@{\qstring}}}
+Strings are delimited by \verb!"! (double quote), and enclose a
+sequence of any characters different from \verb!"! or the sequence
+\verb!""! to denote the double quote character. In grammars, the
+entry for quoted strings is {\qstring}.
+
+\paragraph{Keywords}
+The following identifiers are reserved keywords, and cannot be
+employed otherwise:
+\begin{center}
+\begin{tabular}{llllll}
+\verb!_!          &
+\verb!as!         &
+\verb!at!         &
+\verb!cofix!      &
+\verb!else!       &
+\verb!end!        \\
+%
+\verb!exists!     &
+\verb!exists2!    &
+\verb!fix!        &
+\verb!for!        &
+\verb!forall!     &
+\verb!fun!        \\
+%
+\verb!if!         &
+\verb!IF!         &
+\verb!in!         &
+\verb!let!        &
+\verb!match!      &
+\verb!mod!        \\
+%
+\verb!Prop!       &
+\verb!return!     &
+\verb!Set!        &
+\verb!then!       &
+\verb!Type!       &
+\verb!using!      \\
+%
+\verb!where!      &
+\verb!with!       &
+\end{tabular}
+\end{center}
+
+
+\paragraph{Special tokens}
+The following sequences of characters are special tokens:
+\begin{center}
+\begin{tabular}{lllllll}
+\verb/!/   &
+\verb!%!  &
+\verb!&!   &
+\verb!&&!  &
+\verb!(!   &
+\verb!()!  &
+\verb!)!   \\
+%
+\verb!*!   &
+\verb!+!   &
+\verb!++!  &
+\verb!,!   &
+\verb!-!   &
+\verb!->!  &
+\verb!.!   \\
+%
+\verb!.(!  &
+\verb!..!  &
+\verb!/!   &
+\verb!/\!  &
+\verb!:!   &
+\verb!::!  &
+\verb!:<!  \\
+%
+\verb!:=!  &
+\verb!:>!  &
+\verb!;!   &
+\verb!<!   &
+\verb!<-!  &
+\verb!<->! &
+\verb!<:!  \\
+%
+\verb!<=!  &
+\verb!<>!  &
+\verb!=!   &
+\verb!=>!  &
+\verb!=_D! &
+\verb!>!   &
+\verb!>->! \\
+%
+\verb!>=!  &
+\verb!?!   &
+\verb!?=!  &
+\verb!@!   &
+\verb![!   &
+\verb!\/!  &
+\verb!]!   \\
+%
+\verb!^!   &
+\verb!{!   &
+\verb!|!   &
+\verb!|-!  &
+\verb!||!  &
+\verb!}!   &
+\verb!~!   \\
+\end{tabular}
+\end{center}
+
+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.
+
+\section{Terms \label{term}\index{Terms}}
+
+\subsection{Syntax of terms}
+
+Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic
+set of terms which form the {\em Calculus of Inductive Constructions}
+(also called \CIC). The formal presentation of {\CIC} is given in
+Chapter \ref{Cic}. Extensions of this syntax are given in chapter
+\ref{Gallina-extension}. How to customize the syntax is described in
+Chapter \ref{Addoc-syntax}.
+
+\begin{figure}[htbp]
+\begin{centerframe}
+\begin{tabular}{lcl@{\quad~}r}  % warning: page width exceeded with \qquad 
+{\term} & ::= &
+         {\tt forall} {\binders} {\tt ,} {\term}  &(\ref{products})\\
+ & $|$ & {\tt fun} {\binders} {\tt =>} {\term} &(\ref{abstractions})\\
+ & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\
+ & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\
+ & $|$ & {\tt let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term}
+         {\tt in} {\term} &(\ref{let-in})\\
+ & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\
+ & $|$ & {\tt let cofix} {\cofixpointbody}
+         {\tt in} {\term} &(\ref{fixpoints})\\
+ & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem}
+         {\tt :=} {\term}
+         {\tt in} {\term}  &(\ref{caseanalysis}, \ref{Mult-match})\\
+ & $|$ & {\tt if} {\term} \zeroone{\ifitem} {\tt then} {\term}
+         {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
+ & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
+ & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
+ & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\
+ & $|$ & {\tt @} {\qualid} \sequence{\term}{}
+            &(\ref{Implicits-explicitation})\\
+ & $|$ & {\term} {\tt \%} {\ident} &(\ref{scopechange})\\
+ & $|$ & {\tt match} \nelist{\caseitem}{\tt ,}
+                 \zeroone{\returntype} {\tt with} &\\
+    &&   ~~~\zeroone{\zeroone{\tt |} \nelist{\eqn}{|}} {\tt end}
+    &(\ref{caseanalysis})\\
+ & $|$ & {\qualid} &(\ref{qualid})\\
+ & $|$ & {\sort} &(\ref{Gallina-sorts})\\
+ & $|$ & {\num} &(\ref{numerals})\\
+ & $|$ & {\_} &(\ref{hole})\\
+ & & &\\
+{\termarg} & ::= & {\term} &\\
+ & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )}
+         &(\ref{Implicits-explicitation})\\
+%% & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )}
+%%         &(\ref{Implicits-explicitation})\\
+&&&\\
+{\binders} & ::= & \nelist{\binder}{}  \\
+&&&\\
+{\binder} & ::= &   {\name} & (\ref{Binders}) \\
+ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\  
+ & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
+& & &\\
+{\name} & ::= & {\ident} &\\
+ & $|$ & {\tt \_} &\\
+&&&\\
+{\qualid} & ::= & {\ident} & \\
+ & $|$ & {\qualid} {\accessident} &\\
+ & & &\\
+{\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} &
+\end{tabular}
+\end{centerframe}
+\caption{Syntax of terms}
+\label{term-syntax}
+\index{term@{\term}}
+\index{sort@{\sort}}
+\end{figure}
+
+
+
+\begin{figure}[htb]
+\begin{centerframe}
+\begin{tabular}{lcl}
+{\fixpointbodies} & ::= &
+         {\fixpointbody} \\
+ & $|$ & {\fixpointbody} {\tt with} \nelist{\fixpointbody}{{\tt with}}
+         {\tt for} {\ident} \\
+{\cofixpointbodies} & ::= &
+         {\cofixpointbody} \\
+ & $|$ & {\cofixpointbody} {\tt with} \nelist{\cofixpointbody}{{\tt with}}
+         {\tt for} {\ident} \\
+&&\\
+{\fixpointbody} & ::= &
+    {\ident} {\binders} \zeroone{\annotation} {\typecstr}
+    {\tt :=} {\term} \\
+{\cofixpointbody} & ::= & {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} \\
+  & &\\
+{\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ 
+&&\\
+{\caseitem} & ::= & {\term} \zeroone{{\tt as} \name}
+     \zeroone{{\tt in} \term} \\
+&&\\
+{\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\
+&&\\
+{\returntype} & ::= & {\tt return} {\term} \\
+&&\\
+{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\
+&&\\
+{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\
+&&\\
+{\pattern} & ::= & {\qualid} \nelist{\pattern}{}  \\
+ & $|$ & {\pattern} {\tt as} {\ident}             \\
+ & $|$ & {\pattern} {\tt \%} {\ident}         \\
+ & $|$ & {\qualid}                              \\
+ & $|$ & {\tt \_}                                  \\
+ & $|$ & {\num}                                 \\
+ & $|$ & {\tt (} \nelist{\orpattern}{,} {\tt )}     \\
+\\
+{\orpattern} & ::= & \nelist{\pattern}{\tt |}\\
+\end{tabular}
+\end{centerframe}
+\caption{Syntax of terms (continued)}
+\label{term-syntax-aux}
+\end{figure}
+
+
+%%%%%%%
+
+\subsection{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}.
+\index{type@{\type}}
+
+
+\subsection{Qualified identifiers and simple identifiers
+\label{qualid}
+\label{ident}}
+
+{\em Qualified identifiers} ({\qualid}) denote {\em global constants}
+(definitions, lemmas, theorems, remarks or facts), {\em global
+variables} (parameters or axioms), {\em inductive
+types} or {\em constructors of inductive types}.
+{\em Simple identifiers} (or shortly {\ident}) are a
+syntactic subset of qualified identifiers.  Identifiers may also
+denote local {\em variables}, what qualified identifiers do not.
+
+\subsection{Numerals
+\label{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~\ref{Addoc-syntax} for details). Initially, numerals are
+bound to Peano's representation of natural numbers
+(see~\ref{libnats}).
+
+Note: negative integers are not at the same level as {\num}, for this
+would make precedence unnatural.
+
+\subsection{Sorts 
+\index{Sorts}
+\index{Type@{\Type}}
+\index{Set@{\Set}}
+\index{Prop@{\Prop}}
+\index{Sorts}
+\label{Gallina-sorts}}
+
+There are three sorts \Set, \Prop\ and \Type.
+\begin{itemize}
+\item \Prop\ is the universe of {\em logical propositions}.
+The logical propositions themselves are typing the proofs.
+We denote propositions by {\form}. This constitutes a semantic
+subclass of the syntactic class {\term}.
+\index{form@{\form}}
+\item \Set\ is is the universe of {\em program
+types} or {\em specifications}.
+The specifications themselves are typing the programs.
+We denote specifications by {\specif}. This constitutes a semantic
+subclass of the syntactic class {\term}.
+\index{specif@{\specif}}
+\item {\Type} is the type of {\Set} and {\Prop}
+\end{itemize}
+\noindent More on sorts can be found in Section~\ref{Sorts}.
+
+\bigskip
+
+{\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}.
+\index{type@{\type}}
+
+\subsection{Binders
+\label{Binders}
+\index{binders}}
+
+Various constructions such as {\tt fun}, {\tt forall}, {\tt fix} and
+{\tt cofix} {\em 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 {\tt \_}.  When the type of a
+bound variable cannot be synthesized by the system, it can be
+specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt
+)}. There is also a notation for a sequence of binding variables
+sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt
+:}\,{\type}\,{\tt )}.
+
+Some constructions allow the binding of a variable to value. This is
+called a ``let-binder''. The entry {\binder} of the grammar accepts
+either an assumption binder as defined above or a let-binder. 
+The notation in the
+latter case is {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )}. In a
+let-binder, only one variable can be introduced at the same
+time. It is also possible to give the type of the variable as follows:
+{\tt (}\,{\ident}\,{\tt :}\,{\term}\,{\tt :=}\,{\term}\,{\tt )}.
+
+Lists of {\binder} are allowed. In the case of {\tt fun} and {\tt
+  forall}, it is intended that at least one binder of the list is an
+assumption otherwise {\tt fun} and {\tt forall} gets identical. Moreover,
+parentheses can be omitted in the case of a single sequence of
+bindings sharing the same type (e.g.: {\tt fun~(x~y~z~:~A)~=>~t} can
+be shortened in {\tt fun~x~y~z~:~A~=>~t}).
+
+\subsection{Abstractions
+\label{abstractions}
+\index{abstractions}}
+
+The expression ``{\tt fun} {\ident} {\tt :} {\type} {\tt =>}~{\term}''
+defines the {\em 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. {\tt fun x:$A$
+=> x} denotes the identity function on type $A$).
+% The variable {\ident} is called the {\em parameter} of the function 
+% (we sometimes say the {\em formal parameter}).
+The keyword {\tt fun} can be followed by several binders as given in
+Section~\ref{Binders}. Functions over several variables are
+equivalent to an iteration of one-variable functions.  For instance the
+expression ``{\tt fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt
+:}~\type~{\tt =>}~{\term}'' denotes the same function as ``{\tt
+fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt =>}~{\ldots}~{\tt
+fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}''. If a let-binder
+occurs in the list of binders, it is expanded to a local definition
+(see Section~\ref{let-in}).
+
+\subsection{Products
+\label{products}
+\index{products}}
+
+The expression ``{\tt forall}~{\ident}~{\tt :}~{\type}{\tt
+,}~{\term}'' denotes the {\em product} of the variable {\ident} of
+type {\type}, over the term {\term}. As for abstractions, {\tt forall}
+is followed by a binder list, and products over several variables are
+equivalent to an iteration of one-variable products. 
+Note that {\term} is intended to be a type.
+
+If the variable {\ident} occurs in {\term}, the product is called {\em
+dependent product}.  The intention behind a dependent product {\tt
+forall}~$x$~{\tt :}~{$A$}{\tt ,}~{$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$ {\tt ->}
+$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The non dependent
+product is used both to denote the propositional implication and
+function types.
+
+\subsection{Applications
+\label{applications}
+\index{applications}}
+
+The expression \term$_0$ \term$_1$ denotes the application of
+\term$_0$ to \term$_1$.
+
+The expression {\tt }\term$_0$ \term$_1$ ...  \term$_n${\tt}
+denotes the application of the term \term$_0$ to the arguments
+\term$_1$ ... then \term$_n$.  It is equivalent to {\tt (} {\ldots}
+{\tt (} {\term$_0$} {\term$_1$} {\tt )} {\ldots} {\tt )} {\term$_n$} {\tt }:
+associativity is to the left.
+
+The notation {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )} for
+arguments is used for making explicit the value of implicit arguments
+(see Section~\ref{Implicits-explicitation}).
+
+\subsection{Type cast
+\label{typecast}
+\index{Cast}}
+
+The expression ``{\term}~{\tt :}~{\type}'' is a type cast
+expression. It enforces the type of {\term} to be {\type}.
+
+\subsection{Inferable subterms
+\label{hole}
+\index{\_}}
+
+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.
+
+\subsection{Local definitions (let-in)
+\label{let-in}
+\index{Local definitions}
+\index{let-in}}
+
+
+{\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes
+the local binding of \term$_1$ to the variable $\ident$ in
+\term$_2$. 
+There is a syntactic sugar for local definition of functions: {\tt
+let} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} {\tt :=} {\term$_1$}
+{\tt in} {\term$_2$} stands for {\tt let} {\ident} {\tt := fun}
+{\binder$_1$} {\ldots} {\binder$_n$} {\tt =>} {\term$_2$} {\tt in}
+{\term$_2$}.
+
+\subsection{Definition by case analysis
+\label{caseanalysis}
+\index{match@{\tt match\ldots with\ldots end}}}
+
+Objects of inductive types can be destructurated by a case-analysis
+construction called {\em pattern-matching} expression.  A
+pattern-matching expression is used to analyze the structure of an
+inductive objects and to apply specific treatments accordingly.
+
+This paragraph describes the basic form of pattern-matching. See
+Section~\ref{Mult-match} and Chapter~\ref{Mult-match-full} for the
+description of the general form. The basic form of pattern-matching is
+characterized by a single {\caseitem} expression, a {\multpattern}
+restricted to a single {\pattern} and {\pattern} restricted to the
+form {\qualid} \nelist{\ident}{}.
+
+The expression {\tt match} {\term$_0$} {\returntype} {\tt with}
+{\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$}
+{\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em
+pattern-matching} over the term {\term$_0$} (expected to be of an
+inductive type $I$).  The terms {\term$_1$}\ldots{\term$_n$} are the
+{\em branches} of the pattern-matching expression. Each of
+{\pattern$_i$} has a form \qualid~\nelist{\ident}{} where {\qualid}
+must denote a constructor. There should be exactly one branch for
+every constructor of $I$.
+
+The {\returntype} expresses the type returned by the whole {\tt match}
+expression. There are several cases.  In the {\em non dependent} case,
+all branches have the same type, and the {\returntype} is the common
+type of branches. In this case, {\returntype} can usually be omitted
+as it can be inferred from the type of the branches\footnote{Except if
+the inductive type is empty in which case there is no equation that can be 
+used to infer the return type.}.
+
+In the {\em 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 ``{\tt as {\ident}}''
+clause where {\ident} is dependent in the return type.
+For instance, in the following example:
+\begin{coq_example*}
+Inductive bool : Type := true : bool | false : bool.
+Inductive eq (A:Type) (x:A) : A -> Prop := refl_equal : eq A x x.
+Inductive or (A:Prop) (B:Prop) : Prop :=
+| or_introl : A -> or A B
+| or_intror : B -> or A B.
+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)
+                (refl_equal bool true)
+   | false => or_intror (eq bool false true) (eq bool false false)
+                (refl_equal bool false)
+   end.
+\end{coq_example*}
+the branches have respective types {\tt or (eq bool true true) (eq
+bool true false)} and {\tt or (eq bool false true) (eq bool false
+false)} while the whole pattern-matching expression has type {\tt or
+(eq bool b true) (eq bool b false)}, the identifier {\tt x} being used
+to represent the dependency.  Remark that when the term being matched
+is a variable, the {\tt 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.
+\begin{coq_example*}
+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)
+                (refl_equal bool true)
+   | false => or_intror (eq bool false true) (eq bool false false)
+                (refl_equal bool false)
+   end.
+\end{coq_example*}
+
+The second subcase is only relevant for annotated inductive types such
+as the equality predicate (see Section~\ref{Equality}), the order
+predicate on natural numbers % (see Section~\ref{le}) % undefined reference
+or the type of
+lists of a given length (see Section~\ref{listn}). 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 {\tt
+``in~I~\_~$\ldots$~\_~\ident$_1$~$\ldots$~\ident$_n$}'' clause, where
+\begin{itemize}
+\item $I$ is the inductive type of the term being matched;
+
+\item the names \ident$_i$'s correspond to the arguments of the
+inductive type that carry the annotations: the return type is dependent
+on them;
+
+\item the {\_}'s denote the family parameters of the inductive type:
+the return type is not dependent on them.
+\end{itemize}
+
+For instance, in the following example:
+\begin{coq_example*}
+Definition sym_equal (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
+  | refl_equal => refl_equal A x
+  end.
+\end{coq_example*}
+the type of the branch has type {\tt eq~A~x~x} because the third
+argument of {\tt eq} is {\tt x} in the type of the pattern {\tt
+refl\_equal}. On the contrary, the type of the whole pattern-matching
+expression has type {\tt eq~A~y~x} because the third argument of {\tt
+eq} is {\tt y} in the type of {\tt H}. This dependency of the case
+analysis in the third argument of {\tt eq} is expressed by the
+identifier {\tt 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 {\tt as} and {\tt in} are available.
+ 
+There are specific notations for case analysis on types with one or
+two constructors: ``{\tt if {\ldots} then {\ldots} else {\ldots}}''
+and ``{\tt let (}\nelist{\ldots}{,}{\tt ) := } {\ldots} {\tt in}
+{\ldots}'' (see Sections~\ref{if-then-else} and~\ref{Letin}).
+
+%\SeeAlso Section~\ref{Mult-match} for convenient extensions of pattern-matching.
+
+\subsection{Recursive functions
+\label{fixpoints}
+\index{fix@{fix \ident$_i$\{\dots\}}}}
+
+The expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$}
+\texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$
+\binder$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for}
+{\ident$_i$}'' denotes the $i$\nth component of a block of functions
+defined by mutual well-founded recursion. It is the local counterpart
+of the {\tt Fixpoint} command. See Section~\ref{Fixpoint} for more
+details. When $n=1$, the ``{\tt for}~{\ident$_i$}'' clause is omitted.
+
+The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :}
+{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binder$_n$ {\tt
+:} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$\nth component of
+a block of terms defined by a mutual guarded co-recursion. It is the
+local counterpart of the {\tt CoFixpoint} command. See
+Section~\ref{CoFixpoint} for more details. When $n=1$, the ``{\tt
+for}~{\ident$_i$}'' clause is omitted.
+
+The association of a single fixpoint and a local
+definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
+  :=}~{\ldots}~{\tt in}~{\ldots}'' stands for ``{\tt let}~$f$~{\tt :=
+  fix}~$f$~\ldots~{\tt :=}~{\ldots}~{\tt in}~{\ldots}''. The same
+  applies for co-fixpoints.
+
+
+\section{The Vernacular
+\label{Vernacular}}
+
+\begin{figure}[tbp]
+\begin{centerframe}
+\begin{tabular}{lcl}
+{\sentence} & ::= & {\assumption} \\
+            & $|$ & {\definition} \\
+            & $|$ & {\inductive} \\
+            & $|$ & {\fixpoint} \\
+            & $|$ & {\assertion} {\proof} \\
+&&\\
+%% Assumptions
+{\assumption} & ::= & {\assumptionkeyword} {\assums} {\tt .} \\
+&&\\
+{\assumptionkeyword} & $\!\!$ ::= & {\tt Axiom} $|$ {\tt Conjecture} \\
+  & $|$  & {\tt Parameter} $|$  {\tt Parameters} \\
+  & $|$  & {\tt Variable}  $|$ {\tt Variables}  \\
+  & $|$  & {\tt Hypothesis}  $|$ {\tt Hypotheses}\\
+&&\\
+{\assums} & ::= & \nelist{\ident}{} {\tt :} {\term} \\
+          & $|$ & \nelist{{\tt (} \nelist{\ident}{} {\tt :} {\term} {\tt )}}{} \\
+&&\\
+%% Definitions
+{\definition} & ::= & 
+         {\tt Definition} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\
+ & $|$ & {\tt Let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\
+&&\\
+%% Inductives
+{\inductive} & ::= & 
+           {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
+ & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
+           & & \\
+{\inductivebody} & ::= & 
+  {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\
+   && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\
+           & & \\  %% TODO: where ...
+%% Fixpoints
+{\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\
+       & $|$ &  {\tt CoFixpoint} \nelist{\cofixpointbody}{with} {\tt .} \\
+&&\\
+%% Lemmas & proofs
+{\assertion} & ::= &
+  {\statkwd} {\ident} \zeroone{\binders} {\tt :} {\term} {\tt .} \\
+&&\\
+  {\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} \\
+   & $|$ & {\tt Remark} $|$ {\tt Fact}\\
+   & $|$ & {\tt Corollary} $|$ {\tt Proposition} \\
+   & $|$ & {\tt Definition} $|$ {\tt Example} \\\\
+&&\\
+{\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\
+   & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\
+   & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}\\
+\end{tabular}
+\end{centerframe}
+\caption{Syntax of sentences}
+\label{sentences-syntax}
+\end{figure}
+
+Figure \ref{sentences-syntax} describes {\em The Vernacular} which is the
+language of commands of \gallina.  A sentence of the vernacular
+language, like in many natural languages, begins with a capital letter
+and ends with a dot.
+
+The different kinds of command are described hereafter. They all suppose
+that the terms occurring in the sentences are well-typed.
+
+%%
+%% Axioms and Parameters
+%%
+\subsection{Assumptions
+\index{Declarations}
+\label{Declarations}}
+
+Assumptions extend the environment\index{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}.
+
+\subsubsection{{\tt Axiom {\ident} :{\term} .}
+\comindex{Axiom}
+\label{Axiom}}
+
+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.
+
+\begin{ErrMsgs}
+\item \errindex{{\ident} already exists}
+\end{ErrMsgs}
+
+\begin{Variants} 
+\item \comindex{Parameter}\comindex{Parameters}
+  {\tt Parameter {\ident} :{\term}.} \\
+  Is equivalent to {\tt Axiom {\ident} : {\term}}
+
+\item {\tt Parameter {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
+  Adds $n$ parameters with specification {\term}
+
+\item
+ {\tt Parameter\,%
+(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
+\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
+{\term$_n$} {\tt )}.}\\ 
+  Adds $n$ blocks of parameters with different specifications.
+
+\item \comindex{Conjecture}
+  {\tt Conjecture {\ident} :{\term}.}\\
+  Is equivalent to {\tt Axiom {\ident} : {\term}}.
+\end{Variants}
+
+\noindent {\bf Remark: } It is possible to replace {\tt Parameter} by
+{\tt Parameters}.
+
+
+\subsubsection{{\tt Variable {\ident} :{\term}}.
+\comindex{Variable}
+\comindex{Variables}
+\label{Variable}}
+
+This command links {\term} to the name {\ident} in the context of the
+current section (see Section~\ref{Section} for a description of the section
+mechanism). When the current section is closed, name {\ident} will be
+unknown and every object using this variable will be explicitly
+parametrized (the variable is {\em discharged}). Using the {\tt
+Variable} command out of any section is equivalent to using {\tt Parameter}.
+
+\begin{ErrMsgs}
+\item \errindex{{\ident} already exists}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Variable {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
+  Links {\term} to names {\ident$_1$}\ldots{\ident$_n$}.
+\item
+ {\tt Variable\,%
+(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
+\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
+{\term$_n$} {\tt )}.}\\ 
+  Adds $n$ blocks of variables with different specifications.
+\item \comindex{Hypothesis}
+      \comindex{Hypotheses}
+ {\tt Hypothesis {\ident} {\tt :}{\term}.} \\
+  \texttt{Hypothesis} is a synonymous of \texttt{Variable}
+\end{Variants}
+
+\noindent {\bf Remark: } It is possible to replace {\tt Variable} by
+{\tt Variables} and {\tt Hypothesis} by {\tt Hypotheses}.
+
+It is advised to use the keywords \verb:Axiom: and \verb:Hypothesis:
+for logical postulates (i.e. when the assertion {\term} is of sort
+\verb:Prop:), and to use the keywords \verb:Parameter: and
+\verb:Variable: in other cases (corresponding to the declaration of an
+abstract mathematical entity).
+
+%%
+%% Definitions
+%%
+\subsection{Definitions
+\index{Definitions}
+\label{Basic-definitions}}
+
+Definitions extend the environment\index{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\index{delta-reduction@$\delta$-reduction} (see
+Section~\ref{delta}).  A definition is accepted by the system if and
+only if the defined term is well-typed in the current context of the
+definition and if the name is not already used. The name defined by
+the definition is called a {\em constant}\index{Constant} and the term
+it refers to is its {\em body}.  A definition has a type which is the
+type of its body.
+
+A formal presentation of constants and environments is given in
+Section~\ref{Typed-terms}.
+
+\subsubsection{\tt Definition {\ident} := {\term}.
+\comindex{Definition}}
+
+This command binds {\term} to the name {\ident} in the
+environment, provided that {\term} is well-typed.
+
+\begin{ErrMsgs}
+\item \errindex{{\ident} already exists}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Definition {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
+  It checks that the type of {\term$_2$} is definitionally equal to
+  {\term$_1$}, and registers {\ident} as being of type {\term$_1$},
+  and bound to value {\term$_2$}.
+\item {\tt Definition {\ident} {\binder$_1$}\ldots{\binder$_n$}
+       {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
+  This is equivalent to \\
+   {\tt Definition\,{\ident}\,{\tt :\,forall}\,%
+       {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
+       {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
+       {\tt .}
+
+\item {\tt Example {\ident} := {\term}.}\\
+{\tt Example {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
+{\tt Example {\ident} {\binder$_1$}\ldots{\binder$_n$}
+       {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
+\comindex{Example}
+These are synonyms of the {\tt Definition} forms.
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{Error: The term {\term} has type {\type} while it is expected to have type {\type}}
+\end{ErrMsgs}
+
+\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}.
+
+\subsubsection{\tt Let {\ident} := {\term}.
+\comindex{Let}}
+
+This command binds the value {\term} to the name {\ident} in the
+environment of the current section. The name {\ident} disappears
+when the current section is eventually closed, and, all
+persistent objects (such as theorems) defined within the
+section and depending on {\ident} are prefixed by the local definition
+{\tt let {\ident} := {\term} in}.
+
+\begin{ErrMsgs}
+\item \errindex{{\ident} already exists}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.}
+\end{Variants}
+
+\SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque},
+\ref{Transparent} (opaque/transparent constants), \ref{unfold} (tactic
+    {\tt unfold}).
+
+%%
+%% Inductive Types
+%%
+\subsection{Inductive definitions
+\index{Inductive definitions} 
+\label{gal_Inductive_Definitions}
+\comindex{Inductive}
+\label{Inductive}}
+
+We gradually explain simple inductive types, simple
+annotated inductive types, simple parametric inductive types, 
+mutually inductive types. We explain also co-inductive types.
+
+\subsubsection{Simple inductive types}
+
+The definition of a simple inductive type has the following form:
+
+\medskip
+{\tt 
+\begin{tabular}{l}
+Inductive {\ident} : {\sort} :=  \\
+\begin{tabular}{clcl}
+   & {\ident$_1$}  &:& {\type$_1$} \\
+ | & {\ldots} && \\
+ | & {\ident$_n$} &:& {\type$_n$}
+\end{tabular}
+\end{tabular}
+}
+\medskip
+
+The name {\ident} is the name of the inductively defined type and
+{\sort} is the universes where it lives.
+The names {\ident$_1$}, {\ldots}, {\ident$_n$}
+are the names of its constructors and {\type$_1$}, {\ldots},
+{\type$_n$} their respective types. The types of the constructors have
+to satisfy a {\em positivity condition} (see Section~\ref{Positivity})
+for {\ident}.  This condition ensures the soundness of the inductive
+definition.  If this is the case, the constants {\ident},
+{\ident$_1$}, {\ldots}, {\ident$_n$} are added to the environment with
+their respective types.  Accordingly to the universe where
+the inductive type lives ({\it e.g.} its type {\sort}), {\Coq} provides a
+number of destructors for {\ident}.  Destructors are named
+{\ident}{\tt\_ind}, {\ident}{\tt \_rec} or {\ident}{\tt \_rect} which
+respectively correspond to elimination principles on {\tt Prop}, {\tt
+Set} and {\tt 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 {\tt Inductive} definitions.
+
+The set of natural numbers is defined as:
+\begin{coq_example}
+Inductive nat : Set :=
+  | O : nat
+  | S : nat -> nat.
+\end{coq_example}
+
+The type {\tt nat} is defined as the least \verb:Set: containing {\tt
+  O} and closed by the {\tt S} constructor. The constants {\tt nat},
+{\tt O} and {\tt S} are added to the environment.
+
+Now let us have a look at the elimination principles. They are three
+of them:
+{\tt nat\_ind}, {\tt nat\_rec} and {\tt nat\_rect}.  The type of {\tt
+  nat\_ind} is:
+\begin{coq_example}
+Check nat_ind.
+\end{coq_example}
+
+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 ({\tt
+forall n:nat, P n}) by induction on {\tt n}.
+
+The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except
+that they pertain to {\tt (P:nat->Set)} and {\tt (P:nat->Type)}
+respectively . They correspond to primitive induction principles
+(allowing dependent types) respectively over sorts \verb:Set: and
+\verb:Type:. The constant {\ident}{\tt \_ind} is always provided,
+whereas {\ident}{\tt \_rec} and {\ident}{\tt \_rect} can be impossible
+to derive (for example, when {\ident} is a proposition).
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{Variants}
+\item 
+\begin{coq_example*}
+Inductive nat : Set := O | S (_:nat).
+\end{coq_example*}
+In the case where inductive types have no annotations (next section
+gives an example of such annotations), 
+%the positivity condition implies that 
+a constructor can be defined by only giving the type of
+its arguments.
+\end{Variants}
+
+\subsubsection{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:
+
+\begin{coq_example}
+Inductive even : nat -> Prop :=
+  | even_0 : even O
+  | even_SS : forall n:nat, even n -> even (S (S n)).
+\end{coq_example}
+
+The type {\tt nat->Prop} means that {\tt even} is a unary predicate
+(inductively defined) over natural numbers.  The type of its two
+constructors are the defining clauses of the predicate {\tt even}. The
+type of {\tt even\_ind} is:
+
+\begin{coq_example}
+Check even_ind.
+\end{coq_example}
+
+From a mathematical point of view it asserts that the natural numbers
+satisfying the predicate {\tt even} are exactly in the smallest set of
+naturals satisfying the clauses {\tt even\_0} or {\tt even\_SS}. This
+is why, when we want to prove any predicate {\tt P} over elements of
+{\tt even}, it is enough to prove it for {\tt O} and to prove that if
+any natural number {\tt n} satisfies {\tt P} its double successor {\tt
+  (S (S n))} satisfies also {\tt P}. This is indeed analogous to the
+structural induction principle we got for {\tt nat}.
+
+\begin{ErrMsgs}
+\item \errindex{Non strictly positive occurrence of {\ident} in {\type}}
+\item \errindex{The conclusion of {\type} is not valid; it must be
+built from {\ident}}
+\end{ErrMsgs}
+
+\subsubsection{Parametrized inductive types}
+In the previous example, each constructor introduces a
+different instance of the predicate {\tt even}. In some cases, 
+all the constructors introduces the same generic instance of the
+inductive definition, in which case, instead of an annotation, we use
+a context of parameters which are binders shared by all the
+constructors of the definition.
+
+% Inductive types may be parameterized. Parameters differ from inductive
+% type annotations in the fact that recursive invokations of inductive
+% types must always be done with the same values of parameters as its
+% specification.
+
+The general scheme is:
+\begin{center}
+{\tt Inductive} {\ident} {\binder$_1$}\ldots{\binder$_k$} : {\term} :=
+    {\ident$_1$}: {\term$_1$} | {\ldots} | {\ident$_n$}: \term$_n$
+{\tt .}
+\end{center}
+Parameters differ from inductive type annotations in the fact that the
+conclusion of each type of constructor {\term$_i$} invoke the inductive
+type with the same values of parameters as its specification.
+
+
+
+A typical example is the definition of polymorphic lists:
+\begin{coq_example*}
+Inductive list (A:Set) : Set :=
+  | nil : list A
+  | cons : A -> list A -> list A.
+\end{coq_example*}
+
+Note that in the type of {\tt nil} and {\tt cons}, we write {\tt
+  (list A)} and not just {\tt list}.\\ The constants {\tt nil} and
+{\tt cons} will have respectively types:
+
+\begin{coq_example}
+Check nil.
+Check cons.
+\end{coq_example}
+
+Types of destructors are also quantified with {\tt (A:Set)}.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{Variants}
+\item
+\begin{coq_example*}
+Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
+\end{coq_example*}
+This is an alternative definition of lists where we specify the
+arguments of the constructors rather than their full type.
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{The {\num}th argument of {\ident} must be {\ident'} in
+{\type}}
+\end{ErrMsgs}
+
+\paragraph{New from \Coq{} V8.1} The condition on parameters for
+inductive definitions has been relaxed since \Coq{} V8.1. It is now
+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~:
+\begin{coq_example}
+Inductive list2 (A:Set) : Set :=
+  | nil2 : list2 A
+  | cons2 : A -> list2 (A*A) -> list2 A.
+\end{coq_example}
+\begin{coq_eval}
+Reset list2.
+\end{coq_eval}
+that can also be written by specifying only the type of the arguments:
+\begin{coq_example*}
+Inductive list2 (A:Set) : Set := nil2 | cons2 (_:A) (_:list2 (A*A)).
+\end{coq_example*}
+But the following definition will give an error:
+\begin{coq_example}
+Inductive listw (A:Set) : Set :=
+  | nilw : listw (A*A)
+  | consw : A -> listw (A*A) -> listw (A*A).
+\end{coq_example}
+Because the conclusion of the type of constructors should be {\tt
+  listw A} in both cases. 
+
+A parametrized 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.
+
+\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{Tac-induction}.
+
+
+\subsubsection{Mutually defined inductive types
+\comindex{Inductive}
+\label{Mutual-Inductive}}
+
+The definition of a block of mutually inductive types has the form:
+
+\medskip
+{\tt 
+\begin{tabular}{l}
+Inductive {\ident$_1$} : {\type$_1$} :=  \\
+\begin{tabular}{clcl}
+   & {\ident$_1^1$}     &:& {\type$_1^1$} \\
+ | & {\ldots} && \\
+ | & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$}
+\end{tabular}  \\
+with\\
+~{\ldots} \\
+with {\ident$_m$} : {\type$_m$} := \\
+\begin{tabular}{clcl}
+   & {\ident$_1^m$}     &:& {\type$_1^m$} \\
+ | & {\ldots} \\
+ | & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}.
+\end{tabular}
+\end{tabular}
+}
+\medskip
+
+\noindent It has the same semantics as the above {\tt Inductive}
+definition for each \ident$_1$, {\ldots}, \ident$_m$. All names
+\ident$_1$, {\ldots}, \ident$_m$ and \ident$_1^1$, \dots,
+\ident$_{n_m}^m$ are simultaneously added to the environment. Then
+well-typing of constructors can be checked. Each one of the
+\ident$_1$, {\ldots}, \ident$_m$ can be used on its own.
+
+It is also possible to parametrize these inductive definitions.
+However, parameters correspond to a local
+context in which the whole set of inductive declarations is done.  For
+this reason, the parameters must be strictly the same for each
+inductive types The extended syntax is:
+
+\medskip
+{\tt 
+\begin{tabular}{l}
+Inductive {\ident$_1$} {\params} : {\type$_1$} :=  \\
+\begin{tabular}{clcl}
+   & {\ident$_1^1$}     &:& {\type$_1^1$} \\
+ | & {\ldots} && \\
+ | & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$}
+\end{tabular}  \\
+with\\
+~{\ldots} \\
+with {\ident$_m$} {\params} : {\type$_m$} := \\
+\begin{tabular}{clcl}
+   & {\ident$_1^m$}     &:& {\type$_1^m$} \\
+ | & {\ldots} \\
+ | & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}.
+\end{tabular}
+\end{tabular}
+}
+\medskip
+
+\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.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Variables A B : Set.
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | leaf : B -> forest
+  | cons : tree -> forest -> forest.
+\end{coq_example*}
+
+This declaration generates automatically six induction
+principles. They are respectively 
+called {\tt tree\_rec}, {\tt tree\_ind}, {\tt
+  tree\_rect}, {\tt forest\_rec}, {\tt forest\_ind}, {\tt
+  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 {\tt
+  tree\_rec} and {\tt forest\_rec}.
+
+\begin{coq_example}
+Check tree_rec.
+Check forest_rec.
+\end{coq_example}
+
+Assume we want to parametrize our mutual inductive definitions with
+the two type variables $A$ and $B$, the declaration should be done the
+following way:
+
+\begin{coq_eval}
+Reset tree.
+\end{coq_eval}
+\begin{coq_example*}
+Inductive tree (A B:Set) : Set :=
+    node : A -> forest A B -> tree A B
+with forest (A B:Set) : Set :=
+  | leaf : B -> forest A B
+  | cons : tree A B -> forest A B -> forest A B.
+\end{coq_example*}
+
+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. 
+
+\SeeAlso Section~\ref{Section}.
+
+\subsubsection{Co-inductive types
+\label{CoInductiveTypes}
+\comindex{CoInductive}}
+
+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
+{\it finite} number of 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 \texttt{CoInductive} command:
+\begin{coq_example}
+CoInductive Stream : Set :=
+    Seq : nat -> Stream -> Stream.
+\end{coq_example}
+
+The syntax of this command is the same as the command \texttt{Inductive}
+(see Section~\ref{gal_Inductive_Definitions}). 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
+\texttt{hd:Stream->nat} and \texttt{tl:Str->Str} can be defined as
+follows:
+\begin{coq_example}
+Definition hd (x:Stream) := let (a,s) := x in a.
+Definition tl (x:Stream) := let (a,s) := x in s.
+\end{coq_example}
+
+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:
+
+\begin{coq_example}
+CoInductive EqSt : Stream -> Stream -> Prop :=
+    eqst :
+      forall s1 s2:Stream,
+        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
+\end{coq_example}
+
+In order to prove the extensionally equality of two streams $s_1$ and
+$s_2$ we have to construct an infinite proof of equality, that is,
+an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see
+how to introduce infinite objects in Section~\ref{CoFixpoint}.
+
+%%
+%% (Co-)Fixpoints
+%%
+\subsection{Definition of recursive functions}
+
+\subsubsection{Definition of functions by recursion over inductive objects}
+
+This section describes the primitive form of definition by recursion
+over inductive objects. See Section~\ref{Function} for more advanced
+constructions. The command:
+\begin{center}
+  \texttt{Fixpoint {\ident} {\params} {\tt \{struct}
+  \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ 
+  \comindex{Fixpoint}\label{Fixpoint}}
+\end{center}
+allows to define functions by pattern-matching over inductive objects 
+using a fixed point construction.
+The meaning of this declaration is to define {\it ident} a recursive
+function with arguments specified by the binders in {\params} such
+that {\it ident} applied to arguments corresponding to these binders
+has type \type$_0$, and is equivalent to the expression \term$_0$. The
+type of the {\ident} is consequently {\tt forall {\params} {\tt,}
+  \type$_0$} and the value is equivalent to {\tt fun {\params} {\tt
+    =>} \term$_0$}.
+
+To be accepted, a {\tt Fixpoint} definition has to satisfy some
+syntactical constraints on a special argument called the decreasing
+argument. They are needed to ensure that the {\tt Fixpoint} definition
+always terminates. The point of the {\tt \{struct \ident {\tt \}}}
+annotation is to let the user tell the system which argument decreases
+along the recursive calls. For instance, one can define the addition 
+function as :
+
+\begin{coq_example}
+Fixpoint add (n m:nat) {struct n} : nat :=
+  match n with
+  | O => m
+  | S p => S (add p m)
+  end.
+\end{coq_example}
+
+The {\tt \{struct \ident {\tt \}}} annotation may be left implicit, in
+this case the system try successively arguments from left to right
+until it finds one that satisfies the decreasing condition. Note that
+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.
+
+The {\tt match} operator matches a value (here \verb: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 \verb:n:
+equals \verb:O: we return \verb:m:, and when \verb:n: equals 
+\verb:(S p): we return \verb:(S (add p m)):.
+
+The {\tt match} operator is formally described
+in detail in Section~\ref{Caseexpr}.  The system recognizes that in
+the inductive call {\tt (add p m)} the first argument actually
+decreases because it is a {\em pattern variable} coming from {\tt match
+  n with}.
+
+\Example The following definition is not correct and generates an
+error message:
+
+\begin{coq_eval}
+Set Printing Depth 50.
+(********** The following is not correct and should produce **********)
+(*********      Error: Recursive call to wrongplus ...      **********)
+\end{coq_eval}
+\begin{coq_example}
+Fixpoint wrongplus (n m:nat) {struct n} : nat :=
+  match m with
+  | O => n
+  | S p => S (wrongplus n p)
+  end.
+\end{coq_example}
+
+because the declared decreasing argument {\tt n} actually does not
+decrease in the recursive call.  The function computing the addition
+over the second argument should rather be written:
+
+\begin{coq_example*}
+Fixpoint plus (n m:nat) {struct m} : nat :=
+  match m with
+  | O => n
+  | S p => S (plus n p)
+  end.
+\end{coq_example*}
+
+The ordinary match operation on natural numbers can be mimicked in the
+following way.
+\begin{coq_example*}
+Fixpoint nat_match 
+  (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C :=
+  match n with
+  | O => f0
+  | S p => fS p (nat_match C f0 fS p)
+  end.
+\end{coq_example*}
+The recursive call may not only be on direct subterms of the recursive
+variable {\tt n} but also on a deeper subterm and we can directly
+write the function {\tt mod2} which gives the remainder modulo 2 of a
+natural number.
+\begin{coq_example*}
+Fixpoint mod2 (n:nat) : nat :=
+  match n with
+  | O => O
+  | S p => match p with
+           | O => S O
+           | S q => mod2 q
+           end
+  end.
+\end{coq_example*}
+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.
+
+The {\tt Fixpoint} construction enjoys also the {\tt with} extension
+to define functions over mutually defined inductive types or more
+generally any mutually recursive definitions.
+
+\begin{Variants}
+\item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\
+        with {\ldots} \\
+        with {\ident$_m$} {\params$_m$} :{\type$_m$} :=  {\term$_m$}}\\
+        Allows to define simultaneously {\ident$_1$}, {\ldots},
+        {\ident$_m$}.
+\end{Variants}
+
+\Example 
+The size of trees and forests can be defined the following way: 
+\begin{coq_eval}
+Reset Initial.
+Variables A B : Set.
+Inductive tree : Set :=
+    node : A -> forest -> tree
+with forest : Set :=
+  | leaf : B -> forest
+  | cons : tree -> forest -> forest.
+\end{coq_eval}
+\begin{coq_example*}
+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.
+\end{coq_example*}
+A generic command {\tt Scheme} is useful to build automatically various
+mutual induction principles. It is described in Section~\ref{Scheme}.
+
+\subsubsection{Definitions of recursive objects in co-inductive types}
+
+The command:
+\begin{center}
+  \texttt{CoFixpoint {\ident} : \type$_0$ := \term$_0$}
+  \comindex{CoFixpoint}\label{CoFixpoint}
+\end{center}
+introduces a method for constructing an infinite object of a
+coinduc\-tive type. For example, the stream containing all natural
+numbers can be introduced applying the following method to the number
+\texttt{O} (see Section~\ref{CoInductiveTypes} for the definition of
+{\tt Stream}, {\tt hd} and {\tt tl}):
+\begin{coq_eval}
+Reset Initial.
+CoInductive Stream : Set :=
+    Seq : nat -> Stream -> Stream.
+Definition hd (x:Stream) := match x with
+                            | Seq a s => a
+                            end.
+Definition tl (x:Stream) := match x with
+                            | Seq a s => s
+                            end.
+\end{coq_eval}
+\begin{coq_example}
+CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
+\end{coq_example}
+
+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 \texttt{from} is guarded by an
+application of \texttt{Seq}. On the contrary, the following recursive
+function does not satisfy the guard condition:
+
+\begin{coq_eval}
+Set Printing Depth 50.
+(********** The following is not correct and should produce **********)
+(***************** Error: Unguarded recursive call *******************)
+\end{coq_eval}
+\begin{coq_example}
+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).
+\end{coq_example}
+
+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 analysis expression.  In
+any other context, it is considered as a canonical expression which is
+completely evaluated. We can test this using the command
+\texttt{Eval}, which computes the normal forms of a term:
+
+\begin{coq_example}
+Eval compute in (from 0).
+Eval compute in (hd (from 0)).
+Eval compute in (tl (from 0)).
+\end{coq_example}
+
+\begin{Variants}
+\item{\tt CoFixpoint {\ident$_1$} {\params} :{\type$_1$} :=
+  {\term$_1$}}\\ As for most constructions, arguments of co-fixpoints
+  expressions can be introduced before the {\tt :=} sign.
+\item{\tt CoFixpoint {\ident$_1$} :{\type$_1$} := {\term$_1$}\\
+     with\\
+        \mbox{}\hspace{0.1cm} $\ldots$  \\
+        with {\ident$_m$}   : {\type$_m$} := {\term$_m$}}\\
+As in the \texttt{Fixpoint} command (see Section~\ref{Fixpoint}), it
+is possible to introduce a block of mutually dependent methods.
+\end{Variants}
+
+%%
+%% Theorems & Lemmas
+%%
+\subsection{Assertions and proofs}
+\label{Assertions}
+
+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~\ref{Proof-handling} and the tactics in Chapter~\ref{Tactics}.
+The basic assertion command is:
+
+\subsubsection{\tt Theorem {\ident} \zeroone{\binders} : {\type}.
+\comindex{Theorem}}
+
+After the statement is asserted, {\Coq} needs a proof. Once a proof of
+{\type} under the assumptions represented by {\binders} is given and
+validated, the proof is generalized into a proof of {\tt forall
+  \zeroone{\binders}, {\type}} and the theorem is bound to the name
+{\ident} in the environment.
+
+\begin{ErrMsgs}
+
+\item \errindex{The term {\form} has type {\ldots} which should be Set,
+    Prop or Type}
+
+\item \errindexbis{{\ident} already exists}{already exists}
+ 
+  The name you provided is already defined. You have then to choose
+  another name.
+
+\end{ErrMsgs}
+
+\begin{Variants} 
+\item {\tt Lemma {\ident} \zeroone{\binders} : {\type}.}\comindex{Lemma}\\
+  {\tt Remark {\ident} \zeroone{\binders} : {\type}.}\comindex{Remark}\\
+  {\tt Fact {\ident} \zeroone{\binders} : {\type}.}\comindex{Fact}\\
+  {\tt Corollary {\ident} \zeroone{\binders} : {\type}.}\comindex{Corollary}\\
+  {\tt Proposition {\ident} \zeroone{\binders} : {\type}.}\comindex{Proposition}
+
+These commands are synonyms of \texttt{Theorem {\ident} \zeroone{\binders} : {\type}}.
+
+\item {\tt Theorem \nelist{{\ident} \zeroone{\binders}: {\type}}{with}.}
+
+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 {\tt Fixpoint} or {\tt CoFixpoint}
+(see Section~\ref{CoFixpoint}) 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 {\tt Fixpoint} or {\tt CoFixpoint} definition, the induction
+hypotheses have to be used on {\em structurally smaller} arguments
+(for a {\tt Fixpoint}) or be {\em guarded by a constructor} (for a {\tt
+  CoFixpoint}).  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 command
+{\tt Guarded} (see Section~\ref{Guarded}).
+
+The command can be used also with {\tt Lemma},
+{\tt Remark}, etc. instead of {\tt Theorem}.
+
+\item {\tt Definition {\ident} \zeroone{\binders} : {\type}.}
+
+This allows to define a term of type {\type} using the proof editing mode. It
+behaves as {\tt Theorem} but is intended to be used in conjunction with
+  {\tt Defined} (see \ref{Defined}) in order to define a
+ constant of which the computational behavior is relevant.
+
+The command can be used also with {\tt Example} instead
+of {\tt Definition}.
+
+\SeeAlso Sections~\ref{Opaque} and~\ref{Transparent} ({\tt Opaque}
+and {\tt Transparent}) and~\ref{unfold} (tactic {\tt unfold}).
+
+\item {\tt Let {\ident} \zeroone{\binders} : {\type}.}
+
+Like {\tt Definition {\ident} \zeroone{\binders} : {\type}.} except
+that the definition is turned into a local definition generalized over
+the declarations depending on it after closing the current section.
+
+\item {\tt Fixpoint \nelist{{\ident} {\binders} \zeroone{\annotation} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.}
+\comindex{Fixpoint}
+
+This generalizes the syntax of {\tt 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 by {\tt
+  Defined}.
+
+\item {\tt CoFixpoint \nelist{{\ident} \zeroone{\binders} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.}
+\comindex{CoFixpoint}
+
+This generalizes the syntax of {\tt CoFixpoint} so that one or more bodies
+can be defined interactively using the proof editing mode.
+
+\end{Variants}
+
+\subsubsection{{\tt Proof.} {\dots} {\tt Qed.}
+\comindex{Proof}
+\comindex{Qed}}
+
+A proof starts by the keyword {\tt 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
+\ref{Tactics}. Besides tactics, there are commands to manage the proof
+editing mode. They are described in Chapter~\ref{Proof-handling}. When
+the proof is completed it should be validated and put in the
+environment using the keyword {\tt Qed}.
+\medskip
+
+\ErrMsg
+\begin{enumerate}
+\item \errindex{{\ident} already exists}
+\end{enumerate}
+
+\begin{Remarks}
+\item Several statements can be simultaneously asserted.
+\item 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. 
+\item {\tt Proof} is recommended but can currently be omitted. On the
+opposite side, {\tt Qed} (or {\tt Defined}, see below) is mandatory to
+validate a proof.
+\item Proofs ended by {\tt Qed} are declared opaque. Their content
+  cannot be unfolded (see \ref{Conversion-tactics}), thus realizing
+  some form of {\em proof-irrelevance}. To be able to unfold a proof,
+  the proof should be ended by {\tt Defined} (see below).
+\end{Remarks}
+
+\begin{Variants}
+\item \comindex{Defined}
+  {\tt Proof.} {\dots} {\tt Defined.}\\
+  Same as {\tt Proof.} {\dots} {\tt Qed.} but the proof is
+  then declared transparent, which means that its
+  content can be explicitly used for type-checking and that it
+  can be unfolded in conversion tactics (see
+  \ref{Conversion-tactics}, \ref{Opaque}, \ref{Transparent}).
+%Not claimed to be part of Gallina...
+%\item {\tt Proof.} {\dots} {\tt Save.}\\
+%  Same as {\tt Proof.} {\dots} {\tt Qed.}
+%\item {\tt Goal} \type {\dots} {\tt Save} \ident \\
+%  Same as {\tt Lemma} \ident {\tt :} \type \dots {\tt Save.}
+%  This is intended to be used in the interactive mode.
+\item \comindex{Admitted}
+  {\tt Proof.} {\dots} {\tt Admitted.}\\
+  Turns the current asserted statement into an axiom and exits the
+  proof mode.
+\end{Variants}
+
+% Local Variables: 
+% mode: LaTeX
+% TeX-master: "Reference-Manual"
+% End: 
+
-- 
cgit v1.2.3

