\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}
  Show.
\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{\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 8890 2006-06-01 21:33:26Z msozeau $ 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: