diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 491 |
1 files changed, 491 insertions, 0 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex new file mode 100644 index 00000000..ed1e6e63 --- /dev/null +++ b/doc/refman/Program.tex @@ -0,0 +1,491 @@ +\def\Program{\textsc{Program}} +\def\Russel{\textsc{Russel}} + +\achapter{The \Program{} tactic} +\label{Program} +\aauthor{Matthieu Sozeau} +\index{Program} + +\begin{flushleft} + \em The status of \Program is experimental. +\end{flushleft} + +We present here the \Coq\ \Program tactic commands, used to build certified +\Coq programs, elaborating them from their algorithmic skeleton and a +rich specification. It can be sought of as a dual of extraction \ref{Extraction}. +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. Input terms and types are typed in an extended system (\Russel) 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} +\comindex{Program Fixpoint} + +The next two commands are similar to they standard counterparts +\ref{Simpl-definitions} and \ref{Fixpoint} in that +they define constants. However, they may require the user to prove some +goals to construct the final definitions. + +\section{\tt Program Definition {\ident} := {\term}. + \comindex{Program Definition}\label{ProgramDefinition}} + +This command types the value {\term} in \Russel and generate subgoals +corresponding to proof obligations. Once solved, 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 :=}}\,% + {\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} + +\section{\tt Program Fixpoint {\ident} {\params} {\tt \{order\}} : type$_0$ := \term$_0$ + \comindex{Program Fixpoint} + \label{ProgramFixpoint}} + +This command allows to define objects using a fixed point +construction. The meaning of this declaration is to define {\it ident} +a recursive function with arguments specified by +{\binder$_1$}\ldots{\binder$_n$} such that {\it ident} applied to +arguments corresponding to these binders has type \type$_0$, and is +equivalent to the expression \term$_0$. The type of the {\ident} is +consequently {\tt forall {\params} {\tt,} \type$_0$} +and the value is equivalent to {\tt fun {\params} {\tt =>} \term$_0$}. + +There are two ways to define fixpoints with \Program{}, structural and +well-founded recursion. + +\subsection{\tt Program Fixpoint {\ident} {\params} {\tt \{struct} + \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ + \comindex{Program Fixpoint Struct} + \label{ProgramFixpointStruct}} + +To be accepted, a structural {\tt Fixpoint} definition has to satisfy some +syntactical constraints on a special argument called the decreasing +argument. They are needed to ensure that the {\tt Fixpoint} definition +always terminates. The point of the {\tt \{struct \ident {\tt \}}} +annotation is to let the user tell the system which argument decreases +along the recursive calls. This annotation may be left implicit for +fixpoints with one argument. For instance, one can define the identity +function on naturals as : + +\begin{coq_example} +Program Fixpoint id (n : nat) : { x : nat | x = n } := + match n with + | O => O + | S p => S (id p) + end. +\end{coq_example} + +The {\tt match} operator matches a value (here \verb:n:) with the +various constructors of its (inductive) type. The remaining arguments +give the respective values to be returned, as functions of the +parameters of the corresponding constructor. Thus here when \verb:n: +equals \verb:O: we return \verb:0:, and when \verb:n: equals +\verb:(S p): we return \verb:(S (id p)):. + +The {\tt match} operator is formally described +in detail in Section~\ref{Caseexpr}. The system recognizes that in +the inductive call {\tt (id p)} the argument actually +decreases because it is a {\em pattern variable} coming from {\tt match + n with}. + +Here again, proof obligations may be generated. In our example, we would +have one for each branch: +\begin{coq_example} +Show. +\end{coq_example} + +% \subsection{\tt Program Fixpoint {\ident} {(\ident_$_0$ : \type_$_0$) +% \cdots (\ident_$_n$ : \type_$_n$)} {\tt \{wf} +% \ident$_i$ \term_{wf} {\tt \}} : type$_t$ := \term$_0$ +% \comindex{Program Fixpoint Wf} +% \label{ProgramFixpointWf}} + +% To be accepted, a well-founded {\tt Fixpoint} definition has to satisfy some +% logical constraints on the decreasing argument. +% They are needed to ensure that the {\tt Fixpoint} definition +% always terminates. The point of the {\tt \{wf \ident \term {\tt \}}} +% annotation is to let the user tell the system which argument decreases +% in which well-founded relation along the recursive calls. +% The term \term$_0$ will be typed in a different context than usual, +% The typing problem will in fact be reduced to: + +% % \begin{center} +% % {\tt forall} {\params} {\ident : (\ident$_0$ : type$_0$) \cdots +% % \{ \ident$_i'$ : \type$_i$ | \term_{wf} \ident$_i'$ \ident$_i$ \} +% % \cdots (\ident$_n$ : type$_n$), type$_t$} : type$_t$ := \term$_0$ +% % \end{center} + +% \begin{coq_example} +% Program Fixpoint id (n : nat) : { x : nat | x = n } := +% match n with +% | O => O +% | S p => S (id p) +% end +% \end{coq_example} + +% The {\tt match} operator matches a value (here \verb:n:) with the +% various constructors of its (inductive) type. The remaining arguments +% give the respective values to be returned, as functions of the +% parameters of the corresponding constructor. Thus here when \verb:n: +% equals \verb:O: we return \verb:0:, and when \verb:n: equals +% \verb:(S p): we return \verb:(S (id p)):. + +% The {\tt match} operator is formally described +% in detail in Section~\ref{Caseexpr}. The system recognizes that in +% the inductive call {\tt (id p)} the argument actually +% decreases because it is a {\em pattern variable} coming from {\tt match +% n with}. + +% Here again, proof obligations may be generated. In our example, we would +% have one for each branch: +% \begin{coq_example} +% Show. +% \end{coq_example} +% \begin{coq_eval} +% Abort. +% \end{coq_eval} + + + + +% \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*} + +% This module contains a theorem {\tt eucl\_dev}, and its extracted term +% is of type +% \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. +% We can now extract this program to \ocaml: + +% \begin{coq_eval} +% Reset Initial. +% \end{coq_eval} +% \begin{coq_example} +% Require Import Euclid. +% Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec. +% Recursive Extraction eucl_dev. +% \end{coq_example} + +% The inlining of {\tt gt\_wf\_rec} and {\tt lt\_wf\_rec} 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{coq_example} +% Extraction "euclid" eucl_dev. +% \end{coq_example} + +% Let us play the resulting program: + +% \begin{verbatim} +% # #use "euclid.ml";; +% type sumbool = Left | Right +% type nat = O | S of nat +% type diveucl = Divex of nat * nat +% val minus : nat -> nat -> nat = <fun> +% val le_lt_dec : nat -> nat -> sumbool = <fun> +% val le_gt_dec : nat -> nat -> sumbool = <fun> +% 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 i2n = function 0 -> O | n -> S (i2n (n-1));; +% val i2n : int -> nat = <fun> +% # let rec n2i = function O -> 0 | S p -> 1+(n2i p);; +% val n2i : nat -> int = <fun> +% # let div a b = +% let Divex (q,r) = eucl_dev (i2n b) (i2n a) in (n2i q, n2i r);; +% div : int -> int -> int * int = <fun> +% # div 173 15;; +% - : int * int = 11, 8 +% \end{verbatim} + +% \asubsection{Another detailed example: Heapsort} + +% The file {\tt Heap.v} +% contains the proof of an efficient list sorting algorithm described by +% Bjerner. Is is an adaptation of the well-known {\em heapsort} +% algorithm to functional languages. The main function is {\tt +% treesort}, whose type is shown below: + + +% \begin{coq_eval} +% Reset Initial. +% Require Import Relation_Definitions. +% Require Import List. +% Require Import Sorting. +% Require Import Permutation. +% \end{coq_eval} +% \begin{coq_example} +% Require Import Heap. +% Check treesort. +% \end{coq_example} + +% Let's now extract this function: + +% \begin{coq_example} +% Extraction Inline sort_rec is_heap_rec. +% Extraction NoInline list_to_heap. +% Extraction "heapsort" treesort. +% \end{coq_example} + +% One more time, the {\tt Extraction Inline} and {\tt NoInline} +% directives are cosmetic. Without it, everything goes right, +% but the output is less readable. +% Here is the produced file {\tt heapsort.ml}: + +% \begin{verbatim} +% type nat = +% | O +% | S of nat + +% type 'a sig2 = +% 'a +% (* singleton inductive, whose constructor was exist2 *) + +% type sumbool = +% | Left +% | Right + +% type 'a list = +% | Nil +% | Cons of 'a * 'a list + +% type 'a multiset = +% 'a -> nat +% (* singleton inductive, whose constructor was Bag *) + +% type 'a merge_lem = +% 'a list +% (* singleton inductive, whose constructor was merge_exist *) + +% (** val merge : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool) -> +% 'a1 list -> 'a1 list -> 'a1 merge_lem **) + +% let rec merge leA_dec eqA_dec l1 l2 = +% match l1 with +% | Nil -> l2 +% | Cons (a, l) -> +% let rec f = function +% | Nil -> Cons (a, l) +% | Cons (a0, l3) -> +% (match leA_dec a a0 with +% | Left -> Cons (a, +% (merge leA_dec eqA_dec l (Cons (a0, l3)))) +% | Right -> Cons (a0, (f l3))) +% in f l2 + +% type 'a tree = +% | Tree_Leaf +% | Tree_Node of 'a * 'a tree * 'a tree + +% type 'a insert_spec = +% 'a tree +% (* singleton inductive, whose constructor was insert_exist *) + +% (** val insert : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool) -> +% 'a1 tree -> 'a1 -> 'a1 insert_spec **) + +% let rec insert leA_dec eqA_dec t a = +% match t with +% | Tree_Leaf -> Tree_Node (a, Tree_Leaf, Tree_Leaf) +% | Tree_Node (a0, t0, t1) -> +% let h3 = fun x -> insert leA_dec eqA_dec t0 x in +% (match leA_dec a0 a with +% | Left -> Tree_Node (a0, t1, (h3 a)) +% | Right -> Tree_Node (a, t1, (h3 a0))) + +% type 'a build_heap = +% 'a tree +% (* singleton inductive, whose constructor was heap_exist *) + +% (** val list_to_heap : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> +% sumbool) -> 'a1 list -> 'a1 build_heap **) + +% let rec list_to_heap leA_dec eqA_dec = function +% | Nil -> Tree_Leaf +% | Cons (a, l0) -> +% insert leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l0) a + +% type 'a flat_spec = +% 'a list +% (* singleton inductive, whose constructor was flat_exist *) + +% (** val heap_to_list : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> +% sumbool) -> 'a1 tree -> 'a1 flat_spec **) + +% let rec heap_to_list leA_dec eqA_dec = function +% | Tree_Leaf -> Nil +% | Tree_Node (a, t0, t1) -> Cons (a, +% (merge leA_dec eqA_dec (heap_to_list leA_dec eqA_dec t0) +% (heap_to_list leA_dec eqA_dec t1))) + +% (** val treesort : ('a1 -> 'a1 -> sumbool) -> ('a1 -> 'a1 -> sumbool) +% -> 'a1 list -> 'a1 list sig2 **) + +% let treesort leA_dec eqA_dec l = +% heap_to_list leA_dec eqA_dec (list_to_heap leA_dec eqA_dec l) + +% \end{verbatim} + +% Let's test it: +% % Format.set_margin 72;; +% \begin{verbatim} +% # #use "heapsort.ml";; +% type sumbool = Left | Right +% type nat = O | S of nat +% type 'a tree = Tree_Leaf | Tree_Node of 'a * 'a tree * 'a tree +% type 'a list = Nil | Cons of 'a * 'a list +% val merge : +% ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list = <fun> +% val heap_to_list : +% ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun> +% val insert : +% ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun> +% val list_to_heap : +% ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun> +% val treesort : +% ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun> +% \end{verbatim} + +% One can remark that the argument of {\tt treesort} corresponding to +% {\tt eqAdec} is never used in the informative part of the terms, +% only in the logical parts. So the extracted {\tt treesort} never use +% it, hence this {\tt 'b} argument. We will use {\tt ()} for this +% argument. Only remains the {\tt leAdec} +% argument (of type {\tt 'a -> 'a -> sumbool}) to really provide. + +% \begin{verbatim} +% # let leAdec x y = if x <= y then Left else Right;; +% val leAdec : 'a -> 'a -> sumbool = <fun> +% # let rec listn = function 0 -> Nil +% | n -> Cons(Random.int 10000,listn (n-1));; +% val listn : int -> int list = <fun> +% # treesort leAdec () (listn 9);; +% - : int list = Cons (160, Cons (883, Cons (1874, Cons (3275, Cons +% (5392, Cons (7320, Cons (8512, Cons (9632, Cons (9876, Nil))))))))) +% \end{verbatim} + +% Some tests on longer lists (10000 elements) show that the program is +% quite efficient for Caml code. + + +% \asubsection{The Standard Library} + +% As a test, we propose an automatic extraction of the +% Standard Library of \Coq. In particular, we will find back the +% two previous examples, {\tt Euclid} and {\tt Heapsort}. +% Go to directory {\tt contrib/extraction/test} of the sources of \Coq, +% and run commands: +% \begin{verbatim} +% make tree; make +% \end{verbatim} +% This will extract all Standard Library files and compile them. +% It is done via many {\tt Extraction Module}, with some customization +% (see subdirectory {\tt custom}). + +% %The result of this extraction of the Standard Library can be browsed +% %at URL +% %\begin{flushleft} +% %\url{http://www.lri.fr/~letouzey/extraction}. +% %\end{flushleft} + +% %Reals theory is normally not extracted, since it is an axiomatic +% %development. We propose nonetheless a dummy realization of those +% %axioms, to test, run: \\ +% % +% %\mbox{\tt make reals}\\ + +% This test works also with Haskell. In the same directory, run: +% \begin{verbatim} +% make tree; make -f Makefile.haskell +% \end{verbatim} +% The haskell compiler currently used is {\tt hbc}. Any other should +% also work, just adapt the {\tt Makefile.haskell}. In particular {\tt +% ghc} is known to work. + +% \asubsection{Extraction's horror museum} + +% Some pathological examples of extraction are grouped in the file +% \begin{verbatim} +% contrib/extraction/test_extraction.v +% \end{verbatim} +% 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 (just run {\tt make} in those directories): + +% \begin{itemize} +% \item Bordeaux/Additions +% \item Bordeaux/EXCEPTIONS +% \item Bordeaux/SearchTrees +% \item Dyade/BDDS +% \item Lannion +% \item Lyon/CIRCUITS +% \item Lyon/FIRING-SQUAD +% \item Marseille/CIRCUITS +% \item Muenchen/Higman +% \item Nancy/FOUnify +% \item Rocq/ARITH/Chinese +% \item Rocq/COC +% \item Rocq/GRAPHS +% \item Rocq/HIGMAN +% \item Sophia-Antipolis/Stalmarck +% \item Suresnes/BDD +% \end{itemize} + +% Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are +% the only 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}. + +% $Id: Program.tex 8688 2006-04-07 15:08:12Z msozeau $ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |