diff options
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 1723 |
1 files changed, 0 insertions, 1723 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex deleted file mode 100644 index 1c258b20..00000000 --- a/doc/refman/RefMan-gal.tex +++ /dev/null @@ -1,1723 +0,0 @@ -\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!<=! & -\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 $ |