From 3bda731dacad8826e0a05d14b5cf935fedf4f4c6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 9 Apr 2018 13:22:00 +0200 Subject: [Sphinx] Move chapter 1 to new infrastructure --- Makefile.doc | 1 - doc/refman/RefMan-gal.tex | 1737 -------------------- doc/refman/Reference-Manual.tex | 1 - .../language/gallina-specification-language.rst | 1736 +++++++++++++++++++ 4 files changed, 1736 insertions(+), 1739 deletions(-) delete mode 100644 doc/refman/RefMan-gal.tex create mode 100644 doc/sphinx/language/gallina-specification-language.rst diff --git a/Makefile.doc b/Makefile.doc index b9443f723..add38941a 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -57,7 +57,6 @@ ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS) DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ - RefMan-gal.v.tex \ RefMan-ltac.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex deleted file mode 100644 index 41ea0a5dc..000000000 --- a/doc/refman/RefMan-gal.tex +++ /dev/null @@ -1,1737 +0,0 @@ -\chapter{The \gallina{} specification language -\label{Gallina}\index{Gallina}} -%HEVEA\cutname{gallina.html} -\label{BNF-syntax} % Used referred to as a chapter label - -This chapter describes \gallina, the specification language of {\Coq}. -It allows developing mathematical theories and proofs of specifications -of programs. The theories are built from axioms, hypotheses, -parameters, lemmas, theorems and definitions of constants, functions, -predicates and sets. The syntax of logical objects involved in -theories is described in Section~\ref{term}. The language of -commands, called {\em The Vernacular} is described in section -\ref{Vernacular}. - -In {\Coq}, logical objects are typed to ensure their logical -correctness. The rules implemented by the typing algorithm are described in -Chapter \ref{Cic}. - -\subsection*{About the grammars in the manual -\index{BNF metasyntax}} - -Grammars are presented in Backus-Naur form (BNF). Terminal symbols are -set in {\tt typewriter font}. In addition, there are special -notations for regular expressions. - -An expression enclosed in square brackets \zeroone{\ldots} means at -most one occurrence of this expression (this corresponds to an -optional component). - -The notation ``\nelist{\entry}{sep}'' stands for a non empty -sequence of expressions parsed by {\entry} and -separated by the literal ``{\tt sep}''\footnote{This is similar to the -expression ``{\entry} $\{$ {\tt sep} {\entry} $\}$'' in -standard BNF, or ``{\entry}~{$($} {\tt sep} {\entry} {$)$*}'' in -the syntax of regular expressions.}. - -Similarly, the notation ``\nelist{\entry}{}'' stands for a non -empty sequence of expressions parsed by the ``{\entry}'' entry, -without any separator between. - -Finally, the notation ``\sequence{\entry}{\tt sep}'' stands for a -possibly empty sequence of expressions parsed by the ``{\entry}'' entry, -separated by the literal ``{\tt sep}''. - -\section{Lexical conventions -\label{lexical}\index{Lexical conventions}} - -\paragraph{Blanks} -Space, newline and horizontal tabulation are considered as blanks. -Blanks are ignored but they separate tokens. - -\paragraph{Comments} - -Comments in {\Coq} are enclosed between {\tt (*} and {\tt - *)}\index{Comments}, and can be nested. They can contain any -character. However, string literals must be correctly closed. Comments -are treated as blanks. - -\paragraph{Identifiers and access identifiers} - -Identifiers, written {\ident}, are sequences of letters, digits, -\verb!_! and \verb!'!, that do not start with a digit or \verb!'!. -That is, they are recognized by the following lexical class: - -\index{ident@\ident} -\begin{center} -\begin{tabular}{rcl} -{\firstletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt \_} -$\mid$ {\tt unicode-letter} -\\ -{\subsequentletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt 0..9} -$\mid$ {\tt \_} % $\mid$ {\tt \$} -$\mid$ {\tt '} -$\mid$ {\tt unicode-letter} -$\mid$ {\tt unicode-id-part} \\ -{\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{} -\end{tabular} -\end{center} -All characters are meaningful. In particular, identifiers are -case-sensitive. The entry {\tt unicode-letter} non-exhaustively -includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, -Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical -letter-like symbols, hyphens, non-breaking space, {\ldots} The entry -{\tt unicode-id-part} non-exhaustively includes symbols for prime -letters and subscripts. - -Access identifiers, written {\accessident}, are identifiers prefixed -by \verb!.! (dot) without blank. They are used in the syntax of qualified -identifiers. - -\paragraph{Natural numbers and integers} -Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign. - -\index{num@{\num}} -\index{integer@{\integer}} -\begin{center} -\begin{tabular}{r@{\quad::=\quad}l} -{\digit} & {\tt 0..9} \\ -{\num} & \nelistwithoutblank{\digit}{} \\ -{\integer} & \zeroone{\tt -}{\num} \\ -\end{tabular} -\end{center} - -\paragraph[Strings]{Strings\label{strings} -\index{string@{\qstring}}} -Strings are delimited by \verb!"! (double quote), and enclose a -sequence of any characters different from \verb!"! or the sequence -\verb!""! to denote the double quote character. In grammars, the -entry for quoted strings is {\qstring}. - -\paragraph{Keywords} -The following identifiers are reserved keywords, and cannot be -employed otherwise: -\begin{center} -\begin{tabular}{llllll} -\verb!_! & -\verb!as! & -\verb!at! & -\verb!cofix! & -\verb!else! & -\verb!end! \\ -% -\verb!exists! & -\verb!exists2! & -\verb!fix! & -\verb!for! & -\verb!forall! & -\verb!fun! \\ -% -\verb!if! & -\verb!IF! & -\verb!in! & -\verb!let! & -\verb!match! & -\verb!mod! \\ -% -\verb!Prop! & -\verb!return! & -\verb!Set! & -\verb!then! & -\verb!Type! & -\verb!using! \\ -% -\verb!where! & -\verb!with! & -\end{tabular} -\end{center} - - -\paragraph{Special tokens} -The following sequences of characters are special tokens: -\begin{center} -\begin{tabular}{lllllll} -\verb/!/ & -\verb!%! & -\verb!&! & -\verb!&&! & -\verb!(! & -\verb!()! & -\verb!)! \\ -% -\verb!*! & -\verb!+! & -\verb!++! & -\verb!,! & -\verb!-! & -\verb!->! & -\verb!.! \\ -% -\verb!.(! & -\verb!..! & -\verb!/! & -\verb!/\! & -\verb!:! & -\verb!::! & -\verb!:! & -\verb!;! & -\verb!! & -\verb!<:! \\ -% -\verb!<=! & -\verb!<>! & -\verb!=! & -\verb!=>! & -\verb!=_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 syntax of -the terms of the {\em Calculus of Inductive Constructions} (also -called \CIC). The formal presentation of {\CIC} is given in Chapter -\ref{Cic}. Extensions of this syntax are given in chapter -\ref{Gallina-extension}. How to customize the syntax is described in Chapter -\ref{Addoc-syntax}. - -\begin{figure}[htbp] -\begin{centerframe} -\begin{tabular}{lcl@{\quad~}r} % warning: page width exceeded with \qquad -{\term} & ::= & - {\tt forall} {\binders} {\tt ,} {\term} &(\ref{products})\\ - & $|$ & {\tt fun} {\binders} {\tt =>} {\term} &(\ref{abstractions})\\ - & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\ - & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\ - & $|$ & {\tt let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} - {\tt in} {\term} &(\ref{let-in})\\ - & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\ - & $|$ & {\tt let cofix} {\cofixpointbody} - {\tt in} {\term} &(\ref{fixpoints})\\ - & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem} - {\tt :=} {\term} - {\tt in} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ - & $|$ & {\tt let '} {\pattern} \zeroone{{\tt in} {\term}} {\tt :=} {\term} - \zeroone{\returntype} {\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{typecast})\\ - & $|$ & {\term} {\tt :>} &(\ref{ProgramSyntax})\\ - & $|$ & {\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})\\ - & $|$ & {\tt (} {\term} {\tt )} & \\ - & & &\\ -{\termarg} & ::= & {\term} &\\ - & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )} - &(\ref{Implicits-explicitation})\\ -%% & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )} -%% &(\ref{Implicits-explicitation})\\ -&&&\\ -{\binders} & ::= & \nelist{\binder}{} \\ -&&&\\ -{\binder} & ::= & {\name} & (\ref{Binders}) \\ - & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ - & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\ - & $|$ & {\tt '} {\pattern} &\\ -& & &\\ -{\name} & ::= & {\ident} &\\ - & $|$ & {\tt \_} &\\ -&&&\\ -{\qualid} & ::= & {\ident} & \\ - & $|$ & {\qualid} {\accessident} &\\ - & & &\\ -{\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} & -\end{tabular} -\end{centerframe} -\caption{Syntax of terms} -\label{term-syntax} -\index{term@{\term}} -\index{sort@{\sort}} -\end{figure} - - - -\begin{figure}[htb] -\begin{centerframe} -\begin{tabular}{lcl} -{\fixpointbodies} & ::= & - {\fixpointbody} \\ - & $|$ & {\fixpointbody} {\tt with} \nelist{\fixpointbody}{{\tt with}} - {\tt for} {\ident} \\ -{\cofixpointbodies} & ::= & - {\cofixpointbody} \\ - & $|$ & {\cofixpointbody} {\tt with} \nelist{\cofixpointbody}{{\tt with}} - {\tt for} {\ident} \\ -&&\\ -{\fixpointbody} & ::= & - {\ident} {\binders} \zeroone{\annotation} {\typecstr} - {\tt :=} {\term} \\ -{\cofixpointbody} & ::= & {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} \\ - & &\\ -{\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ -&&\\ -{\caseitem} & ::= & {\term} \zeroone{{\tt as} \name} - \zeroone{{\tt in} \qualid \sequence{\pattern}{}} \\ -&&\\ -{\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\ -&&\\ -{\returntype} & ::= & {\tt return} {\term} \\ -&&\\ -{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\ -&&\\ -{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\ -&&\\ -{\pattern} & ::= & {\qualid} \nelist{\pattern}{} \\ - & $|$ & {\tt @} {\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 such as {\tt fun}, {\tt forall}, {\tt fix} and -{\tt cofix} {\em bind} variables. A binding is represented by an -identifier. If the binding variable is not used in the expression, the -identifier can be replaced by the symbol {\tt \_}. When the type of a -bound variable cannot be synthesized by the system, it can be -specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt -)}. There is also a notation for a sequence of binding variables -sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt -:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote, -e.g. {\tt '(x,y)}. - -Some constructions allow the binding of a variable to value. This is -called a ``let-binder''. The entry {\binder} of the grammar accepts -either an assumption binder as defined above or a let-binder. -The notation in the -latter case is {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )}. In a -let-binder, only one variable can be introduced at the same -time. It is also possible to give the type of the variable as follows: -{\tt (}\,{\ident}\,{\tt :}\,{\term}\,{\tt :=}\,{\term}\,{\tt )}. - -Lists of {\binder} are allowed. In the case of {\tt fun} and {\tt - forall}, it is intended that at least one binder of the list is an -assumption otherwise {\tt fun} and {\tt forall} gets identical. Moreover, -parentheses can be omitted in the case of a single sequence of -bindings sharing the same type (e.g.: {\tt fun~(x~y~z~:~A)~=>~t} can -be shortened in {\tt fun~x~y~z~:~A~=>~t}). - -\subsection{Abstractions -\label{abstractions} -\index{abstractions}} -\index{fun@{{\tt fun \ldots => \ldots}}} - -The expression ``{\tt fun} {\ident} {\tt :} {\type} {\tt =>}~{\term}'' -defines the {\em abstraction} of the variable {\ident}, of type -{\type}, over the term {\term}. It denotes a function of the variable -{\ident} that evaluates to the expression {\term} (e.g. {\tt fun x:$A$ -=> x} denotes the identity function on type $A$). -% The variable {\ident} is called the {\em parameter} of the function -% (we sometimes say the {\em formal parameter}). -The keyword {\tt fun} can be followed by several binders as given in -Section~\ref{Binders}. Functions over several variables are -equivalent to an iteration of one-variable functions. For instance the -expression ``{\tt fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt -:}~\type~{\tt =>}~{\term}'' denotes the same function as ``{\tt -fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt =>}~{\ldots}~{\tt -fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}''. If a let-binder -occurs in the list of binders, it is expanded to a let-in definition -(see Section~\ref{let-in}). - -\subsection{Products -\label{products} -\index{products}} -\index{forall@{{\tt forall \ldots, \ldots}}} - -The expression ``{\tt forall}~{\ident}~{\tt :}~{\type}{\tt -,}~{\term}'' denotes the {\em product} of the variable {\ident} of -type {\type}, over the term {\term}. As for abstractions, {\tt forall} -is followed by a binder list, and products over several variables are -equivalent to an iteration of one-variable products. -Note that {\term} is intended to be a type. - -If the variable {\ident} occurs in {\term}, the product is called {\em -dependent product}. The intention behind a dependent product {\tt -forall}~$x$~{\tt :}~{$A$}{\tt ,}~{$B$} is twofold. It denotes either -the universal quantification of the variable $x$ of type $A$ in the -proposition $B$ or the functional dependent product from $A$ to $B$ (a -construction usually written $\Pi_{x:A}.B$ in set theory). - -Non dependent product types have a special notation: ``$A$ {\tt ->} -$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The {\em non dependent -product} is used both to denote the propositional implication and -function types. - -\subsection{Applications -\label{applications} -\index{applications}} - -The expression \term$_0$ \term$_1$ denotes the application of -\term$_0$ to \term$_1$. - -The expression {\tt }\term$_0$ \term$_1$ ... \term$_n${\tt} -denotes the application of the term \term$_0$ to the arguments -\term$_1$ ... then \term$_n$. It is equivalent to {\tt (} {\ldots} -{\tt (} {\term$_0$} {\term$_1$} {\tt )} {\ldots} {\tt )} {\term$_n$} {\tt }: -associativity is to the left. - -The notation {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )} for -arguments is used for making explicit the value of implicit arguments -(see Section~\ref{Implicits-explicitation}). - -\subsection{Type cast -\label{typecast} -\index{Cast}} -\index{cast@{{\tt(\ldots: \ldots)}}} - -The expression ``{\term}~{\tt :}~{\type}'' is a type cast -expression. It enforces the type of {\term} to be {\type}. - -``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine for checking -that {\term} has type {\type}. - -\subsection{Inferable subterms -\label{hole} -\index{\_}} - -Expressions often contain redundant pieces of information. Subterms that -can be automatically inferred by {\Coq} can be replaced by the -symbol ``\_'' and {\Coq} will guess the missing piece of information. - -\subsection{Let-in definitions -\label{let-in} -\index{Let-in definitions} -\index{let-in}} -\index{let@{{\tt let \ldots := \ldots in \ldots}}} - - -{\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 let-in definition of functions: {\tt -let} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} {\tt :=} {\term$_1$} -{\tt in} {\term$_2$} stands for {\tt let} {\ident} {\tt := fun} -{\binder$_1$} {\ldots} {\binder$_n$} {\tt =>} {\term$_1$} {\tt in} -{\term$_2$}. - -\subsection{Definition by case analysis -\label{caseanalysis} -\index{match@{\tt match\ldots with\ldots end}}} - -Objects of inductive types can be destructurated by a case-analysis -construction called {\em pattern-matching} expression. A -pattern-matching expression is used to analyze the structure of an -inductive objects and to apply specific treatments accordingly. - -This paragraph describes the basic form of pattern-matching. See -Section~\ref{Mult-match} and Chapter~\ref{Mult-match-full} for the -description of the general form. The basic form of pattern-matching is -characterized by a single {\caseitem} expression, a {\multpattern} -restricted to a single {\pattern} and {\pattern} restricted to the -form {\qualid} \nelist{\ident}{}. - -The expression {\tt match} {\term$_0$} {\returntype} {\tt with} -{\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$} -{\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em -pattern-matching} over the term {\term$_0$} (expected to be of an -inductive type $I$). The terms {\term$_1$}\ldots{\term$_n$} are the -{\em branches} of the pattern-matching expression. Each of -{\pattern$_i$} has a form \qualid~\nelist{\ident}{} where {\qualid} -must denote a constructor. There should be exactly one branch for -every constructor of $I$. - -The {\returntype} expresses the type returned by the whole {\tt match} -expression. There are several cases. In the {\em non dependent} case, -all branches have the same type, and the {\returntype} is the common -type of branches. In this case, {\returntype} can usually be omitted -as it can be inferred from the type of the branches\footnote{Except if -the inductive type is empty in which case there is no equation that can be -used to infer the return type.}. - -In the {\em dependent} case, there are three subcases. In the first -subcase, the type in each branch may depend on the exact value being -matched in the branch. In this case, the whole pattern-matching itself -depends on the term being matched. This dependency of the term being -matched in the return type is expressed with an ``{\tt as {\ident}}'' -clause where {\ident} is dependent in the return type. -For instance, in the following example: -\begin{coq_example*} -Inductive bool : Type := true : bool | false : bool. -Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. -Inductive or (A:Prop) (B:Prop) : Prop := -| or_introl : A -> or A B -| or_intror : B -> or A B. -Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) -:= match b as x return or (eq bool x true) (eq bool x false) with - | true => or_introl (eq bool true true) (eq bool true false) - (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) - (eq_refl bool false) - end. -\end{coq_example*} -the branches have respective types {\tt or (eq bool true true) (eq -bool true false)} and {\tt or (eq bool false true) (eq bool false -false)} while the whole pattern-matching expression has type {\tt or -(eq bool b true) (eq bool b false)}, the identifier {\tt x} being used -to represent the dependency. Remark that when the term being matched -is a variable, the {\tt as} clause can be omitted and the term being -matched can serve itself as binding name in the return type. For -instance, the following alternative definition is accepted and has the -same meaning as the previous one. -\begin{coq_eval} -Reset bool_case. -\end{coq_eval} -\begin{coq_example*} -Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) -:= match b return or (eq bool b true) (eq bool b false) with - | true => or_introl (eq bool true true) (eq bool true false) - (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) - (eq_refl bool false) - end. -\end{coq_example*} - -The second subcase is only relevant for annotated inductive types such -as the equality predicate (see Section~\ref{Equality}), the order -predicate on natural numbers % (see Section~\ref{le}) % undefined reference -or the type of -lists of a given length (see Section~\ref{listn}). In this configuration, -the type of each branch can depend on the type dependencies specific -to the branch and the whole pattern-matching expression has a type -determined by the specific dependencies in the type of the term being -matched. This dependency of the return type in the annotations of the -inductive type is expressed using a - ``in~I~\_~$\ldots$~\_~\pattern$_1$~$\ldots$~\pattern$_n$'' clause, where -\begin{itemize} -\item $I$ is the inductive type of the term being matched; - -\item the {\_}'s are matching the parameters of the inductive type: -the return type is not dependent on them. - -\item the \pattern$_i$'s are matching the annotations of the inductive - type: the return type is dependent on them - -\item in the basic case which we describe below, each \pattern$_i$ is a - name \ident$_i$; see \ref{match-in-patterns} for the general case - -\end{itemize} - -For instance, in the following example: -\begin{coq_example*} -Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := - match H in eq _ _ z return eq A z x with - | eq_refl _ _ => eq_refl A x - end. -\end{coq_example*} -the type of the branch has type {\tt eq~A~x~x} because the third -argument of {\tt eq} is {\tt x} in the type of the pattern {\tt -refl\_equal}. On the contrary, the type of the whole pattern-matching -expression has type {\tt eq~A~y~x} because the third argument of {\tt -eq} is {\tt y} in the type of {\tt H}. This dependency of the case -analysis in the third argument of {\tt eq} is expressed by the -identifier {\tt z} in the return type. - -Finally, the third subcase is a combination of the first and second -subcase. In particular, it only applies to pattern-matching on terms -in a type with annotations. For this third subcase, both -the clauses {\tt as} and {\tt in} are available. - -There are specific notations for case analysis on types with one or -two constructors: ``{\tt if {\ldots} then {\ldots} else {\ldots}}'' -and ``{\tt let (}\nelist{\ldots}{,}{\tt ) := } {\ldots} {\tt in} -{\ldots}'' (see Sections~\ref{if-then-else} and~\ref{Letin}). - -%\SeeAlso Section~\ref{Mult-match} for convenient extensions of pattern-matching. - -\subsection{Recursive functions -\label{fixpoints} -\index{fix@{fix \ident$_i$\{\dots\}}}} - -The expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$} -\texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$ -\binder$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for} -{\ident$_i$}'' denotes the $i$\nth component of a block of functions -defined by mutual well-founded recursion. It is the local counterpart -of the {\tt Fixpoint} command. See Section~\ref{Fixpoint} for more -details. When $n=1$, the ``{\tt for}~{\ident$_i$}'' clause is omitted. - -The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :} -{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binder$_n$ {\tt -:} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$\nth component of -a block of terms defined by a mutual guarded co-recursion. It is the -local counterpart of the {\tt CoFixpoint} command. See -Section~\ref{CoFixpoint} for more details. When $n=1$, the ``{\tt -for}~{\ident$_i$}'' clause is omitted. - -The association of a single fixpoint and a local -definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt - :=}~{\ldots}~{\tt in}~{\ldots}'' stands for ``{\tt let}~$f$~{\tt := - fix}~$f$~\ldots~{\tt :=}~{\ldots}~{\tt in}~{\ldots}''. The same - applies for co-fixpoints. - - -\section{The Vernacular -\label{Vernacular}} - -\begin{figure}[tbp] -\begin{centerframe} -\begin{tabular}{lcl} -{\sentence} & ::= & {\assumption} \\ - & $|$ & {\definition} \\ - & $|$ & {\inductive} \\ - & $|$ & {\fixpoint} \\ - & $|$ & {\assertion} {\proof} \\ -&&\\ -%% Assumptions -{\assumption} & ::= & {\assumptionkeyword} {\assums} {\tt .} \\ -&&\\ -{\assumptionkeyword} & $\!\!$ ::= & {\tt Axiom} $|$ {\tt Conjecture} \\ - & $|$ & {\tt Parameter} $|$ {\tt Parameters} \\ - & $|$ & {\tt Variable} $|$ {\tt Variables} \\ - & $|$ & {\tt Hypothesis} $|$ {\tt Hypotheses}\\ -&&\\ -{\assums} & ::= & \nelist{\ident}{} {\tt :} {\term} \\ - & $|$ & \nelist{{\tt (} \nelist{\ident}{} {\tt :} {\term} {\tt )}}{} \\ -&&\\ -%% Definitions -{\definition} & ::= & - \zeroone{\tt Local} {\tt Definition} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ - & $|$ & {\tt Let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ -&&\\ -%% Inductives -{\inductive} & ::= & - {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\ - & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ - & & \\ -{\inductivebody} & ::= & - {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\ - && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\ - & & \\ %% TODO: where ... -%% Fixpoints -{\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\ - & $|$ & {\tt CoFixpoint} \nelist{\cofixpointbody}{with} {\tt .} \\ -&&\\ -%% Lemmas & proofs -{\assertion} & ::= & - {\statkwd} {\ident} \zeroone{\binders} {\tt :} {\term} {\tt .} \\ -&&\\ - {\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} \\ - & $|$ & {\tt Remark} $|$ {\tt Fact}\\ - & $|$ & {\tt Corollary} $|$ {\tt Proposition} \\ - & $|$ & {\tt Definition} $|$ {\tt Example} \\\\ -&&\\ -{\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\ - & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\ - & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}\\ -\end{tabular} -\end{centerframe} -\caption{Syntax of sentences} -\label{sentences-syntax} -\end{figure} - -Figure \ref{sentences-syntax} describes {\em The Vernacular} which is the -language of commands of \gallina. A sentence of the vernacular -language, like in many natural languages, begins with a capital letter -and ends with a dot. - -The different kinds of command are described hereafter. They all suppose -that the terms occurring in the sentences are well-typed. - -%% -%% Axioms and Parameters -%% -\subsection{Assumptions -\index{Declarations} -\label{Declarations}} - -Assumptions extend the environment\index{Environment} with axioms, -parameters, hypotheses or variables. An assumption binds an {\ident} -to a {\type}. It is accepted by {\Coq} if and only if this {\type} is -a correct type in the environment preexisting the declaration and if -{\ident} was not previously defined in the same module. This {\type} -is considered to be the type (or specification, or statement) assumed -by {\ident} and we say that {\ident} has type {\type}. - -\subsubsection{{\tt Axiom {\ident} :{\term} .} -\comindex{Axiom} -\label{Axiom}} - -This command links {\term} to the name {\ident} as its specification -in the global context. The fact asserted by {\term} is thus assumed as -a postulate. - -\begin{ErrMsgs} -\item \errindex{{\ident} already exists} -\end{ErrMsgs} - -\begin{Variants} -\item \comindex{Parameter}\comindex{Parameters} - {\tt Parameter {\ident} :{\term}.} \\ - Is equivalent to {\tt Axiom {\ident} : {\term}} - -\item {\tt Parameter {\ident$_1$} {\ldots} {\ident$_n$} {\tt :}{\term}.}\\ - Adds $n$ parameters with specification {\term} - -\item - {\tt Parameter\,% -(\,{\ident$_{1,1}$} {\ldots} {\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\;% -\ldots\;{\tt (}\,{\ident$_{n,1}$}{\ldots}{\ident$_{n,k_n}$}\,{\tt :}\,% -{\term$_n$} {\tt )}.}\\ - Adds $n$ blocks of parameters with different specifications. - -\item {\tt Local Axiom {\ident} : {\term}.}\\ -\comindex{Local Axiom} - Such axioms are never made accessible through their unqualified name by - {\tt Import} and its variants (see \ref{Import}). You have to explicitly - give their fully qualified name to refer to them. - -\item \comindex{Conjecture} - {\tt Conjecture {\ident} :{\term}.}\\ - Is equivalent to {\tt Axiom {\ident} : {\term}}. -\end{Variants} - -\noindent {\bf Remark: } It is possible to replace {\tt Parameter} by -{\tt Parameters}. - - -\subsubsection{{\tt Variable {\ident} :{\term}}. -\comindex{Variable} -\comindex{Variables} -\label{Variable}} - -This command links {\term} to the name {\ident} in the context of the -current section (see Section~\ref{Section} for a description of the section -mechanism). When the current section is closed, name {\ident} will be -unknown and every object using this variable will be explicitly -parametrized (the variable is {\em discharged}). Using the {\tt -Variable} command out of any section is equivalent to using {\tt -Local Parameter}. - -\begin{ErrMsgs} -\item \errindex{{\ident} already exists} -\end{ErrMsgs} - -\begin{Variants} -\item {\tt Variable {\ident$_1$} {\ldots} {\ident$_n$} {\tt :}{\term}.}\\ - Links {\term} to names {\ident$_1$} {\ldots} {\ident$_n$}. -\item - {\tt Variable\,% -(\,{\ident$_{1,1}$} {\ldots} {\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\;% -\ldots\;{\tt (}\,{\ident$_{n,1}$} {\ldots}{\ident$_{n,k_n}$}\,{\tt :}\,% -{\term$_n$} {\tt )}.}\\ - Adds $n$ blocks of variables with different specifications. -\item \comindex{Hypothesis} - \comindex{Hypotheses} - {\tt Hypothesis {\ident} {\tt :}{\term}.} \\ - \texttt{Hypothesis} is a synonymous of \texttt{Variable} -\end{Variants} - -\noindent {\bf Remark: } It is possible to replace {\tt Variable} by -{\tt Variables} and {\tt Hypothesis} by {\tt Hypotheses}. - -It is advised to use the keywords \verb:Axiom: and \verb:Hypothesis: -for logical postulates (i.e. when the assertion {\term} is of sort -\verb:Prop:), and to use the keywords \verb:Parameter: and -\verb:Variable: in other cases (corresponding to the declaration of an -abstract mathematical entity). - -%% -%% Definitions -%% -\subsection{Definitions -\index{Definitions} -\label{Basic-definitions}} - -Definitions extend the environment\index{Environment} with -associations of names to terms. A definition can be seen as a way to -give a meaning to a name or as a way to abbreviate a term. In any -case, the name can later be replaced at any time by its definition. - -The operation of unfolding a name into its definition is called -$\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see -Section~\ref{delta}). A definition is accepted by the system if and -only if the defined term is well-typed in the current context of the -definition and if the name is not already used. The name defined by -the definition is called a {\em constant}\index{Constant} and the term -it refers to is its {\em body}. A definition has a type which is the -type of its body. - -A formal presentation of constants and environments is given in -Section~\ref{Typed-terms}. - -\subsubsection{\tt Definition {\ident} := {\term}. -\label{Definition} -\comindex{Definition}} - -This command binds {\term} to the name {\ident} in the -environment, provided that {\term} is well-typed. - -\begin{ErrMsgs} -\item \errindex{{\ident} already exists} -\end{ErrMsgs} - -\begin{Variants} -\item {\tt Definition} {\ident} {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\ - 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$}{\tt .}\\ - 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 Local Definition {\ident} := {\term}.}\\ -\comindex{Local Definition} - Such definitions are never made accessible through their unqualified name by - {\tt Import} and its variants (see \ref{Import}). You have to explicitly - give their fully qualified name to refer to them. -\item {\tt Example {\ident} := {\term}.}\\ -{\tt Example} {\ident} {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\ -{\tt Example} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} - {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\ -\comindex{Example} -These are synonyms of the {\tt Definition} forms. -\end{Variants} - -\begin{ErrMsgs} -\item \errindex{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 let-in definition -{\tt let {\ident} := {\term} in}. Using the {\tt -Let} command out of any section is equivalent to using {\tt -Local Definition}. - -\begin{ErrMsgs} -\item \errindex{{\ident} already exists} -\end{ErrMsgs} - -\begin{Variants} -\item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.} -\item {\tt Let Fixpoint {\ident} \nelist{\fixpointbody}{with} {\tt .}.} -\item {\tt Let CoFixpoint {\ident} \nelist{\cofixpointbody}{with} {\tt .}.} -\end{Variants} - -\SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque}, -\ref{Transparent} (opaque/transparent constants), \ref{unfold} (tactic - {\tt unfold}). - -%% -%% Inductive Types -%% -\subsection{Inductive definitions -\index{Inductive definitions} -\label{gal-Inductive-Definitions} -\comindex{Inductive} -\label{Inductive} -\comindex{Variant} -\label{Variant}} - -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 -\begin{tabular}{l} -{\tt Inductive} {\ident} {\tt :} {\sort} {\tt :=} \\ -\begin{tabular}{clcl} - & {\ident$_1$} & {\tt :} & {\type$_1$} \\ - {\tt |} & {\ldots} && \\ - {\tt |} & {\ident$_n$} & {\tt :} & {\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 names {\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 names {\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 proving some universal property of natural numbers ({\tt -forall n:nat, P n}) by induction on {\tt n}. - -The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except -that they pertain to {\tt (P:nat->Set)} and {\tt (P:nat->Type)} -respectively . They correspond to primitive induction principles -(allowing dependent types) respectively over sorts \verb:Set: and -\verb:Type:. The constant {\ident}{\tt \_ind} is always provided, -whereas {\ident}{\tt \_rec} and {\ident}{\tt \_rect} can be impossible -to derive (for example, when {\ident} is a proposition). - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{Variants} -\item -\begin{coq_example*} -Inductive nat : Set := O | S (_:nat). -\end{coq_example*} -In the case where inductive types have no annotations (next section -gives an example of such annotations), -%the positivity condition implies that -a constructor can be defined by only giving the type of -its arguments. -\end{Variants} - -\subsubsection{Simple annotated inductive types} - -In an annotated inductive types, the universe where the inductive -type is defined is no longer a simple sort, but what is called an -arity, which is a type whose conclusion is a sort. - -As an example of annotated inductive types, let us define the -$even$ predicate: - -\begin{coq_example} -Inductive even : nat -> Prop := - | even_0 : even O - | even_SS : forall n:nat, even n -> even (S (S n)). -\end{coq_example} - -The type {\tt nat->Prop} means that {\tt even} is a unary predicate -(inductively defined) over natural numbers. The type of its two -constructors are the defining clauses of the predicate {\tt even}. The -type of {\tt even\_ind} is: - -\begin{coq_example} -Check even_ind. -\end{coq_example} - -From a mathematical point of view it asserts that the natural numbers -satisfying the predicate {\tt even} are exactly in the smallest set of -naturals satisfying the clauses {\tt even\_0} or {\tt even\_SS}. This -is why, when we want to prove any predicate {\tt P} over elements of -{\tt even}, it is enough to prove it for {\tt O} and to prove that if -any natural number {\tt n} satisfies {\tt P} its double successor {\tt - (S (S n))} satisfies also {\tt P}. This is indeed analogous to the -structural induction principle we got for {\tt nat}. - -\begin{ErrMsgs} -\item \errindex{Non strictly positive occurrence of {\ident} in {\type}} -\item \errindex{The conclusion of {\type} is not valid; it must be -built from {\ident}} -\end{ErrMsgs} - -\subsubsection{Parametrized inductive types} -In the previous example, each constructor introduces a -different instance of the predicate {\tt even}. In some cases, -all the constructors introduces the same generic instance of the -inductive definition, in which case, instead of an annotation, we use -a context of parameters which are binders shared by all the -constructors of the definition. - -% Inductive types may be parameterized. Parameters differ from inductive -% type annotations in the fact that recursive invokations of inductive -% types must always be done with the same values of parameters as its -% specification. - -The general scheme is: -\begin{center} -{\tt Inductive} {\ident} {\binder$_1$}\ldots{\binder$_k$} : {\term} := - {\ident$_1$}: {\term$_1$} | {\ldots} | {\ident$_n$}: \term$_n$ -{\tt .} -\end{center} -Parameters differ from inductive type annotations in the fact that the -conclusion of each type of constructor {\term$_i$} invoke the inductive -type with the same values of parameters as its specification. - - - -A typical example is the definition of polymorphic lists: -\begin{coq_example*} -Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. -\end{coq_example*} - -Note that in the type of {\tt nil} and {\tt cons}, we write {\tt - (list A)} and not just {\tt list}.\\ The constructors {\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. -\item -\begin{coq_example*} -Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B. -\end{coq_example*} -The {\tt Variant} keyword is identical to the {\tt Inductive} keyword, -except that it disallows recursive definition of types (in particular -lists cannot be defined with the {\tt Variant} keyword). No induction -scheme is generated for this variant, unless the option -{\tt Nonrecursive Elimination Schemes} is set -(see~\ref{set-nonrecursive-elimination-schemes}). -\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} -Fail Inductive listw (A:Set) : Set := - | nilw : listw (A*A) - | consw : A -> listw (A*A) -> listw (A*A). -\end{coq_example} -Because the conclusion of the type of constructors should be {\tt - listw A} in both cases. - -A parametrized inductive definition can be defined using -annotations instead of parameters but it will sometimes give a -different (bigger) sort for the inductive definition and will produce -a less convenient rule for case elimination. - -\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{Tac-induction}. - - -\subsubsection{Mutually defined inductive types -\comindex{Inductive} -\label{Mutual-Inductive}} - -The definition of a block of mutually inductive types has the form: - -\medskip -{\tt -\begin{tabular}{l} -Inductive {\ident$_1$} : {\type$_1$} := \\ -\begin{tabular}{clcl} - & {\ident$_1^1$} &:& {\type$_1^1$} \\ - | & {\ldots} && \\ - | & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$} -\end{tabular} \\ -with\\ -~{\ldots} \\ -with {\ident$_m$} : {\type$_m$} := \\ -\begin{tabular}{clcl} - & {\ident$_1^m$} &:& {\type$_1^m$} \\ - | & {\ldots} \\ - | & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}. -\end{tabular} -\end{tabular} -} -\medskip - -\noindent It has the same semantics as the above {\tt Inductive} -definition for each \ident$_1$, {\ldots}, \ident$_m$. All names -\ident$_1$, {\ldots}, \ident$_m$ and \ident$_1^1$, \dots, -\ident$_{n_m}^m$ are simultaneously added to the environment. Then -well-typing of constructors can be checked. Each one of the -\ident$_1$, {\ldots}, \ident$_m$ can be used on its own. - -It is also possible to parametrize these inductive definitions. -However, parameters correspond to a local -context in which the whole set of inductive declarations is done. For -this reason, the parameters must be strictly the same for each -inductive types The extended syntax is: - -\medskip -\begin{tabular}{l} -{\tt Inductive} {\ident$_1$} {\params} {\tt :} {\type$_1$} {\tt :=} \\ -\begin{tabular}{clcl} - & {\ident$_1^1$} &{\tt :}& {\type$_1^1$} \\ - {\tt |} & {\ldots} && \\ - {\tt |} & {\ident$_{n_1}^1$} &{\tt :}& {\type$_{n_1}^1$} -\end{tabular} \\ -{\tt with}\\ -~{\ldots} \\ -{\tt with} {\ident$_m$} {\params} {\tt :} {\type$_m$} {\tt :=} \\ -\begin{tabular}{clcl} - & {\ident$_1^m$} &{\tt :}& {\type$_1^m$} \\ - {\tt |} & {\ldots} \\ - {\tt |} & {\ident$_{n_m}^m$} &{\tt :}& {\type$_{n_m}^m$}. -\end{tabular} -\end{tabular} -\medskip - -\Example -The typical example of a mutual inductive data type is the one for -trees and forests. We assume given two types $A$ and $B$ as variables. -It can be declared the following way. - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example*} -Variables A B : Set. -Inductive tree : Set := - node : A -> forest -> tree -with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. -\end{coq_example*} - -This declaration generates automatically six induction -principles. They are respectively -called {\tt tree\_rec}, {\tt tree\_ind}, {\tt - tree\_rect}, {\tt forest\_rec}, {\tt forest\_ind}, {\tt - forest\_rect}. These ones are not the most general ones but are -just the induction principles corresponding to each inductive part -seen as a single inductive definition. - -To illustrate this point on our example, we give the types of {\tt - tree\_rec} and {\tt forest\_rec}. - -\begin{coq_example} -Check tree_rec. -Check forest_rec. -\end{coq_example} - -Assume we want to parametrize our mutual inductive definitions with -the two type variables $A$ and $B$, the declaration should be done the -following way: - -\begin{coq_eval} -Reset tree. -\end{coq_eval} -\begin{coq_example*} -Inductive tree (A B:Set) : Set := - node : A -> forest A B -> tree A B -with forest (A B:Set) : Set := - | leaf : B -> forest A B - | cons : tree A B -> forest A B -> forest A B. -\end{coq_example*} - -Assume we define an inductive definition inside a section. When the -section is closed, the variables declared in the section and occurring -free in the declaration are added as parameters to the inductive -definition. - -\SeeAlso Section~\ref{Section}. - -\subsubsection{Co-inductive types -\label{CoInductiveTypes} -\comindex{CoInductive}} - -The objects of an inductive type are well-founded with respect to the -constructors of the type. In other words, such objects contain only a -{\it finite} number of constructors. Co-inductive types arise from -relaxing this condition, and admitting types whose objects contain an -infinity of constructors. Infinite objects are introduced by a -non-ending (but effective) process of construction, defined in terms -of the constructors of the type. - -An example of a co-inductive type is the type of infinite sequences of -natural numbers, usually called streams. It can be introduced in \Coq\ -using the \texttt{CoInductive} command: -\begin{coq_example} -CoInductive Stream : Set := - Seq : nat -> Stream -> Stream. -\end{coq_example} - -The syntax of this command is the same as the command \texttt{Inductive} -(see Section~\ref{gal-Inductive-Definitions}). Notice that no -principle of induction is derived from the definition of a -co-inductive type, since such principles only make sense for inductive -ones. For co-inductive ones, the only elimination principle is case -analysis. For example, the usual destructors on streams -\texttt{hd:Stream->nat} and \texttt{tl:Str->Str} can be defined as -follows: -\begin{coq_example} -Definition hd (x:Stream) := let (a,s) := x in a. -Definition tl (x:Stream) := let (a,s) := x in s. -\end{coq_example} - -Definition of co-inductive predicates and blocks of mutually -co-inductive definitions are also allowed. An example of a -co-inductive predicate is the extensional equality on streams: - -\begin{coq_example} -CoInductive EqSt : Stream -> Stream -> Prop := - eqst : - forall s1 s2:Stream, - hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. -\end{coq_example} - -In order to prove the extensionally equality of two streams $s_1$ and -$s_2$ we have to construct an infinite proof of equality, that is, -an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see -how to introduce infinite objects in Section~\ref{CoFixpoint}. - -%% -%% (Co-)Fixpoints -%% -\subsection{Definition of recursive functions} - -\subsubsection{Definition of functions by recursion over inductive objects} - -This section describes the primitive form of definition by recursion -over inductive objects. See Section~\ref{Function} for more advanced -constructions. The command: -\begin{center} - \texttt{Fixpoint {\ident} {\params} {\tt \{struct} - \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ - \comindex{Fixpoint}\label{Fixpoint}} -\end{center} -allows defining functions by pattern-matching over inductive objects -using a fixed point construction. -The meaning of this declaration is to define {\it ident} a recursive -function with arguments specified by the binders in {\params} such -that {\it ident} applied to arguments corresponding to these binders -has type \type$_0$, and is equivalent to the expression \term$_0$. The -type of the {\ident} is consequently {\tt forall {\params} {\tt,} - \type$_0$} and the value is equivalent to {\tt fun {\params} {\tt - =>} \term$_0$}. - -To be accepted, a {\tt Fixpoint} definition has to satisfy some -syntactical constraints on a special argument called the decreasing -argument. They are needed to ensure that the {\tt Fixpoint} definition -always terminates. The point of the {\tt \{struct \ident {\tt \}}} -annotation is to let the user tell the system which argument decreases -along the recursive calls. For instance, one can define the addition -function as : - -\begin{coq_example} -Fixpoint add (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (add p m) - end. -\end{coq_example} - -The {\tt \{struct \ident {\tt \}}} annotation may be left implicit, in -this case the system try successively arguments from left to right -until it finds one that satisfies the decreasing condition. Note that -some fixpoints may have several arguments that fit as decreasing -arguments, and this choice influences the reduction of the -fixpoint. Hence an explicit annotation must be used if the leftmost -decreasing argument is not the desired one. Writing explicit -annotations can also speed up type-checking of large mutual fixpoints. - -The {\tt match} operator matches a value (here \verb:n:) with the -various constructors of its (inductive) type. The remaining arguments -give the respective values to be returned, as functions of the -parameters of the corresponding constructor. Thus here when \verb:n: -equals \verb:O: we return \verb:m:, and when \verb:n: equals -\verb:(S p): we return \verb:(S (add p m)):. - -The {\tt match} operator is formally described -in detail in Section~\ref{Caseexpr}. The system recognizes that in -the inductive call {\tt (add p m)} the first argument actually -decreases because it is a {\em pattern variable} coming from {\tt match - n with}. - -\Example The following definition is not correct and generates an -error message: - -\begin{coq_eval} -Set Printing Depth 50. -\end{coq_eval} -% (********** The following is not correct and should produce **********) -% (********* Error: Recursive call to wrongplus ... **********) -\begin{coq_example} -Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := - match m with - | O => n - | S p => S (wrongplus n p) - end. -\end{coq_example} - -because the declared decreasing argument {\tt n} actually does not -decrease in the recursive call. The function computing the addition -over the second argument should rather be written: - -\begin{coq_example*} -Fixpoint plus (n m:nat) {struct m} : nat := - match m with - | O => n - | S p => S (plus n p) - end. -\end{coq_example*} - -The ordinary match operation on natural numbers can be mimicked in the -following way. -\begin{coq_example*} -Fixpoint nat_match - (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C := - match n with - | O => f0 - | S p => fS p (nat_match C f0 fS p) - end. -\end{coq_example*} -The recursive call may not only be on direct subterms of the recursive -variable {\tt n} but also on a deeper subterm and we can directly -write the function {\tt mod2} which gives the remainder modulo 2 of a -natural number. -\begin{coq_example*} -Fixpoint mod2 (n:nat) : nat := - match n with - | O => O - | S p => match p with - | O => S O - | S q => mod2 q - end - end. -\end{coq_example*} -In order to keep the strong normalization property, the fixed point -reduction will only be performed when the argument in position of the -decreasing argument (which type should be in an inductive definition) -starts with a constructor. - -The {\tt Fixpoint} construction enjoys also the {\tt with} extension -to define functions over mutually defined inductive types or more -generally any mutually recursive definitions. - -\begin{Variants} -\item {\tt Fixpoint} {\ident$_1$} {\params$_1$} {\tt :} {\type$_1$} {\tt :=} {\term$_1$}\\ - {\tt with} {\ldots} \\ - {\tt with} {\ident$_m$} {\params$_m$} {\tt :} {\type$_m$} {\tt :=} {\term$_m$}\\ - Allows to define simultaneously {\ident$_1$}, {\ldots}, - {\ident$_m$}. -\end{Variants} - -\Example -The size of trees and forests can be defined the following way: -\begin{coq_eval} -Reset Initial. -Variables A B : Set. -Inductive tree : Set := - node : A -> forest -> tree -with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. -\end{coq_eval} -\begin{coq_example*} -Fixpoint tree_size (t:tree) : nat := - match t with - | node a f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | leaf b => 1 - | cons t f' => (tree_size t + forest_size f') - end. -\end{coq_example*} -A generic command {\tt Scheme} is useful to build automatically various -mutual induction principles. It is described in Section~\ref{Scheme}. - -\subsubsection{Definitions of recursive objects in co-inductive types} - -The command: -\begin{center} - \texttt{CoFixpoint {\ident} : \type$_0$ := \term$_0$} - \comindex{CoFixpoint}\label{CoFixpoint} -\end{center} -introduces a method for constructing an infinite object of a -coinduc\-tive type. For example, the stream containing all natural -numbers can be introduced applying the following method to the number -\texttt{O} (see Section~\ref{CoInductiveTypes} for the definition of -{\tt Stream}, {\tt hd} and {\tt tl}): -\begin{coq_eval} -Reset Initial. -CoInductive Stream : Set := - Seq : nat -> Stream -> Stream. -Definition hd (x:Stream) := match x with - | Seq a s => a - end. -Definition tl (x:Stream) := match x with - | Seq a s => s - end. -\end{coq_eval} -\begin{coq_example} -CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). -\end{coq_example} - -Oppositely to recursive ones, there is no decreasing argument in a -co-recursive definition. To be admissible, a method of construction -must provide at least one extra constructor of the infinite object for -each iteration. A syntactical guard condition is imposed on -co-recursive definitions in order to ensure this: each recursive call -in the definition must be protected by at least one constructor, and -only by constructors. That is the case in the former definition, where -the single recursive call of \texttt{from} is guarded by an -application of \texttt{Seq}. On the contrary, the following recursive -function does not satisfy the guard condition: - -\begin{coq_eval} -Set Printing Depth 50. -\end{coq_eval} -% (********** The following is not correct and should produce **********) -% (***************** Error: Unguarded recursive call *******************) -\begin{coq_example} -Fail 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$} {\tt :} {\type$_1$} {\tt :=} {\term$_1$}\\ - {\tt with}\\ - \mbox{}\hspace{0.1cm} {\ldots} \\ - {\tt with} {\ident$_m$} {\tt :} {\type$_m$} {\tt :=} {\term$_m$}\\ -As in the \texttt{Fixpoint} command (see Section~\ref{Fixpoint}), it -is possible to introduce a block of mutually dependent methods. -\end{Variants} - -%% -%% Theorems & Lemmas -%% -\subsection{Assertions and proofs} -\label{Assertions} - -An assertion states a proposition (or a type) of which the proof (or -an inhabitant of the type) is interactively built using tactics. The -interactive proof mode is described in -Chapter~\ref{Proof-handling} and the tactics in Chapter~\ref{Tactics}. -The basic assertion command is: - -\subsubsection{\tt Theorem {\ident} \zeroone{\binders} : {\type}. -\comindex{Theorem}} - -After the statement is asserted, {\Coq} needs a proof. Once a proof of -{\type} under the assumptions represented by {\binders} is given and -validated, the proof is generalized into a proof of {\tt forall - \zeroone{\binders}, {\type}} and the theorem is bound to the name -{\ident} in the environment. - -\begin{ErrMsgs} - -\item \errindex{The term {\form} has type {\ldots} which should be Set, - Prop or Type} - -\item \errindexbis{{\ident} already exists}{already exists} - - The name you provided is already defined. You have then to choose - another name. - -\end{ErrMsgs} - -\begin{Variants} -\item {\tt Lemma {\ident} \zeroone{\binders} : {\type}.}\comindex{Lemma}\\ - {\tt Remark {\ident} \zeroone{\binders} : {\type}.}\comindex{Remark}\\ - {\tt Fact {\ident} \zeroone{\binders} : {\type}.}\comindex{Fact}\\ - {\tt Corollary {\ident} \zeroone{\binders} : {\type}.}\comindex{Corollary}\\ - {\tt Proposition {\ident} \zeroone{\binders} : {\type}.}\comindex{Proposition} - -These commands are synonyms of \texttt{Theorem {\ident} \zeroone{\binders} : {\type}}. - -\item {\tt Theorem \nelist{{\ident} \zeroone{\binders}: {\type}}{with}.} - -This command is useful for theorems that are proved by simultaneous -induction over a mutually inductive assumption, or that assert mutually -dependent statements in some mutual co-inductive type. It is equivalent -to {\tt Fixpoint} or {\tt CoFixpoint} -(see Section~\ref{CoFixpoint}) but using tactics to build the proof of -the statements (or the body of the specification, depending on the -point of view). The inductive or co-inductive types on which the -induction or coinduction has to be done is assumed to be non ambiguous -and is guessed by the system. - -Like in a {\tt Fixpoint} or {\tt CoFixpoint} definition, the induction -hypotheses have to be used on {\em structurally smaller} arguments -(for a {\tt Fixpoint}) or be {\em guarded by a constructor} (for a {\tt - CoFixpoint}). The verification that recursive proof arguments are -correct is done only at the time of registering the lemma in the -environment. To know if the use of induction hypotheses is correct at -some time of the interactive development of a proof, use the command -{\tt Guarded} (see Section~\ref{Guarded}). - -The command can be used also with {\tt Lemma}, -{\tt Remark}, etc. instead of {\tt Theorem}. - -\item {\tt Definition {\ident} \zeroone{\binders} : {\type}.} - -This allows defining a term of type {\type} using the proof editing mode. It -behaves as {\tt Theorem} but is intended to be used in conjunction with - {\tt Defined} (see \ref{Defined}) in order to define a - constant of which the computational behavior is relevant. - -The command can be used also with {\tt Example} instead -of {\tt Definition}. - -\SeeAlso Sections~\ref{Opaque} and~\ref{Transparent} ({\tt Opaque} -and {\tt Transparent}) and~\ref{unfold} (tactic {\tt unfold}). - -\item {\tt Let {\ident} \zeroone{\binders} : {\type}.} - -Like {\tt Definition {\ident} \zeroone{\binders} : {\type}.} except -that the definition is turned into a let-in definition generalized over -the declarations depending on it after closing the current section. - -\item {\tt Fixpoint \nelist{{\ident} {\binders} \zeroone{\annotation} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.} -\comindex{Fixpoint} - -This generalizes the syntax of {\tt Fixpoint} so that one or more -bodies can be defined interactively using the proof editing mode (when -a body is omitted, its type is mandatory in the syntax). When the -block of proofs is completed, it is intended to be ended by {\tt - Defined}. - -\item {\tt CoFixpoint \nelist{{\ident} \zeroone{\binders} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.} -\comindex{CoFixpoint} - -This generalizes the syntax of {\tt CoFixpoint} so that one or more bodies -can be defined interactively using the proof editing mode. - -\end{Variants} - -\subsubsection{{\tt Proof.} {\dots} {\tt Qed.} -\comindex{Proof} -\comindex{Qed}} - -A proof starts by the keyword {\tt Proof}. Then {\Coq} enters the -proof editing mode until the proof is completed. The proof editing -mode essentially contains tactics that are described in chapter -\ref{Tactics}. Besides tactics, there are commands to manage the proof -editing mode. They are described in Chapter~\ref{Proof-handling}. When -the proof is completed it should be validated and put in the -environment using the keyword {\tt Qed}. -\medskip - -\ErrMsg -\begin{enumerate} -\item \errindex{{\ident} already exists} -\end{enumerate} - -\begin{Remarks} -\item Several statements can be simultaneously asserted. -\item Not only other assertions but any vernacular command can be given -while in the process of proving a given assertion. In this case, the command is -understood as if it would have been given before the statements still to be -proved. -\item {\tt Proof} is recommended but can currently be omitted. On the -opposite side, {\tt Qed} (or {\tt Defined}, see below) is mandatory to -validate a proof. -\item Proofs ended by {\tt Qed} are declared opaque. Their content - cannot be unfolded (see \ref{Conversion-tactics}), thus realizing - some form of {\em proof-irrelevance}. To be able to unfold a proof, - the proof should be ended by {\tt Defined} (see below). -\end{Remarks} - -\begin{Variants} -\item \comindex{Defined} - {\tt Proof.} {\dots} {\tt Defined.}\\ - Same as {\tt Proof.} {\dots} {\tt Qed.} but the proof is - then declared transparent, which means that its - content can be explicitly used for type-checking and that it - can be unfolded in conversion tactics (see - \ref{Conversion-tactics}, \ref{Opaque}, \ref{Transparent}). -%Not claimed to be part of Gallina... -%\item {\tt Proof.} {\dots} {\tt Save.}\\ -% Same as {\tt Proof.} {\dots} {\tt Qed.} -%\item {\tt Goal} \type {\dots} {\tt Save} \ident \\ -% Same as {\tt Lemma} \ident {\tt :} \type \dots {\tt Save.} -% This is intended to be used in the interactive mode. -\item \comindex{Admitted} - {\tt Proof.} {\dots} {\tt Admitted.}\\ - Turns the current asserted statement into an axiom and exits the - proof mode. -\end{Variants} - -% Local Variables: -% mode: LaTeX -% TeX-master: "Reference-Manual" -% End: - diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index d373f76bf..ba4018d77 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -94,7 +94,6 @@ Options A and B of the licence are {\em not} elected.} %BEGIN LATEX \defaultheaders %END LATEX -\include{RefMan-gal.v}% Gallina \part{The proof engine} diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst new file mode 100644 index 000000000..96ea9627b --- /dev/null +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -0,0 +1,1736 @@ +\chapter{The \gallina{} specification language +\label{Gallina}\index{Gallina}} +%HEVEA\cutname{gallina.html} +\label{BNF-syntax} % Used referred to as a chapter label + +This chapter describes \gallina, the specification language of {\Coq}. +It allows developing mathematical theories and proofs of specifications +of programs. The theories are built from axioms, hypotheses, +parameters, lemmas, theorems and definitions of constants, functions, +predicates and sets. The syntax of logical objects involved in +theories is described in Section~\ref{term}. The language of +commands, called {\em The Vernacular} is described in section +\ref{Vernacular}. + +In {\Coq}, logical objects are typed to ensure their logical +correctness. The rules implemented by the typing algorithm are described in +Chapter \ref{Cic}. + +\subsection*{About the grammars in the manual +\index{BNF metasyntax}} + +Grammars are presented in Backus-Naur form (BNF). Terminal symbols are +set in {\tt typewriter font}. In addition, there are special +notations for regular expressions. + +An expression enclosed in square brackets \zeroone{\ldots} means at +most one occurrence of this expression (this corresponds to an +optional component). + +The notation ``\nelist{\entry}{sep}'' stands for a non empty +sequence of expressions parsed by {\entry} and +separated by the literal ``{\tt sep}''\footnote{This is similar to the +expression ``{\entry} $\{$ {\tt sep} {\entry} $\}$'' in +standard BNF, or ``{\entry}~{$($} {\tt sep} {\entry} {$)$*}'' in +the syntax of regular expressions.}. + +Similarly, the notation ``\nelist{\entry}{}'' stands for a non +empty sequence of expressions parsed by the ``{\entry}'' entry, +without any separator between. + +Finally, the notation ``\sequence{\entry}{\tt sep}'' stands for a +possibly empty sequence of expressions parsed by the ``{\entry}'' entry, +separated by the literal ``{\tt sep}''. + +\section{Lexical conventions +\label{lexical}\index{Lexical conventions}} + +\paragraph{Blanks} +Space, newline and horizontal tabulation are considered as blanks. +Blanks are ignored but they separate tokens. + +\paragraph{Comments} + +Comments in {\Coq} are enclosed between {\tt (*} and {\tt + *)}\index{Comments}, and can be nested. They can contain any +character. However, string literals must be correctly closed. Comments +are treated as blanks. + +\paragraph{Identifiers and access identifiers} + +Identifiers, written {\ident}, are sequences of letters, digits, +\verb!_! and \verb!'!, that do not start with a digit or \verb!'!. +That is, they are recognized by the following lexical class: + +\index{ident@\ident} +\begin{center} +\begin{tabular}{rcl} +{\firstletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt \_} +$\mid$ {\tt unicode-letter} +\\ +{\subsequentletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt 0..9} +$\mid$ {\tt \_} % $\mid$ {\tt \$} +$\mid$ {\tt '} +$\mid$ {\tt unicode-letter} +$\mid$ {\tt unicode-id-part} \\ +{\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{} +\end{tabular} +\end{center} +All characters are meaningful. In particular, identifiers are +case-sensitive. The entry {\tt unicode-letter} non-exhaustively +includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, +Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical +letter-like symbols, hyphens, non-breaking space, {\ldots} The entry +{\tt unicode-id-part} non-exhaustively includes symbols for prime +letters and subscripts. + +Access identifiers, written {\accessident}, are identifiers prefixed +by \verb!.! (dot) without blank. They are used in the syntax of qualified +identifiers. + +\paragraph{Natural numbers and integers} +Numerals are sequences of digits. Integers are numerals optionally preceded by a minus sign. + +\index{num@{\num}} +\index{integer@{\integer}} +\begin{center} +\begin{tabular}{r@{\quad::=\quad}l} +{\digit} & {\tt 0..9} \\ +{\num} & \nelistwithoutblank{\digit}{} \\ +{\integer} & \zeroone{\tt -}{\num} \\ +\end{tabular} +\end{center} + +\paragraph[Strings]{Strings\label{strings} +\index{string@{\qstring}}} +Strings are delimited by \verb!"! (double quote), and enclose a +sequence of any characters different from \verb!"! or the sequence +\verb!""! to denote the double quote character. In grammars, the +entry for quoted strings is {\qstring}. + +\paragraph{Keywords} +The following identifiers are reserved keywords, and cannot be +employed otherwise: +\begin{center} +\begin{tabular}{llllll} +\verb!_! & +\verb!as! & +\verb!at! & +\verb!cofix! & +\verb!else! & +\verb!end! \\ +% +\verb!exists! & +\verb!exists2! & +\verb!fix! & +\verb!for! & +\verb!forall! & +\verb!fun! \\ +% +\verb!if! & +\verb!IF! & +\verb!in! & +\verb!let! & +\verb!match! & +\verb!mod! \\ +% +\verb!Prop! & +\verb!return! & +\verb!Set! & +\verb!then! & +\verb!Type! & +\verb!using! \\ +% +\verb!where! & +\verb!with! & +\end{tabular} +\end{center} + + +\paragraph{Special tokens} +The following sequences of characters are special tokens: +\begin{center} +\begin{tabular}{lllllll} +\verb/!/ & +\verb!%! & +\verb!&! & +\verb!&&! & +\verb!(! & +\verb!()! & +\verb!)! \\ +% +\verb!*! & +\verb!+! & +\verb!++! & +\verb!,! & +\verb!-! & +\verb!->! & +\verb!.! \\ +% +\verb!.(! & +\verb!..! & +\verb!/! & +\verb!/\! & +\verb!:! & +\verb!::! & +\verb!:! & +\verb!;! & +\verb!! & +\verb!<:! \\ +% +\verb!<=! & +\verb!<>! & +\verb!=! & +\verb!=>! & +\verb!=_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 syntax of +the terms of the {\em Calculus of Inductive Constructions} (also +called \CIC). The formal presentation of {\CIC} is given in Chapter +\ref{Cic}. Extensions of this syntax are given in chapter +\ref{Gallina-extension}. How to customize the syntax is described in Chapter +\ref{Addoc-syntax}. + +\begin{figure}[htbp] +\begin{centerframe} +\begin{tabular}{lcl@{\quad~}r} % warning: page width exceeded with \qquad +{\term} & ::= & + {\tt forall} {\binders} {\tt ,} {\term} &(\ref{products})\\ + & $|$ & {\tt fun} {\binders} {\tt =>} {\term} &(\ref{abstractions})\\ + & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\ + & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\ + & $|$ & {\tt let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} + {\tt in} {\term} &(\ref{let-in})\\ + & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\ + & $|$ & {\tt let cofix} {\cofixpointbody} + {\tt in} {\term} &(\ref{fixpoints})\\ + & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem} + {\tt :=} {\term} + {\tt in} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ + & $|$ & {\tt let '} {\pattern} \zeroone{{\tt in} {\term}} {\tt :=} {\term} + \zeroone{\returntype} {\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{typecast})\\ + & $|$ & {\term} {\tt :>} &(\ref{ProgramSyntax})\\ + & $|$ & {\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})\\ + & $|$ & {\tt (} {\term} {\tt )} & \\ + & & &\\ +{\termarg} & ::= & {\term} &\\ + & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )} + &(\ref{Implicits-explicitation})\\ +%% & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )} +%% &(\ref{Implicits-explicitation})\\ +&&&\\ +{\binders} & ::= & \nelist{\binder}{} \\ +&&&\\ +{\binder} & ::= & {\name} & (\ref{Binders}) \\ + & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ + & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\ + & $|$ & {\tt '} {\pattern} &\\ +& & &\\ +{\name} & ::= & {\ident} &\\ + & $|$ & {\tt \_} &\\ +&&&\\ +{\qualid} & ::= & {\ident} & \\ + & $|$ & {\qualid} {\accessident} &\\ + & & &\\ +{\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} & +\end{tabular} +\end{centerframe} +\caption{Syntax of terms} +\label{term-syntax} +\index{term@{\term}} +\index{sort@{\sort}} +\end{figure} + + + +\begin{figure}[htb] +\begin{centerframe} +\begin{tabular}{lcl} +{\fixpointbodies} & ::= & + {\fixpointbody} \\ + & $|$ & {\fixpointbody} {\tt with} \nelist{\fixpointbody}{{\tt with}} + {\tt for} {\ident} \\ +{\cofixpointbodies} & ::= & + {\cofixpointbody} \\ + & $|$ & {\cofixpointbody} {\tt with} \nelist{\cofixpointbody}{{\tt with}} + {\tt for} {\ident} \\ +&&\\ +{\fixpointbody} & ::= & + {\ident} {\binders} \zeroone{\annotation} {\typecstr} + {\tt :=} {\term} \\ +{\cofixpointbody} & ::= & {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} \\ + & &\\ +{\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ +&&\\ +{\caseitem} & ::= & {\term} \zeroone{{\tt as} \name} + \zeroone{{\tt in} \qualid \sequence{\pattern}{}} \\ +&&\\ +{\ifitem} & ::= & \zeroone{{\tt as} {\name}} {\returntype} \\ +&&\\ +{\returntype} & ::= & {\tt return} {\term} \\ +&&\\ +{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\ +&&\\ +{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\ +&&\\ +{\pattern} & ::= & {\qualid} \nelist{\pattern}{} \\ + & $|$ & {\tt @} {\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 such as {\tt fun}, {\tt forall}, {\tt fix} and +{\tt cofix} {\em bind} variables. A binding is represented by an +identifier. If the binding variable is not used in the expression, the +identifier can be replaced by the symbol {\tt \_}. When the type of a +bound variable cannot be synthesized by the system, it can be +specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt +)}. There is also a notation for a sequence of binding variables +sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt +:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote, +e.g. {\tt '(x,y)}. + +Some constructions allow the binding of a variable to value. This is +called a ``let-binder''. The entry {\binder} of the grammar accepts +either an assumption binder as defined above or a let-binder. +The notation in the +latter case is {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )}. In a +let-binder, only one variable can be introduced at the same +time. It is also possible to give the type of the variable as follows: +{\tt (}\,{\ident}\,{\tt :}\,{\term}\,{\tt :=}\,{\term}\,{\tt )}. + +Lists of {\binder} are allowed. In the case of {\tt fun} and {\tt + forall}, it is intended that at least one binder of the list is an +assumption otherwise {\tt fun} and {\tt forall} gets identical. Moreover, +parentheses can be omitted in the case of a single sequence of +bindings sharing the same type (e.g.: {\tt fun~(x~y~z~:~A)~=>~t} can +be shortened in {\tt fun~x~y~z~:~A~=>~t}). + +\subsection{Abstractions +\label{abstractions} +\index{abstractions}} +\index{fun@{{\tt fun \ldots => \ldots}}} + +The expression ``{\tt fun} {\ident} {\tt :} {\type} {\tt =>}~{\term}'' +defines the {\em abstraction} of the variable {\ident}, of type +{\type}, over the term {\term}. It denotes a function of the variable +{\ident} that evaluates to the expression {\term} (e.g. {\tt fun x:$A$ +=> x} denotes the identity function on type $A$). +% The variable {\ident} is called the {\em parameter} of the function +% (we sometimes say the {\em formal parameter}). +The keyword {\tt fun} can be followed by several binders as given in +Section~\ref{Binders}. Functions over several variables are +equivalent to an iteration of one-variable functions. For instance the +expression ``{\tt fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt +:}~\type~{\tt =>}~{\term}'' denotes the same function as ``{\tt +fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt =>}~{\ldots}~{\tt +fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}''. If a let-binder +occurs in the list of binders, it is expanded to a let-in definition +(see Section~\ref{let-in}). + +\subsection{Products +\label{products} +\index{products}} +\index{forall@{{\tt forall \ldots, \ldots}}} + +The expression ``{\tt forall}~{\ident}~{\tt :}~{\type}{\tt +,}~{\term}'' denotes the {\em product} of the variable {\ident} of +type {\type}, over the term {\term}. As for abstractions, {\tt forall} +is followed by a binder list, and products over several variables are +equivalent to an iteration of one-variable products. +Note that {\term} is intended to be a type. + +If the variable {\ident} occurs in {\term}, the product is called {\em +dependent product}. The intention behind a dependent product {\tt +forall}~$x$~{\tt :}~{$A$}{\tt ,}~{$B$} is twofold. It denotes either +the universal quantification of the variable $x$ of type $A$ in the +proposition $B$ or the functional dependent product from $A$ to $B$ (a +construction usually written $\Pi_{x:A}.B$ in set theory). + +Non dependent product types have a special notation: ``$A$ {\tt ->} +$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. The {\em non dependent +product} is used both to denote the propositional implication and +function types. + +\subsection{Applications +\label{applications} +\index{applications}} + +The expression \term$_0$ \term$_1$ denotes the application of +\term$_0$ to \term$_1$. + +The expression {\tt }\term$_0$ \term$_1$ ... \term$_n${\tt} +denotes the application of the term \term$_0$ to the arguments +\term$_1$ ... then \term$_n$. It is equivalent to {\tt (} {\ldots} +{\tt (} {\term$_0$} {\term$_1$} {\tt )} {\ldots} {\tt )} {\term$_n$} {\tt }: +associativity is to the left. + +The notation {\tt (}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )} for +arguments is used for making explicit the value of implicit arguments +(see Section~\ref{Implicits-explicitation}). + +\subsection{Type cast +\label{typecast} +\index{Cast}} +\index{cast@{{\tt(\ldots: \ldots)}}} + +The expression ``{\term}~{\tt :}~{\type}'' is a type cast +expression. It enforces the type of {\term} to be {\type}. + +``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine for checking +that {\term} has type {\type}. + +\subsection{Inferable subterms +\label{hole} +\index{\_}} + +Expressions often contain redundant pieces of information. Subterms that +can be automatically inferred by {\Coq} can be replaced by the +symbol ``\_'' and {\Coq} will guess the missing piece of information. + +\subsection{Let-in definitions +\label{let-in} +\index{Let-in definitions} +\index{let-in}} +\index{let@{{\tt let \ldots := \ldots in \ldots}}} + + +{\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 let-in definition of functions: {\tt +let} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} {\tt :=} {\term$_1$} +{\tt in} {\term$_2$} stands for {\tt let} {\ident} {\tt := fun} +{\binder$_1$} {\ldots} {\binder$_n$} {\tt =>} {\term$_1$} {\tt in} +{\term$_2$}. + +\subsection{Definition by case analysis +\label{caseanalysis} +\index{match@{\tt match\ldots with\ldots end}}} + +Objects of inductive types can be destructurated by a case-analysis +construction called {\em pattern-matching} expression. A +pattern-matching expression is used to analyze the structure of an +inductive objects and to apply specific treatments accordingly. + +This paragraph describes the basic form of pattern-matching. See +Section~\ref{Mult-match} and Chapter~\ref{Mult-match-full} for the +description of the general form. The basic form of pattern-matching is +characterized by a single {\caseitem} expression, a {\multpattern} +restricted to a single {\pattern} and {\pattern} restricted to the +form {\qualid} \nelist{\ident}{}. + +The expression {\tt match} {\term$_0$} {\returntype} {\tt with} +{\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$} +{\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em +pattern-matching} over the term {\term$_0$} (expected to be of an +inductive type $I$). The terms {\term$_1$}\ldots{\term$_n$} are the +{\em branches} of the pattern-matching expression. Each of +{\pattern$_i$} has a form \qualid~\nelist{\ident}{} where {\qualid} +must denote a constructor. There should be exactly one branch for +every constructor of $I$. + +The {\returntype} expresses the type returned by the whole {\tt match} +expression. There are several cases. In the {\em non dependent} case, +all branches have the same type, and the {\returntype} is the common +type of branches. In this case, {\returntype} can usually be omitted +as it can be inferred from the type of the branches\footnote{Except if +the inductive type is empty in which case there is no equation that can be +used to infer the return type.}. + +In the {\em dependent} case, there are three subcases. In the first +subcase, the type in each branch may depend on the exact value being +matched in the branch. In this case, the whole pattern-matching itself +depends on the term being matched. This dependency of the term being +matched in the return type is expressed with an ``{\tt as {\ident}}'' +clause where {\ident} is dependent in the return type. +For instance, in the following example: +\begin{coq_example*} +Inductive bool : Type := true : bool | false : bool. +Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. +Inductive or (A:Prop) (B:Prop) : Prop := +| or_introl : A -> or A B +| or_intror : B -> or A B. +Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) +:= match b as x return or (eq bool x true) (eq bool x false) with + | true => or_introl (eq bool true true) (eq bool true false) + (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) + (eq_refl bool false) + end. +\end{coq_example*} +the branches have respective types {\tt or (eq bool true true) (eq +bool true false)} and {\tt or (eq bool false true) (eq bool false +false)} while the whole pattern-matching expression has type {\tt or +(eq bool b true) (eq bool b false)}, the identifier {\tt x} being used +to represent the dependency. Remark that when the term being matched +is a variable, the {\tt as} clause can be omitted and the term being +matched can serve itself as binding name in the return type. For +instance, the following alternative definition is accepted and has the +same meaning as the previous one. +\begin{coq_eval} +Reset bool_case. +\end{coq_eval} +\begin{coq_example*} +Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) +:= match b return or (eq bool b true) (eq bool b false) with + | true => or_introl (eq bool true true) (eq bool true false) + (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) + (eq_refl bool false) + end. +\end{coq_example*} + +The second subcase is only relevant for annotated inductive types such +as the equality predicate (see Section~\ref{Equality}), the order +predicate on natural numbers % (see Section~\ref{le}) % undefined reference +or the type of +lists of a given length (see Section~\ref{listn}). In this configuration, +the type of each branch can depend on the type dependencies specific +to the branch and the whole pattern-matching expression has a type +determined by the specific dependencies in the type of the term being +matched. This dependency of the return type in the annotations of the +inductive type is expressed using a + ``in~I~\_~$\ldots$~\_~\pattern$_1$~$\ldots$~\pattern$_n$'' clause, where +\begin{itemize} +\item $I$ is the inductive type of the term being matched; + +\item the {\_}'s are matching the parameters of the inductive type: +the return type is not dependent on them. + +\item the \pattern$_i$'s are matching the annotations of the inductive + type: the return type is dependent on them + +\item in the basic case which we describe below, each \pattern$_i$ is a + name \ident$_i$; see \ref{match-in-patterns} for the general case + +\end{itemize} + +For instance, in the following example: +\begin{coq_example*} +Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := + match H in eq _ _ z return eq A z x with + | eq_refl _ _ => eq_refl A x + end. +\end{coq_example*} +the type of the branch has type {\tt eq~A~x~x} because the third +argument of {\tt eq} is {\tt x} in the type of the pattern {\tt +refl\_equal}. On the contrary, the type of the whole pattern-matching +expression has type {\tt eq~A~y~x} because the third argument of {\tt +eq} is {\tt y} in the type of {\tt H}. This dependency of the case +analysis in the third argument of {\tt eq} is expressed by the +identifier {\tt z} in the return type. + +Finally, the third subcase is a combination of the first and second +subcase. In particular, it only applies to pattern-matching on terms +in a type with annotations. For this third subcase, both +the clauses {\tt as} and {\tt in} are available. + +There are specific notations for case analysis on types with one or +two constructors: ``{\tt if {\ldots} then {\ldots} else {\ldots}}'' +and ``{\tt let (}\nelist{\ldots}{,}{\tt ) := } {\ldots} {\tt in} +{\ldots}'' (see Sections~\ref{if-then-else} and~\ref{Letin}). + +%\SeeAlso Section~\ref{Mult-match} for convenient extensions of pattern-matching. + +\subsection{Recursive functions +\label{fixpoints} +\index{fix@{fix \ident$_i$\{\dots\}}}} + +The expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$} +\texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$ +\binder$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for} +{\ident$_i$}'' denotes the $i$\nth component of a block of functions +defined by mutual well-founded recursion. It is the local counterpart +of the {\tt Fixpoint} command. See Section~\ref{Fixpoint} for more +details. When $n=1$, the ``{\tt for}~{\ident$_i$}'' clause is omitted. + +The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :} +{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binder$_n$ {\tt +:} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$\nth component of +a block of terms defined by a mutual guarded co-recursion. It is the +local counterpart of the {\tt CoFixpoint} command. See +Section~\ref{CoFixpoint} for more details. When $n=1$, the ``{\tt +for}~{\ident$_i$}'' clause is omitted. + +The association of a single fixpoint and a local +definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt + :=}~{\ldots}~{\tt in}~{\ldots}'' stands for ``{\tt let}~$f$~{\tt := + fix}~$f$~\ldots~{\tt :=}~{\ldots}~{\tt in}~{\ldots}''. The same + applies for co-fixpoints. + + +\section{The Vernacular +\label{Vernacular}} + +\begin{figure}[tbp] +\begin{centerframe} +\begin{tabular}{lcl} +{\sentence} & ::= & {\assumption} \\ + & $|$ & {\definition} \\ + & $|$ & {\inductive} \\ + & $|$ & {\fixpoint} \\ + & $|$ & {\assertion} {\proof} \\ +&&\\ +%% Assumptions +{\assumption} & ::= & {\assumptionkeyword} {\assums} {\tt .} \\ +&&\\ +{\assumptionkeyword} & $\!\!$ ::= & {\tt Axiom} $|$ {\tt Conjecture} \\ + & $|$ & {\tt Parameter} $|$ {\tt Parameters} \\ + & $|$ & {\tt Variable} $|$ {\tt Variables} \\ + & $|$ & {\tt Hypothesis} $|$ {\tt Hypotheses}\\ +&&\\ +{\assums} & ::= & \nelist{\ident}{} {\tt :} {\term} \\ + & $|$ & \nelist{{\tt (} \nelist{\ident}{} {\tt :} {\term} {\tt )}}{} \\ +&&\\ +%% Definitions +{\definition} & ::= & + \zeroone{\tt Local} {\tt Definition} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ + & $|$ & {\tt Let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ +&&\\ +%% Inductives +{\inductive} & ::= & + {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\ + & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ + & & \\ +{\inductivebody} & ::= & + {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\ + && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\ + & & \\ %% TODO: where ... +%% Fixpoints +{\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\ + & $|$ & {\tt CoFixpoint} \nelist{\cofixpointbody}{with} {\tt .} \\ +&&\\ +%% Lemmas & proofs +{\assertion} & ::= & + {\statkwd} {\ident} \zeroone{\binders} {\tt :} {\term} {\tt .} \\ +&&\\ + {\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} \\ + & $|$ & {\tt Remark} $|$ {\tt Fact}\\ + & $|$ & {\tt Corollary} $|$ {\tt Proposition} \\ + & $|$ & {\tt Definition} $|$ {\tt Example} \\\\ +&&\\ +{\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\ + & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\ + & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}\\ +\end{tabular} +\end{centerframe} +\caption{Syntax of sentences} +\label{sentences-syntax} +\end{figure} + +Figure \ref{sentences-syntax} describes {\em The Vernacular} which is the +language of commands of \gallina. A sentence of the vernacular +language, like in many natural languages, begins with a capital letter +and ends with a dot. + +The different kinds of command are described hereafter. They all suppose +that the terms occurring in the sentences are well-typed. + +%% +%% Axioms and Parameters +%% +\subsection{Assumptions +\index{Declarations} +\label{Declarations}} + +Assumptions extend the environment\index{Environment} with axioms, +parameters, hypotheses or variables. An assumption binds an {\ident} +to a {\type}. It is accepted by {\Coq} if and only if this {\type} is +a correct type in the environment preexisting the declaration and if +{\ident} was not previously defined in the same module. This {\type} +is considered to be the type (or specification, or statement) assumed +by {\ident} and we say that {\ident} has type {\type}. + +\subsubsection{{\tt Axiom {\ident} :{\term} .} +\comindex{Axiom} +\label{Axiom}} + +This command links {\term} to the name {\ident} as its specification +in the global context. The fact asserted by {\term} is thus assumed as +a postulate. + +\begin{ErrMsgs} +\item \errindex{{\ident} already exists} +\end{ErrMsgs} + +\begin{Variants} +\item \comindex{Parameter}\comindex{Parameters} + {\tt Parameter {\ident} :{\term}.} \\ + Is equivalent to {\tt Axiom {\ident} : {\term}} + +\item {\tt Parameter {\ident$_1$} {\ldots} {\ident$_n$} {\tt :}{\term}.}\\ + Adds $n$ parameters with specification {\term} + +\item + {\tt Parameter\,% +(\,{\ident$_{1,1}$} {\ldots} {\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\;% +\ldots\;{\tt (}\,{\ident$_{n,1}$}{\ldots}{\ident$_{n,k_n}$}\,{\tt :}\,% +{\term$_n$} {\tt )}.}\\ + Adds $n$ blocks of parameters with different specifications. + +\item {\tt Local Axiom {\ident} : {\term}.}\\ +\comindex{Local Axiom} + Such axioms are never made accessible through their unqualified name by + {\tt Import} and its variants (see \ref{Import}). You have to explicitly + give their fully qualified name to refer to them. + +\item \comindex{Conjecture} + {\tt Conjecture {\ident} :{\term}.}\\ + Is equivalent to {\tt Axiom {\ident} : {\term}}. +\end{Variants} + +\noindent {\bf Remark: } It is possible to replace {\tt Parameter} by +{\tt Parameters}. + + +\subsubsection{{\tt Variable {\ident} :{\term}}. +\comindex{Variable} +\comindex{Variables} +\label{Variable}} + +This command links {\term} to the name {\ident} in the context of the +current section (see Section~\ref{Section} for a description of the section +mechanism). When the current section is closed, name {\ident} will be +unknown and every object using this variable will be explicitly +parametrized (the variable is {\em discharged}). Using the {\tt +Variable} command out of any section is equivalent to using {\tt +Local Parameter}. + +\begin{ErrMsgs} +\item \errindex{{\ident} already exists} +\end{ErrMsgs} + +\begin{Variants} +\item {\tt Variable {\ident$_1$} {\ldots} {\ident$_n$} {\tt :}{\term}.}\\ + Links {\term} to names {\ident$_1$} {\ldots} {\ident$_n$}. +\item + {\tt Variable\,% +(\,{\ident$_{1,1}$} {\ldots} {\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\;% +\ldots\;{\tt (}\,{\ident$_{n,1}$} {\ldots}{\ident$_{n,k_n}$}\,{\tt :}\,% +{\term$_n$} {\tt )}.}\\ + Adds $n$ blocks of variables with different specifications. +\item \comindex{Hypothesis} + \comindex{Hypotheses} + {\tt Hypothesis {\ident} {\tt :}{\term}.} \\ + \texttt{Hypothesis} is a synonymous of \texttt{Variable} +\end{Variants} + +\noindent {\bf Remark: } It is possible to replace {\tt Variable} by +{\tt Variables} and {\tt Hypothesis} by {\tt Hypotheses}. + +It is advised to use the keywords \verb:Axiom: and \verb:Hypothesis: +for logical postulates (i.e. when the assertion {\term} is of sort +\verb:Prop:), and to use the keywords \verb:Parameter: and +\verb:Variable: in other cases (corresponding to the declaration of an +abstract mathematical entity). + +%% +%% Definitions +%% +\subsection{Definitions +\index{Definitions} +\label{Basic-definitions}} + +Definitions extend the environment\index{Environment} with +associations of names to terms. A definition can be seen as a way to +give a meaning to a name or as a way to abbreviate a term. In any +case, the name can later be replaced at any time by its definition. + +The operation of unfolding a name into its definition is called +$\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see +Section~\ref{delta}). A definition is accepted by the system if and +only if the defined term is well-typed in the current context of the +definition and if the name is not already used. The name defined by +the definition is called a {\em constant}\index{Constant} and the term +it refers to is its {\em body}. A definition has a type which is the +type of its body. + +A formal presentation of constants and environments is given in +Section~\ref{Typed-terms}. + +\subsubsection{\tt Definition {\ident} := {\term}. +\label{Definition} +\comindex{Definition}} + +This command binds {\term} to the name {\ident} in the +environment, provided that {\term} is well-typed. + +\begin{ErrMsgs} +\item \errindex{{\ident} already exists} +\end{ErrMsgs} + +\begin{Variants} +\item {\tt Definition} {\ident} {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\ + 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$}{\tt .}\\ + 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 Local Definition {\ident} := {\term}.}\\ +\comindex{Local Definition} + Such definitions are never made accessible through their unqualified name by + {\tt Import} and its variants (see \ref{Import}). You have to explicitly + give their fully qualified name to refer to them. +\item {\tt Example {\ident} := {\term}.}\\ +{\tt Example} {\ident} {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\ +{\tt Example} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} + {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\ +\comindex{Example} +These are synonyms of the {\tt Definition} forms. +\end{Variants} + +\begin{ErrMsgs} +\item \errindex{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 let-in definition +{\tt let {\ident} := {\term} in}. Using the {\tt +Let} command out of any section is equivalent to using {\tt +Local Definition}. + +\begin{ErrMsgs} +\item \errindex{{\ident} already exists} +\end{ErrMsgs} + +\begin{Variants} +\item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.} +\item {\tt Let Fixpoint {\ident} \nelist{\fixpointbody}{with} {\tt .}.} +\item {\tt Let CoFixpoint {\ident} \nelist{\cofixpointbody}{with} {\tt .}.} +\end{Variants} + +\SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque}, +\ref{Transparent} (opaque/transparent constants), \ref{unfold} (tactic + {\tt unfold}). + +%% +%% Inductive Types +%% +\subsection{Inductive definitions +\index{Inductive definitions} +\label{gal-Inductive-Definitions} +\comindex{Inductive} +\label{Inductive} +\comindex{Variant} +\label{Variant}} + +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 +\begin{tabular}{l} +{\tt Inductive} {\ident} {\tt :} {\sort} {\tt :=} \\ +\begin{tabular}{clcl} + & {\ident$_1$} & {\tt :} & {\type$_1$} \\ + {\tt |} & {\ldots} && \\ + {\tt |} & {\ident$_n$} & {\tt :} & {\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 names {\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 names {\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 proving some universal property of natural numbers ({\tt +forall n:nat, P n}) by induction on {\tt n}. + +The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except +that they pertain to {\tt (P:nat->Set)} and {\tt (P:nat->Type)} +respectively . They correspond to primitive induction principles +(allowing dependent types) respectively over sorts \verb:Set: and +\verb:Type:. The constant {\ident}{\tt \_ind} is always provided, +whereas {\ident}{\tt \_rec} and {\ident}{\tt \_rect} can be impossible +to derive (for example, when {\ident} is a proposition). + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{Variants} +\item +\begin{coq_example*} +Inductive nat : Set := O | S (_:nat). +\end{coq_example*} +In the case where inductive types have no annotations (next section +gives an example of such annotations), +%the positivity condition implies that +a constructor can be defined by only giving the type of +its arguments. +\end{Variants} + +\subsubsection{Simple annotated inductive types} + +In an annotated inductive types, the universe where the inductive +type is defined is no longer a simple sort, but what is called an +arity, which is a type whose conclusion is a sort. + +As an example of annotated inductive types, let us define the +$even$ predicate: + +\begin{coq_example} +Inductive even : nat -> Prop := + | even_0 : even O + | even_SS : forall n:nat, even n -> even (S (S n)). +\end{coq_example} + +The type {\tt nat->Prop} means that {\tt even} is a unary predicate +(inductively defined) over natural numbers. The type of its two +constructors are the defining clauses of the predicate {\tt even}. The +type of {\tt even\_ind} is: + +\begin{coq_example} +Check even_ind. +\end{coq_example} + +From a mathematical point of view it asserts that the natural numbers +satisfying the predicate {\tt even} are exactly in the smallest set of +naturals satisfying the clauses {\tt even\_0} or {\tt even\_SS}. This +is why, when we want to prove any predicate {\tt P} over elements of +{\tt even}, it is enough to prove it for {\tt O} and to prove that if +any natural number {\tt n} satisfies {\tt P} its double successor {\tt + (S (S n))} satisfies also {\tt P}. This is indeed analogous to the +structural induction principle we got for {\tt nat}. + +\begin{ErrMsgs} +\item \errindex{Non strictly positive occurrence of {\ident} in {\type}} +\item \errindex{The conclusion of {\type} is not valid; it must be +built from {\ident}} +\end{ErrMsgs} + +\subsubsection{Parametrized inductive types} +In the previous example, each constructor introduces a +different instance of the predicate {\tt even}. In some cases, +all the constructors introduces the same generic instance of the +inductive definition, in which case, instead of an annotation, we use +a context of parameters which are binders shared by all the +constructors of the definition. + +% Inductive types may be parameterized. Parameters differ from inductive +% type annotations in the fact that recursive invokations of inductive +% types must always be done with the same values of parameters as its +% specification. + +The general scheme is: +\begin{center} +{\tt Inductive} {\ident} {\binder$_1$}\ldots{\binder$_k$} : {\term} := + {\ident$_1$}: {\term$_1$} | {\ldots} | {\ident$_n$}: \term$_n$ +{\tt .} +\end{center} +Parameters differ from inductive type annotations in the fact that the +conclusion of each type of constructor {\term$_i$} invoke the inductive +type with the same values of parameters as its specification. + + + +A typical example is the definition of polymorphic lists: +\begin{coq_example*} +Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. +\end{coq_example*} + +Note that in the type of {\tt nil} and {\tt cons}, we write {\tt + (list A)} and not just {\tt list}.\\ The constructors {\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. +\item +\begin{coq_example*} +Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B. +\end{coq_example*} +The {\tt Variant} keyword is identical to the {\tt Inductive} keyword, +except that it disallows recursive definition of types (in particular +lists cannot be defined with the {\tt Variant} keyword). No induction +scheme is generated for this variant, unless the option +{\tt Nonrecursive Elimination Schemes} is set +(see~\ref{set-nonrecursive-elimination-schemes}). +\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} +Fail Inductive listw (A:Set) : Set := + | nilw : listw (A*A) + | consw : A -> listw (A*A) -> listw (A*A). +\end{coq_example} +Because the conclusion of the type of constructors should be {\tt + listw A} in both cases. + +A parametrized inductive definition can be defined using +annotations instead of parameters but it will sometimes give a +different (bigger) sort for the inductive definition and will produce +a less convenient rule for case elimination. + +\SeeAlso Sections~\ref{Cic-inductive-definitions} and~\ref{Tac-induction}. + + +\subsubsection{Mutually defined inductive types +\comindex{Inductive} +\label{Mutual-Inductive}} + +The definition of a block of mutually inductive types has the form: + +\medskip +{\tt +\begin{tabular}{l} +Inductive {\ident$_1$} : {\type$_1$} := \\ +\begin{tabular}{clcl} + & {\ident$_1^1$} &:& {\type$_1^1$} \\ + | & {\ldots} && \\ + | & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$} +\end{tabular} \\ +with\\ +~{\ldots} \\ +with {\ident$_m$} : {\type$_m$} := \\ +\begin{tabular}{clcl} + & {\ident$_1^m$} &:& {\type$_1^m$} \\ + | & {\ldots} \\ + | & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}. +\end{tabular} +\end{tabular} +} +\medskip + +\noindent It has the same semantics as the above {\tt Inductive} +definition for each \ident$_1$, {\ldots}, \ident$_m$. All names +\ident$_1$, {\ldots}, \ident$_m$ and \ident$_1^1$, \dots, +\ident$_{n_m}^m$ are simultaneously added to the environment. Then +well-typing of constructors can be checked. Each one of the +\ident$_1$, {\ldots}, \ident$_m$ can be used on its own. + +It is also possible to parametrize these inductive definitions. +However, parameters correspond to a local +context in which the whole set of inductive declarations is done. For +this reason, the parameters must be strictly the same for each +inductive types The extended syntax is: + +\medskip +\begin{tabular}{l} +{\tt Inductive} {\ident$_1$} {\params} {\tt :} {\type$_1$} {\tt :=} \\ +\begin{tabular}{clcl} + & {\ident$_1^1$} &{\tt :}& {\type$_1^1$} \\ + {\tt |} & {\ldots} && \\ + {\tt |} & {\ident$_{n_1}^1$} &{\tt :}& {\type$_{n_1}^1$} +\end{tabular} \\ +{\tt with}\\ +~{\ldots} \\ +{\tt with} {\ident$_m$} {\params} {\tt :} {\type$_m$} {\tt :=} \\ +\begin{tabular}{clcl} + & {\ident$_1^m$} &{\tt :}& {\type$_1^m$} \\ + {\tt |} & {\ldots} \\ + {\tt |} & {\ident$_{n_m}^m$} &{\tt :}& {\type$_{n_m}^m$}. +\end{tabular} +\end{tabular} +\medskip + +\Example +The typical example of a mutual inductive data type is the one for +trees and forests. We assume given two types $A$ and $B$ as variables. +It can be declared the following way. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Variables A B : Set. +Inductive tree : Set := + node : A -> forest -> tree +with forest : Set := + | leaf : B -> forest + | cons : tree -> forest -> forest. +\end{coq_example*} + +This declaration generates automatically six induction +principles. They are respectively +called {\tt tree\_rec}, {\tt tree\_ind}, {\tt + tree\_rect}, {\tt forest\_rec}, {\tt forest\_ind}, {\tt + forest\_rect}. These ones are not the most general ones but are +just the induction principles corresponding to each inductive part +seen as a single inductive definition. + +To illustrate this point on our example, we give the types of {\tt + tree\_rec} and {\tt forest\_rec}. + +\begin{coq_example} +Check tree_rec. +Check forest_rec. +\end{coq_example} + +Assume we want to parametrize our mutual inductive definitions with +the two type variables $A$ and $B$, the declaration should be done the +following way: + +\begin{coq_eval} +Reset tree. +\end{coq_eval} +\begin{coq_example*} +Inductive tree (A B:Set) : Set := + node : A -> forest A B -> tree A B +with forest (A B:Set) : Set := + | leaf : B -> forest A B + | cons : tree A B -> forest A B -> forest A B. +\end{coq_example*} + +Assume we define an inductive definition inside a section. When the +section is closed, the variables declared in the section and occurring +free in the declaration are added as parameters to the inductive +definition. + +\SeeAlso Section~\ref{Section}. + +\subsubsection{Co-inductive types +\label{CoInductiveTypes} +\comindex{CoInductive}} + +The objects of an inductive type are well-founded with respect to the +constructors of the type. In other words, such objects contain only a +{\it finite} number of constructors. Co-inductive types arise from +relaxing this condition, and admitting types whose objects contain an +infinity of constructors. Infinite objects are introduced by a +non-ending (but effective) process of construction, defined in terms +of the constructors of the type. + +An example of a co-inductive type is the type of infinite sequences of +natural numbers, usually called streams. It can be introduced in \Coq\ +using the \texttt{CoInductive} command: +\begin{coq_example} +CoInductive Stream : Set := + Seq : nat -> Stream -> Stream. +\end{coq_example} + +The syntax of this command is the same as the command \texttt{Inductive} +(see Section~\ref{gal-Inductive-Definitions}). Notice that no +principle of induction is derived from the definition of a +co-inductive type, since such principles only make sense for inductive +ones. For co-inductive ones, the only elimination principle is case +analysis. For example, the usual destructors on streams +\texttt{hd:Stream->nat} and \texttt{tl:Str->Str} can be defined as +follows: +\begin{coq_example} +Definition hd (x:Stream) := let (a,s) := x in a. +Definition tl (x:Stream) := let (a,s) := x in s. +\end{coq_example} + +Definition of co-inductive predicates and blocks of mutually +co-inductive definitions are also allowed. An example of a +co-inductive predicate is the extensional equality on streams: + +\begin{coq_example} +CoInductive EqSt : Stream -> Stream -> Prop := + eqst : + forall s1 s2:Stream, + hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. +\end{coq_example} + +In order to prove the extensionally equality of two streams $s_1$ and +$s_2$ we have to construct an infinite proof of equality, that is, +an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see +how to introduce infinite objects in Section~\ref{CoFixpoint}. + +%% +%% (Co-)Fixpoints +%% +\subsection{Definition of recursive functions} + +\subsubsection{Definition of functions by recursion over inductive objects} + +This section describes the primitive form of definition by recursion +over inductive objects. See Section~\ref{Function} for more advanced +constructions. The command: +\begin{center} + \texttt{Fixpoint {\ident} {\params} {\tt \{struct} + \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ + \comindex{Fixpoint}\label{Fixpoint}} +\end{center} +allows defining functions by pattern-matching over inductive objects +using a fixed point construction. +The meaning of this declaration is to define {\it ident} a recursive +function with arguments specified by the binders in {\params} such +that {\it ident} applied to arguments corresponding to these binders +has type \type$_0$, and is equivalent to the expression \term$_0$. The +type of the {\ident} is consequently {\tt forall {\params} {\tt,} + \type$_0$} and the value is equivalent to {\tt fun {\params} {\tt + =>} \term$_0$}. + +To be accepted, a {\tt Fixpoint} definition has to satisfy some +syntactical constraints on a special argument called the decreasing +argument. They are needed to ensure that the {\tt Fixpoint} definition +always terminates. The point of the {\tt \{struct \ident {\tt \}}} +annotation is to let the user tell the system which argument decreases +along the recursive calls. For instance, one can define the addition +function as : + +\begin{coq_example} +Fixpoint add (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (add p m) + end. +\end{coq_example} + +The {\tt \{struct \ident {\tt \}}} annotation may be left implicit, in +this case the system try successively arguments from left to right +until it finds one that satisfies the decreasing condition. Note that +some fixpoints may have several arguments that fit as decreasing +arguments, and this choice influences the reduction of the +fixpoint. Hence an explicit annotation must be used if the leftmost +decreasing argument is not the desired one. Writing explicit +annotations can also speed up type-checking of large mutual fixpoints. + +The {\tt match} operator matches a value (here \verb:n:) with the +various constructors of its (inductive) type. The remaining arguments +give the respective values to be returned, as functions of the +parameters of the corresponding constructor. Thus here when \verb:n: +equals \verb:O: we return \verb:m:, and when \verb:n: equals +\verb:(S p): we return \verb:(S (add p m)):. + +The {\tt match} operator is formally described +in detail in Section~\ref{Caseexpr}. The system recognizes that in +the inductive call {\tt (add p m)} the first argument actually +decreases because it is a {\em pattern variable} coming from {\tt match + n with}. + +\Example The following definition is not correct and generates an +error message: + +\begin{coq_eval} +Set Printing Depth 50. +\end{coq_eval} +% (********** The following is not correct and should produce **********) +% (********* Error: Recursive call to wrongplus ... **********) +\begin{coq_example} +Fail Fixpoint wrongplus (n m:nat) {struct n} : nat := + match m with + | O => n + | S p => S (wrongplus n p) + end. +\end{coq_example} + +because the declared decreasing argument {\tt n} actually does not +decrease in the recursive call. The function computing the addition +over the second argument should rather be written: + +\begin{coq_example*} +Fixpoint plus (n m:nat) {struct m} : nat := + match m with + | O => n + | S p => S (plus n p) + end. +\end{coq_example*} + +The ordinary match operation on natural numbers can be mimicked in the +following way. +\begin{coq_example*} +Fixpoint nat_match + (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C := + match n with + | O => f0 + | S p => fS p (nat_match C f0 fS p) + end. +\end{coq_example*} +The recursive call may not only be on direct subterms of the recursive +variable {\tt n} but also on a deeper subterm and we can directly +write the function {\tt mod2} which gives the remainder modulo 2 of a +natural number. +\begin{coq_example*} +Fixpoint mod2 (n:nat) : nat := + match n with + | O => O + | S p => match p with + | O => S O + | S q => mod2 q + end + end. +\end{coq_example*} +In order to keep the strong normalization property, the fixed point +reduction will only be performed when the argument in position of the +decreasing argument (which type should be in an inductive definition) +starts with a constructor. + +The {\tt Fixpoint} construction enjoys also the {\tt with} extension +to define functions over mutually defined inductive types or more +generally any mutually recursive definitions. + +\begin{Variants} +\item {\tt Fixpoint} {\ident$_1$} {\params$_1$} {\tt :} {\type$_1$} {\tt :=} {\term$_1$}\\ + {\tt with} {\ldots} \\ + {\tt with} {\ident$_m$} {\params$_m$} {\tt :} {\type$_m$} {\tt :=} {\term$_m$}\\ + Allows to define simultaneously {\ident$_1$}, {\ldots}, + {\ident$_m$}. +\end{Variants} + +\Example +The size of trees and forests can be defined the following way: +\begin{coq_eval} +Reset Initial. +Variables A B : Set. +Inductive tree : Set := + node : A -> forest -> tree +with forest : Set := + | leaf : B -> forest + | cons : tree -> forest -> forest. +\end{coq_eval} +\begin{coq_example*} +Fixpoint tree_size (t:tree) : nat := + match t with + | node a f => S (forest_size f) + end + with forest_size (f:forest) : nat := + match f with + | leaf b => 1 + | cons t f' => (tree_size t + forest_size f') + end. +\end{coq_example*} +A generic command {\tt Scheme} is useful to build automatically various +mutual induction principles. It is described in Section~\ref{Scheme}. + +\subsubsection{Definitions of recursive objects in co-inductive types} + +The command: +\begin{center} + \texttt{CoFixpoint {\ident} : \type$_0$ := \term$_0$} + \comindex{CoFixpoint}\label{CoFixpoint} +\end{center} +introduces a method for constructing an infinite object of a +coinduc\-tive type. For example, the stream containing all natural +numbers can be introduced applying the following method to the number +\texttt{O} (see Section~\ref{CoInductiveTypes} for the definition of +{\tt Stream}, {\tt hd} and {\tt tl}): +\begin{coq_eval} +Reset Initial. +CoInductive Stream : Set := + Seq : nat -> Stream -> Stream. +Definition hd (x:Stream) := match x with + | Seq a s => a + end. +Definition tl (x:Stream) := match x with + | Seq a s => s + end. +\end{coq_eval} +\begin{coq_example} +CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). +\end{coq_example} + +Oppositely to recursive ones, there is no decreasing argument in a +co-recursive definition. To be admissible, a method of construction +must provide at least one extra constructor of the infinite object for +each iteration. A syntactical guard condition is imposed on +co-recursive definitions in order to ensure this: each recursive call +in the definition must be protected by at least one constructor, and +only by constructors. That is the case in the former definition, where +the single recursive call of \texttt{from} is guarded by an +application of \texttt{Seq}. On the contrary, the following recursive +function does not satisfy the guard condition: + +\begin{coq_eval} +Set Printing Depth 50. +\end{coq_eval} +% (********** The following is not correct and should produce **********) +% (***************** Error: Unguarded recursive call *******************) +\begin{coq_example} +Fail 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$} {\tt :} {\type$_1$} {\tt :=} {\term$_1$}\\ + {\tt with}\\ + \mbox{}\hspace{0.1cm} {\ldots} \\ + {\tt with} {\ident$_m$} {\tt :} {\type$_m$} {\tt :=} {\term$_m$}\\ +As in the \texttt{Fixpoint} command (see Section~\ref{Fixpoint}), it +is possible to introduce a block of mutually dependent methods. +\end{Variants} + +%% +%% Theorems & Lemmas +%% +\subsection{Assertions and proofs} +\label{Assertions} + +An assertion states a proposition (or a type) of which the proof (or +an inhabitant of the type) is interactively built using tactics. The +interactive proof mode is described in +Chapter~\ref{Proof-handling} and the tactics in Chapter~\ref{Tactics}. +The basic assertion command is: + +\subsubsection{\tt Theorem {\ident} \zeroone{\binders} : {\type}. +\comindex{Theorem}} + +After the statement is asserted, {\Coq} needs a proof. Once a proof of +{\type} under the assumptions represented by {\binders} is given and +validated, the proof is generalized into a proof of {\tt forall + \zeroone{\binders}, {\type}} and the theorem is bound to the name +{\ident} in the environment. + +\begin{ErrMsgs} + +\item \errindex{The term {\form} has type {\ldots} which should be Set, + Prop or Type} + +\item \errindexbis{{\ident} already exists}{already exists} + + The name you provided is already defined. You have then to choose + another name. + +\end{ErrMsgs} + +\begin{Variants} +\item {\tt Lemma {\ident} \zeroone{\binders} : {\type}.}\comindex{Lemma}\\ + {\tt Remark {\ident} \zeroone{\binders} : {\type}.}\comindex{Remark}\\ + {\tt Fact {\ident} \zeroone{\binders} : {\type}.}\comindex{Fact}\\ + {\tt Corollary {\ident} \zeroone{\binders} : {\type}.}\comindex{Corollary}\\ + {\tt Proposition {\ident} \zeroone{\binders} : {\type}.}\comindex{Proposition} + +These commands are synonyms of \texttt{Theorem {\ident} \zeroone{\binders} : {\type}}. + +\item {\tt Theorem \nelist{{\ident} \zeroone{\binders}: {\type}}{with}.} + +This command is useful for theorems that are proved by simultaneous +induction over a mutually inductive assumption, or that assert mutually +dependent statements in some mutual co-inductive type. It is equivalent +to {\tt Fixpoint} or {\tt CoFixpoint} +(see Section~\ref{CoFixpoint}) but using tactics to build the proof of +the statements (or the body of the specification, depending on the +point of view). The inductive or co-inductive types on which the +induction or coinduction has to be done is assumed to be non ambiguous +and is guessed by the system. + +Like in a {\tt Fixpoint} or {\tt CoFixpoint} definition, the induction +hypotheses have to be used on {\em structurally smaller} arguments +(for a {\tt Fixpoint}) or be {\em guarded by a constructor} (for a {\tt + CoFixpoint}). The verification that recursive proof arguments are +correct is done only at the time of registering the lemma in the +environment. To know if the use of induction hypotheses is correct at +some time of the interactive development of a proof, use the command +{\tt Guarded} (see Section~\ref{Guarded}). + +The command can be used also with {\tt Lemma}, +{\tt Remark}, etc. instead of {\tt Theorem}. + +\item {\tt Definition {\ident} \zeroone{\binders} : {\type}.} + +This allows defining a term of type {\type} using the proof editing mode. It +behaves as {\tt Theorem} but is intended to be used in conjunction with + {\tt Defined} (see \ref{Defined}) in order to define a + constant of which the computational behavior is relevant. + +The command can be used also with {\tt Example} instead +of {\tt Definition}. + +\SeeAlso Sections~\ref{Opaque} and~\ref{Transparent} ({\tt Opaque} +and {\tt Transparent}) and~\ref{unfold} (tactic {\tt unfold}). + +\item {\tt Let {\ident} \zeroone{\binders} : {\type}.} + +Like {\tt Definition {\ident} \zeroone{\binders} : {\type}.} except +that the definition is turned into a let-in definition generalized over +the declarations depending on it after closing the current section. + +\item {\tt Fixpoint \nelist{{\ident} {\binders} \zeroone{\annotation} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.} +\comindex{Fixpoint} + +This generalizes the syntax of {\tt Fixpoint} so that one or more +bodies can be defined interactively using the proof editing mode (when +a body is omitted, its type is mandatory in the syntax). When the +block of proofs is completed, it is intended to be ended by {\tt + Defined}. + +\item {\tt CoFixpoint \nelist{{\ident} \zeroone{\binders} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.} +\comindex{CoFixpoint} + +This generalizes the syntax of {\tt CoFixpoint} so that one or more bodies +can be defined interactively using the proof editing mode. + +\end{Variants} + +\subsubsection{{\tt Proof.} {\dots} {\tt Qed.} +\comindex{Proof} +\comindex{Qed}} + +A proof starts by the keyword {\tt Proof}. Then {\Coq} enters the +proof editing mode until the proof is completed. The proof editing +mode essentially contains tactics that are described in chapter +\ref{Tactics}. Besides tactics, there are commands to manage the proof +editing mode. They are described in Chapter~\ref{Proof-handling}. When +the proof is completed it should be validated and put in the +environment using the keyword {\tt Qed}. +\medskip + +\ErrMsg +\begin{enumerate} +\item \errindex{{\ident} already exists} +\end{enumerate} + +\begin{Remarks} +\item Several statements can be simultaneously asserted. +\item Not only other assertions but any vernacular command can be given +while in the process of proving a given assertion. In this case, the command is +understood as if it would have been given before the statements still to be +proved. +\item {\tt Proof} is recommended but can currently be omitted. On the +opposite side, {\tt Qed} (or {\tt Defined}, see below) is mandatory to +validate a proof. +\item Proofs ended by {\tt Qed} are declared opaque. Their content + cannot be unfolded (see \ref{Conversion-tactics}), thus realizing + some form of {\em proof-irrelevance}. To be able to unfold a proof, + the proof should be ended by {\tt Defined} (see below). +\end{Remarks} + +\begin{Variants} +\item \comindex{Defined} + {\tt Proof.} {\dots} {\tt Defined.}\\ + Same as {\tt Proof.} {\dots} {\tt Qed.} but the proof is + then declared transparent, which means that its + content can be explicitly used for type-checking and that it + can be unfolded in conversion tactics (see + \ref{Conversion-tactics}, \ref{Opaque}, \ref{Transparent}). +%Not claimed to be part of Gallina... +%\item {\tt Proof.} {\dots} {\tt Save.}\\ +% Same as {\tt Proof.} {\dots} {\tt Qed.} +%\item {\tt Goal} \type {\dots} {\tt Save} \ident \\ +% Same as {\tt Lemma} \ident {\tt :} \type \dots {\tt Save.} +% This is intended to be used in the interactive mode. +\item \comindex{Admitted} + {\tt Proof.} {\dots} {\tt Admitted.}\\ + Turns the current asserted statement into an axiom and exits the + proof mode. +\end{Variants} + +% Local Variables: +% mode: LaTeX +% TeX-master: "Reference-Manual" +% End: -- cgit v1.2.3