\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: