From 2f30bb4855cc4f3f96aa6904b9b8c48414100bb4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 12 Mar 2018 22:01:51 +0100 Subject: [Sphinx] Move chapter 2 to new infrastructure --- Makefile.doc | 2 +- doc/refman/RefMan-ext.tex | 2152 ---------------------------- doc/refman/RefMan-mod.tex | 428 ------ doc/refman/Reference-Manual.tex | 1 - doc/sphinx/language/gallina-extensions.rst | 2152 ++++++++++++++++++++++++++++ 5 files changed, 2153 insertions(+), 2582 deletions(-) delete mode 100644 doc/refman/RefMan-ext.tex delete mode 100644 doc/refman/RefMan-mod.tex create mode 100644 doc/sphinx/language/gallina-extensions.rst diff --git a/Makefile.doc b/Makefile.doc index e6ab89efc..0f99f0530 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -57,7 +57,7 @@ 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-ext.v.tex \ + RefMan-gal.v.tex \ RefMan-mod.v.tex RefMan-tac.v.tex \ RefMan-cic.v.tex RefMan-lib.v.tex \ RefMan-tacex.v.tex RefMan-syn.v.tex \ diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex deleted file mode 100644 index a1950d136..000000000 --- a/doc/refman/RefMan-ext.tex +++ /dev/null @@ -1,2152 +0,0 @@ -\chapter[Extensions of \Gallina{}]{Extensions of \Gallina{}\label{Gallina-extension}\index{Gallina}} -%HEVEA\cutname{gallina-ext.html} - -{\gallina} is the kernel language of {\Coq}. We describe here extensions of -the Gallina's syntax. - -\section{Record types -\comindex{Record} -\comindex{Inductive} -\comindex{CoInductive} -\label{Record}} - -The \verb+Record+ construction is a macro allowing the definition of -records as is done in many programming languages. Its syntax is -described on Figure~\ref{record-syntax}. In fact, the \verb+Record+ -macro is more general than the usual record types, since it allows -also for ``manifest'' expressions. In this sense, the \verb+Record+ -construction allows defining ``signatures''. - -\begin{figure}[h] -\begin{centerframe} -\begin{tabular}{lcl} -{\sentence} & ++= & {\record}\\ - & & \\ -{\record} & ::= & - {\recordkw} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\ -&& ~~~~\zeroone{\ident} - \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ - & & \\ -{\recordkw} & ::= & - {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\ - & & \\ -{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\ - & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\ -\end{tabular} -\end{centerframe} -\caption{Syntax for the definition of {\tt Record}} -\label{record-syntax} -\end{figure} - -\noindent In the expression -\begin{quote} -{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\ - {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\ - {\ident$_n$} \binders$_n$ : {\term$_n$} \}.} -\end{quote} -\noindent the identifier {\ident} is the name of the defined record -and {\sort} is its type. The identifier {\ident$_0$} is the name of -its constructor. If {\ident$_0$} is omitted, the default name {\tt -Build\_{\ident}} is used. -If {\sort} is omitted, the default sort is {\Type}. -The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of -fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots, -{\tt forall {\binders$_n$}, {\term$_n$}} -their respective types. Remark that the type of {\ident$_i$} may -depend on the previous {\ident$_j$} (for $j bottom; - Rat_irred_cond : - forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. -\end{coq_example} - -Remark here that the field \verb+Rat_bottom_cond+ depends -on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends -on both \verb+top+ and \verb+bottom+. - -Let us now see the work done by the {\tt Record} macro. First the -macro generates a variant type definition with just one constructor: -\begin{quote} -{\tt Variant {\ident} {\params} : {\sort} := \\ - {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).} -\end{quote} -To build an object of type {\ident}, one should provide the -constructor {\ident$_0$} with $n$ terms filling the fields of -the record. - -As an example, let us define the rational $1/2$: -\begin{coq_example*} -Theorem one_two_irred : - forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. -Admitted. -\end{coq_example*} -\begin{coq_example} -Definition half := mkRat true 1 2 (O_S 1) one_two_irred. -\end{coq_example} -\begin{coq_example} -Check half. -\end{coq_example} - -\begin{figure}[t] -\begin{centerframe} -\begin{tabular}{lcl} -{\term} & ++= & - \verb!{|! \zeroone{\nelist{\fielddef}{;}} \verb!|}! \\ - & & \\ -{\fielddef} & ::= & {\name} \zeroone{\binders} := {\term} \\ -\end{tabular} -\end{centerframe} -\caption{Syntax for constructing elements of a \texttt{Record} using named fields} -\label{fig:fieldsyntax} -\end{figure} - -Alternatively, the following syntax allows creating objects by using named fields, as -shown on Figure~\ref{fig:fieldsyntax}. The -fields do not have to be in any particular order, nor do they have to be all -present if the missing ones can be inferred or prompted for (see -Section~\ref{Program}). - -\begin{coq_example} -Definition half' := - {| sign := true; - Rat_bottom_cond := O_S 1; - Rat_irred_cond := one_two_irred |}. -\end{coq_example} - -This syntax can be disabled globally for printing by -\begin{quote} -{\tt Unset Printing Records.} -\optindex{Printing Records} -\end{quote} -For a given type, one can override this using either -\begin{quote} -{\tt Add Printing Record {\ident}.} -\end{quote} -to get record syntax or -\begin{quote} -{\tt Add Printing Constructor {\ident}.} -\end{quote} -to get constructor syntax. - -This syntax can also be used for pattern matching. - -\begin{coq_example} -Eval compute in ( - match half with - | {| sign := true; top := n |} => n - | _ => 0 - end). -\end{coq_example} - -The macro generates also, when it is possible, the projection -functions for destructuring an object of type {\ident}. These -projection functions are given the names of the corresponding -fields. If a field is named ``\verb=_='' then no projection is built -for it. In our example: - -\begin{coq_example} -Eval compute in top half. -Eval compute in bottom half. -Eval compute in Rat_bottom_cond half. -\end{coq_example} - -An alternative syntax for projections based on a dot notation is -available: - -\begin{coq_example} -Eval compute in half.(top). -\end{coq_example} - -It can be activated for printing with the command -\optindex{Printing Projections} -\begin{quote} -{\tt Set Printing Projections.} -\end{quote} - -\begin{coq_example} -Set Printing Projections. -Check top half. -\end{coq_example} - -The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}. -When {\qualid} denotes a projection, the syntax {\tt - {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax -{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to -{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax -{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to -{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} -is the object projected and the other arguments are the parameters of -the inductive type. - -\begin{figure}[t] -\begin{centerframe} -\begin{tabular}{lcl} -{\term} & ++= & {\term} {\tt .(} {\qualid} {\tt )}\\ - & $|$ & {\term} {\tt .(} {\qualid} \nelist{\termarg}{} {\tt )}\\ - & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )} -\end{tabular} -\end{centerframe} -\caption{Syntax for \texttt{Record} projections} -\label{fig:projsyntax} -\end{figure} - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{Remarks} - -\item Records defined with the {\tt Record} keyword are not allowed to be -recursive (references to the record's name in the type of its field -raises an error). To define recursive records, one can use the {\tt -Inductive} and {\tt CoInductive} keywords, resulting in an inductive -or co-inductive record. -A \emph{caveat}, however, is that records -cannot appear in mutually inductive (or co-inductive) definitions. - -\item Induction schemes are automatically generated for inductive records. -Automatic generation of induction schemes for non-recursive records -defined with the {\tt Record} keyword can be activated with the -{\tt Nonrecursive Elimination Schemes} option -(see~\ref{set-nonrecursive-elimination-schemes}). - -\item {\tt Structure} is a synonym of the keyword {\tt Record}. - -\end{Remarks} - -\begin{Warnings} -\item {\tt {\ident$_i$} cannot be defined.} - - It can happen that the definition of a projection is impossible. - This message is followed by an explanation of this impossibility. - There may be three reasons: - \begin{enumerate} - \item The name {\ident$_i$} already exists in the environment (see - Section~\ref{Axiom}). - \item The body of {\ident$_i$} uses an incorrect elimination for - {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}). - \item The type of the projections {\ident$_i$} depends on previous - projections which themselves could not be defined. - \end{enumerate} -\end{Warnings} - -\begin{ErrMsgs} - -\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.} - - The record name {\ident} appears in the type of its fields, but uses - the keyword {\tt Record}. Use the keyword {\tt Inductive} or {\tt - CoInductive} instead. -\item \errindex{Cannot handle mutually (co)inductive records.} - - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. -\item During the definition of the one-constructor inductive - definition, all the errors of inductive definitions, as described in - Section~\ref{gal-Inductive-Definitions}, may also occur. - -\end{ErrMsgs} - -\SeeAlso Coercions and records in Section~\ref{Coercions-and-records} -of the chapter devoted to coercions. - -\subsection{Primitive Projections} -\optindex{Primitive Projections} -\optindex{Printing Primitive Projection Parameters} -\optindex{Printing Primitive Projection Compatibility} -\index{Primitive projections} -\label{prim-proj} - -The option {\tt Set Primitive Projections} turns on the use of primitive -projections when defining subsequent records (even through the {\tt - Inductive} and {\tt CoInductive} commands). Primitive projections -extended the Calculus of Inductive Constructions with a new binary term -constructor {\tt r.(p)} representing a primitive projection p applied to -a record object {\tt r} (i.e., primitive projections are always -applied). Even if the record type has parameters, these do not appear at -applications of the projection, considerably reducing the sizes of terms -when manipulating parameterized records and typechecking time. On the -user level, primitive projections can be used as a replacement for the -usual defined ones, although there are a few notable differences. - -The internally omitted parameters can be reconstructed at printing time -even though they are absent in the actual AST manipulated by the kernel. This -can be obtained by setting the {\tt Printing Primitive Projection Parameters} -flag. Another compatibility printing can be activated thanks to the -{\tt Printing Primitive Projection Compatibility} option which governs the -printing of pattern-matching over primitive records. - -\subsubsection{Primitive Record Types} -When the {\tt Set Primitive Projections} option is on, definitions of -record types change meaning. When a type is declared with primitive -projections, its {\tt match} construct is disabled (see -\ref{primproj:compat} though). To eliminate the (co-)inductive type, one -must use its defined primitive projections. - -There are currently two ways to introduce primitive records types: -\begin{itemize} -\item Through the {\tt Record} command, in which case the type has to be - non-recursive. The defined type enjoys eta-conversion definitionally, - that is the generalized form of surjective pairing for records: - {\tt $r$ = Build\_R ($r$.($p_1$) .. $r$.($p_n$))}. Eta-conversion allows to define - dependent elimination for these types as well. -\item Through the {\tt Inductive} and {\tt CoInductive} commands, when - the body of the definition is a record declaration of the form {\tt - Build\_R \{ $p_1$ : $t_1$; .. ; $p_n$ : $t_n$ \}}. In this case the types can be - recursive and eta-conversion is disallowed. These kind of record types - differ from their traditional versions in the sense that dependent - elimination is not available for them and only non-dependent case analysis - can be defined. -\end{itemize} - -\subsubsection{Reduction} - -The basic reduction rule of a primitive projection is {\tt $p_i$ - (Build\_R $t_1$ .. $t_n$) $\rightarrow_{\iota}$ $t_i$}. However, to take the $\delta$ flag into -account, projections can be in two states: folded or unfolded. An -unfolded primitive projection application obeys the rule above, while -the folded version delta-reduces to the unfolded version. This allows to -precisely mimic the usual unfolding rules of constants. Projections -obey the usual {\tt simpl} flags of the {\tt Arguments} command in particular. - -There is currently no way to input unfolded primitive projections at the -user-level, and one must use the {\tt Printing Primitive Projection - Compatibility} to display unfolded primitive projections as matches -and distinguish them from folded ones. - -\subsubsection{Compatibility Projections and {\tt match}} -\label{primproj:compat} -To ease compatibility with ordinary record types, each primitive -projection is also defined as a ordinary constant taking parameters and -an object of the record type as arguments, and whose body is an -application of the unfolded primitive projection of the same name. These -constants are used when elaborating partial applications of the -projection. One can distinguish them from applications of the primitive -projection if the {\tt Printing Primitive Projection Parameters} option -is off: for a primitive projection application, parameters are printed -as underscores while for the compatibility projections they are printed -as usual. - -Additionally, user-written {\tt match} constructs on primitive records -are desugared into substitution of the projections, they cannot be -printed back as {\tt match} constructs. - - % - r.(p) and (p r) elaborate to native projection application, and - % the parameters cannot be mentioned. The following arguments are - % parsed according to the remaining implicit arguments declared for the - % projection (i.e. the implicit arguments after the record type - % argument). In dot notation, the record type argument is considered - % explicit no matter what its implicit status is. - % - r.(@p params) and @p args are parsed as regular applications of the - % projection with explicit parameters. - % - [simpl p] is forbidden, but [simpl @p] will simplify both the projection - % and its explicit [@p] version. - % - [unfold p] has no effect on projection applications unless it is applied - % to a constructor. If the explicit version appears it reduces to the - % projection application. - % - [pattern x at n], [rewrite x at n] and in general abstraction and selection - % of occurrences may fail due to the disappearance of parameters. - -\section{Variants and extensions of {\mbox{\tt match}} -\label{Extensions-of-match} -\index{match@{\tt match\ldots with\ldots end}}} - -\subsection{Multiple and nested pattern-matching -\index{ML-like patterns} -\label{Mult-match}} - -The basic version of \verb+match+ allows pattern-matching on simple -patterns. As an extension, multiple nested patterns or disjunction of -patterns are allowed, as in ML-like languages. - -The extension just acts as a macro that is expanded during parsing -into a sequence of {\tt match} on simple patterns. Especially, a -construction defined using the extended {\tt match} is generally -printed under its expanded form (see~\texttt{Set Printing Matching} in -section~\ref{SetPrintingMatching}). - -\SeeAlso Chapter~\ref{Mult-match-full}. - -\subsection{Pattern-matching on boolean values: the {\tt if} expression -\label{if-then-else} -\index{if@{\tt if ... then ... else}}} - -For inductive types with exactly two constructors and for -pattern-matchings expressions which do not depend on the arguments of -the constructors, it is possible to use a {\tt if ... then ... else} -notation. For instance, the definition - -\begin{coq_example} -Definition not (b:bool) := - match b with - | true => false - | false => true - end. -\end{coq_example} - -\noindent can be alternatively written - -\begin{coq_eval} -Reset not. -\end{coq_eval} -\begin{coq_example} -Definition not (b:bool) := if b then false else true. -\end{coq_example} - -More generally, for an inductive type with constructors {\tt C$_1$} -and {\tt C$_2$}, we have the following equivalence - -\smallskip - -{\tt if {\term} \zeroone{\ifitem} then {\term}$_1$ else {\term}$_2$} $\equiv$ -\begin{tabular}[c]{l} -{\tt match {\term} \zeroone{\ifitem} with}\\ -{\tt \verb!|! C$_1$ \_ {\ldots} \_ \verb!=>! {\term}$_1$} \\ -{\tt \verb!|! C$_2$ \_ {\ldots} \_ \verb!=>! {\term}$_2$} \\ -{\tt end} -\end{tabular} - -Here is an example. - -\begin{coq_example} -Check (fun x (H:{x=0}+{x<>0}) => - match H with - | left _ => true - | right _ => false - end). -\end{coq_example} - -Notice that the printing uses the {\tt if} syntax because {\tt sumbool} is -declared as such (see Section~\ref{printing-options}). - -\subsection{Irrefutable patterns: the destructuring {\tt let} variants -\index{let in@{\tt let ... in}} -\label{Letin}} - -Pattern-matching on terms inhabiting inductive type having only one -constructor can be alternatively written using {\tt let ... in ...} -constructions. There are two variants of them. - -\subsubsection{First destructuring {\tt let} syntax} -The expression {\tt let -(}~{\ident$_1$},\ldots,{\ident$_n$}~{\tt ) :=}~{\term$_0$}~{\tt -in}~{\term$_1$} performs case analysis on a {\term$_0$} which must be in -an inductive type with one constructor having itself $n$ arguments. Variables -{\ident$_1$}\ldots{\ident$_n$} are bound to the $n$ arguments of the -constructor in expression {\term$_1$}. For instance, the definition - -\begin{coq_example} -Definition fst (A B:Set) (H:A * B) := match H with - | pair x y => x - end. -\end{coq_example} - -can be alternatively written - -\begin{coq_eval} -Reset fst. -\end{coq_eval} -\begin{coq_example} -Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. -\end{coq_example} -Notice that reduction is different from regular {\tt let ... in ...} -construction since it happens only if {\term$_0$} is in constructor -form. Otherwise, the reduction is blocked. - -The pretty-printing of a definition by matching on a -irrefutable pattern can either be done using {\tt match} or the {\tt -let} construction (see Section~\ref{printing-options}). - -If {\term} inhabits an inductive type with one constructor {\tt C}, -we have an equivalence between - -{\tt let ({\ident}$_1$,\ldots,{\ident}$_n$) \zeroone{\ifitem} := {\term} in {\term}'} - -\noindent and - -{\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end} - - -\subsubsection{Second destructuring {\tt let} syntax\index{let '... in@\texttt{let '... in}}} - -Another destructuring {\tt let} syntax is available for inductive types with -one constructor by giving an arbitrary pattern instead of just a tuple -for all the arguments. For example, the preceding example can be written: -\begin{coq_eval} -Reset fst. -\end{coq_eval} -\begin{coq_example} -Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. -\end{coq_example} - -This is useful to match deeper inside tuples and also to use notations -for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary -patterns to do the deconstruction. For example: - -\begin{coq_example} -Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := - let '((a,b), (c, d)) := x in (a,b,c,d). -Notation " x 'With' p " := (exist _ x p) (at level 20). -Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := - let 'x With p := t in x. -\end{coq_example} - -When printing definitions which are written using this construct it -takes precedence over {\tt let} printing directives for the datatype -under consideration (see Section~\ref{printing-options}). - -\subsection{Controlling pretty-printing of {\tt match} expressions -\label{printing-options}} - -The following commands give some control over the pretty-printing of -{\tt match} expressions. - -\subsubsection{Printing nested patterns -\label{SetPrintingMatching} -\optindex{Printing Matching}} - -The Calculus of Inductive Constructions knows pattern-matching only -over simple patterns. It is however convenient to re-factorize nested -pattern-matching into a single pattern-matching over a nested pattern. -{\Coq}'s printer try to do such limited re-factorization. - -\begin{quote} -{\tt Set Printing Matching.} -\end{quote} -This tells {\Coq} to try to use nested patterns. This is the default -behavior. - -\begin{quote} -{\tt Unset Printing Matching.} -\end{quote} -This tells {\Coq} to print only simple pattern-matching problems in -the same way as the {\Coq} kernel handles them. - -\begin{quote} -{\tt Test Printing Matching.} -\end{quote} -This tells if the printing matching mode is on or off. The default is -on. - -\subsubsection{Factorization of clauses with same right-hand side} -\label{SetPrintingFactorizableMatchPatterns} -\optindex{Printing Factorizable Match Patterns} - -When several patterns share the same right-hand side, it is -additionally possible to share the clauses using disjunctive patterns. -Assuming that the printing matching mode is on, whether {\Coq}'s -printer shall try to do this kind of factorization is governed by the -following commands: - -\begin{quote} -{\tt Set Printing Factorizable Match Patterns.} -\end{quote} -This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default -behavior. - -\begin{quote} -{\tt Unset Printing Factorizable Match Patterns.} -\end{quote} -This tells {\Coq}'s printer not to try to use disjunctive patterns. - -\begin{quote} -{\tt Test Printing Factorizable Match Patterns.} -\end{quote} -This tells if the factorization of clauses with same right-hand side is -on or off. - -\subsubsection{Use of a default clause} -\label{SetPrintingAllowDefaultClause} -\optindex{Printing Allow Default Clause} - -When several patterns share the same right-hand side which do not -depend on the arguments of the patterns, yet an extra factorization is -possible: the disjunction of patterns can be replaced with a ``{\tt - \_}'' default clause. Assuming that the printing matching mode and -the factorization mode are on, whether {\Coq}'s printer shall try to -use a default clause is governed by the following commands: - -\begin{quote} -{\tt Set Printing Allow Default Clause.} -\end{quote} -This tells {\Coq}'s printer to use a default clause when relevant. This is the default -behavior. - -\begin{quote} -{\tt Unset Printing Allow Default Clause.} -\end{quote} -This tells {\Coq}'s printer not to use a default clause. - -\begin{quote} -{\tt Test Printing Allow Default Clause.} -\end{quote} -This tells if the use of a default clause is allowed. - -\subsubsection{Printing of wildcard pattern -\optindex{Printing Wildcard}} - -Some variables in a pattern may not occur in the right-hand side of -the pattern-matching clause. There are options to control the -display of these variables. - -\begin{quote} -{\tt Set Printing Wildcard.} -\end{quote} -The variables having no occurrences in the right-hand side of the -pattern-matching clause are just printed using the wildcard symbol -``{\tt \_}''. - -\begin{quote} -{\tt Unset Printing Wildcard.} -\end{quote} -The variables, even useless, are printed using their usual name. But some -non dependent variables have no name. These ones are still printed -using a ``{\tt \_}''. - -\begin{quote} -{\tt Test Printing Wildcard.} -\end{quote} -This tells if the wildcard printing mode is on or off. The default is -to print wildcard for useless variables. - -\subsubsection{Printing of the elimination predicate -\optindex{Printing Synth}} - -In most of the cases, the type of the result of a matched term is -mechanically synthesizable. Especially, if the result type does not -depend of the matched term. - -\begin{quote} -{\tt Set Printing Synth.} -\end{quote} -The result type is not printed when {\Coq} knows that it can -re-synthesize it. - -\begin{quote} -{\tt Unset Printing Synth.} -\end{quote} -This forces the result type to be always printed. - -\begin{quote} -{\tt Test Printing Synth.} -\end{quote} -This tells if the non-printing of synthesizable types is on or off. -The default is to not print synthesizable types. - -\subsubsection{Printing matching on irrefutable pattern -\label{AddPrintingLet} -\comindex{Add Printing Let {\ident}} -\comindex{Remove Printing Let {\ident}} -\comindex{Test Printing Let for {\ident}} -\comindex{Print Table Printing Let}} - -If an inductive type has just one constructor, -pattern-matching can be written using the first destructuring let syntax. - -\begin{quote} -{\tt Add Printing Let {\ident}.} -\end{quote} -This adds {\ident} to the list of inductive types for which -pattern-matching is written using a {\tt let} expression. - -\begin{quote} -{\tt Remove Printing Let {\ident}.} -\end{quote} -This removes {\ident} from this list. Note that removing an inductive -type from this list has an impact only for pattern-matching written using -\texttt{match}. Pattern-matching explicitly written using a destructuring -let are not impacted. - -\begin{quote} -{\tt Test Printing Let for {\ident}.} -\end{quote} -This tells if {\ident} belongs to the list. - -\begin{quote} -{\tt Print Table Printing Let.} -\end{quote} -This prints the list of inductive types for which pattern-matching is -written using a {\tt let} expression. - -The list of inductive types for which pattern-matching is written -using a {\tt let} expression is managed synchronously. This means that -it is sensible to the command {\tt Reset}. - -\subsubsection{Printing matching on booleans -\comindex{Add Printing If {\ident}} -\comindex{Remove Printing If {\ident}} -\comindex{Test Printing If for {\ident}} -\comindex{Print Table Printing If}} - -If an inductive type is isomorphic to the boolean type, -pattern-matching can be written using {\tt if} ... {\tt then} ... {\tt - else} ... - -\begin{quote} -{\tt Add Printing If {\ident}.} -\end{quote} -This adds {\ident} to the list of inductive types for which -pattern-matching is written using an {\tt if} expression. - -\begin{quote} -{\tt Remove Printing If {\ident}.} -\end{quote} -This removes {\ident} from this list. - -\begin{quote} -{\tt Test Printing If for {\ident}.} -\end{quote} -This tells if {\ident} belongs to the list. - -\begin{quote} -{\tt Print Table Printing If.} -\end{quote} -This prints the list of inductive types for which pattern-matching is -written using an {\tt if} expression. - -The list of inductive types for which pattern-matching is written -using an {\tt if} expression is managed synchronously. This means that -it is sensible to the command {\tt Reset}. - -\subsubsection{Example} - -This example emphasizes what the printing options offer. - -\begin{coq_example} -Definition snd (A B:Set) (H:A * B) := match H with - | pair x y => y - end. -Test Printing Let for prod. -Print snd. -Remove Printing Let prod. -Unset Printing Synth. -Unset Printing Wildcard. -Print snd. -\end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\subsection{Printing \mbox{\tt match} templates} - -The {\tt Show Match} vernacular command prints a {\tt match} template for -a given type. See Section~\ref{Show}. - -% \subsection{Still not dead old notations} - -% The following variant of {\tt match} is inherited from older version -% of {\Coq}. - -% \medskip -% \begin{tabular}{lcl} -% {\term} & ::= & {\annotation} {\tt Match} {\term} {\tt with} {\terms} {\tt end}\\ -% \end{tabular} -% \medskip - -% This syntax is a macro generating a combination of {\tt match} with {\tt -% Fix} implementing a combinator for primitive recursion equivalent to -% the {\tt Match} construction of \Coq\ V5.8. It is provided only for -% sake of compatibility with \Coq\ V5.8. It is recommended to avoid it. -% (see Section~\ref{Matchexpr}). - -% There is also a notation \texttt{Case} that is the -% ancestor of \texttt{match}. Again, it is still in the code for -% compatibility with old versions but the user should not use it. - -% Explained in RefMan-gal.tex -%% \section{Forced type} - -%% In some cases, one may wish to assign a particular type to a term. The -%% syntax to force the type of a term is the following: - -%% \medskip -%% \begin{tabular}{lcl} -%% {\term} & ++= & {\term} {\tt :} {\term}\\ -%% \end{tabular} -%% \medskip - -%% It forces the first term to be of type the second term. The -%% type must be compatible with -%% the term. More precisely it must be either a type convertible to -%% the automatically inferred type (see Chapter~\ref{Cic}) or a type -%% coercible to it, (see \ref{Coercions}). When the type of a -%% whole expression is forced, it is usually not necessary to give the types of -%% the variables involved in the term. - -%% Example: - -%% \begin{coq_example} -%% Definition ID := forall X:Set, X -> X. -%% Definition id := (fun X x => x):ID. -%% Check id. -%% \end{coq_example} - -\section{Advanced recursive functions} - -The following \emph{experimental} command is available -when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: -\begin{center} - \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - \{decrease\_annot\} : type$_0$ := \term$_0$} - \comindex{Function} - \label{Function} -\end{center} -This command can be seen as a generalization of {\tt Fixpoint}. It is actually -a wrapper for several ways of defining a function \emph{and other useful - related objects}, namely: an induction principle that reflects the -recursive structure of the function (see \ref{FunInduction}) and its -fixpoint equality. - The meaning of this -declaration is to define a function {\it ident}, similarly to {\tt - Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be -given (unless the function is not recursive), but it might not -necessarily be \emph{structurally} decreasing. The point of the {\tt - \{\}} annotation is to name the decreasing argument \emph{and} to -describe which kind of decreasing criteria must be used to ensure -termination of recursive calls. - -The {\tt Function} construction also enjoys the {\tt with} extension -to define mutually recursive definitions. However, this feature does -not work for non structurally recursive functions. % VRAI?? - -See the documentation of {\tt functional induction} -(see Section~\ref{FunInduction}) and {\tt Functional Scheme} -(see Section~\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the -induction principle to easily reason about the function. - -\noindent {\bf Remark: } To obtain the right principle, it is better -to put rigid parameters of the function as first arguments. For -example it is better to define plus like this: - -\begin{coq_example*} -Function plus (m n : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus m p) - end. -\end{coq_example*} -\noindent than like this: -\begin{coq_eval} -Reset plus. -\end{coq_eval} -\begin{coq_example*} -Function plus (n m : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus p m) - end. -\end{coq_example*} - -\paragraph[Limitations]{Limitations\label{sec:Function-limitations}} -\term$_0$ must be built as a \emph{pure pattern-matching tree} -(\texttt{match...with}) with applications only \emph{at the end} of -each branch. - -Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~: -\begin{coq_eval} -Require List. -\end{coq_eval} -\begin{coq_example*} -Fail Function wrong (C:nat) : nat := - List.hd 0 (List.map wrong (C::nil)). -\end{coq_example*} - -For now dependent cases are not treated for non structurally terminating functions. - - - -\begin{ErrMsgs} -\item \errindex{The recursive argument must be specified} -\item \errindex{No argument name \ident} -\item \errindex{Cannot use mutual definition with well-founded - recursion or measure} - -\item \errindex{Cannot define graph for \ident\dots} (warning) - - The generation of the graph relation \texttt{(R\_\ident)} used to - compute the induction scheme of \ident\ raised a typing error. Only - the ident is defined; the induction scheme will not be generated. - - This error happens generally when: - - \begin{itemize} - \item the definition uses pattern matching on dependent types, which - \texttt{Function} cannot deal with yet. - \item the definition is not a \emph{pattern-matching tree} as - explained above. - \end{itemize} - -\item \errindex{Cannot define principle(s) for \ident\dots} (warning) - - The generation of the graph relation \texttt{(R\_\ident)} succeeded - but the induction principle could not be built. Only the ident is - defined. Please report. - -\item \errindex{Cannot build functional inversion principle} (warning) - - \texttt{functional inversion} will not be available for the - function. -\end{ErrMsgs} - - -\SeeAlso{\ref{FunScheme}, \ref{FunScheme-examples}, \ref{FunInduction}} - -Depending on the {\tt \{$\ldots$\}} annotation, different definition -mechanisms are used by {\tt Function}. More precise description -given below. - -\begin{Variants} -\item \texttt{ Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - : type$_0$ := \term$_0$} - - Defines the not recursive function \ident\ as if declared with - \texttt{Definition}. Moreover the following are defined: - - \begin{itemize} - \item {\tt\ident\_rect}, {\tt\ident\_rec} and {\tt\ident\_ind}, - which reflect the pattern matching structure of \term$_0$ (see the - documentation of {\tt Inductive} \ref{Inductive}); - \item The inductive \texttt{R\_\ident} corresponding to the graph of - \ident\ (silently); - \item \texttt{\ident\_complete} and \texttt{\ident\_correct} which are - inversion information linking the function and its graph. - \end{itemize} -\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$} - - Defines the structural recursive function \ident\ as if declared - with \texttt{Fixpoint}. Moreover the following are defined: - - \begin{itemize} - \item The same objects as above; - \item The fixpoint equation of \ident: \texttt{\ident\_equation}. - \end{itemize} - -\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt - \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := - \term$_0$} -\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$} - -Defines a recursive function by well founded recursion. \textbf{The -module \texttt{Recdef} of the standard library must be loaded for this -feature}. The {\tt \{\}} annotation is mandatory and must be one of -the following: -\begin{itemize} -\item {\tt \{measure} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ - being the decreasing argument and \term$_1$ being a function - from type of \ident$_0$ to \texttt{nat} for which value on the - decreasing argument decreases (for the {\tt lt} order on {\tt - nat}) at each recursive call of \term$_0$. Parameters of the - function are bound in \term$_0$; -\item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being - the decreasing argument and \term$_1$ an ordering relation on - the type of \ident$_0$ (i.e. of type T$_{\ident_0}$ - $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which - the decreasing argument decreases at each recursive call of - \term$_0$. The order must be well founded. Parameters of the - function are bound in \term$_0$. -\end{itemize} - -Depending on the annotation, the user is left with some proof -obligations that will be used to define the function. These proofs -are: proofs that each recursive call is actually decreasing with -respect to the given criteria, and (if the criteria is \texttt{wf}) a -proof that the ordering relation is well founded. - -%Completer sur measure et wf - -Once proof obligations are discharged, the following objects are -defined: - -\begin{itemize} -\item The same objects as with the \texttt{struct}; -\item The lemma \texttt{\ident\_tcc} which collects all proof - obligations in one property; -\item The lemmas \texttt{\ident\_terminate} and \texttt{\ident\_F} - which is needed to be inlined during extraction of \ident. -\end{itemize} - - - -%Complete!! -The way this recursive function is defined is the subject of several -papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles Barthe, -Julien Forest, David Pichardie, and Vlad Rusu on the other hand. - -%Exemples ok ici - -\bigskip - -\noindent {\bf Remark: } Proof obligations are presented as several -subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independent which means that in order to -% abort them you will have to abort each separately. - - - -%The decreasing argument cannot be dependent of another?? - -%Exemples faux ici -\end{Variants} - - -\section{Section mechanism -\index{Sections} -\label{Section}} - -The sectioning mechanism can be used to to organize a proof in -structured sections. Then local declarations become available (see -Section~\ref{Basic-definitions}). - -\subsection{\tt Section {\ident}\comindex{Section}} - -This command is used to open a section named {\ident}. - -%% Discontinued ? -%% \begin{Variants} -%% \comindex{Chapter} -%% \item{\tt Chapter {\ident}}\\ -%% Same as {\tt Section {\ident}} -%% \end{Variants} - -\subsection{\tt End {\ident} -\comindex{End}} - -This command closes the section named {\ident}. After closing of the -section, the local declarations (variables and local definitions) get -{\em discharged}, meaning that they stop being visible and that all -global objects defined in the section are generalized with respect to -the variables and local definitions they each depended on in the -section. - - -Here is an example : -\begin{coq_example} -Section s1. -Variables x y : nat. -Let y' := y. -Definition x' := S x. -Definition x'' := x' + y'. -Print x'. -End s1. -Print x'. -Print x''. -\end{coq_example} -Notice the difference between the value of {\tt x'} and {\tt x''} -inside section {\tt s1} and outside. - -\begin{ErrMsgs} -\item \errindex{This is not the last opened section} -\end{ErrMsgs} - -\begin{Remarks} -\item Most commands, like {\tt Hint}, {\tt Notation}, option management, ... -which appear inside a section are canceled when the -section is closed. -% see Section~\ref{LongNames} -%\item Usually all identifiers must be distinct. -%However, a name already used in a closed section (see \ref{Section}) -%can be reused. In this case, the old name is no longer accessible. - -% Obsolète -%\item A module implicitly open a section. Be careful not to name a -%module with an identifier already used in the module (see \ref{compiled}). -\end{Remarks} - -\input{RefMan-mod.v} - -\section{Libraries and qualified names} - -\subsection{Names of libraries -\label{Libraries} -\index{Libraries}} - -The theories developed in {\Coq} are stored in {\em library files} -which are hierarchically classified into {\em libraries} and {\em - sublibraries}. To express this hierarchy, library names are -represented by qualified identifiers {\qualid}, i.e. as list of -identifiers separated by dots (see Section~\ref{qualid}). For -instance, the library file {\tt Mult} of the standard {\Coq} library -{\tt Arith} is named {\tt Coq.Arith.Mult}. The identifier that starts -the name of a library is called a {\em library root}. All library -files of the standard library of {\Coq} have the reserved root {\tt Coq} -but library file names based on other roots can be obtained by using -{\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options -{\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an -interactive {\Coq} session starts, a library of root {\tt Top} is -started, unless option {\tt -top} is set (see -Section~\ref{coqoptions}). - -\subsection{Qualified names -\label{LongNames} -\index{Qualified identifiers} -\index{Absolute names}} - -Library files are modules which possibly contain submodules which -eventually contain constructions (axioms, parameters, definitions, -lemmas, theorems, remarks or facts). The {\em absolute name}, or {\em -full name}, of a construction in some library file is a qualified -identifier starting with the logical name of the library file, -followed by the sequence of submodules names encapsulating the -construction and ended by the proper name of the construction. -Typically, the absolute name {\tt Coq.Init.Logic.eq} denotes Leibniz' -equality defined in the module {\tt Logic} in the sublibrary {\tt -Init} of the standard library of \Coq. - -The proper name that ends the name of a construction is the {\it short -name} (or sometimes {\it base name}) of the construction (for -instance, the short name of {\tt Coq.Init.Logic.eq} is {\tt eq}). Any -partial suffix of the absolute name is a {\em partially qualified name} -(e.g. {\tt Logic.eq} is a partially qualified name for {\tt -Coq.Init.Logic.eq}). Especially, the short name of a construction is -its shortest partially qualified name. - -{\Coq} does not accept two constructions (definition, theorem, ...) -with the same absolute name but different constructions can have the -same short name (or even same partially qualified names as soon as the -full names are different). - -Notice that the notion of absolute, partially qualified and -short names also applies to library file names. - -\paragraph{Visibility} - -{\Coq} maintains a table called {\it name table} which maps partially -qualified names of constructions to absolute names. This table is -updated by the commands {\tt Require} (see \ref{Require}), {\tt -Import} and {\tt Export} (see \ref{Import}) and also each time a new -declaration is added to the context. An absolute name is called {\it -visible} from a given short or partially qualified name when this -latter name is enough to denote it. This means that the short or -partially qualified name is mapped to the absolute name in {\Coq} name -table. Definitions flagged as {\tt Local} are only accessible with their -fully qualified name (see \ref{Definition}). - -It may happen that a visible name is hidden by the short name or a -qualified name of another construction. In this case, the name that -has been hidden must be referred to using one more level of -qualification. To ensure that a construction always remains -accessible, absolute names can never be hidden. - -Examples: -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example} -Check 0. -Definition nat := bool. -Check 0. -Check Datatypes.nat. -Locate nat. -\end{coq_example} - -\SeeAlso Command {\tt Locate} in Section~\ref{Locate} and {\tt Locate -Library} in Section~\ref{Locate Library}. - -\subsection{Libraries and filesystem\label{loadpath}\index{Loadpath} -\index{Physical paths} \index{Logical paths}} - -Please note that the questions described here have been subject to -redesign in Coq v8.5. Former versions of Coq use the same terminology -to describe slightly different things. - -Compiled files (\texttt{.vo} and \texttt{.vio}) store sub-libraries. In -order to refer to them inside {\Coq}, a translation from file-system -names to {\Coq} names is needed. In this translation, names in the -file system are called {\em physical} paths while {\Coq} names are -contrastingly called {\em logical} names. - -A logical prefix {\tt Lib} can be associated to a physical path -\textrm{\textsl{path}} using the command line option {\tt -Q} -\textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are -recursively associated to the logical path {\tt Lib} extended with the -corresponding suffix coming from the physical path. For instance, the -folder {\tt path/fOO/Bar} maps to {\tt Lib.fOO.Bar}. Subdirectories -corresponding to invalid {\Coq} identifiers are skipped, and, by -convention, subdirectories named {\tt CVS} or {\tt \_darcs} are -skipped too. - -Thanks to this mechanism, {\texttt{.vo}} files are made available through the -logical name of the folder they are in, extended with their own basename. For -example, the name associated to the file {\tt path/fOO/Bar/File.vo} is -{\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers. -When compiling a source file, the {\texttt{.vo}} file stores its logical name, -so that an error is issued if it is loaded with the wrong loadpath afterwards. - -Some folders have a special status and are automatically put in the path. -{\Coq} commands associate automatically a logical path to files -in the repository trees rooted at the directory from where the command -is launched, \textit{coqlib}\texttt{/user-contrib/}, the directories -listed in the \verb:$COQPATH:, \verb:${XDG_DATA_HOME}/coq/: and -\verb:${XDG_DATA_DIRS}/coq/: environment variables (see -\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}) -with the same physical-to-logical translation and with an empty logical prefix. - -The command line option \texttt{-R} is a variant of \texttt{-Q} which has the -strictly same behavior regarding loadpaths, but which also makes the -corresponding \texttt{.vo} files available through their short names in a -way not unlike the {\tt Import} command (see~{\ref{Import}}). For instance, -\texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file -\texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but -allows this file to be accessed through the short names \texttt{fOO.Bar.File}, -\texttt{Bar.File} and \texttt{File}. If several files with identical base name -are present in different subdirectories of a recursive loadpath, which of -these files is found first may be system-dependent and explicit -qualification is recommended. The {\tt From} argument of the {\tt Require} -command can be used to bypass the implicit shortening by providing an absolute -root to the required file (see~\ref{Require}). - -There also exists another independent loadpath mechanism attached to {\ocaml} -object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files -as described above. The {\ocaml} loadpath is managed using the option -\texttt{-I path} (in the {\ocaml} world, there is neither a notion of logical -name prefix nor a way to access files in subdirectories of \texttt{path}). -See the command \texttt{Declare ML Module} in Section~\ref{compiled} to -understand the need of the {\ocaml} loadpath. - -See Section~\ref{coqoptions} for a more general view over the {\Coq} -command line options. - -%% \paragraph{The special case of remarks and facts} -%% -%% In contrast with definitions, lemmas, theorems, axioms and parameters, -%% the absolute name of remarks includes the segment of sections in which -%% it is defined. Concretely, if a remark {\tt R} is defined in -%% subsection {\tt S2} of section {\tt S1} in module {\tt M}, then its -%% absolute name is {\tt M.S1.S2.R}. The same for facts, except that the -%% name of the innermost section is dropped from the full name. Then, if -%% a fact {\tt F} is defined in subsection {\tt S2} of section {\tt S1} -%% in module {\tt M}, then its absolute name is {\tt M.S1.F}. - -\section{Implicit arguments -\index{Implicit arguments} -\label{Implicit Arguments}} - -An implicit argument of a function is an argument which can be -inferred from contextual knowledge. There are different kinds of -implicit arguments that can be considered implicit in different -ways. There are also various commands to control the setting or the -inference of implicit arguments. - -\subsection{The different kinds of implicit arguments} - -\subsubsection{Implicit arguments inferable from the knowledge of other -arguments of a function} - -The first kind of implicit arguments covers the arguments that are -inferable from the knowledge of the type of other arguments of the -function, or of the type of the surrounding context of the -application. Especially, such implicit arguments correspond to -parameters dependent in the type of the function. Typical implicit -arguments are the type arguments in polymorphic functions. -There are several kinds of such implicit arguments. - -\paragraph{Strict Implicit Arguments.} -An implicit argument can be either strict or non strict. An implicit -argument is said {\em strict} if, whatever the other arguments of the -function are, it is still inferable from the type of some other -argument. Technically, an implicit argument is strict if it -corresponds to a parameter which is not applied to a variable which -itself is another parameter of the function (since this parameter -may erase its arguments), not in the body of a {\tt match}, and not -itself applied or matched against patterns (since the original -form of the argument can be lost by reduction). - -For instance, the first argument of -\begin{quote} -\verb|cons: forall A:Set, A -> list A -> list A| -\end{quote} -in module {\tt List.v} is strict because {\tt list} is an inductive -type and {\tt A} will always be inferable from the type {\tt -list A} of the third argument of {\tt cons}. -On the contrary, the second argument of a term of type -\begin{quote} -\verb|forall P:nat->Prop, forall n:nat, P n -> ex nat P| -\end{quote} -is implicit but not strict, since it can only be inferred from the -type {\tt P n} of the third argument and if {\tt P} is, e.g., {\tt -fun \_ => True}, it reduces to an expression where {\tt n} does not -occur any longer. The first argument {\tt P} is implicit but not -strict either because it can only be inferred from {\tt P n} and {\tt -P} is not canonically inferable from an arbitrary {\tt n} and the -normal form of {\tt P n} (consider e.g. that {\tt n} is {\tt 0} and -the third argument has type {\tt True}, then any {\tt P} of the form -{\tt fun n => match n with 0 => True | \_ => \mbox{\em anything} end} would -be a solution of the inference problem). - -\paragraph{Contextual Implicit Arguments.} -An implicit argument can be {\em contextual} or not. An implicit -argument is said {\em contextual} if it can be inferred only from the -knowledge of the type of the context of the current expression. For -instance, the only argument of -\begin{quote} -\verb|nil : forall A:Set, list A| -\end{quote} -is contextual. Similarly, both arguments of a term of type -\begin{quote} -\verb|forall P:nat->Prop, forall n:nat, P n \/ n = 0| -\end{quote} -are contextual (moreover, {\tt n} is strict and {\tt P} is not). - -\paragraph{Reversible-Pattern Implicit Arguments.} -There is another class of implicit arguments that can be reinferred -unambiguously if all the types of the remaining arguments are -known. This is the class of implicit arguments occurring in the type -of another argument in position of reversible pattern, which means it -is at the head of an application but applied only to uninstantiated -distinct variables. Such an implicit argument is called {\em -reversible-pattern implicit argument}. A typical example is the -argument {\tt P} of {\tt nat\_rec} in -\begin{quote} -{\tt nat\_rec : forall P : nat -> Set, - P 0 -> (forall n : nat, P n -> P (S n)) -> forall x : nat, P x}. -\end{quote} -({\tt P} is reinferable by abstracting over {\tt n} in the type {\tt P n}). - -See Section~\ref{SetReversiblePatternImplicit} for the automatic declaration -of reversible-pattern implicit arguments. - -\subsubsection{Implicit arguments inferable by resolution} - -This corresponds to a class of non dependent implicit arguments that -are solved based on the structure of their type only. - -\subsection{Maximal or non maximal insertion of implicit arguments} - -In case a function is partially applied, and the next argument to be -applied is an implicit argument, two disciplines are applicable. In the -first case, the function is considered to have no arguments furtherly: -one says that the implicit argument is not maximally inserted. In -the second case, the function is considered to be implicitly applied -to the implicit arguments it is waiting for: one says that the -implicit argument is maximally inserted. - -Each implicit argument can be declared to have to be inserted -maximally or non maximally. This can be governed argument per argument -by the command {\tt Implicit Arguments} (see~\ref{ImplicitArguments}) -or globally by the command {\tt Set Maximal Implicit Insertion} -(see~\ref{SetMaximalImplicitInsertion}). See also -Section~\ref{PrintImplicit}. - -\subsection{Casual use of implicit arguments} - -In a given expression, if it is clear that some argument of a function -can be inferred from the type of the other arguments, the user can -force the given argument to be guessed by replacing it by ``{\tt \_}''. If -possible, the correct argument will be automatically generated. - -\begin{ErrMsgs} - -\item \errindex{Cannot infer a term for this placeholder} - - {\Coq} was not able to deduce an instantiation of a ``{\tt \_}''. - -\end{ErrMsgs} - -\subsection{Declaration of implicit arguments -\comindex{Arguments}} -\label{ImplicitArguments} - -In case one wants that some arguments of a given object (constant, -inductive types, constructors, assumptions, local or not) are always -inferred by Coq, one may declare once and for all which are the expected -implicit arguments of this object. There are two ways to do this, -a priori and a posteriori. - -\subsubsection{Implicit Argument Binders} - -In the first setting, one wants to explicitly give the implicit -arguments of a declared object as part of its definition. To do this, one has -to surround the bindings of implicit arguments by curly braces: -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example} -Definition id {A : Type} (x : A) : A := x. -\end{coq_example} - -This automatically declares the argument {\tt A} of {\tt id} as a -maximally inserted implicit argument. One can then do as-if the argument -was absent in every situation but still be able to specify it if needed: -\begin{coq_example} -Definition compose {A B C} (g : B -> C) (f : A -> B) := - fun x => g (f x). -Goal forall A, compose id id = id (A:=A). -\end{coq_example} - -The syntax is supported in all top-level definitions: {\tt Definition}, -{\tt Fixpoint}, {\tt Lemma} and so on. For (co-)inductive datatype -declarations, the semantics are the following: an inductive parameter -declared as an implicit argument need not be repeated in the inductive -definition but will become implicit for the constructors of the -inductive only, not the inductive type itself. For example: - -\begin{coq_example} -Inductive list {A : Type} : Type := -| nil : list -| cons : A -> list -> list. -Print list. -\end{coq_example} - -One can always specify the parameter if it is not uniform using the -usual implicit arguments disambiguation syntax. - -\subsubsection{Declaring Implicit Arguments} - -To set implicit arguments a posteriori, one can use the -command: -\begin{quote} -\tt Arguments {\qualid} \nelist{\possiblybracketedident}{} -\end{quote} -where the list of {\possiblybracketedident} is a prefix of the list of arguments -of {\qualid} where the ones to be declared implicit are surrounded by square -brackets and the ones to be declared as maximally inserted implicits are -surrounded by curly braces. - -After the above declaration is issued, implicit arguments can just (and -have to) be skipped in any expression involving an application of -{\qualid}. - -Implicit arguments can be cleared with the following syntax: - -\begin{quote} -{\tt Arguments {\qualid} : clear implicits -\comindex{Arguments}} -\end{quote} - -\begin{Variants} -\item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{} -\comindex{Global Arguments}} - -Tell to recompute the implicit arguments of {\qualid} after ending of -the current section if any, enforcing the implicit arguments known -from inside the section to be the ones declared by the command. - -\item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{} -\comindex{Local Arguments}} - -When in a module, tell not to activate the implicit arguments of -{\qualid} declared by this command to contexts that require the -module. - -\item {\tt \zeroone{Global {\sl |} Local} Arguments {\qualid} \sequence{\nelist{\possiblybracketedident}{}}{,}} - -For names of constants, inductive types, constructors, lemmas which -can only be applied to a fixed number of arguments (this excludes for -instance constants whose type is polymorphic), multiple -implicit arguments decflarations can be given. -Depending on the number of arguments {\qualid} is applied -to in practice, the longest applicable list of implicit arguments is -used to select which implicit arguments are inserted. - -For printing, the omitted arguments are the ones of the longest list -of implicit arguments of the sequence. - -\end{Variants} - -\Example -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example*} -Inductive list (A:Type) : Type := - | nil : list A - | cons : A -> list A -> list A. -\end{coq_example*} -\begin{coq_example} -Check (cons nat 3 (nil nat)). -Arguments cons [A] _ _. -Arguments nil [A]. -Check (cons 3 nil). -Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := - match l with nil => nil | cons a t => cons (f a) (map A B f t) end. -Fixpoint length (A:Type) (l:list A) : nat := - match l with nil => 0 | cons _ m => S (length A m) end. -Arguments map [A B] f l. -Arguments length {A} l. (* A has to be maximally inserted *) -Check (fun l:list (list nat) => map length l). -Arguments map [A B] f l, [A] B f l, A B f l. -Check (fun l => map length l = map (list nat) nat length l). -\end{coq_example} - -\Rem To know which are the implicit arguments of an object, use the command -{\tt Print Implicit} (see \ref{PrintImplicit}). - -\subsection{Automatic declaration of implicit arguments} - -{\Coq} can also automatically detect what are the implicit arguments -of a defined object. The command is just -\begin{quote} -{\tt Arguments {\qualid} : default implicits -\comindex{Arguments}} -\end{quote} -The auto-detection is governed by options telling if strict, -contextual, or reversible-pattern implicit arguments must be -considered or not (see -Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversiblePatternImplicit} -and also~\ref{SetMaximalImplicitInsertion}). - -\begin{Variants} -\item {\tt Global Arguments {\qualid} : default implicits -\comindex{Global Arguments}} - -Tell to recompute the implicit arguments of {\qualid} after ending of -the current section if any. - -\item {\tt Local Arguments {\qualid} : default implicits -\comindex{Local Arguments}} - -When in a module, tell not to activate the implicit arguments of -{\qualid} computed by this declaration to contexts that requires the -module. - -\end{Variants} - -\Example -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example*} -Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. -\end{coq_example*} -\begin{coq_example} -Arguments cons : default implicits. -Print Implicit cons. -Arguments nil : default implicits. -Print Implicit nil. -Set Contextual Implicit. -Arguments nil : default implicits. -Print Implicit nil. -\end{coq_example} - -The computation of implicit arguments takes account of the -unfolding of constants. For instance, the variable {\tt p} below has -type {\tt (Transitivity R)} which is reducible to {\tt forall x,y:U, R x -y -> forall z:U, R y z -> R x z}. As the variables {\tt x}, {\tt y} and -{\tt z} appear strictly in body of the type, they are implicit. - -\begin{coq_example*} -Variable X : Type. -Definition Relation := X -> X -> Prop. -Definition Transitivity (R:Relation) := - forall x y:X, R x y -> forall z:X, R y z -> R x z. -Variables (R : Relation) (p : Transitivity R). -Arguments p : default implicits. -\end{coq_example*} -\begin{coq_example} -Print p. -Print Implicit p. -\end{coq_example} -\begin{coq_example*} -Variables (a b c : X) (r1 : R a b) (r2 : R b c). -\end{coq_example*} -\begin{coq_example} -Check (p r1 r2). -\end{coq_example} - -\subsection{Mode for automatic declaration of implicit arguments -\label{Auto-implicit} -\optindex{Implicit Arguments}} - -In case one wants to systematically declare implicit the arguments -detectable as such, one may switch to the automatic declaration of -implicit arguments mode by using the command -\begin{quote} -\tt Set Implicit Arguments. -\end{quote} -Conversely, one may unset the mode by using {\tt Unset Implicit -Arguments}. The mode is off by default. Auto-detection of implicit -arguments is governed by options controlling whether strict and -contextual implicit arguments have to be considered or not. - -\subsection{Controlling strict implicit arguments -\optindex{Strict Implicit} -\label{SetStrictImplicit}} - -When the mode for automatic declaration of implicit arguments is on, -the default is to automatically set implicit only the strict implicit -arguments plus, for historical reasons, a small subset of the non -strict implicit arguments. To relax this constraint and to -set implicit all non strict implicit arguments by default, use the command -\begin{quote} -\tt Unset Strict Implicit. -\end{quote} -Conversely, use the command {\tt Set Strict Implicit} to -restore the original mode that declares implicit only the strict implicit arguments plus a small subset of the non strict implicit arguments. - -In the other way round, to capture exactly the strict implicit arguments and no more than the strict implicit arguments, use the command: -\optindex{Strongly Strict Implicit} -\begin{quote} -\tt Set Strongly Strict Implicit. -\end{quote} -Conversely, use the command {\tt Unset Strongly Strict Implicit} to -let the option ``{\tt Strict Implicit}'' decide what to do. - -\Rem In versions of {\Coq} prior to version 8.0, the default was to -declare the strict implicit arguments as implicit. - -\subsection{Controlling contextual implicit arguments -\optindex{Contextual Implicit} -\label{SetContextualImplicit}} - -By default, {\Coq} does not automatically set implicit the contextual -implicit arguments. To tell {\Coq} to infer also contextual implicit -argument, use command -\begin{quote} -\tt Set Contextual Implicit. -\end{quote} -Conversely, use command {\tt Unset Contextual Implicit} to -unset the contextual implicit mode. - -\subsection{Controlling reversible-pattern implicit arguments -\optindex{Reversible Pattern Implicit} -\label{SetReversiblePatternImplicit}} - -By default, {\Coq} does not automatically set implicit the reversible-pattern -implicit arguments. To tell {\Coq} to infer also reversible-pattern implicit -argument, use command -\begin{quote} -\tt Set Reversible Pattern Implicit. -\end{quote} -Conversely, use command {\tt Unset Reversible Pattern Implicit} to -unset the reversible-pattern implicit mode. - -\subsection{Controlling the insertion of implicit arguments not followed by explicit arguments -\optindex{Maximal Implicit Insertion} -\label{SetMaximalImplicitInsertion}} - -Implicit arguments can be declared to be automatically inserted when a -function is partially applied and the next argument of the function is -an implicit one. In case the implicit arguments are automatically -declared (with the command {\tt Set Implicit Arguments}), the command -\begin{quote} -\tt Set Maximal Implicit Insertion. -\end{quote} -is used to tell to declare the implicit arguments with a maximal -insertion status. By default, automatically declared implicit -arguments are not declared to be insertable maximally. To restore the -default mode for maximal insertion, use command {\tt Unset Maximal -Implicit Insertion}. - -\subsection{Explicit applications -\index{Explicitly given implicit arguments} -\label{Implicits-explicitation} -\index{qualid@{\qualid}} \index{\symbol{64}}} - -In presence of non strict or contextual argument, or in presence of -partial applications, the synthesis of implicit arguments may fail, so -one may have to give explicitly certain implicit arguments of an -application. The syntax for this is {\tt (\ident:=\term)} where {\ident} -is the name of the implicit argument and {\term} is its corresponding -explicit term. Alternatively, one can locally deactivate the hiding of -implicit arguments of a function by using the notation -{\tt @{\qualid}~{\term}$_1$..{\term}$_n$}. This syntax extension is -given Figure~\ref{fig:explicitations}. -\begin{figure} -\begin{centerframe} -\begin{tabular}{lcl} -{\term} & ++= & @ {\qualid} \nelist{\term}{}\\ -& $|$ & @ {\qualid}\\ -& $|$ & {\qualid} \nelist{\textrm{\textsl{argument}}}{}\\ -\\ -{\textrm{\textsl{argument}}} & ::= & {\term} \\ -& $|$ & {\tt ({\ident}:={\term})}\\ -\end{tabular} -\end{centerframe} -\caption{Syntax for explicitly giving implicit arguments} -\label{fig:explicitations} -\end{figure} - -\noindent {\bf Example (continued): } -\begin{coq_example} -Check (p r1 (z:=c)). -Check (p (x:=a) (y:=b) r1 (z:=c) r2). -\end{coq_example} - -\subsection{Renaming implicit arguments -\comindex{Arguments} -} - -Implicit arguments names can be redefined using the following syntax: -\begin{quote} -{\tt Arguments {\qualid} \nelist{\name}{} : rename} -\end{quote} - -With the {\tt assert} flag, {\tt Arguments} can be used to assert -that a given object has the expected number of arguments and that -these arguments are named as expected. - -\noindent {\bf Example (continued): } -\begin{coq_example} -Arguments p [s t] _ [u] _: rename. -Check (p r1 (u:=c)). -Check (p (s:=a) (t:=b) r1 (u:=c) r2). -Fail Arguments p [s t] _ [w] _ : assert. -\end{coq_example} - - -\subsection{Displaying what the implicit arguments are -\comindex{Print Implicit} -\label{PrintImplicit}} - -To display the implicit arguments associated to an object, and to know -if each of them is to be used maximally or not, use the command -\begin{quote} -\tt Print Implicit {\qualid}. -\end{quote} - -\subsection{Explicit displaying of implicit arguments for pretty-printing -\optindex{Printing Implicit} -\optindex{Printing Implicit Defensive}} - -By default the basic pretty-printing rules hide the inferable implicit -arguments of an application. To force printing all implicit arguments, -use command -\begin{quote} -{\tt Set Printing Implicit.} -\end{quote} -Conversely, to restore the hiding of implicit arguments, use command -\begin{quote} -{\tt Unset Printing Implicit.} -\end{quote} - -By default the basic pretty-printing rules display the implicit arguments that are not detected as strict implicit arguments. This ``defensive'' mode can quickly make the display cumbersome so this can be deactivated by using the command -\begin{quote} -{\tt Unset Printing Implicit Defensive.} -\end{quote} -Conversely, to force the display of non strict arguments, use command -\begin{quote} -{\tt Set Printing Implicit Defensive.} -\end{quote} - -\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}. - -\subsection{Interaction with subtyping} - -When an implicit argument can be inferred from the type of more than -one of the other arguments, then only the type of the first of these -arguments is taken into account, and not an upper type of all of -them. As a consequence, the inference of the implicit argument of -``='' fails in -\begin{coq_example*} -Fail Check nat = Prop. -\end{coq_example*} - -but succeeds in -\begin{coq_example*} -Check Prop = nat. -\end{coq_example*} - -\subsection{Deactivation of implicit arguments for parsing} -\optindex{Parsing Explicit} - -Use of implicit arguments can be deactivated by issuing the command: -\begin{quote} -{\tt Set Parsing Explicit.} -\end{quote} - -In this case, all arguments of constants, inductive types, -constructors, etc, including the arguments declared as implicit, have -to be given as if none arguments were implicit. By symmetry, this also -affects printing. To restore parsing and normal printing of implicit -arguments, use: -\begin{quote} -{\tt Unset Parsing Explicit.} -\end{quote} - -\subsection{Canonical structures -\comindex{Canonical Structure}} - -A canonical structure is an instance of a record/structure type that -can be used to solve unification problems involving a projection -applied to an unknown structure instance (an implicit argument) and -a value. The complete documentation of canonical structures can be found -in Chapter~\ref{CS-full}, here only a simple example is given. - -Assume that {\qualid} denotes an object $(Build\_struc~ c_1~ \ldots~ c_n)$ in -the -structure {\em struct} of which the fields are $x_1$, ..., -$x_n$. Assume that {\qualid} is declared as a canonical structure -using the command -\begin{quote} -{\tt Canonical Structure {\qualid}.} -\end{quote} -Then, each time an equation of the form $(x_i~ -\_)=_{\beta\delta\iota\zeta}c_i$ has to be solved during the -type-checking process, {\qualid} is used as a solution. Otherwise -said, {\qualid} is canonically used to extend the field $c_i$ into a -complete structure built on $c_i$. - -Canonical structures are particularly useful when mixed with -coercions and strict implicit arguments. Here is an example. -\begin{coq_example*} -Require Import Relations. -Require Import EqNat. -Set Implicit Arguments. -Unset Strict Implicit. -Structure Setoid : Type := - {Carrier :> Set; - Equal : relation Carrier; - Prf_equiv : equivalence Carrier Equal}. -Definition is_law (A B:Setoid) (f:A -> B) := - forall x y:A, Equal x y -> Equal (f x) (f y). -Axiom eq_nat_equiv : equivalence nat eq_nat. -Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. -Canonical Structure nat_setoid. -\end{coq_example*} - -Thanks to \texttt{nat\_setoid} declared as canonical, the implicit -arguments {\tt A} and {\tt B} can be synthesized in the next statement. -\begin{coq_example} -Lemma is_law_S : is_law S. -\end{coq_example} - -\Rem If a same field occurs in several canonical structure, then -only the structure declared first as canonical is considered. - -\begin{Variants} -\item {\tt Canonical Structure {\ident} := {\term} : {\type}.}\\ - {\tt Canonical Structure {\ident} := {\term}.}\\ - {\tt Canonical Structure {\ident} : {\type} := {\term}.} - -These are equivalent to a regular definition of {\ident} followed by -the declaration - -{\tt Canonical Structure {\ident}}. -\end{Variants} - -\SeeAlso more examples in user contribution \texttt{category} -(\texttt{Rocq/ALGEBRA}). - -\subsubsection{Print Canonical Projections. -\comindex{Print Canonical Projections}} - -This displays the list of global names that are components of some -canonical structure. For each of them, the canonical structure of -which it is a projection is indicated. For instance, the above example -gives the following output: - -\begin{coq_example} -Print Canonical Projections. -\end{coq_example} - -\subsection{Implicit types of variables} -\comindex{Implicit Types} - -It is possible to bind variable names to a given type (e.g. in a -development using arithmetic, it may be convenient to bind the names -{\tt n} or {\tt m} to the type {\tt nat} of natural numbers). The -command for that is -\begin{quote} -\tt Implicit Types \nelist{\ident}{} : {\type} -\end{quote} -The effect of the command is to automatically set the type of bound -variables starting with {\ident} (either {\ident} itself or -{\ident} followed by one or more single quotes, underscore or digits) -to be {\type} (unless the bound variable is already declared with an -explicit type in which case, this latter type is considered). - -\Example -\begin{coq_example} -Require Import List. -Implicit Types m n : nat. -Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m. -intros m n. -Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. -\end{coq_example} - -\begin{Variants} -\item {\tt Implicit Type {\ident} : {\type}}\\ -This is useful for declaring the implicit type of a single variable. -\item - {\tt Implicit Types\,% -(\,{\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 implicit types with different specifications. -\end{Variants} - - -\subsection{Implicit generalization -\label{implicit-generalization} -\comindex{Generalizable Variables}} -% \textquoteleft since \` doesn't do what we want -\index{0genimpl@{\textquoteleft\{\ldots\}}} -\index{0genexpl@{\textquoteleft(\ldots)}} - -Implicit generalization is an automatic elaboration of a statement with -free variables into a closed statement where these variables are -quantified explicitly. Implicit generalization is done inside binders -starting with a \texttt{\`{}} and terms delimited by \texttt{\`{}\{ \}} and -\texttt{\`{}( )}, always introducing maximally inserted implicit arguments for -the generalized variables. Inside implicit generalization -delimiters, free variables in the current context are automatically -quantified using a product or a lambda abstraction to generate a closed -term. In the following statement for example, the variables \texttt{n} -and \texttt{m} are automatically generalized and become explicit -arguments of the lemma as we are using \texttt{\`{}( )}: - -\begin{coq_example} -Generalizable All Variables. -Lemma nat_comm : `(n = n + 0). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} -One can control the set of generalizable identifiers with the -\texttt{Generalizable} vernacular command to avoid unexpected -generalizations when mistyping identifiers. There are three variants of -the command: - -\begin{quote} -{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} -\end{quote} - -\begin{Variants} -\item {\tt Generalizable All Variables.} All variables are candidate for - generalization if they appear free in the context under a - generalization delimiter. This may result in confusing errors in - case of typos. In such cases, the context will probably contain some - unexpected generalized variable. - -\item {\tt Generalizable No Variables.} Disable implicit generalization - entirely. This is the default behavior. - -\item {\tt Generalizable Variable(s)? {\ident$_1$ \ident$_n$}.} - Allow generalization of the given identifiers only. Calling this - command multiple times adds to the allowed identifiers. - -\item {\tt Global Generalizable} Allows to export the choice of - generalizable variables. -\end{Variants} - -One can also use implicit generalization for binders, in which case the -generalized variables are added as binders and set maximally implicit. -\begin{coq_example*} -Definition id `(x : A) : A := x. -\end{coq_example*} -\begin{coq_example} -Print id. -\end{coq_example} - -The generalizing binders \texttt{\`{}\{ \}} and \texttt{\`{}( )} work similarly to -their explicit counterparts, only binding the generalized variables -implicitly, as maximally-inserted arguments. In these binders, the -binding name for the bound object is optional, whereas the type is -mandatory, dually to regular binders. - -\section{Coercions -\label{Coercions} -\index{Coercions}} - -Coercions can be used to implicitly inject terms from one {\em class} in -which they reside into another one. A {\em class} is either a sort -(denoted by the keyword {\tt Sortclass}), a product type (denoted by the -keyword {\tt Funclass}), or a type constructor (denoted by its name), -e.g. an inductive type or any constant with a type of the form -\texttt{forall} $(x_1:A_1) .. (x_n:A_n),~s$ where $s$ is a sort. - -Then the user is able to apply an -object that is not a function, but can be coerced to a function, and -more generally to consider that a term of type A is of type B provided -that there is a declared coercion between A and B. The main command is -\comindex{Coercion} -\begin{quote} -\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}. -\end{quote} -which declares the construction denoted by {\qualid} as a -coercion between {\class$_1$} and {\class$_2$}. - -More details and examples, and a description of the commands related -to coercions are provided in Chapter~\ref{Coercions-full}. - -\section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll} -\optindex{Printing All}} - -Coercions, implicit arguments, the type of pattern-matching, but also -notations (see Chapter~\ref{Addoc-syntax}) can obfuscate the behavior -of some tactics (typically the tactics applying to occurrences of -subterms are sensitive to the implicit arguments). The command -\begin{quote} -{\tt Set Printing All.} -\end{quote} -deactivates all high-level printing features such as coercions, -implicit arguments, returned type of pattern-matching, notations and -various syntactic sugar for pattern-matching or record projections. -Otherwise said, {\tt Set Printing All} includes the effects -of the commands {\tt Set Printing Implicit}, {\tt Set Printing -Coercions}, {\tt Set Printing Synth}, {\tt Unset Printing Projections} -and {\tt Unset Printing Notations}. To reactivate the high-level -printing features, use the command -\begin{quote} -{\tt Unset Printing All.} -\end{quote} - -\section[Printing universes]{Printing universes\label{PrintingUniverses} -\optindex{Printing Universes}} - -The following command: -\begin{quote} -{\tt Set Printing Universes} -\end{quote} -activates the display of the actual level of each occurrence of -{\Type}. See Section~\ref{Sorts} for details. This wizard option, in -combination with \texttt{Set Printing All} (see -section~\ref{SetPrintingAll}) can help to diagnose failures to unify -terms apparently identical but internally different in the Calculus of -Inductive Constructions. To reactivate the display of the actual level -of the occurrences of {\Type}, use -\begin{quote} -{\tt Unset Printing Universes.} -\end{quote} - -\comindex{Print Universes} -\comindex{Print Sorted Universes} - -The constraints on the internal level of the occurrences of {\Type} -(see Section~\ref{Sorts}) can be printed using the command -\begin{quote} -{\tt Print \zeroone{Sorted} Universes.} -\end{quote} -If the optional {\tt Sorted} option is given, each universe will be -made equivalent to a numbered label reflecting its level (with a -linear ordering) in the universe hierarchy. - -This command also accepts an optional output filename: -\begin{quote} -\tt Print \zeroone{Sorted} Universes {\str}. -\end{quote} -If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are -printed in the DOT language, and can be processed by Graphviz -tools. The format is unspecified if {\str} doesn't end in -\texttt{.dot} or \texttt{.gv}. - -\section[Existential variables]{Existential variables\label{ExistentialVariables}} -\label{evars} - -Coq terms can include existential variables which -represents unknown subterms to eventually be replaced by actual -subterms. - -Existential variables are generated in place of unsolvable implicit -arguments or ``{\tt \_}'' placeholders when using commands such as -\texttt{Check} (see Section~\ref{Check}) or when using tactics such as -\texttt{refine}~(see Section~\ref{refine}), as well as in place of unsolvable -instances when using tactics such that \texttt{eapply} (see -Section~\ref{eapply}). An existential variable is defined in a -context, which is the context of variables of the placeholder which -generated the existential variable, and a type, which is the expected -type of the placeholder. - -As a consequence of typing constraints, existential variables can be -duplicated in such a way that they possibly appear in different -contexts than their defining context. Thus, any occurrence of a given -existential variable comes with an instance of its original context. In the -simple case, when an existential variable denotes the placeholder -which generated it, or is used in the same context as the one in which -it was generated, the context is not displayed and the existential -variable is represented by ``?'' followed by an identifier. - -\begin{coq_example} -Parameter identity : forall (X:Set), X -> X. -Check identity _ _. -Check identity _ (fun x => _). -\end{coq_example} - -In the general case, when an existential variable ?{\ident} -appears outside of its context of definition, its instance, written under -the form \verb!@{id1:=term1; ...; idn:=termn}!, is appending to its -name, indicating how the variables of its defining context are -instantiated. The variables of the context of the existential -variables which are instantiated by themselves are not written, unless -the flag {\tt Printing Existential Instances} is on (see -Section~\ref{SetPrintingExistentialInstances}), and this is why an -existential variable used in the same context as its context of -definition is written with no instance. - -\begin{coq_example} -Check (fun x y => _) 0 1. -Set Printing Existential Instances. -Check (fun x y => _) 0 1. -\end{coq_example} - -\begin{coq_eval} -Unset Printing Existential Instances. -\end{coq_eval} - -Existential variables can be named by the user upon creation using -the syntax {\tt ?[\ident]}. This is useful when the existential -variable needs to be explicitly handled later in the script (e.g. -with a named-goal selector, see~\ref{ltac:selector}). - -\subsection{Explicit displaying of existential instances for pretty-printing -\label{SetPrintingExistentialInstances} -\optindex{Printing Existential Instances}} - -The command: -\begin{quote} -{\tt Set Printing Existential Instances} -\end{quote} -activates the full display of how the context of an existential variable is -instantiated at each of the occurrences of the existential variable. - -To deactivate the full display of the instances of existential -variables, use -\begin{quote} -{\tt Unset Printing Existential Instances.} -\end{quote} - -\subsection{Solving existential variables using tactics} -\ttindex{ltac:( \ldots )} - -\def\expr{\textrm{\textsl{tacexpr}}} - -Instead of letting the unification engine try to solve an existential variable -by itself, one can also provide an explicit hole together with a tactic to solve -it. Using the syntax {\tt ltac:(\expr)}, the user can put a -tactic anywhere a term is expected. The order of resolution is not specified and -is implementation-dependent. The inner tactic may use any variable defined in -its scope, including repeated alternations between variables introduced by term -binding as well as those introduced by tactic binding. The expression {\expr} -can be any tactic expression as described at section~\ref{TacticLanguage}. - -\begin{coq_example*} -Definition foo (x : nat) : nat := ltac:(exact x). -\end{coq_example*} - -This construction is useful when one wants to define complicated terms using -highly automated tactics without resorting to writing the proof-term by means of -the interactive proof engine. - -This mechanism is comparable to the {\tt Declare Implicit Tactic} command -defined at~\ref{DeclareImplicit}, except that the used tactic is local to each -hole instead of being declared globally. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex deleted file mode 100644 index b4e270e6c..000000000 --- a/doc/refman/RefMan-mod.tex +++ /dev/null @@ -1,428 +0,0 @@ -\section{Module system -\index{Modules} -\label{section:Modules}} - -The module system provides a way of packaging related elements -together, as well as a means of massive abstraction. - -\begin{figure}[t] -\begin{centerframe} -\begin{tabular}{rcl} -{\modtype} & ::= & {\qualid} \\ - & $|$ & {\modtype} \texttt{ with Definition }{\qualid} := {\term} \\ - & $|$ & {\modtype} \texttt{ with Module }{\qualid} := {\qualid} \\ - & $|$ & {\qualid} \nelist{\qualid}{}\\ - & $|$ & $!${\qualid} \nelist{\qualid}{}\\ - &&\\ - -{\onemodbinding} & ::= & {\tt ( [Import|Export] \nelist{\ident}{} : {\modtype} )}\\ - &&\\ - -{\modbindings} & ::= & \nelist{\onemodbinding}{}\\ - &&\\ - -{\modexpr} & ::= & \nelist{\qualid}{} \\ - & $|$ & $!$\nelist{\qualid}{} -\end{tabular} -\end{centerframe} -\caption{Syntax of modules} -\end{figure} - -In the syntax of module application, the $!$ prefix indicates that -any {\tt Inline} directive in the type of the functor arguments -will be ignored (see \ref{Inline} below). - -\subsection{\tt Module {\ident} -\comindex{Module}} - -This command is used to start an interactive module named {\ident}. - -\begin{Variants} - -\item{\tt Module {\ident} {\modbindings}} - - Starts an interactive functor with parameters given by {\modbindings}. - -\item{\tt Module {\ident} \verb.:. {\modtype}} - - Starts an interactive module specifying its module type. - -\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}} - - Starts an interactive functor with parameters given by - {\modbindings}, and output module type {\modtype}. - -\item{\tt Module {\ident} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:.{ \modtype$_n$}} - - Starts an interactive module satisfying each {\modtype$_i$}. - -\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}} - - Starts an interactive functor with parameters given by - {\modbindings}. The output module type is verified against each - module type {\modtype$_i$}. - -\item\texttt{Module [Import|Export]} - - Behaves like \texttt{Module}, but automatically imports or exports - the module. - -\end{Variants} -\subsubsection{Reserved commands inside an interactive module: -\comindex{Include}} -\begin{enumerate} -\item {\tt Include {\module}} - - Includes the content of {\module} in the current interactive - module. Here {\module} can be a module expression or a module type - expression. If {\module} is a high-order module or module type - expression then the system tries to instantiate {\module} - by the current interactive module. - -\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} - -is a shortcut for {\tt Include {\module$_1$}} $\ldots$ {\tt Include {\module$_n$}} -\end{enumerate} -\subsection{\tt End {\ident} -\comindex{End}} - -This command closes the interactive module {\ident}. If the module type -was given the content of the module is matched against it and an error -is signaled if the matching fails. If the module is basic (is not a -functor) its components (constants, inductive types, submodules etc) are -now available through the dot notation. - -\begin{ErrMsgs} -\item \errindex{No such label {\ident}} -\item \errindex{Signature components for label {\ident} do not match} -\item \errindex{This is not the last opened module} -\end{ErrMsgs} - - -\subsection{\tt Module {\ident} := {\modexpr} -\comindex{Module}} - -This command defines the module identifier {\ident} to be equal to -{\modexpr}. - -\begin{Variants} -\item{\tt Module {\ident} {\modbindings} := {\modexpr}} - - Defines a functor with parameters given by {\modbindings} and body {\modexpr}. - -% Particular cases of the next 2 items -%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}} -% -% Defines a module with body {\modexpr} and interface {\modtype}. -%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}} -% -% Defines a module with body {\modexpr}, satisfying {\modtype}. - -\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} := - {\modexpr}} - - Defines a functor with parameters given by {\modbindings} (possibly none), - and output module type {\modtype}, with body {\modexpr}. - -\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}:= - {\modexpr}} - - Defines a functor with parameters given by {\modbindings} (possibly none) - with body {\modexpr}. The body is checked against each {\modtype$_i$}. - -\item{\tt Module {\ident} {\modbindings} := {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}} - - is equivalent to an interactive module where each {\modexpr$_i$} are included. - -\end{Variants} - -\subsection{\tt Module Type {\ident} -\comindex{Module Type}} - -This command is used to start an interactive module type {\ident}. - -\begin{Variants} - -\item{\tt Module Type {\ident} {\modbindings}} - - Starts an interactive functor type with parameters given by {\modbindings}. - -\end{Variants} -\subsubsection{Reserved commands inside an interactive module type: -\comindex{Include}\comindex{Inline}} -\label{Inline} -\begin{enumerate} -\item {\tt Include {\module}} - - Same as {\tt Include} inside a module. - -\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} - -is a shortcut for {\tt Include {\module$_1$}} $\ldots$ {\tt Include {\module$_n$}} - -\item {\tt {\assumptionkeyword} Inline {\assums} } - - The instance of this assumption will be automatically expanded at functor - application, except when this functor application is prefixed by a $!$ annotation. -\end{enumerate} -\subsection{\tt End {\ident} -\comindex{End}} - -This command closes the interactive module type {\ident}. - -\begin{ErrMsgs} -\item \errindex{This is not the last opened module type} -\end{ErrMsgs} - -\subsection{\tt Module Type {\ident} := {\modtype}} - -Defines a module type {\ident} equal to {\modtype}. - -\begin{Variants} -\item {\tt Module Type {\ident} {\modbindings} := {\modtype}} - - Defines a functor type {\ident} specifying functors taking arguments - {\modbindings} and returning {\modtype}. - -\item{\tt Module Type {\ident} {\modbindings} := {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}} - - is equivalent to an interactive module type were each {\modtype$_i$} are included. - -\end{Variants} - -\subsection{\tt Declare Module {\ident} : {\modtype} -\comindex{Declare Module}} - -Declares a module {\ident} of type {\modtype}. - -\begin{Variants} - -\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}} - - Declares a functor with parameters {\modbindings} and output module - type {\modtype}. - - -\end{Variants} - - -\subsubsection{Example} - -Let us define a simple module. -\begin{coq_example} -Module M. - Definition T := nat. - Definition x := 0. - Definition y : bool. - exact true. - Defined. -End M. -\end{coq_example} -Inside a module one can define constants, prove theorems and do any -other things that can be done in the toplevel. Components of a closed -module can be accessed using the dot notation: -\begin{coq_example} -Print M.x. -\end{coq_example} -A simple module type: -\begin{coq_example} -Module Type SIG. - Parameter T : Set. - Parameter x : T. -End SIG. -\end{coq_example} - -Now we can create a new module from \texttt{M}, giving it a less -precise specification: the \texttt{y} component is dropped as well -as the body of \texttt{x}. - -\begin{coq_eval} -Set Printing Depth 50. -\end{coq_eval} -% (********** The following is not correct and should produce **********) -% (***************** Error: N.y not a defined object *******************) -\begin{coq_example} -Module N : SIG with Definition T := nat := M. -Print N.T. -Print N.x. -Fail Print N.y. -\end{coq_example} -\begin{coq_eval} -Reset N. -\end{coq_eval} - -\noindent -The definition of \texttt{N} using the module type expression -\texttt{SIG with Definition T:=nat} is equivalent to the following -one: - -\begin{coq_example*} -Module Type SIG'. - Definition T : Set := nat. - Parameter x : T. -End SIG'. -Module N : SIG' := M. -\end{coq_example*} -If we just want to be sure that the our implementation satisfies a -given module type without restricting the interface, we can use a -transparent constraint -\begin{coq_example} -Module P <: SIG := M. -Print P.y. -\end{coq_example} -Now let us create a functor, i.e. a parametric module -\begin{coq_example} -Module Two (X Y: SIG). -\end{coq_example} -\begin{coq_example*} - Definition T := (X.T * Y.T)%type. - Definition x := (X.x, Y.x). -\end{coq_example*} -\begin{coq_example} -End Two. -\end{coq_example} -and apply it to our modules and do some computations -\begin{coq_example} -Module Q := Two M N. -Eval compute in (fst Q.x + snd Q.x). -\end{coq_example} -In the end, let us define a module type with two sub-modules, sharing -some of the fields and give one of its possible implementations: -\begin{coq_example} -Module Type SIG2. - Declare Module M1 : SIG. - Module M2 <: SIG. - Definition T := M1.T. - Parameter x : T. - End M2. -End SIG2. -\end{coq_example} -\begin{coq_example*} -Module Mod <: SIG2. - Module M1. - Definition T := nat. - Definition x := 1. - End M1. - Module M2 := M. -\end{coq_example*} -\begin{coq_example} -End Mod. -\end{coq_example} -Notice that \texttt{M} is a correct body for the component \texttt{M2} -since its \texttt{T} component is equal \texttt{nat} and hence -\texttt{M1.T} as specified. -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{Remarks} -\item Modules and module types can be nested components of each other. -\item One can have sections inside a module or a module type, but - not a module or a module type inside a section. -\item Commands like \texttt{Hint} or \texttt{Notation} can - also appear inside modules and module types. Note that in case of a - module definition like: - - \smallskip - \noindent - {\tt Module N : SIG := M.} - \smallskip - - or - - \smallskip - {\tt Module N : SIG.\\ - \ \ \dots\\ - End N.} - \smallskip - - hints and the like valid for \texttt{N} are not those defined in - \texttt{M} (or the module body) but the ones defined in - \texttt{SIG}. - -\end{Remarks} - -\subsection{\tt Import {\qualid} -\comindex{Import} -\label{Import}} - -If {\qualid} denotes a valid basic module (i.e. its module type is a -signature), makes its components available by their short names. - -Example: - -\begin{coq_example} -Module Mod. - Definition T:=nat. - Check T. -End Mod. -Check Mod.T. -Fail Check T. (* Incorrect! *) -Import Mod. -Check T. (* Now correct *) -\end{coq_example} -\begin{coq_eval} -Reset Mod. -\end{coq_eval} - -Some features defined in modules are activated only when a module is -imported. This is for instance the case of notations (see -Section~\ref{Notation}). - -Declarations made with the {\tt Local} flag are never imported by the -{\tt Import} command. Such declarations are only accessible through their -fully qualified name. - -Example: - -\begin{coq_example} -Module A. -Module B. -Local Definition T := nat. -End B. -End A. -Import A. -Fail Check B.T. -\end{coq_example} - -\begin{Variants} -\item{\tt Export {\qualid}}\comindex{Export} - - When the module containing the command {\tt Export {\qualid}} is - imported, {\qualid} is imported as well. -\end{Variants} - -\begin{ErrMsgs} - \item \errindexbis{{\qualid} is not a module}{is not a module} -% this error is impossible in the import command -% \item \errindex{Cannot mask the absolute name {\qualid} !} -\end{ErrMsgs} - -\begin{Warnings} - \item Trying to mask the absolute name {\qualid} ! -\end{Warnings} - -\subsection{\tt Print Module {\ident} -\comindex{Print Module} \optindex{Short Module Printing}} - -Prints the module type and (optionally) the body of the module {\ident}. - -For this command and {\tt Print Module Type}, the option {\tt Short - Module Printing} (off by default) disables the printing of the types of fields, -leaving only their names. - -\subsection{\tt Print Module Type {\ident} -\comindex{Print Module Type}} - -Prints the module type corresponding to {\ident}. - -\subsection{\tt Locate Module {\qualid} -\comindex{Locate Module}} - -Prints the full name of the module {\qualid}. - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 4935b70c5..c7a98fce4 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -95,7 +95,6 @@ Options A and B of the licence are {\em not} elected.} \defaultheaders %END LATEX \include{RefMan-gal.v}% Gallina -\include{RefMan-ext.v}% Gallina extensions \include{RefMan-lib.v}% The coq library \include{RefMan-cic.v}% The Calculus of Constructions \include{RefMan-modr}% The module system diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst new file mode 100644 index 000000000..a1950d136 --- /dev/null +++ b/doc/sphinx/language/gallina-extensions.rst @@ -0,0 +1,2152 @@ +\chapter[Extensions of \Gallina{}]{Extensions of \Gallina{}\label{Gallina-extension}\index{Gallina}} +%HEVEA\cutname{gallina-ext.html} + +{\gallina} is the kernel language of {\Coq}. We describe here extensions of +the Gallina's syntax. + +\section{Record types +\comindex{Record} +\comindex{Inductive} +\comindex{CoInductive} +\label{Record}} + +The \verb+Record+ construction is a macro allowing the definition of +records as is done in many programming languages. Its syntax is +described on Figure~\ref{record-syntax}. In fact, the \verb+Record+ +macro is more general than the usual record types, since it allows +also for ``manifest'' expressions. In this sense, the \verb+Record+ +construction allows defining ``signatures''. + +\begin{figure}[h] +\begin{centerframe} +\begin{tabular}{lcl} +{\sentence} & ++= & {\record}\\ + & & \\ +{\record} & ::= & + {\recordkw} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\ +&& ~~~~\zeroone{\ident} + \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ + & & \\ +{\recordkw} & ::= & + {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\ + & & \\ +{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\ + & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\ +\end{tabular} +\end{centerframe} +\caption{Syntax for the definition of {\tt Record}} +\label{record-syntax} +\end{figure} + +\noindent In the expression +\begin{quote} +{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\ + {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\ + {\ident$_n$} \binders$_n$ : {\term$_n$} \}.} +\end{quote} +\noindent the identifier {\ident} is the name of the defined record +and {\sort} is its type. The identifier {\ident$_0$} is the name of +its constructor. If {\ident$_0$} is omitted, the default name {\tt +Build\_{\ident}} is used. +If {\sort} is omitted, the default sort is {\Type}. +The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of +fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots, +{\tt forall {\binders$_n$}, {\term$_n$}} +their respective types. Remark that the type of {\ident$_i$} may +depend on the previous {\ident$_j$} (for $j bottom; + Rat_irred_cond : + forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. +\end{coq_example} + +Remark here that the field \verb+Rat_bottom_cond+ depends +on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends +on both \verb+top+ and \verb+bottom+. + +Let us now see the work done by the {\tt Record} macro. First the +macro generates a variant type definition with just one constructor: +\begin{quote} +{\tt Variant {\ident} {\params} : {\sort} := \\ + {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).} +\end{quote} +To build an object of type {\ident}, one should provide the +constructor {\ident$_0$} with $n$ terms filling the fields of +the record. + +As an example, let us define the rational $1/2$: +\begin{coq_example*} +Theorem one_two_irred : + forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. +Admitted. +\end{coq_example*} +\begin{coq_example} +Definition half := mkRat true 1 2 (O_S 1) one_two_irred. +\end{coq_example} +\begin{coq_example} +Check half. +\end{coq_example} + +\begin{figure}[t] +\begin{centerframe} +\begin{tabular}{lcl} +{\term} & ++= & + \verb!{|! \zeroone{\nelist{\fielddef}{;}} \verb!|}! \\ + & & \\ +{\fielddef} & ::= & {\name} \zeroone{\binders} := {\term} \\ +\end{tabular} +\end{centerframe} +\caption{Syntax for constructing elements of a \texttt{Record} using named fields} +\label{fig:fieldsyntax} +\end{figure} + +Alternatively, the following syntax allows creating objects by using named fields, as +shown on Figure~\ref{fig:fieldsyntax}. The +fields do not have to be in any particular order, nor do they have to be all +present if the missing ones can be inferred or prompted for (see +Section~\ref{Program}). + +\begin{coq_example} +Definition half' := + {| sign := true; + Rat_bottom_cond := O_S 1; + Rat_irred_cond := one_two_irred |}. +\end{coq_example} + +This syntax can be disabled globally for printing by +\begin{quote} +{\tt Unset Printing Records.} +\optindex{Printing Records} +\end{quote} +For a given type, one can override this using either +\begin{quote} +{\tt Add Printing Record {\ident}.} +\end{quote} +to get record syntax or +\begin{quote} +{\tt Add Printing Constructor {\ident}.} +\end{quote} +to get constructor syntax. + +This syntax can also be used for pattern matching. + +\begin{coq_example} +Eval compute in ( + match half with + | {| sign := true; top := n |} => n + | _ => 0 + end). +\end{coq_example} + +The macro generates also, when it is possible, the projection +functions for destructuring an object of type {\ident}. These +projection functions are given the names of the corresponding +fields. If a field is named ``\verb=_='' then no projection is built +for it. In our example: + +\begin{coq_example} +Eval compute in top half. +Eval compute in bottom half. +Eval compute in Rat_bottom_cond half. +\end{coq_example} + +An alternative syntax for projections based on a dot notation is +available: + +\begin{coq_example} +Eval compute in half.(top). +\end{coq_example} + +It can be activated for printing with the command +\optindex{Printing Projections} +\begin{quote} +{\tt Set Printing Projections.} +\end{quote} + +\begin{coq_example} +Set Printing Projections. +Check top half. +\end{coq_example} + +The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}. +When {\qualid} denotes a projection, the syntax {\tt + {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax +{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to +{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax +{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to +{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} +is the object projected and the other arguments are the parameters of +the inductive type. + +\begin{figure}[t] +\begin{centerframe} +\begin{tabular}{lcl} +{\term} & ++= & {\term} {\tt .(} {\qualid} {\tt )}\\ + & $|$ & {\term} {\tt .(} {\qualid} \nelist{\termarg}{} {\tt )}\\ + & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )} +\end{tabular} +\end{centerframe} +\caption{Syntax for \texttt{Record} projections} +\label{fig:projsyntax} +\end{figure} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{Remarks} + +\item Records defined with the {\tt Record} keyword are not allowed to be +recursive (references to the record's name in the type of its field +raises an error). To define recursive records, one can use the {\tt +Inductive} and {\tt CoInductive} keywords, resulting in an inductive +or co-inductive record. +A \emph{caveat}, however, is that records +cannot appear in mutually inductive (or co-inductive) definitions. + +\item Induction schemes are automatically generated for inductive records. +Automatic generation of induction schemes for non-recursive records +defined with the {\tt Record} keyword can be activated with the +{\tt Nonrecursive Elimination Schemes} option +(see~\ref{set-nonrecursive-elimination-schemes}). + +\item {\tt Structure} is a synonym of the keyword {\tt Record}. + +\end{Remarks} + +\begin{Warnings} +\item {\tt {\ident$_i$} cannot be defined.} + + It can happen that the definition of a projection is impossible. + This message is followed by an explanation of this impossibility. + There may be three reasons: + \begin{enumerate} + \item The name {\ident$_i$} already exists in the environment (see + Section~\ref{Axiom}). + \item The body of {\ident$_i$} uses an incorrect elimination for + {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}). + \item The type of the projections {\ident$_i$} depends on previous + projections which themselves could not be defined. + \end{enumerate} +\end{Warnings} + +\begin{ErrMsgs} + +\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.} + + The record name {\ident} appears in the type of its fields, but uses + the keyword {\tt Record}. Use the keyword {\tt Inductive} or {\tt + CoInductive} instead. +\item \errindex{Cannot handle mutually (co)inductive records.} + + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. +\item During the definition of the one-constructor inductive + definition, all the errors of inductive definitions, as described in + Section~\ref{gal-Inductive-Definitions}, may also occur. + +\end{ErrMsgs} + +\SeeAlso Coercions and records in Section~\ref{Coercions-and-records} +of the chapter devoted to coercions. + +\subsection{Primitive Projections} +\optindex{Primitive Projections} +\optindex{Printing Primitive Projection Parameters} +\optindex{Printing Primitive Projection Compatibility} +\index{Primitive projections} +\label{prim-proj} + +The option {\tt Set Primitive Projections} turns on the use of primitive +projections when defining subsequent records (even through the {\tt + Inductive} and {\tt CoInductive} commands). Primitive projections +extended the Calculus of Inductive Constructions with a new binary term +constructor {\tt r.(p)} representing a primitive projection p applied to +a record object {\tt r} (i.e., primitive projections are always +applied). Even if the record type has parameters, these do not appear at +applications of the projection, considerably reducing the sizes of terms +when manipulating parameterized records and typechecking time. On the +user level, primitive projections can be used as a replacement for the +usual defined ones, although there are a few notable differences. + +The internally omitted parameters can be reconstructed at printing time +even though they are absent in the actual AST manipulated by the kernel. This +can be obtained by setting the {\tt Printing Primitive Projection Parameters} +flag. Another compatibility printing can be activated thanks to the +{\tt Printing Primitive Projection Compatibility} option which governs the +printing of pattern-matching over primitive records. + +\subsubsection{Primitive Record Types} +When the {\tt Set Primitive Projections} option is on, definitions of +record types change meaning. When a type is declared with primitive +projections, its {\tt match} construct is disabled (see +\ref{primproj:compat} though). To eliminate the (co-)inductive type, one +must use its defined primitive projections. + +There are currently two ways to introduce primitive records types: +\begin{itemize} +\item Through the {\tt Record} command, in which case the type has to be + non-recursive. The defined type enjoys eta-conversion definitionally, + that is the generalized form of surjective pairing for records: + {\tt $r$ = Build\_R ($r$.($p_1$) .. $r$.($p_n$))}. Eta-conversion allows to define + dependent elimination for these types as well. +\item Through the {\tt Inductive} and {\tt CoInductive} commands, when + the body of the definition is a record declaration of the form {\tt + Build\_R \{ $p_1$ : $t_1$; .. ; $p_n$ : $t_n$ \}}. In this case the types can be + recursive and eta-conversion is disallowed. These kind of record types + differ from their traditional versions in the sense that dependent + elimination is not available for them and only non-dependent case analysis + can be defined. +\end{itemize} + +\subsubsection{Reduction} + +The basic reduction rule of a primitive projection is {\tt $p_i$ + (Build\_R $t_1$ .. $t_n$) $\rightarrow_{\iota}$ $t_i$}. However, to take the $\delta$ flag into +account, projections can be in two states: folded or unfolded. An +unfolded primitive projection application obeys the rule above, while +the folded version delta-reduces to the unfolded version. This allows to +precisely mimic the usual unfolding rules of constants. Projections +obey the usual {\tt simpl} flags of the {\tt Arguments} command in particular. + +There is currently no way to input unfolded primitive projections at the +user-level, and one must use the {\tt Printing Primitive Projection + Compatibility} to display unfolded primitive projections as matches +and distinguish them from folded ones. + +\subsubsection{Compatibility Projections and {\tt match}} +\label{primproj:compat} +To ease compatibility with ordinary record types, each primitive +projection is also defined as a ordinary constant taking parameters and +an object of the record type as arguments, and whose body is an +application of the unfolded primitive projection of the same name. These +constants are used when elaborating partial applications of the +projection. One can distinguish them from applications of the primitive +projection if the {\tt Printing Primitive Projection Parameters} option +is off: for a primitive projection application, parameters are printed +as underscores while for the compatibility projections they are printed +as usual. + +Additionally, user-written {\tt match} constructs on primitive records +are desugared into substitution of the projections, they cannot be +printed back as {\tt match} constructs. + + % - r.(p) and (p r) elaborate to native projection application, and + % the parameters cannot be mentioned. The following arguments are + % parsed according to the remaining implicit arguments declared for the + % projection (i.e. the implicit arguments after the record type + % argument). In dot notation, the record type argument is considered + % explicit no matter what its implicit status is. + % - r.(@p params) and @p args are parsed as regular applications of the + % projection with explicit parameters. + % - [simpl p] is forbidden, but [simpl @p] will simplify both the projection + % and its explicit [@p] version. + % - [unfold p] has no effect on projection applications unless it is applied + % to a constructor. If the explicit version appears it reduces to the + % projection application. + % - [pattern x at n], [rewrite x at n] and in general abstraction and selection + % of occurrences may fail due to the disappearance of parameters. + +\section{Variants and extensions of {\mbox{\tt match}} +\label{Extensions-of-match} +\index{match@{\tt match\ldots with\ldots end}}} + +\subsection{Multiple and nested pattern-matching +\index{ML-like patterns} +\label{Mult-match}} + +The basic version of \verb+match+ allows pattern-matching on simple +patterns. As an extension, multiple nested patterns or disjunction of +patterns are allowed, as in ML-like languages. + +The extension just acts as a macro that is expanded during parsing +into a sequence of {\tt match} on simple patterns. Especially, a +construction defined using the extended {\tt match} is generally +printed under its expanded form (see~\texttt{Set Printing Matching} in +section~\ref{SetPrintingMatching}). + +\SeeAlso Chapter~\ref{Mult-match-full}. + +\subsection{Pattern-matching on boolean values: the {\tt if} expression +\label{if-then-else} +\index{if@{\tt if ... then ... else}}} + +For inductive types with exactly two constructors and for +pattern-matchings expressions which do not depend on the arguments of +the constructors, it is possible to use a {\tt if ... then ... else} +notation. For instance, the definition + +\begin{coq_example} +Definition not (b:bool) := + match b with + | true => false + | false => true + end. +\end{coq_example} + +\noindent can be alternatively written + +\begin{coq_eval} +Reset not. +\end{coq_eval} +\begin{coq_example} +Definition not (b:bool) := if b then false else true. +\end{coq_example} + +More generally, for an inductive type with constructors {\tt C$_1$} +and {\tt C$_2$}, we have the following equivalence + +\smallskip + +{\tt if {\term} \zeroone{\ifitem} then {\term}$_1$ else {\term}$_2$} $\equiv$ +\begin{tabular}[c]{l} +{\tt match {\term} \zeroone{\ifitem} with}\\ +{\tt \verb!|! C$_1$ \_ {\ldots} \_ \verb!=>! {\term}$_1$} \\ +{\tt \verb!|! C$_2$ \_ {\ldots} \_ \verb!=>! {\term}$_2$} \\ +{\tt end} +\end{tabular} + +Here is an example. + +\begin{coq_example} +Check (fun x (H:{x=0}+{x<>0}) => + match H with + | left _ => true + | right _ => false + end). +\end{coq_example} + +Notice that the printing uses the {\tt if} syntax because {\tt sumbool} is +declared as such (see Section~\ref{printing-options}). + +\subsection{Irrefutable patterns: the destructuring {\tt let} variants +\index{let in@{\tt let ... in}} +\label{Letin}} + +Pattern-matching on terms inhabiting inductive type having only one +constructor can be alternatively written using {\tt let ... in ...} +constructions. There are two variants of them. + +\subsubsection{First destructuring {\tt let} syntax} +The expression {\tt let +(}~{\ident$_1$},\ldots,{\ident$_n$}~{\tt ) :=}~{\term$_0$}~{\tt +in}~{\term$_1$} performs case analysis on a {\term$_0$} which must be in +an inductive type with one constructor having itself $n$ arguments. Variables +{\ident$_1$}\ldots{\ident$_n$} are bound to the $n$ arguments of the +constructor in expression {\term$_1$}. For instance, the definition + +\begin{coq_example} +Definition fst (A B:Set) (H:A * B) := match H with + | pair x y => x + end. +\end{coq_example} + +can be alternatively written + +\begin{coq_eval} +Reset fst. +\end{coq_eval} +\begin{coq_example} +Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. +\end{coq_example} +Notice that reduction is different from regular {\tt let ... in ...} +construction since it happens only if {\term$_0$} is in constructor +form. Otherwise, the reduction is blocked. + +The pretty-printing of a definition by matching on a +irrefutable pattern can either be done using {\tt match} or the {\tt +let} construction (see Section~\ref{printing-options}). + +If {\term} inhabits an inductive type with one constructor {\tt C}, +we have an equivalence between + +{\tt let ({\ident}$_1$,\ldots,{\ident}$_n$) \zeroone{\ifitem} := {\term} in {\term}'} + +\noindent and + +{\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end} + + +\subsubsection{Second destructuring {\tt let} syntax\index{let '... in@\texttt{let '... in}}} + +Another destructuring {\tt let} syntax is available for inductive types with +one constructor by giving an arbitrary pattern instead of just a tuple +for all the arguments. For example, the preceding example can be written: +\begin{coq_eval} +Reset fst. +\end{coq_eval} +\begin{coq_example} +Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. +\end{coq_example} + +This is useful to match deeper inside tuples and also to use notations +for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary +patterns to do the deconstruction. For example: + +\begin{coq_example} +Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := + let '((a,b), (c, d)) := x in (a,b,c,d). +Notation " x 'With' p " := (exist _ x p) (at level 20). +Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := + let 'x With p := t in x. +\end{coq_example} + +When printing definitions which are written using this construct it +takes precedence over {\tt let} printing directives for the datatype +under consideration (see Section~\ref{printing-options}). + +\subsection{Controlling pretty-printing of {\tt match} expressions +\label{printing-options}} + +The following commands give some control over the pretty-printing of +{\tt match} expressions. + +\subsubsection{Printing nested patterns +\label{SetPrintingMatching} +\optindex{Printing Matching}} + +The Calculus of Inductive Constructions knows pattern-matching only +over simple patterns. It is however convenient to re-factorize nested +pattern-matching into a single pattern-matching over a nested pattern. +{\Coq}'s printer try to do such limited re-factorization. + +\begin{quote} +{\tt Set Printing Matching.} +\end{quote} +This tells {\Coq} to try to use nested patterns. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Matching.} +\end{quote} +This tells {\Coq} to print only simple pattern-matching problems in +the same way as the {\Coq} kernel handles them. + +\begin{quote} +{\tt Test Printing Matching.} +\end{quote} +This tells if the printing matching mode is on or off. The default is +on. + +\subsubsection{Factorization of clauses with same right-hand side} +\label{SetPrintingFactorizableMatchPatterns} +\optindex{Printing Factorizable Match Patterns} + +When several patterns share the same right-hand side, it is +additionally possible to share the clauses using disjunctive patterns. +Assuming that the printing matching mode is on, whether {\Coq}'s +printer shall try to do this kind of factorization is governed by the +following commands: + +\begin{quote} +{\tt Set Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer not to try to use disjunctive patterns. + +\begin{quote} +{\tt Test Printing Factorizable Match Patterns.} +\end{quote} +This tells if the factorization of clauses with same right-hand side is +on or off. + +\subsubsection{Use of a default clause} +\label{SetPrintingAllowDefaultClause} +\optindex{Printing Allow Default Clause} + +When several patterns share the same right-hand side which do not +depend on the arguments of the patterns, yet an extra factorization is +possible: the disjunction of patterns can be replaced with a ``{\tt + \_}'' default clause. Assuming that the printing matching mode and +the factorization mode are on, whether {\Coq}'s printer shall try to +use a default clause is governed by the following commands: + +\begin{quote} +{\tt Set Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer to use a default clause when relevant. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer not to use a default clause. + +\begin{quote} +{\tt Test Printing Allow Default Clause.} +\end{quote} +This tells if the use of a default clause is allowed. + +\subsubsection{Printing of wildcard pattern +\optindex{Printing Wildcard}} + +Some variables in a pattern may not occur in the right-hand side of +the pattern-matching clause. There are options to control the +display of these variables. + +\begin{quote} +{\tt Set Printing Wildcard.} +\end{quote} +The variables having no occurrences in the right-hand side of the +pattern-matching clause are just printed using the wildcard symbol +``{\tt \_}''. + +\begin{quote} +{\tt Unset Printing Wildcard.} +\end{quote} +The variables, even useless, are printed using their usual name. But some +non dependent variables have no name. These ones are still printed +using a ``{\tt \_}''. + +\begin{quote} +{\tt Test Printing Wildcard.} +\end{quote} +This tells if the wildcard printing mode is on or off. The default is +to print wildcard for useless variables. + +\subsubsection{Printing of the elimination predicate +\optindex{Printing Synth}} + +In most of the cases, the type of the result of a matched term is +mechanically synthesizable. Especially, if the result type does not +depend of the matched term. + +\begin{quote} +{\tt Set Printing Synth.} +\end{quote} +The result type is not printed when {\Coq} knows that it can +re-synthesize it. + +\begin{quote} +{\tt Unset Printing Synth.} +\end{quote} +This forces the result type to be always printed. + +\begin{quote} +{\tt Test Printing Synth.} +\end{quote} +This tells if the non-printing of synthesizable types is on or off. +The default is to not print synthesizable types. + +\subsubsection{Printing matching on irrefutable pattern +\label{AddPrintingLet} +\comindex{Add Printing Let {\ident}} +\comindex{Remove Printing Let {\ident}} +\comindex{Test Printing Let for {\ident}} +\comindex{Print Table Printing Let}} + +If an inductive type has just one constructor, +pattern-matching can be written using the first destructuring let syntax. + +\begin{quote} +{\tt Add Printing Let {\ident}.} +\end{quote} +This adds {\ident} to the list of inductive types for which +pattern-matching is written using a {\tt let} expression. + +\begin{quote} +{\tt Remove Printing Let {\ident}.} +\end{quote} +This removes {\ident} from this list. Note that removing an inductive +type from this list has an impact only for pattern-matching written using +\texttt{match}. Pattern-matching explicitly written using a destructuring +let are not impacted. + +\begin{quote} +{\tt Test Printing Let for {\ident}.} +\end{quote} +This tells if {\ident} belongs to the list. + +\begin{quote} +{\tt Print Table Printing Let.} +\end{quote} +This prints the list of inductive types for which pattern-matching is +written using a {\tt let} expression. + +The list of inductive types for which pattern-matching is written +using a {\tt let} expression is managed synchronously. This means that +it is sensible to the command {\tt Reset}. + +\subsubsection{Printing matching on booleans +\comindex{Add Printing If {\ident}} +\comindex{Remove Printing If {\ident}} +\comindex{Test Printing If for {\ident}} +\comindex{Print Table Printing If}} + +If an inductive type is isomorphic to the boolean type, +pattern-matching can be written using {\tt if} ... {\tt then} ... {\tt + else} ... + +\begin{quote} +{\tt Add Printing If {\ident}.} +\end{quote} +This adds {\ident} to the list of inductive types for which +pattern-matching is written using an {\tt if} expression. + +\begin{quote} +{\tt Remove Printing If {\ident}.} +\end{quote} +This removes {\ident} from this list. + +\begin{quote} +{\tt Test Printing If for {\ident}.} +\end{quote} +This tells if {\ident} belongs to the list. + +\begin{quote} +{\tt Print Table Printing If.} +\end{quote} +This prints the list of inductive types for which pattern-matching is +written using an {\tt if} expression. + +The list of inductive types for which pattern-matching is written +using an {\tt if} expression is managed synchronously. This means that +it is sensible to the command {\tt Reset}. + +\subsubsection{Example} + +This example emphasizes what the printing options offer. + +\begin{coq_example} +Definition snd (A B:Set) (H:A * B) := match H with + | pair x y => y + end. +Test Printing Let for prod. +Print snd. +Remove Printing Let prod. +Unset Printing Synth. +Unset Printing Wildcard. +Print snd. +\end{coq_example} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\subsection{Printing \mbox{\tt match} templates} + +The {\tt Show Match} vernacular command prints a {\tt match} template for +a given type. See Section~\ref{Show}. + +% \subsection{Still not dead old notations} + +% The following variant of {\tt match} is inherited from older version +% of {\Coq}. + +% \medskip +% \begin{tabular}{lcl} +% {\term} & ::= & {\annotation} {\tt Match} {\term} {\tt with} {\terms} {\tt end}\\ +% \end{tabular} +% \medskip + +% This syntax is a macro generating a combination of {\tt match} with {\tt +% Fix} implementing a combinator for primitive recursion equivalent to +% the {\tt Match} construction of \Coq\ V5.8. It is provided only for +% sake of compatibility with \Coq\ V5.8. It is recommended to avoid it. +% (see Section~\ref{Matchexpr}). + +% There is also a notation \texttt{Case} that is the +% ancestor of \texttt{match}. Again, it is still in the code for +% compatibility with old versions but the user should not use it. + +% Explained in RefMan-gal.tex +%% \section{Forced type} + +%% In some cases, one may wish to assign a particular type to a term. The +%% syntax to force the type of a term is the following: + +%% \medskip +%% \begin{tabular}{lcl} +%% {\term} & ++= & {\term} {\tt :} {\term}\\ +%% \end{tabular} +%% \medskip + +%% It forces the first term to be of type the second term. The +%% type must be compatible with +%% the term. More precisely it must be either a type convertible to +%% the automatically inferred type (see Chapter~\ref{Cic}) or a type +%% coercible to it, (see \ref{Coercions}). When the type of a +%% whole expression is forced, it is usually not necessary to give the types of +%% the variables involved in the term. + +%% Example: + +%% \begin{coq_example} +%% Definition ID := forall X:Set, X -> X. +%% Definition id := (fun X x => x):ID. +%% Check id. +%% \end{coq_example} + +\section{Advanced recursive functions} + +The following \emph{experimental} command is available +when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: +\begin{center} + \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + \{decrease\_annot\} : type$_0$ := \term$_0$} + \comindex{Function} + \label{Function} +\end{center} +This command can be seen as a generalization of {\tt Fixpoint}. It is actually +a wrapper for several ways of defining a function \emph{and other useful + related objects}, namely: an induction principle that reflects the +recursive structure of the function (see \ref{FunInduction}) and its +fixpoint equality. + The meaning of this +declaration is to define a function {\it ident}, similarly to {\tt + Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be +given (unless the function is not recursive), but it might not +necessarily be \emph{structurally} decreasing. The point of the {\tt + \{\}} annotation is to name the decreasing argument \emph{and} to +describe which kind of decreasing criteria must be used to ensure +termination of recursive calls. + +The {\tt Function} construction also enjoys the {\tt with} extension +to define mutually recursive definitions. However, this feature does +not work for non structurally recursive functions. % VRAI?? + +See the documentation of {\tt functional induction} +(see Section~\ref{FunInduction}) and {\tt Functional Scheme} +(see Section~\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the +induction principle to easily reason about the function. + +\noindent {\bf Remark: } To obtain the right principle, it is better +to put rigid parameters of the function as first arguments. For +example it is better to define plus like this: + +\begin{coq_example*} +Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. +\end{coq_example*} +\noindent than like this: +\begin{coq_eval} +Reset plus. +\end{coq_eval} +\begin{coq_example*} +Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. +\end{coq_example*} + +\paragraph[Limitations]{Limitations\label{sec:Function-limitations}} +\term$_0$ must be built as a \emph{pure pattern-matching tree} +(\texttt{match...with}) with applications only \emph{at the end} of +each branch. + +Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~: +\begin{coq_eval} +Require List. +\end{coq_eval} +\begin{coq_example*} +Fail Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). +\end{coq_example*} + +For now dependent cases are not treated for non structurally terminating functions. + + + +\begin{ErrMsgs} +\item \errindex{The recursive argument must be specified} +\item \errindex{No argument name \ident} +\item \errindex{Cannot use mutual definition with well-founded + recursion or measure} + +\item \errindex{Cannot define graph for \ident\dots} (warning) + + The generation of the graph relation \texttt{(R\_\ident)} used to + compute the induction scheme of \ident\ raised a typing error. Only + the ident is defined; the induction scheme will not be generated. + + This error happens generally when: + + \begin{itemize} + \item the definition uses pattern matching on dependent types, which + \texttt{Function} cannot deal with yet. + \item the definition is not a \emph{pattern-matching tree} as + explained above. + \end{itemize} + +\item \errindex{Cannot define principle(s) for \ident\dots} (warning) + + The generation of the graph relation \texttt{(R\_\ident)} succeeded + but the induction principle could not be built. Only the ident is + defined. Please report. + +\item \errindex{Cannot build functional inversion principle} (warning) + + \texttt{functional inversion} will not be available for the + function. +\end{ErrMsgs} + + +\SeeAlso{\ref{FunScheme}, \ref{FunScheme-examples}, \ref{FunInduction}} + +Depending on the {\tt \{$\ldots$\}} annotation, different definition +mechanisms are used by {\tt Function}. More precise description +given below. + +\begin{Variants} +\item \texttt{ Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + : type$_0$ := \term$_0$} + + Defines the not recursive function \ident\ as if declared with + \texttt{Definition}. Moreover the following are defined: + + \begin{itemize} + \item {\tt\ident\_rect}, {\tt\ident\_rec} and {\tt\ident\_ind}, + which reflect the pattern matching structure of \term$_0$ (see the + documentation of {\tt Inductive} \ref{Inductive}); + \item The inductive \texttt{R\_\ident} corresponding to the graph of + \ident\ (silently); + \item \texttt{\ident\_complete} and \texttt{\ident\_correct} which are + inversion information linking the function and its graph. + \end{itemize} +\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$} + + Defines the structural recursive function \ident\ as if declared + with \texttt{Fixpoint}. Moreover the following are defined: + + \begin{itemize} + \item The same objects as above; + \item The fixpoint equation of \ident: \texttt{\ident\_equation}. + \end{itemize} + +\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt + \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := + \term$_0$} +\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$} + +Defines a recursive function by well founded recursion. \textbf{The +module \texttt{Recdef} of the standard library must be loaded for this +feature}. The {\tt \{\}} annotation is mandatory and must be one of +the following: +\begin{itemize} +\item {\tt \{measure} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ + being the decreasing argument and \term$_1$ being a function + from type of \ident$_0$ to \texttt{nat} for which value on the + decreasing argument decreases (for the {\tt lt} order on {\tt + nat}) at each recursive call of \term$_0$. Parameters of the + function are bound in \term$_0$; +\item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being + the decreasing argument and \term$_1$ an ordering relation on + the type of \ident$_0$ (i.e. of type T$_{\ident_0}$ + $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which + the decreasing argument decreases at each recursive call of + \term$_0$. The order must be well founded. Parameters of the + function are bound in \term$_0$. +\end{itemize} + +Depending on the annotation, the user is left with some proof +obligations that will be used to define the function. These proofs +are: proofs that each recursive call is actually decreasing with +respect to the given criteria, and (if the criteria is \texttt{wf}) a +proof that the ordering relation is well founded. + +%Completer sur measure et wf + +Once proof obligations are discharged, the following objects are +defined: + +\begin{itemize} +\item The same objects as with the \texttt{struct}; +\item The lemma \texttt{\ident\_tcc} which collects all proof + obligations in one property; +\item The lemmas \texttt{\ident\_terminate} and \texttt{\ident\_F} + which is needed to be inlined during extraction of \ident. +\end{itemize} + + + +%Complete!! +The way this recursive function is defined is the subject of several +papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles Barthe, +Julien Forest, David Pichardie, and Vlad Rusu on the other hand. + +%Exemples ok ici + +\bigskip + +\noindent {\bf Remark: } Proof obligations are presented as several +subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independent which means that in order to +% abort them you will have to abort each separately. + + + +%The decreasing argument cannot be dependent of another?? + +%Exemples faux ici +\end{Variants} + + +\section{Section mechanism +\index{Sections} +\label{Section}} + +The sectioning mechanism can be used to to organize a proof in +structured sections. Then local declarations become available (see +Section~\ref{Basic-definitions}). + +\subsection{\tt Section {\ident}\comindex{Section}} + +This command is used to open a section named {\ident}. + +%% Discontinued ? +%% \begin{Variants} +%% \comindex{Chapter} +%% \item{\tt Chapter {\ident}}\\ +%% Same as {\tt Section {\ident}} +%% \end{Variants} + +\subsection{\tt End {\ident} +\comindex{End}} + +This command closes the section named {\ident}. After closing of the +section, the local declarations (variables and local definitions) get +{\em discharged}, meaning that they stop being visible and that all +global objects defined in the section are generalized with respect to +the variables and local definitions they each depended on in the +section. + + +Here is an example : +\begin{coq_example} +Section s1. +Variables x y : nat. +Let y' := y. +Definition x' := S x. +Definition x'' := x' + y'. +Print x'. +End s1. +Print x'. +Print x''. +\end{coq_example} +Notice the difference between the value of {\tt x'} and {\tt x''} +inside section {\tt s1} and outside. + +\begin{ErrMsgs} +\item \errindex{This is not the last opened section} +\end{ErrMsgs} + +\begin{Remarks} +\item Most commands, like {\tt Hint}, {\tt Notation}, option management, ... +which appear inside a section are canceled when the +section is closed. +% see Section~\ref{LongNames} +%\item Usually all identifiers must be distinct. +%However, a name already used in a closed section (see \ref{Section}) +%can be reused. In this case, the old name is no longer accessible. + +% Obsolète +%\item A module implicitly open a section. Be careful not to name a +%module with an identifier already used in the module (see \ref{compiled}). +\end{Remarks} + +\input{RefMan-mod.v} + +\section{Libraries and qualified names} + +\subsection{Names of libraries +\label{Libraries} +\index{Libraries}} + +The theories developed in {\Coq} are stored in {\em library files} +which are hierarchically classified into {\em libraries} and {\em + sublibraries}. To express this hierarchy, library names are +represented by qualified identifiers {\qualid}, i.e. as list of +identifiers separated by dots (see Section~\ref{qualid}). For +instance, the library file {\tt Mult} of the standard {\Coq} library +{\tt Arith} is named {\tt Coq.Arith.Mult}. The identifier that starts +the name of a library is called a {\em library root}. All library +files of the standard library of {\Coq} have the reserved root {\tt Coq} +but library file names based on other roots can be obtained by using +{\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options +{\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an +interactive {\Coq} session starts, a library of root {\tt Top} is +started, unless option {\tt -top} is set (see +Section~\ref{coqoptions}). + +\subsection{Qualified names +\label{LongNames} +\index{Qualified identifiers} +\index{Absolute names}} + +Library files are modules which possibly contain submodules which +eventually contain constructions (axioms, parameters, definitions, +lemmas, theorems, remarks or facts). The {\em absolute name}, or {\em +full name}, of a construction in some library file is a qualified +identifier starting with the logical name of the library file, +followed by the sequence of submodules names encapsulating the +construction and ended by the proper name of the construction. +Typically, the absolute name {\tt Coq.Init.Logic.eq} denotes Leibniz' +equality defined in the module {\tt Logic} in the sublibrary {\tt +Init} of the standard library of \Coq. + +The proper name that ends the name of a construction is the {\it short +name} (or sometimes {\it base name}) of the construction (for +instance, the short name of {\tt Coq.Init.Logic.eq} is {\tt eq}). Any +partial suffix of the absolute name is a {\em partially qualified name} +(e.g. {\tt Logic.eq} is a partially qualified name for {\tt +Coq.Init.Logic.eq}). Especially, the short name of a construction is +its shortest partially qualified name. + +{\Coq} does not accept two constructions (definition, theorem, ...) +with the same absolute name but different constructions can have the +same short name (or even same partially qualified names as soon as the +full names are different). + +Notice that the notion of absolute, partially qualified and +short names also applies to library file names. + +\paragraph{Visibility} + +{\Coq} maintains a table called {\it name table} which maps partially +qualified names of constructions to absolute names. This table is +updated by the commands {\tt Require} (see \ref{Require}), {\tt +Import} and {\tt Export} (see \ref{Import}) and also each time a new +declaration is added to the context. An absolute name is called {\it +visible} from a given short or partially qualified name when this +latter name is enough to denote it. This means that the short or +partially qualified name is mapped to the absolute name in {\Coq} name +table. Definitions flagged as {\tt Local} are only accessible with their +fully qualified name (see \ref{Definition}). + +It may happen that a visible name is hidden by the short name or a +qualified name of another construction. In this case, the name that +has been hidden must be referred to using one more level of +qualification. To ensure that a construction always remains +accessible, absolute names can never be hidden. + +Examples: +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Check 0. +Definition nat := bool. +Check 0. +Check Datatypes.nat. +Locate nat. +\end{coq_example} + +\SeeAlso Command {\tt Locate} in Section~\ref{Locate} and {\tt Locate +Library} in Section~\ref{Locate Library}. + +\subsection{Libraries and filesystem\label{loadpath}\index{Loadpath} +\index{Physical paths} \index{Logical paths}} + +Please note that the questions described here have been subject to +redesign in Coq v8.5. Former versions of Coq use the same terminology +to describe slightly different things. + +Compiled files (\texttt{.vo} and \texttt{.vio}) store sub-libraries. In +order to refer to them inside {\Coq}, a translation from file-system +names to {\Coq} names is needed. In this translation, names in the +file system are called {\em physical} paths while {\Coq} names are +contrastingly called {\em logical} names. + +A logical prefix {\tt Lib} can be associated to a physical path +\textrm{\textsl{path}} using the command line option {\tt -Q} +\textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are +recursively associated to the logical path {\tt Lib} extended with the +corresponding suffix coming from the physical path. For instance, the +folder {\tt path/fOO/Bar} maps to {\tt Lib.fOO.Bar}. Subdirectories +corresponding to invalid {\Coq} identifiers are skipped, and, by +convention, subdirectories named {\tt CVS} or {\tt \_darcs} are +skipped too. + +Thanks to this mechanism, {\texttt{.vo}} files are made available through the +logical name of the folder they are in, extended with their own basename. For +example, the name associated to the file {\tt path/fOO/Bar/File.vo} is +{\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers. +When compiling a source file, the {\texttt{.vo}} file stores its logical name, +so that an error is issued if it is loaded with the wrong loadpath afterwards. + +Some folders have a special status and are automatically put in the path. +{\Coq} commands associate automatically a logical path to files +in the repository trees rooted at the directory from where the command +is launched, \textit{coqlib}\texttt{/user-contrib/}, the directories +listed in the \verb:$COQPATH:, \verb:${XDG_DATA_HOME}/coq/: and +\verb:${XDG_DATA_DIRS}/coq/: environment variables (see +\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}) +with the same physical-to-logical translation and with an empty logical prefix. + +The command line option \texttt{-R} is a variant of \texttt{-Q} which has the +strictly same behavior regarding loadpaths, but which also makes the +corresponding \texttt{.vo} files available through their short names in a +way not unlike the {\tt Import} command (see~{\ref{Import}}). For instance, +\texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file +\texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but +allows this file to be accessed through the short names \texttt{fOO.Bar.File}, +\texttt{Bar.File} and \texttt{File}. If several files with identical base name +are present in different subdirectories of a recursive loadpath, which of +these files is found first may be system-dependent and explicit +qualification is recommended. The {\tt From} argument of the {\tt Require} +command can be used to bypass the implicit shortening by providing an absolute +root to the required file (see~\ref{Require}). + +There also exists another independent loadpath mechanism attached to {\ocaml} +object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files +as described above. The {\ocaml} loadpath is managed using the option +\texttt{-I path} (in the {\ocaml} world, there is neither a notion of logical +name prefix nor a way to access files in subdirectories of \texttt{path}). +See the command \texttt{Declare ML Module} in Section~\ref{compiled} to +understand the need of the {\ocaml} loadpath. + +See Section~\ref{coqoptions} for a more general view over the {\Coq} +command line options. + +%% \paragraph{The special case of remarks and facts} +%% +%% In contrast with definitions, lemmas, theorems, axioms and parameters, +%% the absolute name of remarks includes the segment of sections in which +%% it is defined. Concretely, if a remark {\tt R} is defined in +%% subsection {\tt S2} of section {\tt S1} in module {\tt M}, then its +%% absolute name is {\tt M.S1.S2.R}. The same for facts, except that the +%% name of the innermost section is dropped from the full name. Then, if +%% a fact {\tt F} is defined in subsection {\tt S2} of section {\tt S1} +%% in module {\tt M}, then its absolute name is {\tt M.S1.F}. + +\section{Implicit arguments +\index{Implicit arguments} +\label{Implicit Arguments}} + +An implicit argument of a function is an argument which can be +inferred from contextual knowledge. There are different kinds of +implicit arguments that can be considered implicit in different +ways. There are also various commands to control the setting or the +inference of implicit arguments. + +\subsection{The different kinds of implicit arguments} + +\subsubsection{Implicit arguments inferable from the knowledge of other +arguments of a function} + +The first kind of implicit arguments covers the arguments that are +inferable from the knowledge of the type of other arguments of the +function, or of the type of the surrounding context of the +application. Especially, such implicit arguments correspond to +parameters dependent in the type of the function. Typical implicit +arguments are the type arguments in polymorphic functions. +There are several kinds of such implicit arguments. + +\paragraph{Strict Implicit Arguments.} +An implicit argument can be either strict or non strict. An implicit +argument is said {\em strict} if, whatever the other arguments of the +function are, it is still inferable from the type of some other +argument. Technically, an implicit argument is strict if it +corresponds to a parameter which is not applied to a variable which +itself is another parameter of the function (since this parameter +may erase its arguments), not in the body of a {\tt match}, and not +itself applied or matched against patterns (since the original +form of the argument can be lost by reduction). + +For instance, the first argument of +\begin{quote} +\verb|cons: forall A:Set, A -> list A -> list A| +\end{quote} +in module {\tt List.v} is strict because {\tt list} is an inductive +type and {\tt A} will always be inferable from the type {\tt +list A} of the third argument of {\tt cons}. +On the contrary, the second argument of a term of type +\begin{quote} +\verb|forall P:nat->Prop, forall n:nat, P n -> ex nat P| +\end{quote} +is implicit but not strict, since it can only be inferred from the +type {\tt P n} of the third argument and if {\tt P} is, e.g., {\tt +fun \_ => True}, it reduces to an expression where {\tt n} does not +occur any longer. The first argument {\tt P} is implicit but not +strict either because it can only be inferred from {\tt P n} and {\tt +P} is not canonically inferable from an arbitrary {\tt n} and the +normal form of {\tt P n} (consider e.g. that {\tt n} is {\tt 0} and +the third argument has type {\tt True}, then any {\tt P} of the form +{\tt fun n => match n with 0 => True | \_ => \mbox{\em anything} end} would +be a solution of the inference problem). + +\paragraph{Contextual Implicit Arguments.} +An implicit argument can be {\em contextual} or not. An implicit +argument is said {\em contextual} if it can be inferred only from the +knowledge of the type of the context of the current expression. For +instance, the only argument of +\begin{quote} +\verb|nil : forall A:Set, list A| +\end{quote} +is contextual. Similarly, both arguments of a term of type +\begin{quote} +\verb|forall P:nat->Prop, forall n:nat, P n \/ n = 0| +\end{quote} +are contextual (moreover, {\tt n} is strict and {\tt P} is not). + +\paragraph{Reversible-Pattern Implicit Arguments.} +There is another class of implicit arguments that can be reinferred +unambiguously if all the types of the remaining arguments are +known. This is the class of implicit arguments occurring in the type +of another argument in position of reversible pattern, which means it +is at the head of an application but applied only to uninstantiated +distinct variables. Such an implicit argument is called {\em +reversible-pattern implicit argument}. A typical example is the +argument {\tt P} of {\tt nat\_rec} in +\begin{quote} +{\tt nat\_rec : forall P : nat -> Set, + P 0 -> (forall n : nat, P n -> P (S n)) -> forall x : nat, P x}. +\end{quote} +({\tt P} is reinferable by abstracting over {\tt n} in the type {\tt P n}). + +See Section~\ref{SetReversiblePatternImplicit} for the automatic declaration +of reversible-pattern implicit arguments. + +\subsubsection{Implicit arguments inferable by resolution} + +This corresponds to a class of non dependent implicit arguments that +are solved based on the structure of their type only. + +\subsection{Maximal or non maximal insertion of implicit arguments} + +In case a function is partially applied, and the next argument to be +applied is an implicit argument, two disciplines are applicable. In the +first case, the function is considered to have no arguments furtherly: +one says that the implicit argument is not maximally inserted. In +the second case, the function is considered to be implicitly applied +to the implicit arguments it is waiting for: one says that the +implicit argument is maximally inserted. + +Each implicit argument can be declared to have to be inserted +maximally or non maximally. This can be governed argument per argument +by the command {\tt Implicit Arguments} (see~\ref{ImplicitArguments}) +or globally by the command {\tt Set Maximal Implicit Insertion} +(see~\ref{SetMaximalImplicitInsertion}). See also +Section~\ref{PrintImplicit}. + +\subsection{Casual use of implicit arguments} + +In a given expression, if it is clear that some argument of a function +can be inferred from the type of the other arguments, the user can +force the given argument to be guessed by replacing it by ``{\tt \_}''. If +possible, the correct argument will be automatically generated. + +\begin{ErrMsgs} + +\item \errindex{Cannot infer a term for this placeholder} + + {\Coq} was not able to deduce an instantiation of a ``{\tt \_}''. + +\end{ErrMsgs} + +\subsection{Declaration of implicit arguments +\comindex{Arguments}} +\label{ImplicitArguments} + +In case one wants that some arguments of a given object (constant, +inductive types, constructors, assumptions, local or not) are always +inferred by Coq, one may declare once and for all which are the expected +implicit arguments of this object. There are two ways to do this, +a priori and a posteriori. + +\subsubsection{Implicit Argument Binders} + +In the first setting, one wants to explicitly give the implicit +arguments of a declared object as part of its definition. To do this, one has +to surround the bindings of implicit arguments by curly braces: +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Definition id {A : Type} (x : A) : A := x. +\end{coq_example} + +This automatically declares the argument {\tt A} of {\tt id} as a +maximally inserted implicit argument. One can then do as-if the argument +was absent in every situation but still be able to specify it if needed: +\begin{coq_example} +Definition compose {A B C} (g : B -> C) (f : A -> B) := + fun x => g (f x). +Goal forall A, compose id id = id (A:=A). +\end{coq_example} + +The syntax is supported in all top-level definitions: {\tt Definition}, +{\tt Fixpoint}, {\tt Lemma} and so on. For (co-)inductive datatype +declarations, the semantics are the following: an inductive parameter +declared as an implicit argument need not be repeated in the inductive +definition but will become implicit for the constructors of the +inductive only, not the inductive type itself. For example: + +\begin{coq_example} +Inductive list {A : Type} : Type := +| nil : list +| cons : A -> list -> list. +Print list. +\end{coq_example} + +One can always specify the parameter if it is not uniform using the +usual implicit arguments disambiguation syntax. + +\subsubsection{Declaring Implicit Arguments} + +To set implicit arguments a posteriori, one can use the +command: +\begin{quote} +\tt Arguments {\qualid} \nelist{\possiblybracketedident}{} +\end{quote} +where the list of {\possiblybracketedident} is a prefix of the list of arguments +of {\qualid} where the ones to be declared implicit are surrounded by square +brackets and the ones to be declared as maximally inserted implicits are +surrounded by curly braces. + +After the above declaration is issued, implicit arguments can just (and +have to) be skipped in any expression involving an application of +{\qualid}. + +Implicit arguments can be cleared with the following syntax: + +\begin{quote} +{\tt Arguments {\qualid} : clear implicits +\comindex{Arguments}} +\end{quote} + +\begin{Variants} +\item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{} +\comindex{Global Arguments}} + +Tell to recompute the implicit arguments of {\qualid} after ending of +the current section if any, enforcing the implicit arguments known +from inside the section to be the ones declared by the command. + +\item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{} +\comindex{Local Arguments}} + +When in a module, tell not to activate the implicit arguments of +{\qualid} declared by this command to contexts that require the +module. + +\item {\tt \zeroone{Global {\sl |} Local} Arguments {\qualid} \sequence{\nelist{\possiblybracketedident}{}}{,}} + +For names of constants, inductive types, constructors, lemmas which +can only be applied to a fixed number of arguments (this excludes for +instance constants whose type is polymorphic), multiple +implicit arguments decflarations can be given. +Depending on the number of arguments {\qualid} is applied +to in practice, the longest applicable list of implicit arguments is +used to select which implicit arguments are inserted. + +For printing, the omitted arguments are the ones of the longest list +of implicit arguments of the sequence. + +\end{Variants} + +\Example +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Inductive list (A:Type) : Type := + | nil : list A + | cons : A -> list A -> list A. +\end{coq_example*} +\begin{coq_example} +Check (cons nat 3 (nil nat)). +Arguments cons [A] _ _. +Arguments nil [A]. +Check (cons 3 nil). +Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := + match l with nil => nil | cons a t => cons (f a) (map A B f t) end. +Fixpoint length (A:Type) (l:list A) : nat := + match l with nil => 0 | cons _ m => S (length A m) end. +Arguments map [A B] f l. +Arguments length {A} l. (* A has to be maximally inserted *) +Check (fun l:list (list nat) => map length l). +Arguments map [A B] f l, [A] B f l, A B f l. +Check (fun l => map length l = map (list nat) nat length l). +\end{coq_example} + +\Rem To know which are the implicit arguments of an object, use the command +{\tt Print Implicit} (see \ref{PrintImplicit}). + +\subsection{Automatic declaration of implicit arguments} + +{\Coq} can also automatically detect what are the implicit arguments +of a defined object. The command is just +\begin{quote} +{\tt Arguments {\qualid} : default implicits +\comindex{Arguments}} +\end{quote} +The auto-detection is governed by options telling if strict, +contextual, or reversible-pattern implicit arguments must be +considered or not (see +Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversiblePatternImplicit} +and also~\ref{SetMaximalImplicitInsertion}). + +\begin{Variants} +\item {\tt Global Arguments {\qualid} : default implicits +\comindex{Global Arguments}} + +Tell to recompute the implicit arguments of {\qualid} after ending of +the current section if any. + +\item {\tt Local Arguments {\qualid} : default implicits +\comindex{Local Arguments}} + +When in a module, tell not to activate the implicit arguments of +{\qualid} computed by this declaration to contexts that requires the +module. + +\end{Variants} + +\Example +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. +\end{coq_example*} +\begin{coq_example} +Arguments cons : default implicits. +Print Implicit cons. +Arguments nil : default implicits. +Print Implicit nil. +Set Contextual Implicit. +Arguments nil : default implicits. +Print Implicit nil. +\end{coq_example} + +The computation of implicit arguments takes account of the +unfolding of constants. For instance, the variable {\tt p} below has +type {\tt (Transitivity R)} which is reducible to {\tt forall x,y:U, R x +y -> forall z:U, R y z -> R x z}. As the variables {\tt x}, {\tt y} and +{\tt z} appear strictly in body of the type, they are implicit. + +\begin{coq_example*} +Variable X : Type. +Definition Relation := X -> X -> Prop. +Definition Transitivity (R:Relation) := + forall x y:X, R x y -> forall z:X, R y z -> R x z. +Variables (R : Relation) (p : Transitivity R). +Arguments p : default implicits. +\end{coq_example*} +\begin{coq_example} +Print p. +Print Implicit p. +\end{coq_example} +\begin{coq_example*} +Variables (a b c : X) (r1 : R a b) (r2 : R b c). +\end{coq_example*} +\begin{coq_example} +Check (p r1 r2). +\end{coq_example} + +\subsection{Mode for automatic declaration of implicit arguments +\label{Auto-implicit} +\optindex{Implicit Arguments}} + +In case one wants to systematically declare implicit the arguments +detectable as such, one may switch to the automatic declaration of +implicit arguments mode by using the command +\begin{quote} +\tt Set Implicit Arguments. +\end{quote} +Conversely, one may unset the mode by using {\tt Unset Implicit +Arguments}. The mode is off by default. Auto-detection of implicit +arguments is governed by options controlling whether strict and +contextual implicit arguments have to be considered or not. + +\subsection{Controlling strict implicit arguments +\optindex{Strict Implicit} +\label{SetStrictImplicit}} + +When the mode for automatic declaration of implicit arguments is on, +the default is to automatically set implicit only the strict implicit +arguments plus, for historical reasons, a small subset of the non +strict implicit arguments. To relax this constraint and to +set implicit all non strict implicit arguments by default, use the command +\begin{quote} +\tt Unset Strict Implicit. +\end{quote} +Conversely, use the command {\tt Set Strict Implicit} to +restore the original mode that declares implicit only the strict implicit arguments plus a small subset of the non strict implicit arguments. + +In the other way round, to capture exactly the strict implicit arguments and no more than the strict implicit arguments, use the command: +\optindex{Strongly Strict Implicit} +\begin{quote} +\tt Set Strongly Strict Implicit. +\end{quote} +Conversely, use the command {\tt Unset Strongly Strict Implicit} to +let the option ``{\tt Strict Implicit}'' decide what to do. + +\Rem In versions of {\Coq} prior to version 8.0, the default was to +declare the strict implicit arguments as implicit. + +\subsection{Controlling contextual implicit arguments +\optindex{Contextual Implicit} +\label{SetContextualImplicit}} + +By default, {\Coq} does not automatically set implicit the contextual +implicit arguments. To tell {\Coq} to infer also contextual implicit +argument, use command +\begin{quote} +\tt Set Contextual Implicit. +\end{quote} +Conversely, use command {\tt Unset Contextual Implicit} to +unset the contextual implicit mode. + +\subsection{Controlling reversible-pattern implicit arguments +\optindex{Reversible Pattern Implicit} +\label{SetReversiblePatternImplicit}} + +By default, {\Coq} does not automatically set implicit the reversible-pattern +implicit arguments. To tell {\Coq} to infer also reversible-pattern implicit +argument, use command +\begin{quote} +\tt Set Reversible Pattern Implicit. +\end{quote} +Conversely, use command {\tt Unset Reversible Pattern Implicit} to +unset the reversible-pattern implicit mode. + +\subsection{Controlling the insertion of implicit arguments not followed by explicit arguments +\optindex{Maximal Implicit Insertion} +\label{SetMaximalImplicitInsertion}} + +Implicit arguments can be declared to be automatically inserted when a +function is partially applied and the next argument of the function is +an implicit one. In case the implicit arguments are automatically +declared (with the command {\tt Set Implicit Arguments}), the command +\begin{quote} +\tt Set Maximal Implicit Insertion. +\end{quote} +is used to tell to declare the implicit arguments with a maximal +insertion status. By default, automatically declared implicit +arguments are not declared to be insertable maximally. To restore the +default mode for maximal insertion, use command {\tt Unset Maximal +Implicit Insertion}. + +\subsection{Explicit applications +\index{Explicitly given implicit arguments} +\label{Implicits-explicitation} +\index{qualid@{\qualid}} \index{\symbol{64}}} + +In presence of non strict or contextual argument, or in presence of +partial applications, the synthesis of implicit arguments may fail, so +one may have to give explicitly certain implicit arguments of an +application. The syntax for this is {\tt (\ident:=\term)} where {\ident} +is the name of the implicit argument and {\term} is its corresponding +explicit term. Alternatively, one can locally deactivate the hiding of +implicit arguments of a function by using the notation +{\tt @{\qualid}~{\term}$_1$..{\term}$_n$}. This syntax extension is +given Figure~\ref{fig:explicitations}. +\begin{figure} +\begin{centerframe} +\begin{tabular}{lcl} +{\term} & ++= & @ {\qualid} \nelist{\term}{}\\ +& $|$ & @ {\qualid}\\ +& $|$ & {\qualid} \nelist{\textrm{\textsl{argument}}}{}\\ +\\ +{\textrm{\textsl{argument}}} & ::= & {\term} \\ +& $|$ & {\tt ({\ident}:={\term})}\\ +\end{tabular} +\end{centerframe} +\caption{Syntax for explicitly giving implicit arguments} +\label{fig:explicitations} +\end{figure} + +\noindent {\bf Example (continued): } +\begin{coq_example} +Check (p r1 (z:=c)). +Check (p (x:=a) (y:=b) r1 (z:=c) r2). +\end{coq_example} + +\subsection{Renaming implicit arguments +\comindex{Arguments} +} + +Implicit arguments names can be redefined using the following syntax: +\begin{quote} +{\tt Arguments {\qualid} \nelist{\name}{} : rename} +\end{quote} + +With the {\tt assert} flag, {\tt Arguments} can be used to assert +that a given object has the expected number of arguments and that +these arguments are named as expected. + +\noindent {\bf Example (continued): } +\begin{coq_example} +Arguments p [s t] _ [u] _: rename. +Check (p r1 (u:=c)). +Check (p (s:=a) (t:=b) r1 (u:=c) r2). +Fail Arguments p [s t] _ [w] _ : assert. +\end{coq_example} + + +\subsection{Displaying what the implicit arguments are +\comindex{Print Implicit} +\label{PrintImplicit}} + +To display the implicit arguments associated to an object, and to know +if each of them is to be used maximally or not, use the command +\begin{quote} +\tt Print Implicit {\qualid}. +\end{quote} + +\subsection{Explicit displaying of implicit arguments for pretty-printing +\optindex{Printing Implicit} +\optindex{Printing Implicit Defensive}} + +By default the basic pretty-printing rules hide the inferable implicit +arguments of an application. To force printing all implicit arguments, +use command +\begin{quote} +{\tt Set Printing Implicit.} +\end{quote} +Conversely, to restore the hiding of implicit arguments, use command +\begin{quote} +{\tt Unset Printing Implicit.} +\end{quote} + +By default the basic pretty-printing rules display the implicit arguments that are not detected as strict implicit arguments. This ``defensive'' mode can quickly make the display cumbersome so this can be deactivated by using the command +\begin{quote} +{\tt Unset Printing Implicit Defensive.} +\end{quote} +Conversely, to force the display of non strict arguments, use command +\begin{quote} +{\tt Set Printing Implicit Defensive.} +\end{quote} + +\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}. + +\subsection{Interaction with subtyping} + +When an implicit argument can be inferred from the type of more than +one of the other arguments, then only the type of the first of these +arguments is taken into account, and not an upper type of all of +them. As a consequence, the inference of the implicit argument of +``='' fails in +\begin{coq_example*} +Fail Check nat = Prop. +\end{coq_example*} + +but succeeds in +\begin{coq_example*} +Check Prop = nat. +\end{coq_example*} + +\subsection{Deactivation of implicit arguments for parsing} +\optindex{Parsing Explicit} + +Use of implicit arguments can be deactivated by issuing the command: +\begin{quote} +{\tt Set Parsing Explicit.} +\end{quote} + +In this case, all arguments of constants, inductive types, +constructors, etc, including the arguments declared as implicit, have +to be given as if none arguments were implicit. By symmetry, this also +affects printing. To restore parsing and normal printing of implicit +arguments, use: +\begin{quote} +{\tt Unset Parsing Explicit.} +\end{quote} + +\subsection{Canonical structures +\comindex{Canonical Structure}} + +A canonical structure is an instance of a record/structure type that +can be used to solve unification problems involving a projection +applied to an unknown structure instance (an implicit argument) and +a value. The complete documentation of canonical structures can be found +in Chapter~\ref{CS-full}, here only a simple example is given. + +Assume that {\qualid} denotes an object $(Build\_struc~ c_1~ \ldots~ c_n)$ in +the +structure {\em struct} of which the fields are $x_1$, ..., +$x_n$. Assume that {\qualid} is declared as a canonical structure +using the command +\begin{quote} +{\tt Canonical Structure {\qualid}.} +\end{quote} +Then, each time an equation of the form $(x_i~ +\_)=_{\beta\delta\iota\zeta}c_i$ has to be solved during the +type-checking process, {\qualid} is used as a solution. Otherwise +said, {\qualid} is canonically used to extend the field $c_i$ into a +complete structure built on $c_i$. + +Canonical structures are particularly useful when mixed with +coercions and strict implicit arguments. Here is an example. +\begin{coq_example*} +Require Import Relations. +Require Import EqNat. +Set Implicit Arguments. +Unset Strict Implicit. +Structure Setoid : Type := + {Carrier :> Set; + Equal : relation Carrier; + Prf_equiv : equivalence Carrier Equal}. +Definition is_law (A B:Setoid) (f:A -> B) := + forall x y:A, Equal x y -> Equal (f x) (f y). +Axiom eq_nat_equiv : equivalence nat eq_nat. +Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. +Canonical Structure nat_setoid. +\end{coq_example*} + +Thanks to \texttt{nat\_setoid} declared as canonical, the implicit +arguments {\tt A} and {\tt B} can be synthesized in the next statement. +\begin{coq_example} +Lemma is_law_S : is_law S. +\end{coq_example} + +\Rem If a same field occurs in several canonical structure, then +only the structure declared first as canonical is considered. + +\begin{Variants} +\item {\tt Canonical Structure {\ident} := {\term} : {\type}.}\\ + {\tt Canonical Structure {\ident} := {\term}.}\\ + {\tt Canonical Structure {\ident} : {\type} := {\term}.} + +These are equivalent to a regular definition of {\ident} followed by +the declaration + +{\tt Canonical Structure {\ident}}. +\end{Variants} + +\SeeAlso more examples in user contribution \texttt{category} +(\texttt{Rocq/ALGEBRA}). + +\subsubsection{Print Canonical Projections. +\comindex{Print Canonical Projections}} + +This displays the list of global names that are components of some +canonical structure. For each of them, the canonical structure of +which it is a projection is indicated. For instance, the above example +gives the following output: + +\begin{coq_example} +Print Canonical Projections. +\end{coq_example} + +\subsection{Implicit types of variables} +\comindex{Implicit Types} + +It is possible to bind variable names to a given type (e.g. in a +development using arithmetic, it may be convenient to bind the names +{\tt n} or {\tt m} to the type {\tt nat} of natural numbers). The +command for that is +\begin{quote} +\tt Implicit Types \nelist{\ident}{} : {\type} +\end{quote} +The effect of the command is to automatically set the type of bound +variables starting with {\ident} (either {\ident} itself or +{\ident} followed by one or more single quotes, underscore or digits) +to be {\type} (unless the bound variable is already declared with an +explicit type in which case, this latter type is considered). + +\Example +\begin{coq_example} +Require Import List. +Implicit Types m n : nat. +Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m. +intros m n. +Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. +\end{coq_example} + +\begin{Variants} +\item {\tt Implicit Type {\ident} : {\type}}\\ +This is useful for declaring the implicit type of a single variable. +\item + {\tt Implicit Types\,% +(\,{\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 implicit types with different specifications. +\end{Variants} + + +\subsection{Implicit generalization +\label{implicit-generalization} +\comindex{Generalizable Variables}} +% \textquoteleft since \` doesn't do what we want +\index{0genimpl@{\textquoteleft\{\ldots\}}} +\index{0genexpl@{\textquoteleft(\ldots)}} + +Implicit generalization is an automatic elaboration of a statement with +free variables into a closed statement where these variables are +quantified explicitly. Implicit generalization is done inside binders +starting with a \texttt{\`{}} and terms delimited by \texttt{\`{}\{ \}} and +\texttt{\`{}( )}, always introducing maximally inserted implicit arguments for +the generalized variables. Inside implicit generalization +delimiters, free variables in the current context are automatically +quantified using a product or a lambda abstraction to generate a closed +term. In the following statement for example, the variables \texttt{n} +and \texttt{m} are automatically generalized and become explicit +arguments of the lemma as we are using \texttt{\`{}( )}: + +\begin{coq_example} +Generalizable All Variables. +Lemma nat_comm : `(n = n + 0). +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} +One can control the set of generalizable identifiers with the +\texttt{Generalizable} vernacular command to avoid unexpected +generalizations when mistyping identifiers. There are three variants of +the command: + +\begin{quote} +{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} +\end{quote} + +\begin{Variants} +\item {\tt Generalizable All Variables.} All variables are candidate for + generalization if they appear free in the context under a + generalization delimiter. This may result in confusing errors in + case of typos. In such cases, the context will probably contain some + unexpected generalized variable. + +\item {\tt Generalizable No Variables.} Disable implicit generalization + entirely. This is the default behavior. + +\item {\tt Generalizable Variable(s)? {\ident$_1$ \ident$_n$}.} + Allow generalization of the given identifiers only. Calling this + command multiple times adds to the allowed identifiers. + +\item {\tt Global Generalizable} Allows to export the choice of + generalizable variables. +\end{Variants} + +One can also use implicit generalization for binders, in which case the +generalized variables are added as binders and set maximally implicit. +\begin{coq_example*} +Definition id `(x : A) : A := x. +\end{coq_example*} +\begin{coq_example} +Print id. +\end{coq_example} + +The generalizing binders \texttt{\`{}\{ \}} and \texttt{\`{}( )} work similarly to +their explicit counterparts, only binding the generalized variables +implicitly, as maximally-inserted arguments. In these binders, the +binding name for the bound object is optional, whereas the type is +mandatory, dually to regular binders. + +\section{Coercions +\label{Coercions} +\index{Coercions}} + +Coercions can be used to implicitly inject terms from one {\em class} in +which they reside into another one. A {\em class} is either a sort +(denoted by the keyword {\tt Sortclass}), a product type (denoted by the +keyword {\tt Funclass}), or a type constructor (denoted by its name), +e.g. an inductive type or any constant with a type of the form +\texttt{forall} $(x_1:A_1) .. (x_n:A_n),~s$ where $s$ is a sort. + +Then the user is able to apply an +object that is not a function, but can be coerced to a function, and +more generally to consider that a term of type A is of type B provided +that there is a declared coercion between A and B. The main command is +\comindex{Coercion} +\begin{quote} +\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}. +\end{quote} +which declares the construction denoted by {\qualid} as a +coercion between {\class$_1$} and {\class$_2$}. + +More details and examples, and a description of the commands related +to coercions are provided in Chapter~\ref{Coercions-full}. + +\section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll} +\optindex{Printing All}} + +Coercions, implicit arguments, the type of pattern-matching, but also +notations (see Chapter~\ref{Addoc-syntax}) can obfuscate the behavior +of some tactics (typically the tactics applying to occurrences of +subterms are sensitive to the implicit arguments). The command +\begin{quote} +{\tt Set Printing All.} +\end{quote} +deactivates all high-level printing features such as coercions, +implicit arguments, returned type of pattern-matching, notations and +various syntactic sugar for pattern-matching or record projections. +Otherwise said, {\tt Set Printing All} includes the effects +of the commands {\tt Set Printing Implicit}, {\tt Set Printing +Coercions}, {\tt Set Printing Synth}, {\tt Unset Printing Projections} +and {\tt Unset Printing Notations}. To reactivate the high-level +printing features, use the command +\begin{quote} +{\tt Unset Printing All.} +\end{quote} + +\section[Printing universes]{Printing universes\label{PrintingUniverses} +\optindex{Printing Universes}} + +The following command: +\begin{quote} +{\tt Set Printing Universes} +\end{quote} +activates the display of the actual level of each occurrence of +{\Type}. See Section~\ref{Sorts} for details. This wizard option, in +combination with \texttt{Set Printing All} (see +section~\ref{SetPrintingAll}) can help to diagnose failures to unify +terms apparently identical but internally different in the Calculus of +Inductive Constructions. To reactivate the display of the actual level +of the occurrences of {\Type}, use +\begin{quote} +{\tt Unset Printing Universes.} +\end{quote} + +\comindex{Print Universes} +\comindex{Print Sorted Universes} + +The constraints on the internal level of the occurrences of {\Type} +(see Section~\ref{Sorts}) can be printed using the command +\begin{quote} +{\tt Print \zeroone{Sorted} Universes.} +\end{quote} +If the optional {\tt Sorted} option is given, each universe will be +made equivalent to a numbered label reflecting its level (with a +linear ordering) in the universe hierarchy. + +This command also accepts an optional output filename: +\begin{quote} +\tt Print \zeroone{Sorted} Universes {\str}. +\end{quote} +If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are +printed in the DOT language, and can be processed by Graphviz +tools. The format is unspecified if {\str} doesn't end in +\texttt{.dot} or \texttt{.gv}. + +\section[Existential variables]{Existential variables\label{ExistentialVariables}} +\label{evars} + +Coq terms can include existential variables which +represents unknown subterms to eventually be replaced by actual +subterms. + +Existential variables are generated in place of unsolvable implicit +arguments or ``{\tt \_}'' placeholders when using commands such as +\texttt{Check} (see Section~\ref{Check}) or when using tactics such as +\texttt{refine}~(see Section~\ref{refine}), as well as in place of unsolvable +instances when using tactics such that \texttt{eapply} (see +Section~\ref{eapply}). An existential variable is defined in a +context, which is the context of variables of the placeholder which +generated the existential variable, and a type, which is the expected +type of the placeholder. + +As a consequence of typing constraints, existential variables can be +duplicated in such a way that they possibly appear in different +contexts than their defining context. Thus, any occurrence of a given +existential variable comes with an instance of its original context. In the +simple case, when an existential variable denotes the placeholder +which generated it, or is used in the same context as the one in which +it was generated, the context is not displayed and the existential +variable is represented by ``?'' followed by an identifier. + +\begin{coq_example} +Parameter identity : forall (X:Set), X -> X. +Check identity _ _. +Check identity _ (fun x => _). +\end{coq_example} + +In the general case, when an existential variable ?{\ident} +appears outside of its context of definition, its instance, written under +the form \verb!@{id1:=term1; ...; idn:=termn}!, is appending to its +name, indicating how the variables of its defining context are +instantiated. The variables of the context of the existential +variables which are instantiated by themselves are not written, unless +the flag {\tt Printing Existential Instances} is on (see +Section~\ref{SetPrintingExistentialInstances}), and this is why an +existential variable used in the same context as its context of +definition is written with no instance. + +\begin{coq_example} +Check (fun x y => _) 0 1. +Set Printing Existential Instances. +Check (fun x y => _) 0 1. +\end{coq_example} + +\begin{coq_eval} +Unset Printing Existential Instances. +\end{coq_eval} + +Existential variables can be named by the user upon creation using +the syntax {\tt ?[\ident]}. This is useful when the existential +variable needs to be explicitly handled later in the script (e.g. +with a named-goal selector, see~\ref{ltac:selector}). + +\subsection{Explicit displaying of existential instances for pretty-printing +\label{SetPrintingExistentialInstances} +\optindex{Printing Existential Instances}} + +The command: +\begin{quote} +{\tt Set Printing Existential Instances} +\end{quote} +activates the full display of how the context of an existential variable is +instantiated at each of the occurrences of the existential variable. + +To deactivate the full display of the instances of existential +variables, use +\begin{quote} +{\tt Unset Printing Existential Instances.} +\end{quote} + +\subsection{Solving existential variables using tactics} +\ttindex{ltac:( \ldots )} + +\def\expr{\textrm{\textsl{tacexpr}}} + +Instead of letting the unification engine try to solve an existential variable +by itself, one can also provide an explicit hole together with a tactic to solve +it. Using the syntax {\tt ltac:(\expr)}, the user can put a +tactic anywhere a term is expected. The order of resolution is not specified and +is implementation-dependent. The inner tactic may use any variable defined in +its scope, including repeated alternations between variables introduced by term +binding as well as those introduced by tactic binding. The expression {\expr} +can be any tactic expression as described at section~\ref{TacticLanguage}. + +\begin{coq_example*} +Definition foo (x : nat) : nat := ltac:(exact x). +\end{coq_example*} + +This construction is useful when one wants to define complicated terms using +highly automated tactics without resorting to writing the proof-term by means of +the interactive proof engine. + +This mechanism is comparable to the {\tt Declare Implicit Tactic} command +defined at~\ref{DeclareImplicit}, except that the used tactic is local to each +hole instead of being declared globally. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3