\chapter{The \gallina{} specification language \label{Gallina}\index{Gallina}} 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 \label{BNF-syntax}\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} \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!=_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@{\qquad}r} {\term} & ::= & {\tt forall} {\binderlist} {\tt ,} {\term} &(\ref{products})\\ & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\ & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\ & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\ & $|$ & {\tt let} {\idparams} {\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})\\ &&&\\ {\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\ & $|$ & {\binder} \nelist{\binderlet}{} &\\ &&&\\ {\binder} & ::= & {\name} & \ref{Binders} \\ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ &&&\\ {\binderlet} & ::= & {\binder} & \ref{Binders} \\ & $|$ & {\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} {\idparams} & ::= & {\ident} \sequence{\binderlet}{} {\typecstr} \\ &&\\ {\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} \nelist{\binderlet}{} \zeroone{\annotation} {\typecstr} {\tt :=} {\term} \\ {\cofixpointbody} & ::= & {\idparams} {\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}. \subsection{Binders \label{Binders} \index{binders}} Various constructions introduce variables which scope is some of its sub-expressions. There is a uniform syntax for this. A binder may be an (unqualified) identifier: the name to use to refer to this variable. If the variable is not to be used, its name can be {\tt \_}. When its type cannot be synthesized by the system, it can be specified with notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt )}. There is a notation for several variables sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt :}\,{\type}\,{\tt )}. Some constructions allow ``let-binders'', that is either a binder as defined above, or a variable with a value. The notation is {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )}. Only one variable can be introduced at the same time. It is also possible to give the type of the variable before the symbol {\tt :=}. The last kind of binders is the ``binder list''. It is either a list of let-binders (the first one not being a variable with value), or {\ident$_1$}\ldots{\ident$_n$}\,{\tt :}\,{\type} if all variables share the same type. {\Coq} terms are typed. {\Coq} types are recognized by the same syntactic class as {\term}. We denote by {\type} the semantic subclass of types inside the syntactic class {\term}. \index{type@{\type}} \subsection{Abstractions \label{abstractions} \index{abstractions}} The expression ``{\tt fun} {\ident} {\tt :} \type {\tt =>}~{\term}'' denotes the {\em abstraction} of the variable {\ident} of type {\type}, over the term {\term}. Put in another way, it is function of formal parameter {\ident} of type {\type} returning {\term}. Keyword {\tt fun} is followed by a ``binder list'', so any of the binders of Section~\ref{Binders} apply. Internally, abstractions are only over one variable. Multiple variable binders are an iteration of the single variable abstraction: notation {\tt fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term} stands for {\tt fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt =>}~{\ldots}~{\tt fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}. Variables with a value expand 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 it is represented by an iteration of single variable products. Non dependent product types have a special notation ``$A$ {\tt ->} $B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. This is to stress on the fact that non dependent product types are usual functional types. \subsection{Applications \label{applications} \index{applications}} The expression \term$_0$ \term$_1$ denotes the application of term \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} {\term$_n$} {\tt }: associativity is to the left. When using implicit arguments mechanism, implicit positions can be forced a value with notation {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )} or {\tt (}\,{\num}\,{\tt :=}\,{\term}\,{\tt )}. See Section~\ref{Implicits-explicitation} for details. \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{\_}} Since there are redundancies, a term can be type-checked without giving it in totality. Subterms that are left to guess by the type-checker are replaced by ``\_''. \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 in} {\term$_2$}. \subsection{Definition by case analysis \label{caseanalysis} \index{match@{\tt match\ldots with\ldots end}}} This paragraph only shows simple variants of case analysis. See Section~\ref{Mult-match} and Chapter~\ref{Mult-match-full} for explanations of the general form. Objects of inductive types can be destructurated by a case-analysis construction, also called pattern-matching in functional languages. In its simple form, a case analysis expression is used to analyze the structure of an inductive objects (upon which constructor it is built). The expression {\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 called branches. In a simple pattern \qualid~\nelist{\ident}{}, the qualified identifier {\qualid} is intended to be a constructor. There should be one branch for every constructor of $I$. The {\returntype} is used to compute the resulting type of the whole {\tt match} expression and the type of the branches. Most of the time, when this type is the same as the types of all the {\term$_i$}, the annotation is not needed\footnote{except if no equation is given, to match the term in an empty type, e.g. the type \texttt{False}}. This annotation has to be given when the resulting type of the whole {\tt match} depends on the actual {\term$_0$} matched. 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}. \SeeAlso Section~\ref{Mult-match} for details and examples. \subsection{Recursive functions \label{fixpoints} \index{fix@{fix \ident$_i$\{\dots\}}}} 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$th 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$} 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$th 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$} 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} & ::= & {\declaration} \\ & $|$ & {\definition} \\ & $|$ & {\inductive} \\ & $|$ & {\fixpoint} \\ & $|$ & {\statement} \zeroone{\proof} \\ &&\\ %% Declarations {\declaration} & ::= & {\declarationkeyword} {\assums} {\tt .} \\ &&\\ {\declarationkeyword} & ::= & {\tt Axiom} $|$ {\tt Conjecture} \\ & $|$ & {\tt Parameter} $|$ {\tt Parameters} \\ & $|$ & {\tt Variable} $|$ {\tt Variables} \\ & $|$ & {\tt Hypothesis} $|$ {\tt Hypotheses}\\ &&\\ {\assums} & ::= & \nelist{\ident}{} {\tt :} {\term} \\ & $|$ & \nelist{\binder}{} \\ &&\\ %% Definitions {\definition} & ::= & {\tt Definition} {\idparams} {\tt :=} {\term} {\tt .} \\ & $|$ & {\tt Let} {\idparams} {\tt :=} {\term} {\tt .} \\ &&\\ %% Inductives {\inductive} & ::= & {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\ & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ & & \\ {\inductivebody} & ::= & {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\ && ~~~\zeroone{\zeroone{\tt |} \nelist{\idparams}{|}} \\ & & \\ %% TODO: where ... %% Fixpoints {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\ & $|$ & {\tt CoFixpoint} \nelist{\cofixpointbody}{with} {\tt .} \\ &&\\ %% Lemmas & proofs {\statement} & ::= & {\statkwd} {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt .} \\ &&\\ {\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} $|$ {\tt Definition} \\ &&\\ {\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{Declarations \index{Declarations} \label{Declarations}} The declaration mechanism allows the user to specify his own basic objects. Declared objects play the role of axioms or parameters in mathematics. A declared object is an {\ident} associated to a \term. A declaration is accepted by {\Coq} if and only if this {\term} is a correct type in the current context of the declaration and \ident\ was not previously defined in the same module. This {\term} is considered to be the type, or specification, of the \ident. \subsubsection{{\tt Axiom {\ident} :{\term} .} \comindex{Axiom} \comindex{Parameter}\comindex{Parameters} \comindex{Conjecture} \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 {\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 {\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} \comindex{Hypothesis} \comindex{Hypotheses}} 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 parameterized (the variable is {\em discharged}). Using the {\tt Variable} command out of any section is equivalent to {\tt Axiom}. \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 {\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{Simpl-definitions}} Definitions differ from declarations in allowing to give a name to a term whereas declarations were just giving a type to a name. That is to say that the name of a defined object can be replaced at any time by its definition. This replacement is called $\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see Section~\ref{delta}). A defined object is accepted by the system if and only if the defining term is well-typed in the current context of the definition. Then the type of the name is the type of term. The defined name is called a {\em constant}\index{Constant} and one says that {\it the constant is added to the environment}\index{Environment}. A formal presentation of constants and environments is given in Section~\ref{Typed-terms}. \subsubsection{\tt Definition {\ident} := {\term}. \comindex{Definition}} This command binds the value {\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} %% %% 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{Parameterized 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 parameterized inductive definition can be defined using annotations instead of parameters but it will sometimes give a different (bigger) sort for the inductive definition and will produce a less convenient rule for case elimination. \SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{Tac-induction}. \subsubsection{Mutually defined inductive types \comindex{Mutual 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 parameterize these inductive definitions. However, parameters correspond to a local context in which the whole set of inductive declarations is done. For this reason, the parameters must be strictly the same for each inductive types The extended syntax is: \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 parameterize 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} (cf. 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{Recursive functions over a inductive type} 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 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. This annotation may be left implicit for fixpoints where only one argument has an inductive type. 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 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 normalisation property, the fixed point reduction will only be performed when the argument in position of the decreasing argument (which type should be in an inductive definition) starts with a constructor. The {\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$} := {\type$_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{A more complex definition of recursive functions} The \emph{experimental} command \begin{center} \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} \{decrease\_annot\} : type$_0$ := \term$_0$} \comindex{Function} \label{Function} \end{center} can be seen as a generalization of {\tt Fixpoint}. It is actually a wrapper for several ways of defining a function \emph{and other useful related objects}, namely: an induction principle that reflects the recursive structure of the function (see \ref{FunInduction}), and its fixpoint equality. The meaning of this declaration is to define a function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be given (unless the function is not recursive), but it must not necessary be \emph{structurally} decreasing. The point of the {\tt \{\}} annotation is to name the decreasing argument \emph{and} to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. The {\tt Function} construction enjoys also the {\tt with} extension to define mutually recursive definitions. However, this feature does not work for non structural recursive functions. % VRAI?? See the documentation of {\tt functional induction} (section \ref{FunInduction}) and {\tt Functional Scheme} (section \ref{FunScheme} and \ref{FunScheme-examples}) for how to use the induction principle to easily reason about the function. \noindent {\bf Remark: } To obtain the right principle, it is better to put rigid parameters of the function as first arguments. For example it is better to define plus like this: \begin{coq_example*} Function plus (m n : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus m p) end. \end{coq_example*} \noindent than like this: \begin{coq_eval} Reset plus. \end{coq_eval} \begin{coq_example*} Function plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus p m) end. \end{coq_example*} \paragraph{Limitations} \label{sec:Function-limitations} \term$_0$ must be build as a \emph{pure pattern-matching tree} (\texttt{match...with}) with applications only \emph{at the end} of each branch. For now dependent cases are not treated. \begin{ErrMsgs} \item \errindex{The recursive argument must be specified} \item \errindex{No argument name \ident} \item \errindex{Cannot use mutual definition with well-founded recursion or measure} \item \errindex{Cannot define graph for \ident\dots} (warning) The generation of the graph relation \texttt{(R\_\ident)} used to compute the induction scheme of \ident\ raised a typing error. Only the ident is defined, the induction scheme will not be generated. This error happens generally when: \begin{itemize} \item the definition uses pattern matching on dependent types, which \texttt{Function} cannot deal with yet. \item the definition is not a \emph{pattern-matching tree} as explained above. \end{itemize} \item \errindex{Cannot define principle(s) for \ident\dots} (warning) The generation of the graph relation \texttt{(R\_\ident)} succeeded but the induction principle could not be built. Only the ident is defined. Please report. \item \errindex{Cannot built inversion information} (warning) \texttt{functional inversion} will not be available for the function. \end{ErrMsgs} \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}} Depending on the {\tt \{$\ldots$\}} annotation, different definition mechanisms are used by {\tt Function}. More precise description given below. \begin{Variants} \item \texttt{ Function {\ident} {\binder$_1$}\ldots{\binder$_n$} : type$_0$ := \term$_0$} Defines the not recursive function \ident\ as if declared with \texttt{Definition}. Moreover the following are defined: \begin{itemize} \item {\tt\ident\_rect}, {\tt\ident\_rec} and {\tt\ident\_ind}, which reflect the pattern matching structure of \term$_0$ (see the documentation of {\tt Inductive} \ref{Inductive}); \item The inductive \texttt{R\_\ident} corresponding to the graph of \ident\ (silently); \item \texttt{\ident\_complete} and \texttt{\ident\_correct} which are inversion information linking the function and its graph. \end{itemize} \item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$} Defines the structural recursive function \ident\ as if declared with \texttt{Fixpoint}. Moreover the following are defined: \begin{itemize} \item The same objects as above; \item The fixpoint equation of \ident: \texttt{\ident\_equation}. \end{itemize} \item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$} \item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$} Defines a recursive function by well founded recursion. \textbf{The module \texttt{Recdef} of the standard library must be loaded for this feature}. The {\tt \{\}} annotation is mandatory and must be one of the following: \begin{itemize} \item {\tt \{measure} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being the decreasing argument and \term$_1$ being a function from type of \ident$_0$ to \texttt{nat} for which value on the decreasing argument decreases (for the {\tt lt} order on {\tt nat}) at each recursive call of \term$_0$, parameters of the function are bound in \term$_0$; \item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being the decreasing argument and \term$_1$ an ordering relation on the type of \ident$_0$ (i.e. of type T$_{\ident_0}$ $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which the decreasing argument decreases at each recursive call of \term$_0$. The order must be well founded. parameters of the function are bound in \term$_0$. \end{itemize} Depending on the annotation, the user is left with some proof obligations that will be used to define the function. These proofs are: proofs that each recursive call is actually decreasing with respect to the given criteria, and (if the criteria is \texttt{wf}) a proof that the ordering relation is well founded. %Completer sur measure et wf Once proof obligations are discharged, the following objects are defined: \begin{itemize} \item The same objects as with the \texttt{struct}; \item The lemma \texttt{\ident\_tcc} which collects all proof obligations in one property; \item The lemmas \texttt{\ident\_terminate} and \texttt{\ident\_F} which is needed to be inlined during extraction of \ident. \end{itemize} %Complete!! The way this recursive function is defined is the subject of several papers by Yves Bertot and Antonia Balaa on one hand and Gilles Barthe, Julien Forest, David Pichardie and Vlad Rusu on the other hand. %Exemples ok ici \bigskip \noindent {\bf Remark: } Proof obligations are presented as several subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independent which means that in order to % abort them you will have to abort each separately. %The decreasing argument cannot be dependent of another?? %Exemples faux ici \end{Variants} \subsubsection{Recursive functions over co-indcutive 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 (cf. Section~\ref{Fixpoint}), it is possible to introduce a block of mutually dependent methods. \end{Variants} %% %% Theorems & Lemmas %% \subsection{Statement and proofs} A statement claims a goal of which the proof is then interactively done using tactics. More on the proof editing mode, statements and proofs can be found in chapter \ref{Proof-handling}. \subsubsection{\tt Theorem {\ident} : {\type}. \comindex{Theorem} \comindex{Lemma} \comindex{Remark} \comindex{Fact}} This command binds {\type} to the name {\ident} in the environment, provided that a proof of {\type} is next given. After a statement, {\Coq} needs a proof. \begin{Variants} \item {\tt Lemma {\ident} : {\type}.}\\ {\tt Remark {\ident} : {\type}.}\\ {\tt Fact {\ident} : {\type}.}\\ {\tt Corollary {\ident} : {\type}.}\\ {\tt Proposition {\ident} : {\type}.}\\ \comindex{Proposition} \comindex{Corollary} All these commands are synonymous of \texttt{Theorem} % Same as {\tt Theorem} except % that if this statement is in one or more levels of sections then the % name {\ident} will be accessible only prefixed by the sections names % when the sections (see \ref{Section} and \ref{LongNames}) will be % closed. % %All proofs of persistent objects (such as theorems) referring to {\ident} % %within the section will be replaced by the proof of {\ident}. % Same as {\tt Remark} except % that the innermost section name is dropped from the full name. \item {\tt Definition {\ident} : {\type}.} \\ Allow to define a term of type {\type} using the proof editing mode. It behaves as {\tt Theorem} but is intended for the interactive definition of expression which computational behaviour will be used by further commands. \SeeAlso~\ref{Transparent} and \ref{unfold}. \end{Variants} \subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} \comindex{Proof} \comindex{Qed} \comindex{Defined} \comindex{Save} \comindex{Goal} \comindex{Admitted}} 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 opened. \item Not only other statements but any vernacular command can be given within the proof editing mode. In this case, the command is understood as if it would have been given before the statements still to be proved. \item {\tt Proof} is recommended but can currently be omitted. On the opposite, {\tt Qed} (or {\tt Defined}, see below) is mandatory to validate a proof. \item Proofs ended by {\tt Qed} are declared opaque (see \ref{Opaque}) and cannot be unfolded by conversion tactics (see \ref{Conversion-tactics}). To be able to unfold a proof, you should end the proof by {\tt Defined} (see below). \end{Remarks} \begin{Variants} \item {\tt Proof} {\tt .} \dots {\tt Defined} {\tt .}\\ Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} but the proof is then declared transparent (see \ref{Transparent}), which means it can be unfolded in conversion tactics (see \ref{Conversion-tactics}). \item {\tt Proof} {\tt .} \dots {\tt Save.}\\ Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} \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. Conversely to named lemmas, anonymous goals cannot be nested. \item {\tt Proof.} \dots {\tt Admitted.}\\ Turns the current conjecture into an axiom and exits editing of current proof. \end{Variants} % Local Variables: % mode: LaTeX % TeX-master: "Reference-Manual" % End: % $Id: RefMan-gal.tex 9127 2006-09-07 15:47:14Z courtieu $