From 26ca22424b286f5ff22a1fa97c38d15e224b3dc2 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Apr 2006 15:08:12 +0000
Subject: - Documentation of the Program tactics. - Fixes to the subtac
 implementation, utility tactic to apply existentials to a function and build
 a dependent sum out of name, constr lists. Also defined a Utils coq module
 for tactics related to subsets and the projections for ex in Prop. -
 Enhancements to inference algorithm added but not used in the default version
 as there are some remaining bugs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Program.tex | 491 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 491 insertions(+)
 create mode 100644 doc/refman/Program.tex

(limited to 'doc/refman/Program.tex')

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
new file mode 100644
index 0000000000..4f3fadcbd5
--- /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$ 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
-- 
cgit v1.2.3

