From be79f2538c6a2911aba80d7c362915e918edaea3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 10:17:35 +0100 Subject: [Sphinx] Move chapter 18 to new infrastructure --- Makefile.doc | 2 +- doc/refman/Coercion.tex | 563 ----------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/implicit-coercions.rst | 563 +++++++++++++++++++++++++++++ 4 files changed, 564 insertions(+), 565 deletions(-) delete mode 100644 doc/refman/Coercion.tex create mode 100644 doc/sphinx/addendum/implicit-coercions.rst diff --git a/Makefile.doc b/Makefile.doc index 2d2b21ad8..8a1c6bb29 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Coercion.v.tex Extraction.v.tex \ + Extraction.v.tex \ Program.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Universes.v.tex \ Misc.v.tex) 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/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 7ce28ccf8..0c159e059 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,7 +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 diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst new file mode 100644 index 000000000..9862a9b30 --- /dev/null +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -0,0 +1,563 @@ +\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: -- cgit v1.2.3