diff options
Diffstat (limited to 'doc/refman/Helm.tex')
| -rw-r--r-- | doc/refman/Helm.tex | 317 |
1 files changed, 0 insertions, 317 deletions
diff --git a/doc/refman/Helm.tex b/doc/refman/Helm.tex deleted file mode 100644 index af34af43..00000000 --- a/doc/refman/Helm.tex +++ /dev/null @@ -1,317 +0,0 @@ -\label{Helm} -\index{XML exportation} -\index{Proof rendering} - -This section describes the exportation of {\Coq} theories to XML that -has been contributed by Claudio Sacerdoti Coen. Currently, the main -applications are the rendering and searching tool -developed within the HELM\footnote{Hypertextual Electronic Library of -Mathematics} and MoWGLI\footnote{Mathematics on the Web, Get it by -Logic and Interfaces} projects mainly at the University of Bologna and -partly at INRIA-Sophia Antipolis. - -\subsection{Practical use of the XML exportation tool} - -The basic way to export the logical content of a file into XML format -is to use {\tt coqc} with option {\tt -xml}. -When the {\tt -xml} flag is set, every definition or declaration is -immediately exported to XML once concluded. -The system environment variable {\tt COQ\_XML\_LIBRARY\_ROOT} must be -previously set to a directory in which the logical structure of the -exported objects is reflected. - - For {\tt Makefile} files generated by \verb+coq_makefile+ (see section - \ref{Makefile}), it is sufficient to compile the files using - \begin{quotation} - \verb+make COQ_XML=-xml+ - \end{quotation} - (or, equivalently, setting the environment variable \verb+COQ_XML+) - - To export a development to XML, the suggested procedure is then: - - \begin{enumerate} - \item add to your own contribution a valid \verb+Make+ file and use - \verb+coq_makefile+ to generate the \verb+Makefile+ from the \verb+Make+ - file. - - \Warning Since logical names are used to structure the XML - hierarchy, always add to the \verb+Make+ file at least one \verb+"-R"+ - option to map physical file names to logical module paths. - \item set the \verb+COQ_XML_LIBRARY_ROOT+ environment variable to - the directory where the XML file hierarchy must be physically - rooted. - \item compile your contribution with \verb+"make COQ_XML=-xml"+ - \end{enumerate} - -\Rem In case the system variable {\tt COQ\_XML\_LIBRARY\_ROOT} is not set, -the output is done on the standard output. Also, the files are -compressed using {\tt gzip} after creation. This is to save disk space -since the XML format is very verbose. - -\subsection{Reflection of the logical structure into the file system} - -For each {\Coq} logical object, several independent files associated -to this object are created. The structure of the long name of the -object is reflected in the directory structure of the file system. -E.g. an object of long name {\tt -{\ident$_1$}.{\ldots}.{\ident$_n$}.{\ident}} is exported to files in the -subdirectory {{\ident$_1$}/{\ldots}/{\ident$_n$}} of the directory -bound to the environment variable {\tt COQ\_XML\_LIBRARY\_ROOT}. - -\subsection{What is exported?} - -The XML exportation tool exports the logical content of {\Coq} -theories. This covers global definitions (including lemmas, theorems, -...), global assumptions (parameters and axioms), local assumptions or -definitions, and inductive definitions. - -Vernacular files are exported to {\tt .theory.xml} files. -%Variables, -%definitions, theorems, axioms and proofs are exported to individual -%files whose suffixes range from {\tt .var.xml}, {\tt .con.xml}, {\tt -%.con.body.xml}, {\tt .con.types.xml} to {\tt .con.proof_tree.xml}. -Comments are pre-processed with {\sf coqdoc} (see section -\ref{coqdoc}). Especially, they have to be enclosed within {\tt (**} -and {\tt *)} to be exported. - -For each inductive definition of name -{\ident$_1$}.{\ldots}.{\ident$_n$}.{\ident}, a file named {\tt -{\ident}.ind.xml} is created in the subdirectory {\tt -{\ident$_1$}/{\ldots}/{\ident$_n$}} of the xml library root -directory. It contains the arities and constructors of the type. For mutual inductive definitions, the file is named after the -name of the first inductive type of the block. - -For each global definition of base name {\tt -{\ident$_1$}.{\ldots}.{\ident$_n$}.{\ident}}, files named -{\tt {\ident}.con.body.xml} and {\tt {\ident}.con.xml} are created in the -subdirectory {\tt {\ident$_1$}/{\ldots}/{\ident$_n$}}. They -respectively contain the body and the type of the definition. - -For each global assumption of base name {\tt -{\ident$_1$}.{\ident$_2$}.{\ldots}.{\ident$_n$}.{\ident}}, a file -named {\tt {\ident}.con.xml} is created in the subdirectory {\tt -{\ident$_1$}/{\ldots}/{\ident$_n$}}. It contains the type of the -global assumption. - -For each local assumption or definition of base name {\ident} located -in sections {\ident$'_1$}, {\ldots}, {\ident$'_p$} of the module {\tt -{\ident$_1$}.{\ident$_2$}.{\ldots}.{\ident$_n$}.{\ident}}, a file -named {\tt {\ident}.var.xml} is created in the subdirectory {\tt -{\ident$_1$}/{\ldots}/{\ident$_n$}/{\ident$'_1$}/\ldots/{\ident$'_p$}}. -It contains its type and, if a definition, its body. - -In order to do proof-rendering (for example in natural language), some -redundant typing information is required, i.e. the type of at least -some of the subterms of the bodies and types of the CIC objects. These -types are called inner types and are exported to files of suffix {\tt -.types.xml} by the exportation tool. - - -% Deactivated -%% \subsection{Proof trees} - -%% For each definition or theorem that has been built with tactics, an -%% extra file of suffix {\tt proof\_tree.xml} is created. It contains the -%% proof scripts and is used for rendering the proof. - -\subsection{Inner types} -\label{inner-types} - -The type of a subterm of a construction is called an {\em inner type} -if it respects the following conditions. - -\begin{enumerate} - \item Its sort is \verb+Prop+\footnote{or {\tt CProp} which is the - "sort"-like definition used in C-CoRN (see - \url{http://vacuumcleaner.cs.kun.nl/c-corn}) to type - computationally relevant predicative propositions.}. - \item It is not a type cast nor an atomic term (variable, constructor or constant). - \item If it's root is an abstraction, then the root's parent node is - not an abstraction, i.e. only the type of the outer abstraction of - a block of nested abstractions is printed. -\end{enumerate} - -The rationale for the 3$^{rd}$ condition is that the type of the inner -abstractions could be easily computed starting from the type of the -outer ones; moreover, the types of the inner abstractions requires a -lot of disk/memory space: removing the 3$^{rd}$ condition leads to XML -file that are two times as big as the ones exported applying the 3$^{rd}$ -condition. - -\subsection{Interactive exportation commands} - -There are also commands to be used interactively in {\tt coqtop}. - -\subsubsection{\tt Print XML {\qualid}} -\comindex{Print XML} - -If the variable {\tt COQ\_XML\_LIBRARY\_ROOT} is set, this command creates -files containing the logical content in XML format of {\qualid}. If -the variable is not set, the result is displayed on the standard -output. - -\begin{Variants} -\item {\tt Print XML File {\str} {\qualid}}\\ -This writes the logical content of {\qualid} in XML format to files -whose prefix is {\str}. -\end{Variants} - -\subsubsection{{\tt Show XML Proof}} -\comindex{Show XML Proof} - -If the variable {\tt COQ\_XML\_LIBRARY\_ROOT} is set, this command creates -files containing the current proof in progress in XML format. It -writes also an XML file made of inner types. If the variable is not -set, the result is displayed on the standard output. - -\begin{Variants} -\item {\tt Show XML File {\str} Proof}\\ This writes the -logical content of {\qualid} in XML format to files whose prefix is -{\str}. -\end{Variants} - -\subsection{Applications: rendering, searching and publishing} - -The HELM team at the University of Bologna has developed tools -exploiting the XML exportation of {\Coq} libraries. This covers -rendering, searching and publishing tools. - -All these tools require a running http server and, if possible, a -MathML compliant browser. The procedure to install the suite of tools -ultimately allowing rendering and searching can be found on the HELM -web site \url{http://helm.cs.unibo.it/library.html}. - -It may be easier though to upload your developments on the HELM http -server and to re-use the infrastructure running on it. This requires -publishing your development. To this aim, follow the instructions on -\url{http://mowgli.cs.unibo.it}. - -Notice that the HELM server already hosts a copy of the standard -library of {\Coq} and of the {\Coq} user contributions. - -\subsection{Technical informations} - -\subsubsection{CIC with Explicit Named Substitutions} - -The exported files are XML encoding of the lambda-terms used by the -\Coq\ system. The implementative details of the \Coq\ system are hidden as much -as possible, so that the XML DTD is a straightforward encoding of the -Calculus of (Co)Inductive Constructions. - -Nevertheless, there is a feature of the \Coq\ system that can not be -hidden in a completely satisfactory way: discharging (see Sect.\ref{Section}). -In \Coq\ it is possible -to open a section, declare variables and use them in the rest of the section -as if they were axiom declarations. Once the section is closed, every definition and theorem in the section is discharged by abstracting it over the section -variables. Variable declarations as well as section declarations are entirely -dropped. Since we are interested in an XML encoding of definitions and -theorems as close as possible to those directly provided the user, we -do not want to export discharged forms. Exporting non-discharged theorem -and definitions together with theorems that rely on the discharged forms -obliges the tools that work on the XML encoding to implement discharging to -achieve logical consistency. Moreover, the rendering of the files can be -misleading, since hyperlinks can be shown between occurrences of the discharge -form of a definition and the non-discharged definition, that are different -objects. - -To overcome the previous limitations, Claudio Sacerdoti Coen developed in his -PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions -with Explicit Named Substitutions, that is a slight extension of CIC where -discharging is not necessary. The DTD of the exported XML files describes -constants, inductive types and variables of the Calculus of (Co)Inductive -Constructions with Explicit Named Substitutions. The conversion to the new -calculus is performed during the exportation phase. - -The following example shows a very small \Coq\ development together with its -version in CIC with Explicit Named Substitutions. - -\begin{verbatim} -# CIC version: # -Section S. - Variable A : Prop. - - Definition impl := A -> A. - - Theorem t : impl. (* uses the undischarged form of impl *) - Proof. - exact (fun (a:A) => a). - Qed. - -End S. - -Theorem t' : (impl False). (* uses the discharged form of impl *) - Proof. - exact (t False). (* uses the discharged form of t *) - Qed. -\end{verbatim} - -\begin{verbatim} -# Corresponding CIC with Explicit Named Substitutions version: # -Section S. - Variable A : Prop. - - Definition impl(A) := A -> A. (* theorems and definitions are - explicitly abstracted over the - variables. The name is sufficient to - completely describe the abstraction *) - - Theorem t(A) : impl. (* impl where A is not instantiated *) - Proof. - exact (fun (a:A) => a). - Qed. - -End S. - -Theorem t'() : impl{False/A}. (* impl where A is instantiated with False - Notice that t' does not depend on A *) - Proof. - exact t{False/A}. (* t where A is instantiated with False *) - Qed. -\end{verbatim} - -Further details on the typing and reduction rules of the calculus can be -found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency -of the calculus is also proved. - -\subsubsection{The CIC with Explicit Named Substitutions XML DTD} - -A copy of the DTD can be found in the file ``\verb+cic.dtd+'' in the -\verb+contrib/xml+ source directory of \Coq. -The following is a very brief overview of the elements described in the DTD. - -\begin{description} - \item[]\texttt{<ConstantType>} - is the root element of the files that correspond to constant types. - \item[]\texttt{<ConstantBody>} - is the root element of the files that correspond to constant bodies. - It is used only for closed definitions and theorems (i.e. when no - metavariable occurs in the body or type of the constant) - \item[]\texttt{<CurrentProof>} - is the root element of the file that correspond to the body of a constant - that depends on metavariables (e.g. unfinished proofs) - \item[]\texttt{<Variable>} - is the root element of the files that correspond to variables - \item[]\texttt{<InductiveTypes>} - is the root element of the files that correspond to blocks - of mutually defined inductive definitions -\end{description} - -The elements - \verb+<LAMBDA>+, \verb+<CAST>+, \verb+<PROD>+, \verb+<REL>+, \verb+<SORT>+, - \verb+<APPLY>+, \verb+<VAR>+, \verb+<META>+, \verb+<IMPLICIT>+, \verb+<CONST>+, \verb+<LETIN>+, \verb+<MUTIND>+, \verb+<MUTCONSTRUCT>+, \verb+<MUTCASE>+, - \verb+<FIX>+ and \verb+<COFIX>+ are used to encode the constructors of CIC. - The \verb+sort+ or \verb+type+ attribute of the element, if present, is - respectively the sort or the type of the term, that is a sort because of the - typing rules of CIC. - -The element \verb+<instantiate>+ correspond to the application of an explicit -named substitution to its first argument, that is a reference to a definition -or declaration in the environment. - -All the other elements are just syntactic sugar. - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |