diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 527 |
1 files changed, 0 insertions, 527 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex deleted file mode 100644 index 4f8f1281..00000000 --- a/doc/refman/Program.tex +++ /dev/null @@ -1,527 +0,0 @@ -\def\Program{\textsc{Program}} -\def\Russell{\textsc{Russell}} -\def\PVS{\textsc{PVS}} - -\achapter{\Program{}} -\label{Program} -\aauthor{Matthieu Sozeau} -\index{Program} - -\begin{flushleft} - \em The status of \Program\ is experimental. -\end{flushleft} - -We present here the new \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 -(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 (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{coq_example*} - match x with - | 0 => t - | S n => u - end. -\end{coq_example*} -will be first rewrote to: -\begin{coq_example*} - (match x as y return (x = y -> _) with - | 0 => fun H : x = 0 -> t - | S n => fun H : x = S n -> u - end) (refl_equal n). -\end{coq_example*} - - This permits to get the proper equalities in the context of proof - obligations inside clauses, without which reasoning is very limited. - -\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} - -The next two commands are similar to their standard counterparts -Definition (section \ref{Simpl-definitions}) and Fixpoint (section \ref{Fixpoint}) in that -they define constants. However, they may require the user to prove some -goals to construct the final definitions. {\em Note:} every subtac -definition must end with the {\tt Defined} vernacular. - -\subsection{\tt Program Definition {\ident} := {\term}. - \comindex{Program Definition}\label{ProgramDefinition}} - -This command types the value {\term} in \Russell\ 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} - -\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 -(section \ref{Fixpoint}), except it may also generate obligations. - -\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} - Obligations. -\end{coq_example} - -\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 currently fail if the traduction to \Coq\ -generates obligations though it can be useful to insert automatic coercions. - -\subsection{Solving obligations} -The following commands are available to manipulate obligations: - -\begin{itemize} -\item {\tt Obligations [of \ident]} Displays all remaining - obligations. -\item {\tt Solve Obligation num [of \ident]} Start the proof of - obligation {\tt num}. -\item {\tt Solve Obligations [of \ident] using} {\tacexpr} Tries to solve - each obligation using the given tactic. -\end{itemize} - - -% \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 9332 2006-11-02 12:23:24Z msozeau $ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |