diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Coercion.tex | 563 | ||||
| -rw-r--r-- | doc/refman/Extraction.tex | 620 | ||||
| -rw-r--r-- | doc/refman/Nsatz.tex | 102 | ||||
| -rw-r--r-- | doc/refman/Polynom.tex | 736 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 329 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 6 | ||||
| -rw-r--r-- | doc/refman/Setoid.tex | 842 |
7 files changed, 0 insertions, 3198 deletions
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex deleted file mode 100644 index 9862a9b30..000000000 --- a/doc/refman/Coercion.tex +++ /dev/null @@ -1,563 +0,0 @@ -\achapter{Implicit Coercions} -%HEVEA\cutname{coercions.html} -\aauthor{Amokrane Saïbi} - -\label{Coercions-full} -\index{Coercions!presentation} - -\asection{General Presentation} - -This section describes the inheritance mechanism of {\Coq}. In {\Coq} with -inheritance, we are not interested in adding any expressive power to -our theory, but only convenience. Given a term, possibly not typable, -we are interested in the problem of determining if it can be well -typed modulo insertion of appropriate coercions. We allow to write: - -\begin{itemize} -\item $f~a$ where $f:forall~ x:A, B$ and $a:A'$ when $A'$ can - be seen in some sense as a subtype of $A$. -\item $x:A$ when $A$ is not a type, but can be seen in - a certain sense as a type: set, group, category etc. -\item $f~a$ when $f$ is not a function, but can be seen in a certain sense - as a function: bijection, functor, any structure morphism etc. -\end{itemize} - -\asection{Classes} -\index{Coercions!classes} - A class with $n$ parameters is any defined name with a type -$forall~ (x_1:A_1)..(x_n:A_n), s$ where $s$ is a sort. Thus a class with -parameters is considered as a single class and not as a family of -classes. An object of a class $C$ is any term of type $C~t_1 -.. t_n$. In addition to these user-classes, we have two abstract -classes: - -\begin{itemize} -\item {\tt Sortclass}, the class of sorts; - its objects are the terms whose type is a sort (e.g., \texttt{Prop} - or \texttt{Type}). -\item {\tt Funclass}, the class of functions; - its objects are all the terms with a functional - type, i.e. of form $forall~ x:A, B$. -\end{itemize} - -Formally, the syntax of a classes is defined on Figure~\ref{fig:classes}. -\begin{figure} -\begin{centerframe} -\begin{tabular}{lcl} -{\class} & ::= & {\qualid} \\ - & $|$ & {\tt Sortclass} \\ - & $|$ & {\tt Funclass} -\end{tabular} -\end{centerframe} -\caption{Syntax of classes} -\label{fig:classes} -\end{figure} - -\asection{Coercions} -\index{Coercions!Funclass} -\index{Coercions!Sortclass} - A name $f$ can be declared as a coercion between a source user-class -$C$ with $n$ parameters and a target class $D$ if one of these -conditions holds: - -\newcommand{\oftype}{\!:\!} - -\begin{itemize} -\item $D$ is a user-class, then the type of $f$ must have the form - $forall~ (x_1 \oftype A_1)..(x_n \oftype A_n)(y\oftype C~x_1..x_n), D~u_1..u_m$ where $m$ - is the number of parameters of $D$. -\item $D$ is {\tt Funclass}, then the type of $f$ must have the form - $forall~ (x_1\oftype A_1)..(x_n\oftype A_n)(y\oftype C~x_1..x_n)(x:A), B$. -\item $D$ is {\tt Sortclass}, then the type of $f$ must have the form - $forall~ (x_1\oftype A_1)..(x_n\oftype A_n)(y\oftype C~x_1..x_n), s$ with $s$ a sort. -\end{itemize} - -We then write $f:C \mbox{\texttt{>->}} D$. The restriction on the type -of coercions is called {\em the uniform inheritance condition}. -Remark: the abstract class {\tt Sortclass} can be used as source class, -but the abstract class {\tt Funclass} cannot. - -To coerce an object $t:C~t_1..t_n$ of $C$ towards $D$, we have to -apply the coercion $f$ to it; the obtained term $f~t_1..t_n~t$ is -then an object of $D$. - -\asection{Identity Coercions} -\index{Coercions!identity} - - Identity coercions are special cases of coercions used to go around -the uniform inheritance condition. Let $C$ and $D$ be two classes -with respectively $n$ and $m$ parameters and -$f:forall~(x_1:T_1)..(x_k:T_k)(y:C~u_1..u_n), D~v_1..v_m$ a function which -does not verify the uniform inheritance condition. To declare $f$ as -coercion, one has first to declare a subclass $C'$ of $C$: - -$$C' := fun~ (x_1:T_1)..(x_k:T_k) => C~u_1..u_n$$ - -\noindent We then define an {\em identity coercion} between $C'$ and $C$: -\begin{eqnarray*} -Id\_C'\_C & := & fun~ (x_1:T_1)..(x_k:T_k)(y:C'~x_1..x_k) => (y:C~u_1..u_n)\\ -\end{eqnarray*} - -We can now declare $f$ as coercion from $C'$ to $D$, since we can -``cast'' its type as -$forall~ (x_1:T_1)..(x_k:T_k)(y:C'~x_1..x_k),D~v_1..v_m$.\\ The identity -coercions have a special status: to coerce an object $t:C'~t_1..t_k$ -of $C'$ towards $C$, we does not have to insert explicitly $Id\_C'\_C$ -since $Id\_C'\_C~t_1..t_k~t$ is convertible with $t$. However we -``rewrite'' the type of $t$ to become an object of $C$; in this case, -it becomes $C~u_1^*..u_k^*$ where each $u_i^*$ is the result of the -substitution in $u_i$ of the variables $x_j$ by $t_j$. - - -\asection{Inheritance Graph} -\index{Coercions!inheritance graph} -Coercions form an inheritance graph with classes as nodes. We call -{\em coercion path} an ordered list of coercions between two nodes of -the graph. A class $C$ is said to be a subclass of $D$ if there is a -coercion path in the graph from $C$ to $D$; we also say that $C$ -inherits from $D$. Our mechanism supports multiple inheritance since a -class may inherit from several classes, contrary to simple inheritance -where a class inherits from at most one class. However there must be -at most one path between two classes. If this is not the case, only -the {\em oldest} one is valid and the others are ignored. So the order -of declaration of coercions is important. - -We extend notations for coercions to coercion paths. For instance -$[f_1;..;f_k]:C \mbox{\texttt{>->}} D$ is the coercion path composed -by the coercions $f_1..f_k$. The application of a coercion path to a -term consists of the successive application of its coercions. - -\asection{Declaration of Coercions} - -%%%%% "Class" is useless, since classes are implicitely defined via coercions. - -% \asubsection{\tt Class {\qualid}.}\comindex{Class} -% Declares {\qualid} as a new class. - -% \begin{ErrMsgs} -% \item {\qualid} \errindex{not declared} -% \item {\qualid} \errindex{is already a class} -% \item \errindex{Type of {\qualid} does not end with a sort} -% \end{ErrMsgs} - -% \begin{Variant} -% \item {\tt Class Local {\qualid}.} \\ -% Declares the construction denoted by {\qualid} as a new local class to -% the current section. -% \end{Variant} - -% END "Class" is useless - -\asubsection{\tt Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.} -\comindex{Coercion} - -Declares the construction denoted by {\qualid} as a coercion between -{\class$_1$} and {\class$_2$}. - -% Useless information -% The classes {\class$_1$} and {\class$_2$} are first declared if necessary. - -\begin{ErrMsgs} -\item {\qualid} \errindex{not declared} -\item {\qualid} \errindex{is already a coercion} -\item \errindex{Funclass cannot be a source class} -\item {\qualid} \errindex{is not a function} -\item \errindex{Cannot find the source class of {\qualid}} -\item \errindex{Cannot recognize {\class$_1$} as a source class of {\qualid}} -\item {\qualid} \errindex{does not respect the uniform inheritance condition} -\item \errindex{Found target class {\class} instead of {\class$_2$}} - -\end{ErrMsgs} - -When the coercion {\qualid} is added to the inheritance graph, non -valid coercion paths are ignored; they are signaled by a warning. -\\[0.3cm] -\noindent {\bf Warning :} -\begin{enumerate} -\item \begin{tabbing} -{\tt Ambiguous paths: }\= $[f_1^1;..;f_{n_1}^1] : C_1\mbox{\tt >->}D_1$\\ - \> {\ldots} \\ - \>$[f_1^m;..;f_{n_m}^m] : C_m\mbox{\tt >->}D_m$ - \end{tabbing} -\end{enumerate} - -\begin{Variants} -\item {\tt Local Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.} -\comindex{Local Coercion}\\ - Declares the construction denoted by {\qualid} as a coercion local to - the current section. - -\item {\tt Coercion {\ident} := {\term}}\comindex{Coercion}\\ - This defines {\ident} just like \texttt{Definition {\ident} := - {\term}}, and then declares {\ident} as a coercion between it - source and its target. - -\item {\tt Coercion {\ident} := {\term} : {\type}}\\ - This defines {\ident} just like - \texttt{Definition {\ident} : {\type} := {\term}}, and then - declares {\ident} as a coercion between it source and its target. - -\item {\tt Local Coercion {\ident} := {\term}}\comindex{Local Coercion}\\ - This defines {\ident} just like \texttt{Let {\ident} := - {\term}}, and then declares {\ident} as a coercion between it - source and its target. - -\item Assumptions can be declared as coercions at declaration -time. This extends the grammar of assumptions from -Figure~\ref{sentences-syntax} as follows: -\comindex{Variable \mbox{\rm (and coercions)}} -\comindex{Axiom \mbox{\rm (and coercions)}} -\comindex{Parameter \mbox{\rm (and coercions)}} -\comindex{Hypothesis \mbox{\rm (and coercions)}} - -\begin{tabular}{lcl} -%% Declarations -{\assumption} & ::= & {\assumptionkeyword} {\assums} {\tt .} \\ -&&\\ -{\assums} & ::= & {\simpleassums} \\ - & $|$ & \nelist{{\tt (} \simpleassums {\tt )}}{} \\ -&&\\ -{\simpleassums} & ::= & \nelist{\ident}{} {\tt :}\zeroone{{\tt >}} {\term}\\ -\end{tabular} - -If the extra {\tt >} is present before the type of some assumptions, these -assumptions are declared as coercions. - -\item Constructors of inductive types can be declared as coercions at -definition time of the inductive type. This extends and modifies the -grammar of inductive types from Figure \ref{sentences-syntax} as follows: -\comindex{Inductive \mbox{\rm (and coercions)}} -\comindex{CoInductive \mbox{\rm (and coercions)}} - -\begin{center} -\begin{tabular}{lcl} -%% Inductives -{\inductive} & ::= & - {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\ - & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ - & & \\ -{\inductivebody} & ::= & - {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\ - && ~~~\zeroone{\zeroone{\tt |} \nelist{\constructor}{|}} \\ - & & \\ -{\constructor} & ::= & {\ident} \zeroone{\binders} \zeroone{{\tt :}\zeroone{\tt >} {\term}} \\ -\end{tabular} -\end{center} - -Especially, if the extra {\tt >} is present in a constructor -declaration, this constructor is declared as a coercion. -\end{Variants} - -\asubsection{\tt Identity Coercion {\ident}:{\class$_1$} >-> {\class$_2$}.} -\comindex{Identity Coercion} - -We check that {\class$_1$} is a constant with a value of the form -$fun~ (x_1:T_1)..(x_n:T_n) => (\mbox{\class}_2~t_1..t_m)$ where $m$ is the -number of parameters of \class$_2$. Then we define an identity -function with the type -$forall~ (x_1:T_1)..(x_n:T_n)(y:\mbox{\class}_1~x_1..x_n), -{\mbox{\class}_2}~t_1..t_m$, and we declare it as an identity -coercion between {\class$_1$} and {\class$_2$}. - -\begin{ErrMsgs} -\item {\class$_1$} \errindex{must be a transparent constant} -\end{ErrMsgs} - -\begin{Variants} -\item {\tt Local Identity Coercion {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\ -Idem but locally to the current section. - -\item {\tt SubClass {\ident} := {\type}.} \\ -\comindex{SubClass} - If {\type} is a class -{\ident'} applied to some arguments then {\ident} is defined and an -identity coercion of name {\tt Id\_{\ident}\_{\ident'}} is -declared. Otherwise said, this is an abbreviation for - -{\tt Definition {\ident} := {\type}.} - - followed by - -{\tt Identity Coercion Id\_{\ident}\_{\ident'}:{\ident} >-> {\ident'}}. - -\item {\tt Local SubClass {\ident} := {\type}.} \\ -Same as before but locally to the current section. - -\end{Variants} - -\asection{Displaying Available Coercions} - -\asubsection{\tt Print Classes.} -\comindex{Print Classes} -Print the list of declared classes in the current context. - -\asubsection{\tt Print Coercions.} -\comindex{Print Coercions} -Print the list of declared coercions in the current context. - -\asubsection{\tt Print Graph.} -\comindex{Print Graph} -Print the list of valid coercion paths in the current context. - -\asubsection{\tt Print Coercion Paths {\class$_1$} {\class$_2$}.} -\comindex{Print Coercion Paths} -Print the list of valid coercion paths from {\class$_1$} to {\class$_2$}. - -\asection{Activating the Printing of Coercions} - -\asubsection{\tt Set Printing Coercions.} -\optindex{Printing Coercions} - -This command forces all the coercions to be printed. -Conversely, to skip the printing of coercions, use - {\tt Unset Printing Coercions}. -By default, coercions are not printed. - -\asubsection{\tt Add Printing Coercion {\qualid}.} -\comindex{Add Printing Coercion} -\comindex{Remove Printing Coercion} - -This command forces coercion denoted by {\qualid} to be printed. -To skip the printing of coercion {\qualid}, use - {\tt Remove Printing Coercion {\qualid}}. -By default, a coercion is never printed. - -\asection{Classes as Records} -\label{Coercions-and-records} -\index{Coercions!and records} -We allow the definition of {\em Structures with Inheritance} (or -classes as records) by extending the existing {\tt Record} macro -(see Section~\ref{Record}). Its new syntax is: - -\begin{center} -\begin{tabular}{l} -{\tt Record \zeroone{>}~{\ident} \zeroone{\binders} : {\sort} := \zeroone{\ident$_0$} \verb+{+} \\ -~~~~\begin{tabular}{l} - {\tt \ident$_1$ $[$:$|$:>$]$ \term$_1$ ;} \\ - ... \\ - {\tt \ident$_n$ $[$:$|$:>$]$ \term$_n$ \verb+}+. } - \end{tabular} -\end{tabular} -\end{center} -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. The identifiers {\ident$_1$}, .., {\ident$_n$} are the -names of its fields and {\term$_1$}, .., {\term$_n$} their respective -types. The alternative {\tt $[$:$|$:>$]$} is ``{\tt :}'' or ``{\tt -:>}''. If {\tt {\ident$_i$}:>{\term$_i$}}, then {\ident$_i$} is -automatically declared as coercion from {\ident} to the class of -{\term$_i$}. Remark that {\ident$_i$} always verifies the uniform -inheritance condition. If the optional ``{\tt >}'' before {\ident} is -present, then {\ident$_0$} (or the default name {\tt Build\_{\ident}} -if {\ident$_0$} is omitted) is automatically declared as a coercion -from the class of {\term$_n$} to {\ident} (this may fail if the -uniform inheritance condition is not satisfied). - -\Rem The keyword {\tt Structure}\comindex{Structure} is a synonym of {\tt -Record}. - -\asection{Coercions and Sections} -\index{Coercions!and sections} - The inheritance mechanism is compatible with the section -mechanism. The global classes and coercions defined inside a section -are redefined after its closing, using their new value and new -type. The classes and coercions which are local to the section are -simply forgotten. -Coercions with a local source class or a local target class, and -coercions which do not verify the uniform inheritance condition any longer -are also forgotten. - -\asection{Coercions and Modules} -\index{Coercions!and modules} - -From Coq version 8.3, the coercions present in a module are activated -only when the module is explicitly imported. Formerly, the coercions -were activated as soon as the module was required, whatever it was -imported or not. - -To recover the behavior of the versions of Coq prior to 8.3, use the -following command: - -\optindex{Automatic Coercions Import} -\begin{verbatim} -Set Automatic Coercions Import. -\end{verbatim} - -To cancel the effect of the option, use instead: - -\begin{verbatim} -Unset Automatic Coercions Import. -\end{verbatim} - -\asection{Examples} - - There are three situations: - -\begin{itemize} -\item $f~a$ is ill-typed where $f:forall~x:A,B$ and $a:A'$. If there is a - coercion path between $A'$ and $A$, $f~a$ is transformed into - $f~a'$ where $a'$ is the result of the application of this - coercion path to $a$. - -We first give an example of coercion between atomic inductive types - -%\begin{\small} -\begin{coq_example} -Definition bool_in_nat (b:bool) := if b then 0 else 1. -Coercion bool_in_nat : bool >-> nat. -Check (0 = true). -Set Printing Coercions. -Check (0 = true). -\end{coq_example} -%\end{small} - -\begin{coq_eval} -Unset Printing Coercions. -\end{coq_eval} - -\Warning ``\verb|Check true=O.|'' fails. This is ``normal'' behaviour of -coercions. To validate \verb|true=O|, the coercion is searched from -\verb=nat= to \verb=bool=. There is none. - -We give an example of coercion between classes with parameters. - -%\begin{\small} -\begin{coq_example} -Parameters - (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set). -Parameter f : forall n:nat, C n -> D (S n) true. -Coercion f : C >-> D. -Parameter g : forall (n:nat) (b:bool), D n b -> E b. -Coercion g : D >-> E. -Parameter c : C 0. -Parameter T : E true -> nat. -Check (T c). -Set Printing Coercions. -Check (T c). -\end{coq_example} -%\end{small} - -\begin{coq_eval} -Unset Printing Coercions. -\end{coq_eval} - -We give now an example using identity coercions. - -%\begin{small} -\begin{coq_example} -Definition D' (b:bool) := D 1 b. -Identity Coercion IdD'D : D' >-> D. -Print IdD'D. -Parameter d' : D' true. -Check (T d'). -Set Printing Coercions. -Check (T d'). -\end{coq_example} -%\end{small} - -\begin{coq_eval} -Unset Printing Coercions. -\end{coq_eval} - - - In the case of functional arguments, we use the monotonic rule of -sub-typing. Approximatively, to coerce $t:forall~x:A, B$ towards -$forall~x:A',B'$, one have to coerce $A'$ towards $A$ and $B$ towards -$B'$. An example is given below: - -%\begin{small} -\begin{coq_example} -Parameters (A B : Set) (h : A -> B). -Coercion h : A >-> B. -Parameter U : (A -> E true) -> nat. -Parameter t : B -> C 0. -Check (U t). -Set Printing Coercions. -Check (U t). -\end{coq_example} -%\end{small} - -\begin{coq_eval} -Unset Printing Coercions. -\end{coq_eval} - - Remark the changes in the result following the modification of the -previous example. - -%\begin{small} -\begin{coq_example} -Parameter U' : (C 0 -> B) -> nat. -Parameter t' : E true -> A. -Check (U' t'). -Set Printing Coercions. -Check (U' t'). -\end{coq_example} -%\end{small} - -\begin{coq_eval} -Unset Printing Coercions. -\end{coq_eval} - -\item An assumption $x:A$ when $A$ is not a type, is ill-typed. It is - replaced by $x:A'$ where $A'$ is the result of the application - to $A$ of the coercion path between the class of $A$ and {\tt - Sortclass} if it exists. This case occurs in the abstraction - $fun~ x:A => t$, universal quantification $forall~x:A, B$, - global variables and parameters of (co-)inductive definitions - and functions. In $forall~x:A, B$, such a coercion path may be - applied to $B$ also if necessary. - -%\begin{small} -\begin{coq_example} -Parameter Graph : Type. -Parameter Node : Graph -> Type. -Coercion Node : Graph >-> Sortclass. -Parameter G : Graph. -Parameter Arrows : G -> G -> Type. -Check Arrows. -Parameter fg : G -> G. -Check fg. -Set Printing Coercions. -Check fg. -\end{coq_example} -%\end{small} - -\begin{coq_eval} -Unset Printing Coercions. -\end{coq_eval} - -\item $f~a$ is ill-typed because $f:A$ is not a function. The term - $f$ is replaced by the term obtained by applying to $f$ the - coercion path between $A$ and {\tt Funclass} if it exists. - -%\begin{small} -\begin{coq_example} -Parameter bij : Set -> Set -> Set. -Parameter ap : forall A B:Set, bij A B -> A -> B. -Coercion ap : bij >-> Funclass. -Parameter b : bij nat nat. -Check (b 0). -Set Printing Coercions. -Check (b 0). -\end{coq_example} -%\end{small} - -\begin{coq_eval} -Unset Printing Coercions. -\end{coq_eval} - -Let us see the resulting graph of this session. - -%\begin{small} -\begin{coq_example} -Print Graph. -\end{coq_example} -%\end{small} - -\end{itemize} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex deleted file mode 100644 index cff7be3e9..000000000 --- a/doc/refman/Extraction.tex +++ /dev/null @@ -1,620 +0,0 @@ -\achapter{Extraction of programs in OCaml and Haskell} -%HEVEA\cutname{extraction.html} -\label{Extraction} -\aauthor{Jean-Christophe Filliâtre and Pierre Letouzey} -\index{Extraction} - -\noindent We present here the \Coq\ extraction commands, used to build certified -and relatively efficient functional programs, extracting them from -either \Coq\ functions or \Coq\ proofs of specifications. The -functional languages available as output are currently \ocaml{}, -\textsc{Haskell} and \textsc{Scheme}. In the following, ``ML'' will -be used (abusively) to refer to any of the three. - -%% \paragraph{Differences with old versions.} -%% The current extraction mechanism is new for version 7.0 of {\Coq}. -%% In particular, the \FW\ toplevel used as an intermediate step between -%% \Coq\ and ML has been withdrawn. It is also not possible -%% any more to import ML objects in this \FW\ toplevel. -%% The current mechanism also differs from -%% the one in previous versions of \Coq: there is no more -%% an explicit toplevel for the language (formerly called \textsc{Fml}). - -Before using any of the commands or options described in this chapter, -the extraction framework should first be loaded explicitly -via {\tt Require Extraction}, or via the more robust -{\tt From Coq Require Extraction}. -Note that in earlier versions of Coq, these commands and options were -directly available without any preliminary {\tt Require}. - -\begin{coq_example} -Require Extraction. -\end{coq_example} - -\asection{Generating ML code} -\comindex{Extraction} -\comindex{Recursive Extraction} -\comindex{Separate Extraction} -\comindex{Extraction Library} -\comindex{Recursive Extraction Library} - -The next two commands are meant to be used for rapid preview of -extraction. They both display extracted term(s) inside \Coq. - -\begin{description} -\item {\tt Extraction \qualid{}.} ~\par - Extraction of a constant or module in the \Coq\ toplevel. - -\item {\tt Recursive Extraction} \qualid$_1$ \dots\ \qualid$_n$. ~\par - Recursive extraction of all the globals (or modules) \qualid$_1$ \dots\ - \qualid$_n$ and all their dependencies in the \Coq\ toplevel. -\end{description} - -%% TODO error messages - -\noindent All the following commands produce real ML files. User can choose to produce -one monolithic file or one file per \Coq\ library. - -\begin{description} -\item {\tt Extraction "{\em file}"} - \qualid$_1$ \dots\ \qualid$_n$. ~\par - Recursive extraction of all the globals (or modules) \qualid$_1$ \dots\ - \qualid$_n$ and all their dependencies in one monolithic file {\em file}. - Global and local identifiers are renamed according to the chosen ML - language to fulfill its syntactic conventions, keeping original - names as much as possible. - -\item {\tt Extraction Library} \ident. ~\par - Extraction of the whole \Coq\ library {\tt\ident.v} to an ML module - {\tt\ident.ml}. In case of name clash, identifiers are here renamed - using prefixes \verb!coq_! or \verb!Coq_! to ensure a - session-independent renaming. - -\item {\tt Recursive Extraction Library} \ident. ~\par - Extraction of the \Coq\ library {\tt\ident.v} and all other modules - {\tt\ident.v} depends on. - -\item {\tt Separate Extraction} - \qualid$_1$ \dots\ \qualid$_n$. ~\par - Recursive extraction of all the globals (or modules) \qualid$_1$ \dots\ - \qualid$_n$ and all their dependencies, just as {\tt - Extraction "{\em file}"}, but instead of producing one monolithic - file, this command splits the produced code in separate ML files, one per - corresponding Coq {\tt .v} file. This command is hence quite similar - to {\tt Recursive Extraction Library}, except that only the needed - parts of Coq libraries are extracted instead of the whole. The - naming convention in case of name clash is the same one as - {\tt Extraction Library}: identifiers are here renamed - using prefixes \verb!coq_! or \verb!Coq_!. -\end{description} - -\noindent The following command is meant to help automatic testing of - the extraction, see for instance the {\tt test-suite} directory - in the \Coq\ sources. - -\begin{description} -\item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par - All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all - their dependencies are extracted to a temporary {\ocaml} file, just as in - {\tt Extraction "{\em file}"}. Then this temporary file and its - signature are compiled with the same {\ocaml} compiler used to built - \Coq. This command succeeds only if the extraction and the {\ocaml} - compilation succeed (and it fails if the current target language - of the extraction is not {\ocaml}). -\end{description} - -\asection{Extraction options} - -\asubsection{Setting the target language} -\comindex{Extraction Language} - -The ability to fix target language is the first and more important -of the extraction options. Default is {\ocaml}. -\begin{description} -\item {\tt Extraction Language OCaml}. -\item {\tt Extraction Language Haskell}. -\item {\tt Extraction Language Scheme}. -\end{description} - -\asubsection{Inlining and optimizations} - -Since {\ocaml} is a strict language, the extracted code has to -be optimized in order to be efficient (for instance, when using -induction principles we do not want to compute all the recursive calls -but only the needed ones). So the extraction mechanism provides an -automatic optimization routine that will be called each time the user -want to generate {\ocaml} programs. The optimizations can be split in two -groups: the type-preserving ones -- essentially constant inlining and -reductions -- and the non type-preserving ones -- some function -abstractions of dummy types are removed when it is deemed safe in order -to have more elegant types. Therefore some constants may not appear in the -resulting monolithic {\ocaml} program. In the case of modular extraction, -even if some inlining is done, the inlined constant are nevertheless -printed, to ensure session-independent programs. - -Concerning Haskell, type-preserving optimizations are less useful -because of laziness. We still make some optimizations, for example in -order to produce more readable code. - -The type-preserving optimizations are controlled by the following \Coq\ options: - -\begin{description} - -\item \optindex{Extraction Optimize} {\tt Unset Extraction Optimize.} - -Default is Set. This controls all type-preserving optimizations made on -the ML terms (mostly reduction of dummy beta/iota redexes, but also -simplifications on Cases, etc). Put this option to Unset if you want a -ML term as close as possible to the Coq term. - -\item \optindex{Extraction Conservative Types} -{\tt Set Extraction Conservative Types.} - -Default is Unset. This controls the non type-preserving optimizations -made on ML terms (which try to avoid function abstraction of dummy -types). Turn this option to Set to make sure that {\tt e:t} -implies that {\tt e':t'} where {\tt e'} and {\tt t'} are the extracted -code of {\tt e} and {\tt t} respectively. - -\item \optindex{Extraction KeepSingleton} -{\tt Set Extraction KeepSingleton.} - -Default is Unset. Normally, when the extraction of an inductive type -produces a singleton type (i.e. a type with only one constructor, and -only one argument to this constructor), the inductive structure is -removed and this type is seen as an alias to the inner type. -The typical example is {\tt sig}. This option allows disabling this -optimization when one wishes to preserve the inductive structure of types. - -\item \optindex{Extraction AutoInline} {\tt Unset Extraction AutoInline.} - -Default is Set. The extraction mechanism -inlines the bodies of some defined constants, according to some heuristics -like size of bodies, uselessness of some arguments, etc. Those heuristics are -not always perfect; if you want to disable this feature, do it by Unset. - -\item \comindex{Extraction Inline} \comindex{Extraction NoInline} -{\tt Extraction [Inline|NoInline] \qualid$_1$ \dots\ \qualid$_n$}. - -In addition to the automatic inline feature, you can tell to -inline some more constants by the {\tt Extraction Inline} command. Conversely, -you can forbid the automatic inlining of some specific constants by -the {\tt Extraction NoInline} command. -Those two commands enable a precise control of what is inlined and what is not. - -\item \comindex{Print Extraction Inline} -{\tt Print Extraction Inline}. - -Prints the current state of the table recording the custom inlinings -declared by the two previous commands. - -\item \comindex{Reset Extraction Inline} -{\tt Reset Extraction Inline}. - -Puts the table recording the custom inlinings back to empty. - -\end{description} - - -\paragraph{Inlining and printing of a constant declaration.} - -A user can explicitly ask for a constant to be extracted by two means: -\begin{itemize} -\item by mentioning it on the extraction command line -\item by extracting the whole \Coq\ module of this constant. -\end{itemize} -In both cases, the declaration of this constant will be present in the -produced file. -But this same constant may or may not be inlined in the following -terms, depending on the automatic/custom inlining mechanism. - - -For the constants non-explicitly required but needed for dependency -reasons, there are two cases: -\begin{itemize} -\item If an inlining decision is taken, whether automatically or not, -all occurrences of this constant are replaced by its extracted body, and -this constant is not declared in the generated file. -\item If no inlining decision is taken, the constant is normally - declared in the produced file. -\end{itemize} - -\asubsection{Extra elimination of useless arguments} - -The following command provides some extra manual control on the -code elimination performed during extraction, in a way which -is independent but complementary to the main elimination -principles of extraction (logical parts and types). - -\begin{description} -\item \comindex{Extraction Implicit} - {\tt Extraction Implicit} \qualid\ [ \ident$_1$ \dots\ \ident$_n$ ]. - -This experimental command allows declaring some arguments of -\qualid\ as implicit, i.e. useless in extracted code and hence to -be removed by extraction. Here \qualid\ can be any function or -inductive constructor, and \ident$_i$ are the names of the concerned -arguments. In fact, an argument can also be referred by a number -indicating its position, starting from 1. -\end{description} - -\noindent When an actual extraction takes place, an error is normally raised if the -{\tt Extraction Implicit} -declarations cannot be honored, that is if any of the implicited -variables still occurs in the final code. This behavior can be relaxed -via the following option: - -\begin{description} -\item \optindex{Extraction SafeImplicits} {\tt Unset Extraction SafeImplicits.} - -Default is Set. When this option is Unset, a warning is emitted -instead of an error if some implicited variables still occur in the -final code of an extraction. This way, the extracted code may be -obtained nonetheless and reviewed manually to locate the source of the issue -(in the code, some comments mark the location of these remaining -implicited variables). -Note that this extracted code might not compile or run properly, -depending of the use of these remaining implicited variables. - -\end{description} - -\asubsection{Realizing axioms}\label{extraction:axioms} - -Extraction will fail if it encounters an informative -axiom not realized (see Section~\ref{extraction:axioms}). -A warning will be issued if it encounters a logical axiom, to remind the -user that inconsistent logical axioms may lead to incorrect or -non-terminating extracted terms. - -It is possible to assume some axioms while developing a proof. Since -these axioms can be any kind of proposition or object or type, they may -perfectly well have some computational content. But a program must be -a closed term, and of course the system cannot guess the program which -realizes an axiom. Therefore, it is possible to tell the system -what ML term corresponds to a given axiom. - -\comindex{Extract Constant} -\begin{description} -\item{\tt Extract Constant \qualid\ => \str.} ~\par - Give an ML extraction for the given constant. - The \str\ may be an identifier or a quoted string. -\item{\tt Extract Inlined Constant \qualid\ => \str.} ~\par - Same as the previous one, except that the given ML terms will - be inlined everywhere instead of being declared via a let. -\end{description} - -\noindent Note that the {\tt Extract Inlined Constant} command is sugar -for an {\tt Extract Constant} followed by a {\tt Extraction Inline}. -Hence a {\tt Reset Extraction Inline} will have an effect on the -realized and inlined axiom. - -Of course, it is the responsibility of the user to ensure that the ML -terms given to realize the axioms do have the expected types. In -fact, the strings containing realizing code are just copied to the -extracted files. The extraction recognizes whether the realized axiom -should become a ML type constant or a ML object declaration. - -\Example -\begin{coq_example*} -Axiom X:Set. -Axiom x:X. -Extract Constant X => "int". -Extract Constant x => "0". -\end{coq_example*} - -\noindent Notice that in the case of type scheme axiom (i.e. whose type is an -arity, that is a sequence of product finished by a sort), then some type -variables have to be given. The syntax is then: - -\begin{description} -\item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.} -\end{description} - -\noindent The number of type variables is checked by the system. - -\Example -\begin{coq_example*} -Axiom Y : Set -> Set -> Set. -Extract Constant Y "'a" "'b" => " 'a*'b ". -\end{coq_example*} - -\noindent Realizing an axiom via {\tt Extract Constant} is only useful in the -case of an informative axiom (of sort Type or Set). A logical axiom -have no computational content and hence will not appears in extracted -terms. But a warning is nonetheless issued if extraction encounters a -logical axiom. This warning reminds user that inconsistent logical -axioms may lead to incorrect or non-terminating extracted terms. - -If an informative axiom has not been realized before an extraction, a -warning is also issued and the definition of the axiom is filled with -an exception labeled {\tt AXIOM TO BE REALIZED}. The user must then -search these exceptions inside the extracted file and replace them by -real code. - -\comindex{Extract Inductive} - -The system also provides a mechanism to specify ML terms for inductive -types and constructors. For instance, the user may want to use the ML -native boolean type instead of \Coq\ one. The syntax is the following: - -\begin{description} -\item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots\ \str\ ] {\it optstring}.}\par - Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first \str) and all its - constructors (between square brackets). If given, the final optional - string should contain a function emulating pattern-matching over this - inductive type. If this optional string is not given, the ML - extraction must be an ML inductive datatype, and the native - pattern-matching of the language will be used. -\end{description} - -\noindent For an inductive type with $k$ constructor, the function used to -emulate the match should expect $(k+1)$ arguments, first the $k$ -branches in functional form, and then the inductive element to -destruct. For instance, the match branch \verb$| S n => foo$ gives the -functional form \verb$(fun n -> foo)$. Note that a constructor with no -argument is considered to have one unit argument, in order to block -early evaluation of the branch: \verb$| O => bar$ leads to the functional -form \verb$(fun () -> bar)$. For instance, when extracting {\tt nat} -into {\tt int}, the code to provide has type: -{\tt (unit->'a)->(int->'a)->int->'a}. - -As for {\tt Extract Inductive}, this command should be used with care: -\begin{itemize} -\item The ML code provided by the user is currently \emph{not} checked at all by - extraction, even for syntax errors. - -\item Extracting an inductive type to a pre-existing ML inductive type -is quite sound. But extracting to a general type (by providing an -ad-hoc pattern-matching) will often \emph{not} be fully rigorously -correct. For instance, when extracting {\tt nat} to {\ocaml}'s {\tt -int}, it is theoretically possible to build {\tt nat} values that are -larger than {\ocaml}'s {\tt max\_int}. It is the user's responsibility to -be sure that no overflow or other bad events occur in practice. - -\item Translating an inductive type to an ML type does \emph{not} -magically improve the asymptotic complexity of functions, even if the -ML type is an efficient representation. For instance, when extracting -{\tt nat} to {\ocaml}'s {\tt int}, the function {\tt mult} stays -quadratic. It might be interesting to associate this translation with -some specific {\tt Extract Constant} when primitive counterparts exist. -\end{itemize} - -\Example -Typical examples are the following: -\begin{coq_eval} -Require Extraction. -\end{coq_eval} -\begin{coq_example} -Extract Inductive unit => "unit" [ "()" ]. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -\end{coq_example} - -\noindent When extracting to {\ocaml}, if an inductive constructor or type -has arity 2 and the corresponding string is enclosed by parentheses, -and the string meets {\ocaml}'s lexical criteria for an infix symbol, -then the rest of the string is used as infix constructor or type. - -\begin{coq_example} -Extract Inductive list => "list" [ "[]" "(::)" ]. -Extract Inductive prod => "(*)" [ "(,)" ]. -\end{coq_example} - -\noindent As an example of translation to a non-inductive datatype, let's turn -{\tt nat} into {\ocaml}'s {\tt int} (see caveat above): -\begin{coq_example} -Extract Inductive nat => int [ "0" "succ" ] - "(fun fO fS n -> if n=0 then fO () else fS (n-1))". -\end{coq_example} - -\asubsection{Avoiding conflicts with existing filenames} - -\comindex{Extraction Blacklist} - -When using {\tt Extraction Library}, the names of the extracted files -directly depends from the names of the \Coq\ files. It may happen that -these filenames are in conflict with already existing files, -either in the standard library of the target language or in other -code that is meant to be linked with the extracted code. -For instance the module {\tt List} exists both in \Coq\ and in {\ocaml}. -It is possible to instruct the extraction not to use particular filenames. - -\begin{description} -\item{\tt Extraction Blacklist} \ident\ \dots\ \ident. ~\par - Instruct the extraction to avoid using these names as filenames - for extracted code. -\item{\tt Print Extraction Blacklist.} ~\par - Show the current list of filenames the extraction should avoid. -\item{\tt Reset Extraction Blacklist.} ~\par - Allow the extraction to use any filename. -\end{description} - -\noindent For {\ocaml}, a typical use of these commands is -{\tt Extraction Blacklist String List}. - -\asection{Differences between \Coq\ and ML type systems} - - -Due to differences between \Coq\ and ML type systems, -some extracted programs are not directly typable in ML. -We now solve this problem (at least in {\ocaml}) by adding -when needed some unsafe casting {\tt Obj.magic}, which give -a generic type {\tt 'a} to any term. - -For example, here are two kinds of problem that can occur: - -\begin{itemize} - \item If some part of the program is {\em very} polymorphic, there - may be no ML type for it. In that case the extraction to ML works - alright but the generated code may be refused by the ML - type-checker. A very well known example is the {\em distr-pair} - function: -\begin{verbatim} -Definition dp := - fun (A B:Set)(x:A)(y:B)(f:forall C:Set, C->C) => (f A x, f B y). -\end{verbatim} - -In {\ocaml}, for instance, the direct extracted term would be -\begin{verbatim} -let dp x y f = Pair((f () x),(f () y)) -\end{verbatim} - -and would have type -\begin{verbatim} -dp : 'a -> 'a -> (unit -> 'a -> 'b) -> ('b,'b) prod -\end{verbatim} - -which is not its original type, but a restriction. - -We now produce the following correct version: -\begin{verbatim} -let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) -\end{verbatim} - - \item Some definitions of \Coq\ may have no counterpart in ML. This - happens when there is a quantification over types inside the type - of a constructor; for example: -\begin{verbatim} -Inductive anything : Type := dummy : forall A:Set, A -> anything. -\end{verbatim} - -which corresponds to the definition of an ML dynamic type. -In {\ocaml}, we must cast any argument of the constructor dummy. - -\end{itemize} - -\noindent Even with those unsafe castings, you should never get error like -``segmentation fault''. In fact even if your program may seem -ill-typed to the {\ocaml} type-checker, it can't go wrong: it comes -from a Coq well-typed terms, so for example inductives will always -have the correct number of arguments, etc. - -More details about the correctness of the extracted programs can be -found in \cite{Let02}. - -We have to say, though, that in most ``realistic'' programs, these -problems do not occur. For example all the programs of Coq library are -accepted by Caml type-checker without any {\tt Obj.magic} (see examples below). - - - -\asection{Some examples} - -We present here two examples of extractions, taken from the -\Coq\ Standard Library. We choose \ocaml\ as target language, -but all can be done in the other dialects with slight modifications. -We then indicate where to find other examples and tests of Extraction. - -\asubsection{A detailed example: Euclidean division} - -The file {\tt Euclid} contains the proof of Euclidean division -(theorem {\tt eucl\_dev}). The natural numbers defined in the example -files are unary integers defined by two constructors $O$ and $S$: -\begin{coq_example*} -Inductive nat : Set := - | O : nat - | S : nat -> nat. -\end{coq_example*} - -\noindent This module contains a theorem {\tt eucl\_dev}, whose type is -\begin{verbatim} -forall b:nat, b > 0 -> forall a:nat, diveucl a b -\end{verbatim} -where {\tt diveucl} is a type for the pair of the quotient and the -modulo, plus some logical assertions that disappear during extraction. -We can now extract this program to \ocaml: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example} -Require Extraction. -Require Import Euclid Wf_nat. -Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2. -Recursive Extraction eucl_dev. -\end{coq_example} - -\noindent The inlining of {\tt gt\_wf\_rec} and others is not -mandatory. It only enhances readability of extracted code. -You can then copy-paste the output to a file {\tt euclid.ml} or let -\Coq\ do it for you with the following command: - -\begin{verbatim} -Extraction "euclid" eucl_dev. -\end{verbatim} - -\noindent Let us play the resulting program: - -\begin{verbatim} -# #use "euclid.ml";; -type nat = O | S of nat -type sumbool = Left | Right -val minus : nat -> nat -> nat = <fun> -val le_lt_dec : nat -> nat -> sumbool = <fun> -val le_gt_dec : nat -> nat -> sumbool = <fun> -type diveucl = Divex of nat * nat -val eucl_dev : nat -> nat -> diveucl = <fun> -# eucl_dev (S (S O)) (S (S (S (S (S O)))));; -- : diveucl = Divex (S (S O), S O) -\end{verbatim} -It is easier to test on \ocaml\ integers: -\begin{verbatim} -# let rec nat_of_int = function 0 -> O | n -> S (nat_of_int (n-1));; -val nat_of_int : int -> nat = <fun> -# let rec int_of_nat = function O -> 0 | S p -> 1+(int_of_nat p);; -val int_of_nat : nat -> int = <fun> -# let div a b = - let Divex (q,r) = eucl_dev (nat_of_int b) (nat_of_int a) - in (int_of_nat q, int_of_nat r);; -val div : int -> int -> int * int = <fun> -# div 173 15;; -- : int * int = (11, 8) -\end{verbatim} - -\noindent Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now -available via a mere {\tt Require Import ExtrOcamlIntConv} and then -adding these functions to the list of functions to extract. This file -{\tt ExtrOcamlIntConv.v} and some others in {\tt plugins/extraction/} -are meant to help building concrete program via extraction. - -\asubsection{Extraction's horror museum} - -Some pathological examples of extraction are grouped in the file\\ -{\tt test-suite/success/extraction.v} of the sources of \Coq. - -\asubsection{Users' Contributions} - -Several of the \Coq\ Users' Contributions use extraction to produce -certified programs. In particular the following ones have an automatic -extraction test: - -\begin{itemize} -\item {\tt additions} -\item {\tt bdds} -\item {\tt canon-bdds} -\item {\tt chinese} -\item {\tt continuations} -\item {\tt coq-in-coq} -\item {\tt exceptions} -\item {\tt firing-squad} -\item {\tt founify} -\item {\tt graphs} -\item {\tt higman-cf} -\item {\tt higman-nw} -\item {\tt hardware} -\item {\tt multiplier} -\item {\tt search-trees} -\item {\tt stalmarck} -\end{itemize} - -\noindent {\tt continuations} and {\tt multiplier} are a bit particular. They are -examples of developments where {\tt Obj.magic} are needed. This is -probably due to an heavy use of impredicativity. After compilation, those -two examples run nonetheless, thanks to the correction of the -extraction~\cite{Let02}. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex deleted file mode 100644 index 1401af10f..000000000 --- a/doc/refman/Nsatz.tex +++ /dev/null @@ -1,102 +0,0 @@ -\achapter{Nsatz: tactics for proving equalities in integral domains} -%HEVEA\cutname{nsatz.html} -\aauthor{Loïc Pottier} - -The tactic \texttt{nsatz} proves goals of the form - -\[ \begin{array}{l} - \forall X_1,\ldots,X_n \in A,\\ - P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) , \ldots , P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ - \vdash P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\ - \end{array} -\] -where $P,Q, P_1,Q_1,\ldots,P_s,Q_s$ are polynomials and A is an integral -domain, i.e. a commutative ring with no zero divisor. For example, A can be -$\mathbb{R}$, $\mathbb{Z}$, of $\mathbb{Q}$. Note that the equality $=$ used in these -goals can be any setoid equality -(see \ref{setoidtactics}) -, not only Leibnitz equality. - -It also proves formulas -\[ \begin{array}{l} - \forall X_1,\ldots,X_n \in A,\\ - P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) \wedge \ldots \wedge P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ - \rightarrow P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\ - \end{array} -\] doing automatic introductions. - -\asection{Using the basic tactic \texttt{nsatz}} -\tacindex{nsatz} - -Load the -\texttt{Nsatz} module: \texttt{Require Import Nsatz}.\\ - and use the tactic \texttt{nsatz}. - -\asection{More about \texttt{nsatz}} - -Hilbert's Nullstellensatz theorem shows how to reduce proofs of equalities on -polynomials on a commutative ring A with no zero divisor to algebraic computations: it is easy to see that if a polynomial -$P$ in $A[X_1,\ldots,X_n]$ verifies $c P^r = \sum_{i=1}^{s} S_i P_i$, with $c -\in A$, $c \not = 0$, $r$ a positive integer, and the $S_i$s in -$A[X_1,\ldots,X_n]$, then $P$ is zero whenever polynomials $P_1,...,P_s$ are -zero (the converse is also true when A is an algebraic closed field: -the method is complete). - -So, proving our initial problem can reduce into finding $S_1,\ldots,S_s$, $c$ -and $r$ such that $c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)$, which will be proved by the -tactic \texttt{ring}. - -This is achieved by the computation of a Groebner basis of the -ideal generated by $P_1-Q_1,...,P_s-Q_s$, with an adapted version of the Buchberger -algorithm. - -This computation is done after a step of {\em reification}, which is -performed using {\em Type Classes} -(see \ref{typeclasses}) -. - -The \texttt{Nsatz} module defines the tactic -\texttt{nsatz}, which can be used without arguments: \\ -\vspace*{3mm} -\texttt{nsatz}\\ -or with the syntax: \\ -\vspace*{3mm} -\texttt{nsatz with radicalmax:={\em number}\%N strategy:={\em number}\%Z parameters:={\em list of variables} variables:={\em list of variables}}\\ -where: - -\begin{itemize} - \item \texttt{radicalmax} is a bound when for searching r s.t.$c (P-Q)^r = -\sum_{i=1..s} S_i (P_i - Q_i)$ - - \item \texttt{strategy} gives the order on variables $X_1,...X_n$ and -the strategy used in Buchberger algorithm (see -\cite{sugar} for details): - - \begin{itemize} - \item strategy = 0: reverse lexicographic order and newest s-polynomial. - \item strategy = 1: reverse lexicographic order and sugar strategy. - \item strategy = 2: pure lexicographic order and newest s-polynomial. - \item strategy = 3: pure lexicographic order and sugar strategy. - \end{itemize} - - \item \texttt{parameters} is the list of variables -$X_{i_1},\ldots,X_{i_k}$ among $X_1,...,X_n$ which are considered as - parameters: computation will be performed with rational fractions in these - variables, i.e. polynomials are considered with coefficients in -$R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non -constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal -which states that $c$ is not zero. - - \item \texttt{variables} is the list of the variables -in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{variables} = {(@nil -R)}, then \texttt{lvar} is replaced by all the variables which are not in -parameters. - -\end{itemize} - -See file \texttt{Nsatz.v} for many examples, specially in geometry. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex deleted file mode 100644 index d9b8b8c52..000000000 --- a/doc/refman/Polynom.tex +++ /dev/null @@ -1,736 +0,0 @@ -\achapter{The \texttt{ring} and \texttt{field} tactic families} -%HEVEA\cutname{ring.html} -\aauthor{Bruno Barras, Benjamin Gr\'egoire, Assia - Mahboubi, Laurent Th\'ery\footnote{based on previous work from - Patrick Loiseleur and Samuel Boutin}} -\label{ring} -\tacindex{ring} - -This chapter presents the tactics dedicated to deal with ring and -field equations. - -\asection{What does this tactic do?} - -\texttt{ring} does associative-commutative rewriting in ring and semi-ring -structures. Assume you have two binary functions $\oplus$ and $\otimes$ -that are associative and commutative, with $\oplus$ distributive on -$\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and -$\otimes$. A \textit{polynomial} is an expression built on variables $V_0, V_1, -\dots$ and constants by application of $\oplus$ and $\otimes$. - -Let an {\it ordered product} be a product of variables $V_{i_1} -\otimes \ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le -i_n$. Let a \textit{monomial} be the product of a constant and an -ordered product. We can order the monomials by the lexicographic -order on products of variables. Let a \textit{canonical sum} be an -ordered sum of monomials that are all different, i.e. each monomial in -the sum is strictly less than the following monomial according to the -lexicographic order. It is an easy theorem to show that every -polynomial is equivalent (modulo the ring properties) to exactly one -canonical sum. This canonical sum is called the \textit{normal form} -of the polynomial. In fact, the actual representation shares monomials -with same prefixes. So what does \texttt{ring}? It normalizes -polynomials over any ring or semi-ring structure. The basic use of -\texttt{ring} is to simplify ring expressions, so that the user does -not have to deal manually with the theorems of associativity and -commutativity. - -\begin{Examples} -\item In the ring of integers, the normal form of -$x (3 + yx + 25(1 - z)) + zx$ is $28x + (-24)xz + xxy$. -\end{Examples} - -\texttt{ring} is also able to compute a normal form modulo monomial -equalities. For example, under the hypothesis that $2x^2 = yz+1$, - the normal form of $2(x + 1)x - x - zy$ is $x+1$. - -\asection{The variables map} - -It is frequent to have an expression built with + and - $\times$, but rarely on variables only. -Let us associate a number to each subterm of a ring -expression in the \gallina\ language. For example in the ring -\texttt{nat}, consider the expression: - -\begin{quotation} -\begin{verbatim} -(plus (mult (plus (f (5)) x) x) - (mult (if b then (4) else (f (3))) (2))) -\end{verbatim} -\end{quotation} - -\noindent As a ring expression, it has 3 subterms. Give each subterm a -number in an arbitrary order: - -\begin{tabular}{ccl} -0 & $\mapsto$ & \verb|if b then (4) else (f (3))| \\ -1 & $\mapsto$ & \verb|(f (5))| \\ -2 & $\mapsto$ & \verb|x| \\ -\end{tabular} - -\noindent Then normalize the ``abstract'' polynomial - -$$((V_1 \otimes V_2) \oplus V_2) \oplus (V_0 \otimes 2) $$ - -\noindent In our example the normal form is: - -$$(2 \otimes V_0) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2)$$ - -\noindent Then substitute the variables by their values in the variables map to -get the concrete normal polynomial: - -\begin{quotation} -\begin{verbatim} -(plus (mult (2) (if b then (4) else (f (3)))) - (plus (mult (f (5)) x) (mult x x))) -\end{verbatim} -\end{quotation} - -\asection{Is it automatic?} - -Yes, building the variables map and doing the substitution after -normalizing is automatically done by the tactic. So you can just forget -this paragraph and use the tactic according to your intuition. - -\asection{Concrete usage in \Coq -\tacindex{ring} -\tacindex{ring\_simplify}} - -The {\tt ring} tactic solves equations upon polynomial expressions of -a ring (or semi-ring) structure. It proceeds by normalizing both hand -sides of the equation (w.r.t. associativity, commutativity and -distributivity, constant propagation, rewriting of monomials) -and comparing syntactically the results. - -{\tt ring\_simplify} applies the normalization procedure described -above to the terms given. The tactic then replaces all occurrences of -the terms given in the conclusion of the goal by their normal -forms. If no term is given, then the conclusion should be an equation -and both hand sides are normalized. -The tactic can also be applied in a hypothesis. - -The tactic must be loaded by \texttt{Require Import Ring}. The ring -structures must be declared with the \texttt{Add Ring} command (see -below). The ring of booleans is predefined; if one wants to use the -tactic on \texttt{nat} one must first require the module -\texttt{ArithRing} (exported by \texttt{Arith}); -for \texttt{Z}, do \texttt{Require Import -ZArithRing} or simply \texttt{Require Import ZArith}; -for \texttt{N}, do \texttt{Require Import NArithRing} or -\texttt{Require Import NArith}. - -\Example -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example*} -Require Import ZArith. -\end{coq_example*} -\begin{coq_example} -Open Scope Z_scope. -Goal forall a b c:Z, - (a + b + c)^2 = - a * a + b^2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c. -\end{coq_example} -\begin{coq_example} -intros; ring. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} -\begin{coq_example} -Goal forall a b:Z, 2*a*b = 30 -> - (a+b)^2 = a^2 + b^2 + 30. -\end{coq_example} -\begin{coq_example} -intros a b H; ring [H]. -\end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{Variants} - \item {\tt ring [\term$_1$ {\ldots} \term$_n$]} decides the equality of two - terms modulo ring operations and rewriting of the equalities - defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$ - {\ldots} \term$_n$ has to be a proof of some equality $m = p$, - where $m$ is a monomial (after ``abstraction''), - $p$ a polynomial and $=$ the corresponding equality of the ring structure. - - \item {\tt ring\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1 \ldots t_m$ in -{\ident}} - performs the simplification in the hypothesis named {\tt ident}. -\end{Variants} - -\Warning \texttt{ring\_simplify \term$_1$; ring\_simplify \term$_2$} is -not equivalent to \texttt{ring\_simplify \term$_1$ \term$_2$}. In the -latter case the variables map is shared between the two terms, and -common subterm $t$ of \term$_1$ and \term$_2$ will have the same -associated variable number. So the first alternative should be -avoided for terms belonging to the same ring theory. - - -\begin{ErrMsgs} -\item \errindex{not a valid ring equation} - The conclusion of the goal is not provable in the corresponding ring - theory. -\item \errindex{arguments of ring\_simplify do not have all the same type} - {\tt ring\_simplify} cannot simplify terms of several rings at the - same time. Invoke the tactic once per ring structure. -\item \errindex{cannot find a declared ring structure over {\tt term}} - No ring has been declared for the type of the terms to be - simplified. Use {\tt Add Ring} first. -\item \errindex{cannot find a declared ring structure for equality - {\tt term}} - Same as above is the case of the {\tt ring} tactic. -\end{ErrMsgs} - -\asection{Adding a ring structure -\comindex{Add Ring}} - -Declaring a new ring consists in proving that a ring signature (a -carrier set, an equality, and ring operations: {\tt -Ring\_theory.ring\_theory} and {\tt Ring\_theory.semi\_ring\_theory}) -satisfies the ring axioms. Semi-rings (rings without $+$ inverse) are -also supported. The equality can be either Leibniz equality, or any -relation declared as a setoid (see~\ref{setoidtactics}). The definition -of ring and semi-rings (see module {\tt Ring\_theory}) is: -\begin{verbatim} -Record ring_theory : Prop := mk_rt { - Radd_0_l : forall x, 0 + x == x; - Radd_sym : forall x y, x + y == y + x; - Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; - Rmul_1_l : forall x, 1 * x == x; - Rmul_sym : forall x y, x * y == y * x; - Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; - Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); - Rsub_def : forall x y, x - y == x + -y; - Ropp_def : forall x, x + (- x) == 0 -}. - -Record semi_ring_theory : Prop := mk_srt { - SRadd_0_l : forall n, 0 + n == n; - SRadd_sym : forall n m, n + m == m + n ; - SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; - SRmul_1_l : forall n, 1*n == n; - SRmul_0_l : forall n, 0*n == 0; - SRmul_sym : forall n m, n*m == m*n; - SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; - SRdistr_l : forall n m p, (n + m)*p == n*p + m*p -}. -\end{verbatim} - -This implementation of {\tt ring} also features a notion of constant -that can be parameterized. This can be used to improve the handling of -closed expressions when operations are effective. It consists in -introducing a type of \emph{coefficients} and an implementation of the -ring operations, and a morphism from the coefficient type to the ring -carrier type. The morphism needs not be injective, nor surjective. - -As -an example, one can consider the real numbers. The set of coefficients -could be the rational numbers, upon which the ring operations can be -implemented. The fact that there exists a morphism is defined by the -following properties: -\begin{verbatim} -Record ring_morph : Prop := mkmorph { - morph0 : [cO] == 0; - morph1 : [cI] == 1; - morph_add : forall x y, [x +! y] == [x]+[y]; - morph_sub : forall x y, [x -! y] == [x]-[y]; - morph_mul : forall x y, [x *! y] == [x]*[y]; - morph_opp : forall x, [-!x] == -[x]; - morph_eq : forall x y, x?=!y = true -> [x] == [y] -}. - -Record semi_morph : Prop := mkRmorph { - Smorph0 : [cO] == 0; - Smorph1 : [cI] == 1; - Smorph_add : forall x y, [x +! y] == [x]+[y]; - Smorph_mul : forall x y, [x *! y] == [x]*[y]; - Smorph_eq : forall x y, x?=!y = true -> [x] == [y] -}. -\end{verbatim} -where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set, -{\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring -operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is -an implementation of this equality, and {\tt [x]} is a notation for -the image of {\tt x} by the ring morphism. - - - -Since {\tt Z} is an initial ring (and {\tt N} is an initial -semi-ring), it can always be considered as a set of -coefficients. There are basically three kinds of (semi-)rings: -\begin{description} -\item[abstract rings] to be used when operations are not - effective. The set of coefficients is {\tt Z} (or {\tt N} for - semi-rings). -\item[computational rings] to be used when operations are - effective. The set of coefficients is the ring itself. The user only - has to provide an implementation for the equality. -\item[customized ring] for other cases. The user has to provide the - coefficient set and the morphism. -\end{description} - -This implementation of ring can also recognize simple -power expressions as ring expressions. A power function is specified by -the following property: -\begin{verbatim} -Section POWER. - Variable Cpow : Set. - Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. - - Record power_theory : Prop := mkpow_th { - rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) - }. - -End POWER. -\end{verbatim} - - -The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$ -($mod_1$,\dots,$mod_2$)}. The name is not relevant. It is just used -for error messages. The term $ring$ is a proof that the ring signature -satisfies the (semi-)ring axioms. The optional list of modifiers is -used to tailor the behavior of the tactic. The following list -describes their syntax and effects: -\begin{description} -\item[abstract] declares the ring as abstract. This is the default. -\item[decidable \term] declares the ring as computational. The expression - \term{} is - the correctness proof of an equality test {\tt ?=!} (which should be - evaluable). Its type should be of - the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}. -\item[morphism \term] declares the ring as a customized one. The expression - \term{} is - a proof that there exists a morphism between a set of coefficient - and the ring carrier (see {\tt Ring\_theory.ring\_morph} and {\tt - Ring\_theory.semi\_morph}). -\item[setoid \term$_1$ \term$_2$] forces the use of given setoid. The - expression \term$_1$ is a proof that the equality is indeed a setoid - (see {\tt Setoid.Setoid\_Theory}), and \term$_2$ a proof that the - ring operations are morphisms (see {\tt Ring\_theory.ring\_eq\_ext} and - {\tt Ring\_theory.sring\_eq\_ext}). This modifier needs not be used if the - setoid and morphisms have been declared. -\item[constants [\ltac]] specifies a tactic expression that, given a term, - returns either an object of the coefficient set that is mapped to - the expression via the morphism, or returns {\tt - InitialRing.NotConstant}. The default behavior is to map only 0 and - 1 to their counterpart in the coefficient set. This is generally not - desirable for non trivial computational rings. -\item[preprocess [\ltac]] - specifies a tactic that is applied as a preliminary step for {\tt - ring} and {\tt ring\_simplify}. It can be used to transform a goal - so that it is better recognized. For instance, {\tt S n} can be - changed to {\tt plus 1 n}. -\item[postprocess [\ltac]] specifies a tactic that is applied as a final step - for {\tt ring\_simplify}. For instance, it can be used to undo - modifications of the preprocessor. -\item[power\_tac {\term} [\ltac]] allows {\tt ring} and {\tt ring\_simplify} to - recognize power expressions with a constant positive integer exponent - (example: $x^2$). The term {\term} is a proof that a given power function - satisfies the specification of a power function ({\term} has to be a - proof of {\tt Ring\_theory.power\_theory}) and {\ltac} specifies a - tactic expression that, given a term, ``abstracts'' it into an - object of type {\tt N} whose interpretation via {\tt Cp\_phi} (the - evaluation function of power coefficient) is the original term, or - returns {\tt InitialRing.NotConstant} if not a constant coefficient - (i.e. {\ltac} is the inverse function of {\tt Cp\_phi}). - See files {\tt plugins/setoid\_ring/ZArithRing.v} and - {\tt plugins/setoid\_ring/RealField.v} for examples. - By default the tactic does not recognize power expressions as ring - expressions. -\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation - when outputting its normal form, i.e writing $x - y$ instead of $x + (-y)$. - The term {\term} is a proof that a given sign function indicates expressions - that are signed ({\term} has to be a - proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/InitialRing.v} for examples of sign function. -\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use monomials -with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function satisfies the specification of an euclidean - division function ({\term} has to be a - proof of {\tt Ring\_theory.div\_theory}). For example, this function is - called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$. - See {\tt plugins/setoid\_ring/InitialRing.v} for examples of div function. - -\end{description} - - -\begin{ErrMsgs} -\item \errindex{bad ring structure} - The proof of the ring structure provided is not of the expected type. -\item \errindex{bad lemma for decidability of equality} - The equality function provided in the case of a computational ring - has not the expected type. -\item \errindex{ring {\it operation} should be declared as a morphism} - A setoid associated to the carrier of the ring structure as been - found, but the ring operation should be declared as - morphism. See~\ref{setoidtactics}. -\end{ErrMsgs} - -\asection{How does it work?} - -The code of \texttt{ring} is a good example of tactic written using -\textit{reflection}. What is reflection? Basically, it is writing -\Coq{} tactics in \Coq, rather than in \ocaml. From the philosophical -point of view, it is using the ability of the Calculus of -Constructions to speak and reason about itself. For the \texttt{ring} -tactic we used \Coq\ as a programming language and also as a proof -environment to build a tactic and to prove it correctness. - -The interested reader is strongly advised to have a look at the file -\texttt{Ring\_polynom.v}. Here a type for polynomials is defined: - -\begin{small} -\begin{flushleft} -\begin{verbatim} -Inductive PExpr : Type := - | PEc : C -> PExpr - | PEX : positive -> PExpr - | PEadd : PExpr -> PExpr -> PExpr - | PEsub : PExpr -> PExpr -> PExpr - | PEmul : PExpr -> PExpr -> PExpr - | PEopp : PExpr -> PExpr - | PEpow : PExpr -> N -> PExpr. -\end{verbatim} -\end{flushleft} -\end{small} - -Polynomials in normal form are defined as: -\begin{small} -\begin{flushleft} -\begin{verbatim} -Inductive Pol : Type := - | Pc : C -> Pol - | Pinj : positive -> Pol -> Pol - | PX : Pol -> positive -> Pol -> Pol. -\end{verbatim} -\end{flushleft} -\end{small} -where {\tt Pinj n P} denotes $P$ in which $V_i$ is replaced by -$V_{i+n}$, and {\tt PX P n Q} denotes $P \otimes V_1^{n} \oplus Q'$, -$Q'$ being $Q$ where $V_i$ is replaced by $V_{i+1}$. - - -Variables maps are represented by list of ring elements, and two -interpretation functions, one that maps a variables map and a -polynomial to an element of the concrete ring, and the second one that -does the same for normal forms: -\begin{small} -\begin{flushleft} -\begin{verbatim} -Definition PEeval : list R -> PExpr -> R := [...]. -Definition Pphi_dev : list R -> Pol -> R := [...]. -\end{verbatim} -\end{flushleft} -\end{small} - -A function to normalize polynomials is defined, and the big theorem is -its correctness w.r.t interpretation, that is: - -\begin{small} -\begin{flushleft} -\begin{verbatim} -Definition norm : PExpr -> Pol := [...]. -Lemma Pphi_dev_ok : - forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. -\end{verbatim} -\end{flushleft} -\end{small} - -So now, what is the scheme for a normalization proof? Let \texttt{p} -be the polynomial expression that the user wants to normalize. First a -little piece of ML code guesses the type of \texttt{p}, the ring -theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a -variables map \texttt{v} such that \texttt{p} is -$\beta\delta\iota$-equivalent to \verb|(PEeval v ap)|. Then we -replace it by \verb|(Pphi_dev v (norm ap))|, using the -main correctness theorem and we reduce it to a concrete expression -\texttt{p'}, which is the concrete normal form of -\texttt{p}. This is summarized in this diagram: -\begin{center} -\begin{tabular}{rcl} -\texttt{p} & $\rightarrow_{\beta\delta\iota}$ - & \texttt{(PEeval v ap)} \\ - & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\ -\texttt{p'} - & $\leftarrow_{\beta\delta\iota}$ - & \texttt{(Pphi\_dev v (norm ap))} -\end{tabular} -\end{center} -The user do not see the right part of the diagram. -From outside, the tactic behaves like a -$\beta\delta\iota$ simplification extended with AC rewriting rules. -Basically, the proof is only the application of the main -correctness theorem to well-chosen arguments. - - -\asection{Dealing with fields -\tacindex{field} -\tacindex{field\_simplify} -\tacindex{field\_simplify\_eq}} - - -The {\tt field} tactic is an extension of the {\tt ring} to deal with -rational expression. Given a rational expression $F=0$. It first reduces the -expression $F$ to a common denominator $N/D= 0$ where $N$ and $D$ are two ring -expressions. -For example, if we take $F = (1 - 1/x) x - x + 1$, this gives -$ N= (x -1) x - x^2 + x$ and $D= x$. It then calls {\tt ring} -to solve $N=0$. Note that {\tt field} also generates non-zero conditions -for all the denominators it encounters in the reduction. -In our example, it generates the condition $x \neq 0$. These -conditions appear as one subgoal which is a conjunction if there are -several denominators. -Non-zero conditions are {\it always} polynomial expressions. For example -when reducing the expression $1/(1 + 1/x)$, two side conditions are -generated: $x\neq 0$ and $x + 1 \neq 0$. Factorized expressions are -broken since a field is an integral domain, and when the equality test -on coefficients is complete w.r.t. the equality of the target field, -constants can be proven different from zero automatically. - -The tactic must be loaded by \texttt{Require Import Field}. New field -structures can be declared to the system with the \texttt{Add Field} -command (see below). The field of real numbers is defined in module -\texttt{RealField} (in texttt{plugins/setoid\_ring}). It is exported -by module \texttt{Rbase}, so that requiring \texttt{Rbase} or -\texttt{Reals} is enough to use the field tactics on real -numbers. Rational numbers in canonical form are also declared as a -field in module \texttt{Qcanon}. - - -\Example -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example*} -Require Import Reals. -\end{coq_example*} -\begin{coq_example} -Open Scope R_scope. -Goal forall x, x <> 0 -> - (1 - 1/x) * x - x + 1 = 0. -\end{coq_example} -\begin{coq_example} -intros; field; auto. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} -\begin{coq_example} -Goal forall x y, y <> 0 -> y = x -> x/y = 1. -\end{coq_example} -\begin{coq_example} -intros x y H H1; field [H1]; auto. -\end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{Variants} - \item {\tt field [\term$_1$ {\ldots} \term$_n$]} decides the equality of two - terms modulo field operations and rewriting of the equalities - defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$ - {\ldots} \term$_n$ has to be a proof of some equality $m = p$, - where $m$ is a monomial (after ``abstraction''), - $p$ a polynomial and $=$ the corresponding equality of the field structure. - Beware that rewriting works with the equality $m=p$ only if $p$ is a - polynomial since rewriting is handled by the underlying {\tt ring} - tactic. - \item {\tt field\_simplify} - performs the simplification in the conclusion of the goal, $F_1 = F_2$ - becomes $N_1/D_1 = N_2/D_2$. A normalization step (the same as the - one for rings) is then applied to $N_1$, $D_1$, $N_2$ and - $D_2$. This way, polynomials remain in factorized form during the - fraction simplifications. This yields smaller expressions when - reducing to the same denominator since common factors can be - canceled. - - \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$]} - performs the simplification in the conclusion of the goal using - the equalities - defined by \term$_1$ {\ldots} \term$_n$. - - \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots -$t_m$} - performs the simplification in the terms $t_1$ \ldots $t_m$ - of the conclusion of the goal using - the equalities - defined by \term$_1$ {\ldots} \term$_n$. - - \item {\tt field\_simplify in $H$} - performs the simplification in the assumption $H$. - - \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] in $H$} - performs the simplification in the assumption $H$ using - the equalities - defined by \term$_1$ {\ldots} \term$_n$. - - \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots -$t_m$ in $H$} - performs the simplification in the terms $t_1$ \ldots $t_n$ - of the assumption $H$ using - the equalities - defined by \term$_1$ {\ldots} \term$_m$. - - \item {\tt field\_simplify\_eq} - performs the simplification in the conclusion of the goal removing - the denominator. $F_1 = F_2$ - becomes $N_1 D_2 = N_2 D_1$. - - \item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$]} - performs the simplification in the conclusion of the goal using - the equalities - defined by \term$_1$ {\ldots} \term$_n$. - - \item {\tt field\_simplify\_eq} in $H$ - performs the simplification in the assumption $H$. - - \item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$] in $H$} - performs the simplification in the assumption $H$ using - the equalities - defined by \term$_1$ {\ldots} \term$_n$. -\end{Variants} - -\asection{Adding a new field structure -\comindex{Add Field}} - -Declaring a new field consists in proving that a field signature (a -carrier set, an equality, and field operations: {\tt -Field\_theory.field\_theory} and {\tt Field\_theory.semi\_field\_theory}) -satisfies the field axioms. Semi-fields (fields without $+$ inverse) are -also supported. The equality can be either Leibniz equality, or any -relation declared as a setoid (see~\ref{setoidtactics}). The definition -of fields and semi-fields is: -\begin{verbatim} -Record field_theory : Prop := mk_field { - F_R : ring_theory rO rI radd rmul rsub ropp req; - F_1_neq_0 : ~ 1 == 0; - Fdiv_def : forall p q, p / q == p * / q; - Finv_l : forall p, ~ p == 0 -> / p * p == 1 -}. - -Record semi_field_theory : Prop := mk_sfield { - SF_SR : semi_ring_theory rO rI radd rmul req; - SF_1_neq_0 : ~ 1 == 0; - SFdiv_def : forall p q, p / q == p * / q; - SFinv_l : forall p, ~ p == 0 -> / p * p == 1 -}. -\end{verbatim} - -The result of the normalization process is a fraction represented by -the following type: -\begin{verbatim} -Record linear : Type := mk_linear { - num : PExpr C; - denum : PExpr C; - condition : list (PExpr C) -}. -\end{verbatim} -where {\tt num} and {\tt denum} are the numerator and denominator; -{\tt condition} is a list of expressions that have appeared as a -denominator during the normalization process. These expressions must -be proven different from zero for the correctness of the algorithm. - -The syntax for adding a new field is {\tt Add Field $name$ : $field$ -($mod_1$,\dots,$mod_2$)}. The name is not relevant. It is just used -for error messages. $field$ is a proof that the field signature -satisfies the (semi-)field axioms. The optional list of modifiers is -used to tailor the behavior of the tactic. Since field tactics are -built upon ring tactics, all modifiers of the {\tt Add Ring} -apply. There is only one specific modifier: -\begin{description} -\item[completeness \term] allows the field tactic to prove - automatically that the image of non-zero coefficients are mapped to - non-zero elements of the field. \term is a proof of {\tt forall x y, - [x] == [y] -> x?=!y = true}, which is the completeness of equality - on coefficients w.r.t. the field equality. -\end{description} - -\asection{History of \texttt{ring}} - -First Samuel Boutin designed the tactic \texttt{ACDSimpl}. -This tactic did lot of rewriting. But the proofs -terms generated by rewriting were too big for \Coq's type-checker. -Let us see why: - -\begin{coq_eval} -Require Import ZArith. -Open Scope Z_scope. -\end{coq_eval} -\begin{coq_example} -Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y. -\end{coq_example} -\begin{coq_example*} -intros; rewrite (Z.mul_comm y z); reflexivity. -Save toto. -\end{coq_example*} -\begin{coq_example} -Print toto. -\end{coq_example} - -At each step of rewriting, the whole context is duplicated in the proof -term. Then, a tactic that does hundreds of rewriting generates huge proof -terms. Since \texttt{ACDSimpl} was too slow, Samuel Boutin rewrote it -using reflection (see his article in TACS'97 \cite{Bou97}). Later, the -stuff was rewritten by Patrick -Loiseleur: the new tactic does not any more require \texttt{ACDSimpl} -to compile and it makes use of $\beta\delta\iota$-reduction -not only to replace the rewriting steps, but also to achieve the -interleaving of computation and -reasoning (see \ref{DiscussReflection}). He also wrote a -few ML code for the \texttt{Add Ring} command, that allow to register -new rings dynamically. - -Proofs terms generated by \texttt{ring} are quite small, they are -linear in the number of $\oplus$ and $\otimes$ operations in the -normalized terms. Type-checking those terms requires some time because it -makes a large use of the conversion rule, but -memory requirements are much smaller. - -\asection{Discussion} -\label{DiscussReflection} - -Efficiency is not the only motivation to use reflection -here. \texttt{ring} also deals with constants, it rewrites for example the -expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the -tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the -expression $34 + 2*(x - 1) + 12$ is interpreted as -$V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3$, -with the variables mapping -$\{V_0 \mt 34; V_1 \mt 2; V_2 \mt x; V_3 \mt 12 \}$. Then it is -rewritten to $34 - x + 2*x + 12$, very far from the expected -result. Here rewriting is not sufficient: you have to do some kind of -reduction (some kind of \textit{computation}) to achieve the -normalization. - -The tactic \texttt{ring} is not only faster than a classical one: -using reflection, we get for free integration of computation and -reasoning that would be very complex to implement in the classic fashion. - -Is it the ultimate way to write tactics? The answer is: yes and -no. The \texttt{ring} tactic uses intensively the conversion rule of -\CIC, that is replaces proof by computation the most as it is -possible. It can be useful in all situations where a classical tactic -generates huge proof terms. Symbolic Processing and Tautologies are in -that case. But there are also tactics like \texttt{auto} or -\texttt{linear} that do many complex computations, using side-effects -and backtracking, and generate a small proof term. Clearly, it would -be significantly less efficient to replace them by tactics using -reflection. - -Another idea suggested by Benjamin Werner: reflection could be used to -couple an external tool (a rewriting program or a model checker) with -\Coq. We define (in \Coq) a type of terms, a type of \emph{traces}, -and prove a correction theorem that states that \emph{replaying -traces} is safe w.r.t some interpretation. Then we let the external -tool do every computation (using side-effects, backtracking, -exception, or others features that are not available in pure lambda -calculus) to produce the trace: now we can check in Coq{} that the -trace has the expected semantic by applying the correction lemma. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex deleted file mode 100644 index 1e204dc83..000000000 --- a/doc/refman/Program.tex +++ /dev/null @@ -1,329 +0,0 @@ -\achapter{\Program{}} -%HEVEA\cutname{program.html} -\label{Program} -\aauthor{Matthieu Sozeau} -\index{Program} - -We present here the \Program\ tactic commands, used to build certified -\Coq\ programs, elaborating them from their algorithmic skeleton and a -rich specification \cite{Sozeau06}. It can be thought of as a dual of extraction -(see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular -functional programming language whilst using as rich a specification as -desired and proving that the code meets the specification using the whole \Coq{} proof -apparatus. This is done using a technique originating from the -``Predicate subtyping'' mechanism of \PVS \cite{Rushby98}, which generates type-checking -conditions while typing a term constrained to a particular type. -Here we insert existential variables in the term, which must be filled -with proofs to get a complete \Coq\ term. \Program\ replaces the -\Program\ tactic by Catherine Parent \cite{Parent95b} which had a similar goal but is no longer -maintained. - -The languages available as input are currently restricted to \Coq's term -language, but may be extended to \ocaml{}, \textsc{Haskell} and others -in the future. We use the same syntax as \Coq\ and permit to use implicit -arguments and the existing coercion mechanism. -Input terms and types are typed in an extended system (\Russell) and -interpreted into \Coq\ terms. The interpretation process may produce -some proof obligations which need to be resolved to create the final term. - -\asection{Elaborating programs} -The main difference from \Coq\ is that an object in a type $T : \Set$ -can be considered as an object of type $\{ x : T~|~P\}$ for any -wellformed $P : \Prop$. -If we go from $T$ to the subset of $T$ verifying property $P$, we must -prove that the object under consideration verifies it. \Russell\ will -generate an obligation for every such coercion. In the other direction, -\Russell\ will automatically insert a projection. - -Another distinction is the treatment of pattern-matching. Apart from the -following differences, it is equivalent to the standard {\tt match} -operation (see Section~\ref{Caseexpr}). -\begin{itemize} -\item Generation of equalities. A {\tt match} expression is always - generalized by the corresponding equality. As an example, - the expression: - -\begin{verbatim} - match x with - | 0 => t - | S n => u - end. -\end{verbatim} -will be first rewritten to: -\begin{verbatim} - (match x as y return (x = y -> _) with - | 0 => fun H : x = 0 -> t - | S n => fun H : x = S n -> u - end) (eq_refl n). -\end{verbatim} - - This permits to get the proper equalities in the context of proof - obligations inside clauses, without which reasoning is very limited. - -\item Generation of inequalities. If a pattern intersects with a - previous one, an inequality is added in the context of the second - branch. See for example the definition of {\tt div2} below, where the second - branch is typed in a context where $\forall p, \_ <> S (S p)$. - -\item Coercion. If the object being matched is coercible to an inductive - type, the corresponding coercion will be automatically inserted. This also - works with the previous mechanism. - -\end{itemize} - -There are options to control the generation of equalities -and coercions. - -\begin{itemize} -\item {\tt Unset Program Cases}\optindex{Program Cases} This deactivates - the special treatment of pattern-matching generating equalities and - inequalities when using \Program\ (it is on by default). All - pattern-matchings and let-patterns are handled using the standard - algorithm of Coq (see Section~\ref{Mult-match-full}) when this option is - deactivated. -\item {\tt Unset Program Generalized Coercion}\optindex{Program - Generalized Coercion} This deactivates the coercion of general - inductive types when using \Program\ (the option is on by default). - Coercion of subset types and pairs is still active in this case. -\end{itemize} - -\subsection{Syntactic control over equalities} -\label{ProgramSyntax} -To give more control over the generation of equalities, the typechecker will -fall back directly to \Coq's usual typing of dependent pattern-matching -if a {\tt return} or {\tt in} clause is specified. Likewise, -the {\tt if} construct is not treated specially by \Program{} so boolean -tests in the code are not automatically reflected in the obligations. -One can use the {\tt dec} combinator to get the correct hypotheses as in: - -\begin{coq_eval} -Require Import Program Arith. -\end{coq_eval} -\begin{coq_example} -Program Definition id (n : nat) : { x : nat | x = n } := - if dec (leb n 0) then 0 - else S (pred n). -\end{coq_example} - -The let tupling construct {\tt let (x1, ..., xn) := t in b} -does not produce an equality, contrary to the let pattern construct -{\tt let '(x1, ..., xn) := t in b}. -Also, {\tt {\term}:>} explicitly asks the system to coerce {\tt \term} to its -support type. It can be useful in notations, for example: -\begin{coq_example} -Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). -\end{coq_example} - -This notation denotes equality on subset types using equality on their -support types, avoiding uses of proof-irrelevance that would come up -when reasoning with equality on the subset types themselves. - -The next two commands are similar to their standard counterparts -Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that -they define constants. However, they may require the user to prove some -goals to construct the final definitions. - -\subsection{\tt Program Definition {\ident} := {\term}. - \comindex{Program Definition}\label{ProgramDefinition}} - -This command types the value {\term} in \Russell\ and generates proof -obligations. Once solved using the commands shown below, it binds the final -\Coq\ term to the name {\ident} in the environment. - -\begin{ErrMsgs} -\item \errindex{{\ident} already exists} -\end{ErrMsgs} - -\begin{Variants} -\item {\tt Program Definition {\ident} {\tt :}{\term$_1$} := - {\term$_2$}.}\\ - It interprets the type {\term$_1$}, potentially generating proof - obligations to be resolved. Once done with them, we have a \Coq\ type - {\term$_1'$}. It then checks that the type of the interpretation of - {\term$_2$} is coercible to {\term$_1'$}, and registers {\ident} as - being of type {\term$_1'$} once the set of obligations generated - during the interpretation of {\term$_2$} and the aforementioned - coercion derivation are solved. -\item {\tt Program Definition {\ident} {\binder$_1$}\ldots{\binder$_n$} - {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\ - This is equivalent to \\ - {\tt Program Definition\,{\ident}\,{\tt :\,forall} % - {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}} \\ - \qquad {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,% - {\tt .} -\end{Variants} - -\begin{ErrMsgs} -\item \errindex{In environment {\dots} the term: {\term$_2$} does not have type - {\term$_1$}}.\\ - \texttt{Actually, it has type {\term$_3$}}. -\end{ErrMsgs} - -\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold} - -\subsection{\tt Program Fixpoint {\ident} {\params} {\tt \{order\}} : type := \term - \comindex{Program Fixpoint} - \label{ProgramFixpoint}} - -The structural fixpoint operator behaves just like the one of Coq -(see Section~\ref{Fixpoint}), except it may also generate obligations. -It works with mutually recursive definitions too. - -\begin{coq_eval} -Admit Obligations. -\end{coq_eval} -\begin{coq_example} -Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := - match n with - | S (S p) => S (div2 p) - | _ => O - end. -\end{coq_example} - -Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are -automatically generated by the pattern-matching compilation algorithm). -\begin{coq_example} - Obligation 1. -\end{coq_example} - -One can use a well-founded order or a measure as termination orders using the syntax: -\begin{coq_eval} -Reset Initial. -Require Import Arith. -Require Import Program. -\end{coq_eval} -\begin{coq_example*} -Program Fixpoint div2 (n : nat) {measure n} : - { x : nat | n = 2 * x \/ n = 2 * x + 1 } := - match n with - | S (S p) => S (div2 p) - | _ => O - end. -\end{coq_example*} - -The order annotation can be either: -\begin{itemize} -\item {\tt measure f (R)?} where {\tt f} is a value of type {\tt X} - computed on any subset of the arguments and the optional - (parenthesised) term {\tt (R)} is a relation - on {\tt X}. By default {\tt X} defaults to {\tt nat} and {\tt R} to - {\tt lt}. -\item {\tt wf R x} which is equivalent to {\tt measure x (R)}. -\end{itemize} - -\paragraph{Caution} -When defining structurally recursive functions, the -generated obligations should have the prototype of the currently defined functional -in their context. In this case, the obligations should be transparent -(e.g. defined using {\tt Defined}) so that the guardedness condition on -recursive calls can be checked by the -kernel's type-checker. There is an optimization in the generation of -obligations which gets rid of the hypothesis corresponding to the -functional when it is not necessary, so that the obligation can be -declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the -context, the proof of the obligation is \emph{required} to be declared transparent. - -No such problems arise when using measures or well-founded recursion. - -\subsection{\tt Program Lemma {\ident} : type. - \comindex{Program Lemma} - \label{ProgramLemma}} - -The \Russell\ language can also be used to type statements of logical -properties. It will generate obligations, try to solve them -automatically and fail if some unsolved obligations remain. -In this case, one can first define the lemma's -statement using {\tt Program Definition} and use it as the goal afterwards. -Otherwise the proof will be started with the elaborated version as a goal. -The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt - Hypothesis}, {\tt Axiom} etc... - -\section{Solving obligations} -The following commands are available to manipulate obligations. The -optional identifier is used when multiple functions have unsolved -obligations (e.g. when defining mutually recursive blocks). The optional -tactic is replaced by the default one if not specified. - -\begin{itemize} -\item {\tt [Local|Global] Obligation Tactic := \tacexpr}\comindex{Obligation Tactic} - Sets the default obligation - solving tactic applied to all obligations automatically, whether to - solve them or when starting to prove one, e.g. using {\tt Next}. - Local makes the setting last only for the current module. Inside - sections, local is the default. -\item {\tt Show Obligation Tactic}\comindex{Show Obligation Tactic} - Displays the current default tactic. -\item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining - obligations. -\item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of - obligation {\tt num}. -\item {\tt Next Obligation [of \ident]}\comindex{Next Obligation} Start the proof of the next - unsolved obligation. -\item {\tt Solve Obligations [of \ident] [with - \tacexpr]}\comindex{Solve Obligations} - Tries to solve - each obligation of \ident using the given tactic or the default one. -\item {\tt Solve All Obligations [with \tacexpr]} Tries to solve - each obligation of every program using the given tactic or the default - one (useful for mutually recursive definitions). -\item {\tt Admit Obligations [of \ident]}\comindex{Admit Obligations} - Admits all obligations (does not work with structurally recursive programs). -\item {\tt Preterm [of \ident]}\comindex{Preterm} - Shows the term that will be fed to - the kernel once the obligations are solved. Useful for debugging. -\item {\tt Set Transparent Obligations}\optindex{Transparent Obligations} - Control whether all obligations should be declared as transparent (the - default), or if the system should infer which obligations can be declared opaque. -\item {\tt Set Hide Obligations}\optindex{Hide Obligations} - Control whether obligations appearing in the term should be hidden - as implicit arguments of the special constant - \texttt{Program.Tactics.obligation}. -\item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} -\emph{Deprecated since 8.7} - This option (on by default) controls whether obligations should have their - context minimized to the set of variables used in the proof of the - obligation, to avoid unnecessary dependencies. -\end{itemize} - -The module {\tt Coq.Program.Tactics} defines the default tactic for solving -obligations called {\tt program\_simpl}. Importing -{\tt Coq.Program.Program} also adds some useful notations, as documented in the file itself. - -\section{Frequently Asked Questions - \label{ProgramFAQ}} - -\begin{itemize} -\item {Ill-formed recursive definitions} - This error can happen when one tries to define a - function by structural recursion on a subset object, which means the Coq - function looks like: - - \verb$Program Fixpoint f (x : A | P) := match x with A b => f b end.$ - - Supposing $b : A$, the argument at the recursive call to f is not a - direct subterm of x as b is wrapped inside an {\tt exist} constructor to build - an object of type \verb${x : A | P}$. Hence the definition is rejected - by the guardedness condition checker. However one can use - wellfounded recursion on subset objects like this: - -\begin{verbatim} -Program Fixpoint f (x : A | P) { measure (size x) } := - match x with A b => f b end. -\end{verbatim} - - One will then just have to prove that the measure decreases at each recursive - call. There are three drawbacks though: - \begin{enumerate} - \item A measure function has to be defined; - \item The reduction is a little more involved, although it works well - using lazy evaluation; - \item Mutual recursion on the underlying inductive type isn't possible - anymore, but nested mutual recursion is always possible. - \end{enumerate} -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% compile-command: "BIBINPUTS=\".\" make QUICK=1 -C ../.. doc/refman/Reference-Manual.pdf" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 7ce28ccf8..cfb3c625b 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,12 +117,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{Coercion.v}% -\include{Extraction.v}% -\include{Program.v}% -\include{Polynom.v}% = Ring -\include{Nsatz.v}% -\include{Setoid.v}% Tactique pour les setoides \include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes \include{Misc.v} diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex deleted file mode 100644 index b7b343112..000000000 --- a/doc/refman/Setoid.tex +++ /dev/null @@ -1,842 +0,0 @@ -\newtheorem{cscexample}{Example} - -\achapter{\protect{Generalized rewriting}} -%HEVEA\cutname{setoid.html} -\aauthor{Matthieu Sozeau} -\label{setoids} - -This chapter presents the extension of several equality related tactics -to work over user-defined structures (called setoids) that are equipped -with ad-hoc equivalence relations meant to behave as equalities. -Actually, the tactics have also been generalized to relations weaker -then equivalences (e.g. rewriting systems). The toolbox also extends the -automatic rewriting capabilities of the system, allowing the specification of -custom strategies for rewriting. - -This documentation is adapted from the previous setoid documentation by -Claudio Sacerdoti Coen (based on previous work by Cl\'ement Renard). -The new implementation is a drop-in replacement for the old one,\footnote{Nicolas -Tabareau helped with the gluing.} hence most of the documentation still applies. - -The work is a complete rewrite of the previous implementation, based on -the type class infrastructure. It also improves on and generalizes -the previous implementation in several ways: -\begin{itemize} -\item User-extensible algorithm. The algorithm is separated in two - parts: generations of the rewriting constraints (done in ML) and - solving of these constraints using type class resolution. As type - class resolution is extensible using tactics, this allows users to define - general ways to solve morphism constraints. -\item Sub-relations. An example extension to the base algorithm is the - ability to define one relation as a subrelation of another so that - morphism declarations on one relation can be used automatically for - the other. This is done purely using tactics and type class search. -\item Rewriting under binders. It is possible to rewrite under binders - in the new implementation, if one provides the proper - morphisms. Again, most of the work is handled in the tactics. -\item First-class morphisms and signatures. Signatures and morphisms are - ordinary Coq terms, hence they can be manipulated inside Coq, put - inside structures and lemmas about them can be proved inside the - system. Higher-order morphisms are also allowed. -\item Performance. The implementation is based on a depth-first search for the first - solution to a set of constraints which can be as fast as linear in the - size of the term, and the size of the proof term is linear - in the size of the original term. Besides, the extensibility allows the - user to customize the proof search if necessary. -\end{itemize} - -\asection{Introduction to generalized rewriting} - -\subsection{Relations and morphisms} - -A parametric \emph{relation} \texttt{R} is any term of type -\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), relation $A$}. The -expression $A$, which depends on $x_1$ \ldots $x_n$, is called the -\emph{carrier} of the relation and \texttt{R} is -said to be a relation over \texttt{A}; the list $x_1,\ldots,x_n$ -is the (possibly empty) list of parameters of the relation. - -\firstexample -\begin{cscexample}[Parametric relation] -It is possible to implement finite sets of elements of type \texttt{A} -as unordered list of elements of type \texttt{A}. The function -\texttt{set\_eq: forall (A: Type), relation (list A)} satisfied by two lists -with the same elements is a parametric relation over \texttt{(list A)} with -one parameter \texttt{A}. The type of \texttt{set\_eq} is convertible with -\texttt{forall (A: Type), list A -> list A -> Prop}. -\end{cscexample} - -An \emph{instance} of a parametric relation \texttt{R} with $n$ parameters -is any term \texttt{(R $t_1$ \ldots $t_n$)}. - -Let \texttt{R} be a relation over \texttt{A} with $n$ parameters. -A term is a parametric proof of reflexivity for \texttt{R} if it has type -\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), - reflexive (R $x_1$ \ldots $x_n$)}. Similar definitions are given for -parametric proofs of symmetry and transitivity. - -\begin{cscexample}[Parametric relation (cont.)] -The \texttt{set\_eq} relation of the previous example can be proved to be -reflexive, symmetric and transitive. -\end{cscexample} - -A parametric unary function $f$ of type -\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$} -covariantly respects two parametric relation instances $R_1$ and $R_2$ if, -whenever $x, y$ satisfy $R_1~x~y$, their images $(f~x)$ and $(f~y)$ -satisfy $R_2~(f~x)~(f~y)$ . An $f$ that respects its input and output relations -will be called a unary covariant \emph{morphism}. We can also say that $f$ is -a monotone function with respect to $R_1$ and $R_2$. -The sequence $x_1,\ldots x_n$ represents the parameters of the morphism. - -Let $R_1$ and $R_2$ be two parametric relations. -The \emph{signature} of a parametric morphism of type -\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$} that -covariantly respects two instances $I_{R_1}$ and $I_{R_2}$ of $R_1$ and $R_2$ is written $I_{R_1} \texttt{++>} I_{R_2}$. -Notice that the special arrow \texttt{++>}, which reminds the reader -of covariance, is placed between the two relation instances, not -between the two carriers. The signature relation instances and morphism will -be typed in a context introducing variables for the parameters. - -The previous definitions are extended straightforwardly to $n$-ary morphisms, -that are required to be simultaneously monotone on every argument. - -Morphisms can also be contravariant in one or more of their arguments. -A morphism is contravariant on an argument associated to the relation instance -$R$ if it is covariant on the same argument when the inverse relation -$R^{-1}$ (\texttt{inverse R} in Coq) is considered. -The special arrow \texttt{-{}->} is used in signatures -for contravariant morphisms. - -Functions having arguments related by symmetric relations instances are both -covariant and contravariant in those arguments. The special arrow -\texttt{==>} is used in signatures for morphisms that are both covariant -and contravariant. - -An instance of a parametric morphism $f$ with $n$ parameters is any term -\texttt{f $t_1$ \ldots $t_n$}. - -\begin{cscexample}[Morphisms] -Continuing the previous example, let -\texttt{union: forall (A: Type), list A -> list A -> list A} perform the union -of two sets by appending one list to the other. \texttt{union} is a binary -morphism parametric over \texttt{A} that respects the relation instance -\texttt{(set\_eq A)}. The latter condition is proved by showing -\texttt{forall (A: Type) (S1 S1' S2 S2': list A), set\_eq A S1 S1' -> - set\_eq A S2 S2' -> set\_eq A (union A S1 S2) (union A S1' S2')}. - -The signature of the function \texttt{union A} is -\texttt{set\_eq A ==> set\_eq A ==> set\_eq A} for all \texttt{A}. -\end{cscexample} - -\begin{cscexample}[Contravariant morphism] -The division function \texttt{Rdiv: R -> R -> R} is a morphism of -signature \texttt{le ++> le -{}-> le} where \texttt{le} is -the usual order relation over real numbers. Notice that division is -covariant in its first argument and contravariant in its second -argument. -\end{cscexample} - -Leibniz equality is a relation and every function is a -morphism that respects Leibniz equality. Unfortunately, Leibniz equality -is not always the intended equality for a given structure. - -In the next section we will describe the commands to register terms as -parametric relations and morphisms. Several tactics that deal with equality -in \Coq\ can also work with the registered relations. -The exact list of tactic will be given in Sect.~\ref{setoidtactics}. -For instance, the -tactic \texttt{reflexivity} can be used to close a goal $R~n~n$ whenever -$R$ is an instance of a registered reflexive relation. However, the tactics -that replace in a context $C[]$ one term with another one related by $R$ -must verify that $C[]$ is a morphism that respects the intended relation. -Currently the verification consists in checking whether $C[]$ is a syntactic -composition of morphism instances that respects some obvious -compatibility constraints. - -\begin{cscexample}[Rewriting] -Continuing the previous examples, suppose that the user must prove -\texttt{set\_eq int (union int (union int S1 S2) S2) (f S1 S2)} under the -hypothesis \texttt{H: set\_eq int S2 (@nil int)}. It is possible to -use the \texttt{rewrite} tactic to replace the first two occurrences of -\texttt{S2} with \texttt{@nil int} in the goal since the context -\texttt{set\_eq int (union int (union int S1 nil) nil) (f S1 S2)}, being -a composition of morphisms instances, is a morphism. However the tactic -will fail replacing the third occurrence of \texttt{S2} unless \texttt{f} -has also been declared as a morphism. -\end{cscexample} - -\subsection{Adding new relations and morphisms} -A parametric relation -\textit{Aeq}\texttt{: forall ($y_1 : \beta_!$ \ldots $y_m : \beta_m$), relation (A $t_1$ \ldots $t_n$)} over -\textit{(A : $\alpha_i$ -> \ldots $\alpha_n$ -> }\texttt{Type}) -can be declared with the following command: - -\comindex{Add Parametric Relation} -\begin{quote} - \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) : - \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\ - ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\ - ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\ - ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\ - \texttt{~as} \textit{id}. -\end{quote} -after having required the \texttt{Setoid} module with the -\texttt{Require Setoid} command. - -The identifier \textit{id} gives a unique name to the morphism and it is -used by the command to generate fresh names for automatically provided lemmas -used internally. - -Notice that the carrier and relation parameters may refer to the context -of variables introduced at the beginning of the declaration, but the -instances need not be made only of variables. -Also notice that \textit{A} is \emph{not} required to be a term -having the same parameters as \textit{Aeq}, although that is often the -case in practice (this departs from the previous implementation). - -\comindex{Add Relation} -In case the carrier and relations are not parametric, one can use the -command \texttt{Add Relation} instead, whose syntax is the same except -there is no local context. - -The proofs of reflexivity, symmetry and transitivity can be omitted if the -relation is not an equivalence relation. The proofs must be instances of the -corresponding relation definitions: e.g. the proof of reflexivity must -have a type convertible to \texttt{reflexive (A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots - $t'_n$)}. Each proof may refer to the introduced variables as well. - -\begin{cscexample}[Parametric relation] -For Leibniz equality, we may declare: -\texttt{Add Parametric Relation (A : Type) :} \texttt{A (@eq A)}\\ -~\zeroone{\texttt{reflexivity proved by} \texttt{@refl\_equal A}}\\ -\ldots -\end{cscexample} - -Some tactics -(\texttt{reflexivity}, \texttt{symmetry}, \texttt{transitivity}) work only -on relations that respect the expected properties. The remaining tactics -(\texttt{replace}, \texttt{rewrite} and derived tactics such as -\texttt{autorewrite}) do not require any properties over the relation. -However, they are able to replace terms with related ones only in contexts -that are syntactic compositions of parametric morphism instances declared with -the following command. - -\comindex{Add Parametric Morphism} -\begin{quote} - \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) : - (\textit{f $t_1$ \ldots $t_n$})\\ - \texttt{~with signature} \textit{sig}\\ - \texttt{~as id}.\\ - \texttt{Proof}\\ - ~\ldots\\ - \texttt{Qed} -\end{quote} - -The command declares \textit{f} as a parametric morphism of signature -\textit{sig}. The identifier \textit{id} gives a unique name to the morphism -and it is used as the base name of the type class instance definition -and as the name of the lemma that proves the well-definedness of the morphism. -The parameters of the morphism as well as the signature may refer to the -context of variables. -The command asks the user to prove interactively that \textit{f} respects -the relations identified from the signature. - -\begin{cscexample} -We start the example by assuming a small theory over homogeneous sets and -we declare set equality as a parametric equivalence relation and -union of two sets as a parametric morphism. -\begin{coq_example*} -Require Export Setoid. -Require Export Relation_Definitions. -Set Implicit Arguments. -Parameter set: Type -> Type. -Parameter empty: forall A, set A. -Parameter eq_set: forall A, set A -> set A -> Prop. -Parameter union: forall A, set A -> set A -> set A. -Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)). -Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)). -Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)). -Axiom empty_neutral: forall A (S: set A), eq_set (union S (empty A)) S. -Axiom union_compat: - forall (A : Type), - forall x x' : set A, eq_set x x' -> - forall y y' : set A, eq_set y y' -> - eq_set (union x y) (union x' y'). -Add Parametric Relation A : (set A) (@eq_set A) - reflexivity proved by (eq_set_refl (A:=A)) - symmetry proved by (eq_set_sym (A:=A)) - transitivity proved by (eq_set_trans (A:=A)) - as eq_set_rel. -Add Parametric Morphism A : (@union A) with -signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor. -Proof. exact (@union_compat A). Qed. -\end{coq_example*} - -\end{cscexample} - -It is possible to reduce the burden of specifying parameters using -(maximally inserted) implicit arguments. If \texttt{A} is always set as -maximally implicit in the previous example, one can write: - -\begin{coq_eval} -Reset Initial. -Require Export Setoid. -Require Export Relation_Definitions. -Parameter set: Type -> Type. -Parameter empty: forall {A}, set A. -Parameter eq_set: forall {A}, set A -> set A -> Prop. -Parameter union: forall {A}, set A -> set A -> set A. -Axiom eq_set_refl: forall {A}, reflexive (set A) eq_set. -Axiom eq_set_sym: forall {A}, symmetric (set A) eq_set. -Axiom eq_set_trans: forall {A}, transitive (set A) eq_set. -Axiom empty_neutral: forall A (S: set A), eq_set (union S empty) S. -Axiom union_compat: - forall (A : Type), - forall x x' : set A, eq_set x x' -> - forall y y' : set A, eq_set y y' -> - eq_set (union x y) (union x' y'). -\end{coq_eval} - -\begin{coq_example*} -Add Parametric Relation A : (set A) eq_set - reflexivity proved by eq_set_refl - symmetry proved by eq_set_sym - transitivity proved by eq_set_trans - as eq_set_rel. -Add Parametric Morphism A : (@union A) with - signature eq_set ==> eq_set ==> eq_set as union_mor. -Proof. exact (@union_compat A). Qed. -\end{coq_example*} - -We proceed now by proving a simple lemma performing a rewrite step -and then applying reflexivity, as we would do working with Leibniz -equality. Both tactic applications are accepted -since the required properties over \texttt{eq\_set} and -\texttt{union} can be established from the two declarations above. - -\begin{coq_example*} -Goal forall (S: set nat), - eq_set (union (union S empty) S) (union S S). -Proof. intros. rewrite empty_neutral. reflexivity. Qed. -\end{coq_example*} - -The tables of relations and morphisms are managed by the type class -instance mechanism. The behavior on section close is to generalize -the instances by the variables of the section (and possibly hypotheses -used in the proofs of instance declarations) but not to export them in -the rest of the development for proof search. One can use the -\texttt{Existing Instance} command to do so outside the section, -using the name of the declared morphism suffixed by \texttt{\_Morphism}, -or use the \texttt{Global} modifier for the corresponding class instance -declaration (see \S\ref{setoid:first-class}) at definition time. -When loading a compiled file or importing a module, -all the declarations of this module will be loaded. - -\subsection{Rewriting and non reflexive relations} -To replace only one argument of an n-ary morphism it is necessary to prove -that all the other arguments are related to themselves by the respective -relation instances. - -\begin{cscexample} -To replace \texttt{(union S empty)} with \texttt{S} in -\texttt{(union (union S empty) S) (union S S)} the rewrite tactic must -exploit the monotony of \texttt{union} (axiom \texttt{union\_compat} in -the previous example). Applying \texttt{union\_compat} by hand we are left -with the goal \texttt{eq\_set (union S S) (union S S)}. -\end{cscexample} - -When the relations associated to some arguments are not reflexive, the tactic -cannot automatically prove the reflexivity goals, that are left to the user. - -Setoids whose relation are partial equivalence relations (PER) -are useful to deal with partial functions. Let \texttt{R} be a PER. We say -that an element \texttt{x} is defined if \texttt{R x x}. A partial function -whose domain comprises all the defined elements only is declared as a -morphism that respects \texttt{R}. Every time a rewriting step is performed -the user must prove that the argument of the morphism is defined. - -\begin{cscexample} -Let \texttt{eqO} be \texttt{fun x y => x = y $\land$ ~x$\neq$ 0} (the smaller PER over -non zero elements). Division can be declared as a morphism of signature -\texttt{eq ==> eq0 ==> eq}. Replace \texttt{x} with \texttt{y} in -\texttt{div x n = div y n} opens the additional goal \texttt{eq0 n n} that -is equivalent to \texttt{n=n $\land$ n$\neq$0}. -\end{cscexample} - -\subsection{Rewriting and non symmetric relations} -When the user works up to relations that are not symmetric, it is no longer -the case that any covariant morphism argument is also contravariant. As a -result it is no longer possible to replace a term with a related one in -every context, since the obtained goal implies the previous one if and -only if the replacement has been performed in a contravariant position. -In a similar way, replacement in an hypothesis can be performed only if -the replaced term occurs in a covariant position. - -\begin{cscexample}[Covariance and contravariance] -Suppose that division over real numbers has been defined as a -morphism of signature \texttt{Z.div: Z.lt ++> Z.lt -{}-> Z.lt} (i.e. -\texttt{Z.div} is increasing in its first argument, but decreasing on the -second one). Let \texttt{<} denotes \texttt{Z.lt}. -Under the hypothesis \texttt{H: x < y} we have -\texttt{k < x / y -> k < x / x}, but not -\texttt{k < y / x -> k < x / x}. -Dually, under the same hypothesis \texttt{k < x / y -> k < y / y} holds, -but \texttt{k < y / x -> k < y / y} does not. -Thus, if the current goal is \texttt{k < x / x}, it is possible to replace -only the second occurrence of \texttt{x} (in contravariant position) -with \texttt{y} since the obtained goal must imply the current one. -On the contrary, if \texttt{k < x / x} is -an hypothesis, it is possible to replace only the first occurrence of -\texttt{x} (in covariant position) with \texttt{y} since -the current hypothesis must imply the obtained one. -\end{cscexample} - -Contrary to the previous implementation, no specific error message will -be raised when trying to replace a term that occurs in the wrong -position. It will only fail because the rewriting constraints are not -satisfiable. However it is possible to use the \texttt{at} modifier to -specify which occurrences should be rewritten. - -As expected, composing morphisms together propagates the variance annotations by -switching the variance every time a contravariant position is traversed. -\begin{cscexample} -Let us continue the previous example and let us consider the goal -\texttt{x / (x / x) < k}. The first and third occurrences of \texttt{x} are -in a contravariant position, while the second one is in covariant position. -More in detail, the second occurrence of \texttt{x} occurs -covariantly in \texttt{(x / x)} (since division is covariant in its first -argument), and thus contravariantly in \texttt{x / (x / x)} (since division -is contravariant in its second argument), and finally covariantly in -\texttt{x / (x / x) < k} (since \texttt{<}, as every transitive relation, -is contravariant in its first argument with respect to the relation itself). -\end{cscexample} - -\subsection{Rewriting in ambiguous setoid contexts} -One function can respect several different relations and thus it can be -declared as a morphism having multiple signatures. - -\begin{cscexample} -Union over homogeneous lists can be given all the following signatures: -\texttt{eq ==> eq ==> eq} (\texttt{eq} being the equality over ordered lists) -\texttt{set\_eq ==> set\_eq ==> set\_eq} (\texttt{set\_eq} being the equality -over unordered lists up to duplicates), -\texttt{multiset\_eq ==> multiset\_eq ==> multiset\_eq} (\texttt{multiset\_eq} -being the equality over unordered lists). -\end{cscexample} - -To declare multiple signatures for a morphism, repeat the \texttt{Add Morphism} -command. - -When morphisms have multiple signatures it can be the case that a rewrite -request is ambiguous, since it is unclear what relations should be used to -perform the rewriting. Contrary to the previous implementation, the -tactic will always choose the first possible solution to the set of -constraints generated by a rewrite and will not try to find \emph{all} -possible solutions to warn the user about. - -\asection{Commands and tactics} -\subsection{First class setoids and morphisms} -\label{setoid:first-class} - -The implementation is based on a first-class representation of -properties of relations and morphisms as type classes. That is, -the various combinations of properties on relations and morphisms -are represented as records and instances of theses classes are put -in a hint database. -For example, the declaration: - -\begin{quote} - \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) : - \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\ - ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\ - ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\ - ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\ - \texttt{~as} \textit{id}. -\end{quote} - -is equivalent to an instance declaration: - -\begin{quote} - \texttt{Instance} ($x_1 : T_1$) \ldots ($x_n : T_k$) \texttt{=>} - \textit{id} : \texttt{@Equivalence} \textit{(A $t_1$ \ldots $t_n$) (Aeq - $t'_1$ \ldots $t'_m$)} :=\\ - ~\zeroone{\texttt{Equivalence\_Reflexive :=} \textit{refl}}\\ - ~\zeroone{\texttt{Equivalence\_Symmetric :=} \textit{sym}}\\ - ~\zeroone{\texttt{Equivalence\_Transitive :=} \textit{trans}}. -\end{quote} - -The declaration itself amounts to the definition of an object of the -record type \texttt{Coq.Classes.RelationClasses.Equivalence} and a -hint added to the \texttt{typeclass\_instances} hint database. -Morphism declarations are also instances of a type class defined in -\texttt{Classes.Morphisms}. -See the documentation on type classes \ref{typeclasses} and -the theories files in \texttt{Classes} for further explanations. - -One can inform the rewrite tactic about morphisms and relations just by -using the typeclass mechanism to declare them using \texttt{Instance} -and \texttt{Context} vernacular commands. -Any object of type \texttt{Proper} (the type of morphism declarations) -in the local context will also be automatically used by the rewriting -tactic to solve constraints. - -Other representations of first class setoids and morphisms can also -be handled by encoding them as records. In the following example, -the projections of the setoid relation and of the morphism function -can be registered as parametric relations and morphisms. -\begin{cscexample}[First class setoids] - -\begin{coq_example*} -Require Import Relation_Definitions Setoid. -Record Setoid: Type := -{ car:Type; - eq:car->car->Prop; - refl: reflexive _ eq; - sym: symmetric _ eq; - trans: transitive _ eq -}. -Add Parametric Relation (s : Setoid) : (@car s) (@eq s) - reflexivity proved by (refl s) - symmetry proved by (sym s) - transitivity proved by (trans s) as eq_rel. -Record Morphism (S1 S2:Setoid): Type := -{ f:car S1 ->car S2; - compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) }. -Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) : - (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor. -Proof. apply (compat S1 S2 M). Qed. -Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2) - (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y). -Proof. intros. rewrite H. reflexivity. Qed. -\end{coq_example*} -\end{cscexample} - -\subsection{Tactics enabled on user provided relations} -\label{setoidtactics} -The following tactics, all prefixed by \texttt{setoid\_}, -deal with arbitrary -registered relations and morphisms. Moreover, all the corresponding unprefixed -tactics (i.e. \texttt{reflexivity}, \texttt{symmetry}, \texttt{transitivity}, -\texttt{replace}, \texttt{rewrite}) -have been extended to fall back to their prefixed counterparts when -the relation involved is not Leibniz equality. Notice, however, that using -the prefixed tactics it is possible to pass additional arguments such as -\texttt{using relation}. -\medskip - -\tacindex{setoid\_reflexivity} -\texttt{setoid\_reflexivity} - -\tacindex{setoid\_symmetry} -\texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}} - -\tacindex{setoid\_transitivity} -\texttt{setoid\_transitivity} - -\tacindex{setoid\_rewrite} -\texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term} -~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}} - -\tacindex{setoid\_replace} -\texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term} -~\zeroone{\texttt{in} \textit{ident}} -~\zeroone{\texttt{using relation} \textit{term}} -~\zeroone{\texttt{by} \textit{tactic}} -\medskip - -The \texttt{using relation} -arguments cannot be passed to the unprefixed form. The latter argument -tells the tactic what parametric relation should be used to replace -the first tactic argument with the second one. If omitted, it defaults -to the \texttt{DefaultRelation} instance on the type of the objects. -By default, it means the most recent \texttt{Equivalence} instance in -the environment, but it can be customized by declaring new -\texttt{DefaultRelation} instances. As Leibniz equality is a declared -equivalence, it will fall back to it if no other relation is declared on -a given type. - -Every derived tactic that is based on the unprefixed forms of the tactics -considered above will also work up to user defined relations. For instance, -it is possible to register hints for \texttt{autorewrite} that are -not proof of Leibniz equalities. In particular it is possible to exploit -\texttt{autorewrite} to simulate normalization in a term rewriting system -up to user defined equalities. - -\subsection{Printing relations and morphisms} -The \texttt{Print Instances} command can be used to show the list of -currently registered \texttt{Reflexive} (using \texttt{Print Instances Reflexive}), -\texttt{Symmetric} or \texttt{Transitive} relations, -\texttt{Equivalence}s, \texttt{PreOrder}s, \texttt{PER}s, and -Morphisms (implemented as \texttt{Proper} instances). When - the rewriting tactics refuse to replace a term in a context -because the latter is not a composition of morphisms, the \texttt{Print Instances} -commands can be useful to understand what additional morphisms should be -registered. - -\subsection{Deprecated syntax and backward incompatibilities} -Due to backward compatibility reasons, the following syntax for the -declaration of setoids and morphisms is also accepted. - -\comindex{Add Setoid} -\begin{quote} - \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident} -\end{quote} -where \textit{Aeq} is a congruence relation without parameters, -\textit{A} is its carrier and \textit{ST} is an object of type -\texttt{(Setoid\_Theory A Aeq)} (i.e. a record packing together the reflexivity, -symmetry and transitivity lemmas). Notice that the syntax is not completely -backward compatible since the identifier was not required. - -\comindex{Add Morphism} -\begin{quote} - \texttt{Add Morphism} \textit{f}:\textit{ident}.\\ - Proof.\\ - \ldots\\ - Qed. -\end{quote} - -The latter command also is restricted to the declaration of morphisms without -parameters. It is not fully backward compatible since the property the user -is asked to prove is slightly different: for $n$-ary morphisms the hypotheses -of the property are permuted; moreover, when the morphism returns a -proposition, the property is now stated using a bi-implication in place of -a simple implication. In practice, porting an old development to the new -semantics is usually quite simple. - -Notice that several limitations of the old implementation have been lifted. -In particular, it is now possible to declare several relations with the -same carrier and several signatures for the same morphism. Moreover, it is -now also possible to declare several morphisms having the same signature. -Finally, the replace and rewrite tactics can be used to replace terms in -contexts that were refused by the old implementation. As discussed in -the next section, the semantics of the new \texttt{setoid\_rewrite} -command differs slightly from the old one and \texttt{rewrite}. - -\asection{Extensions} -\subsection{Rewriting under binders} - -\textbf{Warning}: Due to compatibility issues, this feature is enabled only when calling -the \texttt{setoid\_rewrite} tactics directly and not \texttt{rewrite}. - -To be able to rewrite under binding constructs, one must declare -morphisms with respect to pointwise (setoid) equivalence of functions. -Example of such morphisms are the standard \texttt{all} and \texttt{ex} -combinators for universal and existential quantification respectively. -They are declared as morphisms in the \texttt{Classes.Morphisms\_Prop} -module. For example, to declare that universal quantification is a -morphism for logical equivalence: - -\begin{coq_eval} -Reset Initial. -Require Import Setoid Morphisms. -\end{coq_eval} -\begin{coq_example} -Instance all_iff_morphism (A : Type) : - Proper (pointwise_relation A iff ==> iff) (@all A). -Proof. simpl_relation. -\end{coq_example} -\begin{coq_eval} -Admitted. -\end{coq_eval} - -One then has to show that if two predicates are equivalent at every -point, their universal quantifications are equivalent. Once we have -declared such a morphism, it will be used by the setoid rewriting tactic -each time we try to rewrite under an \texttt{all} application (products -in \Prop{} are implicitly translated to such applications). - -Indeed, when rewriting under a lambda, binding variable $x$, say from -$P~x$ to $Q~x$ using the relation \texttt{iff}, the tactic will generate -a proof of \texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q -x)} from the proof of \texttt{iff (P x) (Q x)} and a constraint of the -form \texttt{Proper (pointwise\_relation A iff ==> ?) m} will be -generated for the surrounding morphism \texttt{m}. - -Hence, one can add higher-order combinators as morphisms by providing -signatures using pointwise extension for the relations on the functional -arguments (or whatever subrelation of the pointwise extension). -For example, one could declare the \texttt{map} combinator on lists as -a morphism: -\begin{coq_eval} -Require Import List Setoid Morphisms. -Set Implicit Arguments. -Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) := -| eq_nil : list_equiv eqA nil nil -| eq_cons : forall x y, eqA x y -> - forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l'). -Generalizable All Variables. -\end{coq_eval} -\begin{coq_example*} -Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : - Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). -\end{coq_example*} - -where \texttt{list\_equiv} implements an equivalence on lists -parameterized by an equivalence on the elements. - -Note that when one does rewriting with a lemma under a binder -using \texttt{setoid\_rewrite}, the application of the lemma may capture -the bound variable, as the semantics are different from rewrite where -the lemma is first matched on the whole term. With the new -\texttt{setoid\_rewrite}, matching is done on each subterm separately -and in its local environment, and all matches are rewritten -\emph{simultaneously} by default. The semantics of the previous -\texttt{setoid\_rewrite} implementation can almost be recovered using -the \texttt{at 1} modifier. - -\subsection{Sub-relations} - -Sub-relations can be used to specify that one relation is included in -another, so that morphisms signatures for one can be used for the other. -If a signature mentions a relation $R$ on the left of an arrow -\texttt{==>}, then the signature also applies for any relation $S$ that -is smaller than $R$, and the inverse applies on the right of an arrow. -One can then declare only a few morphisms instances that generate the complete set -of signatures for a particular constant. By default, the only declared -subrelation is \texttt{iff}, which is a subrelation of \texttt{impl} -and \texttt{inverse impl} (the dual of implication). That's why we can -declare only two morphisms for conjunction: -\texttt{Proper (impl ==> impl ==> impl) and} and -\texttt{Proper (iff ==> iff ==> iff) and}. This is sufficient to satisfy -any rewriting constraints arising from a rewrite using \texttt{iff}, -\texttt{impl} or \texttt{inverse impl} through \texttt{and}. - -Sub-relations are implemented in \texttt{Classes.Morphisms} and are a -prime example of a mostly user-space extension of the algorithm. - -\subsection{Constant unfolding} - -The resolution tactic is based on type classes and hence regards user-defined -constants as transparent by default. This may slow down the resolution -due to a lot of unifications (all the declared \texttt{Proper} -instances are tried at each node of the search tree). -To speed it up, declare your constant as rigid for proof search -using the command \texttt{Typeclasses Opaque} (see \S -\ref{TypeclassesTransparency}). - -\asection{Strategies for rewriting} - -\subsection{Definitions} -The generalized rewriting tactic is based on a set of strategies that -can be combined to obtain custom rewriting procedures. Its set of -strategies is based on Elan's rewriting strategies -\cite{Luttik97specificationof}. Rewriting strategies are applied using -the tactic \texttt{rewrite\_strat $s$} where $s$ is a strategy -expression. Strategies are defined inductively as described by the -following grammar: - -\def\str#1{\texttt{#1}} - -\def\strline#1#2{& \vert & #1 & \text{#2}} -\def\strlinea#1#2#3{& \vert & \str{#1}~#2 & \text{#3}} - -\[\begin{array}{lcll} - s, t, u & ::= & ( s ) & \text{strategy} \\ - \strline{c}{lemma} \\ - \strline{\str{<-}~c}{lemma, right-to-left} \\ - - \strline{\str{fail}}{failure} \\ - \strline{\str{id}}{identity} \\ - \strline{\str{refl}}{reflexivity} \\ - \strlinea{progress}{s}{progress} \\ - \strlinea{try}{s}{failure catch} \\ - - \strline{s~\str{;}~u}{composition} \\ - \strline{\str{choice}~s~t}{left-biased choice} \\ - - \strlinea{repeat}{s}{iteration (+)} \\ - \strlinea{any}{s}{iteration (*)} \\ - - \strlinea{subterm}{s}{one subterm} \\ - \strlinea{subterms}{s}{all subterms} \\ - \strlinea{innermost}{s}{innermost first} \\ - \strlinea{outermost}{s}{outermost first}\\ - \strlinea{bottomup}{s}{bottom-up} \\ - \strlinea{topdown}{s}{top-down} \\ - - \strlinea{hints}{hintdb}{apply hint} \\ - \strlinea{terms}{c \ldots c}{any of the terms}\\ - \strlinea{eval}{redexpr}{apply reduction}\\ - \strlinea{fold}{c}{fold expression} -\end{array}\] - -Actually a few of these are defined in term of the others using -a primitive fixpoint operator: - -\[\begin{array}{lcl} - \str{try}~s & = & \str{choice}~s~\str{id} \\ - \str{any}~s & = & \str{fix}~u. \str{try}~(s~\str{;}~u) \\ - \str{repeat}~s & = & s~\str{;}~\str{any}~s \\ - \str{bottomup}~s & = & - \str{fix}~bu. (\str{choice}~(\str{progress}~(\str{subterms}~bu))~s)~\str{;}~\str{try}~bu \\ - \str{topdown}~s & = & - \str{fix}~td. (\str{choice}~s~(\str{progress}~(\str{subterms}~td)))~\str{;}~\str{try}~td \\ - \str{innermost}~s & = & \str{fix}~i. (\str{choice}~(\str{subterm}~i)~s) \\ - \str{outermost}~s & = & - \str{fix}~o. (\str{choice}~s~(\str{subterm}~o)) -\end{array}\] - -The basic control strategy semantics are straightforward: strategies are -applied to subterms of the term to rewrite, starting from the root of -the term. The lemma strategies unify the left-hand-side of the -lemma with the current subterm and on success rewrite it to the -right-hand-side. Composition can be used to continue rewriting on the -current subterm. The fail strategy always fails while the identity -strategy succeeds without making progress. The reflexivity strategy -succeeds, making progress using a reflexivity proof of -rewriting. Progress tests progress of the argument strategy and fails if -no progress was made, while \str{try} always succeeds, catching -failures. Choice is left-biased: it will launch the first strategy and -fall back on the second one in case of failure. One can iterate a -strategy at least 1 time using \str{repeat} and at least 0 times using -\str{any}. - -The \str{subterm} and \str{subterms} strategies apply their argument -strategy $s$ to respectively one or all subterms of the current term -under consideration, left-to-right. \str{subterm} stops at the first -subterm for which $s$ made progress. The composite strategies -\str{innermost} and \str{outermost} perform a single innermost our outermost -rewrite using their argument strategy. Their counterparts -\str{bottomup} and \str{topdown} perform as many rewritings as possible, -starting from the bottom or the top of the term. - -Hint databases created for \texttt{autorewrite} can also be used by -\texttt{rewrite\_strat} using the \str{hints} strategy that applies any -of the lemmas at the current subterm. The \str{terms} strategy takes the -lemma names directly as arguments. The \str{eval} strategy expects a -reduction expression (see \S\ref{Conversion-tactics}) and succeeds if it -reduces the subterm under consideration. The \str{fold} strategy takes a -term $c$ and tries to \emph{unify} it to the current subterm, converting -it to $c$ on success, it is stronger than the tactic \texttt{fold}. - - -\subsection{Usage} -\tacindex{rewrite\_strat} - -\texttt{rewrite\_strat}~\textit{s}~\zeroone{\texttt{in} \textit{ident}}: - - Rewrite using the strategy \textit{s} in hypothesis \textit{ident} - or the conclusion. - - \begin{ErrMsgs} - \item \errindex{Nothing to rewrite}. If the strategy failed. - \item \errindex{No progress made}. If the strategy succeeded but - made no progress. - \item \errindex{Unable to satisfy the rewriting constraints}. - If the strategy succeeded and made progress but the corresponding - rewriting constraints are not satisfied. - \end{ErrMsgs} - - -The \texttt{setoid\_rewrite}~c tactic is basically equivalent to -\texttt{rewrite\_strat}~(\str{outermost}~c). - - - - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |