1 files changed, 541 insertions, 0 deletions
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
new file mode 100644
index 00000000..5445224b
--- /dev/null
+++ b/doc/refman/Coercion.tex
@@ -0,0 +1,541 @@
+\achapter{Implicit Coercions}
+\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.
+\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 that the abstract classes {\tt Funclass} and {\tt Sortclass}
+cannot be source classes.
+
+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 \errindex{Sortclass 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 inheritance uniform 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$\\
+                       \> ... \\
+                       \>$[f_1^m;..;f_{n_m}^m] : C_m\mbox{\tt >->}D_m$
+      \end{tabbing}
+\end{enumerate}
+
+\begin{Variants}
+\item {\tt Coercion Local {\qualid} : {\class$_1$} >-> {\class$_2$}.}
+\comindex{Coercion Local}\\
+  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 Coercion Local {\ident} := {\term}}\comindex{Coercion Local}\\
+  This defines {\ident} just like \texttt{Local {\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 declarations 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
+{\declaration} & ::= & {\declarationkeyword} {\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} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\
+   && ~~~\zeroone{\zeroone{\tt |} \nelist{\constructor}{|}} \\
+           & & \\
+{\constructor} & ::= &  {\ident} \sequence{\binderlet}{} \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 Identity Coercion Local {\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.}
+\comindex{Set Printing Coercions}
+\comindex{Unset 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 Set Printing Coercion {\qualid}.}
+\comindex{Set Printing Coercion}
+\comindex{Unset Printing Coercion}
+
+This command forces coercion denoted by {\qualid} to be printed.
+To skip the printing of coercion {\qualid}, use
+ {\tt Unset 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} {\binderlet} : {\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{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: