path: root/doc/Program.tex

\achapter{The Program Tactic}
\aauthor{Catherine Parent}
\label{Addoc-program}

The facilities described in this document pertain to a special aspect of
the \Coq\ system: how to associate to a functional program, whose 
specification is written in \gallina, a proof of its correctness.

This methodology is based on the Curry-Howard isomorphism between
functional programs and constructive proofs. This isomorphism allows
the synthesis of a functional program from the constructive part of its
proof of correctness. That is, it is possible to analyze a \Coq\ proof,
to erase all its non-informative parts (roughly speaking, removing the
parts pertaining to sort \Prop, considered as comments, to keep only the
parts pertaining to sort \Set). 

This {\sl realizability interpretation}
was defined by Christine Paulin-Mohring in her PhD dissertation 
\cite{Moh89b}, and
implemented as a {\sl program extraction} facility in previous versions of 
\Coq~ by Benjamin Werner (see \cite{COQ93}). 
However, the corresponding certified program
development methodology was very awkward: the user had to understand very 
precisely the extraction mechanism in order to guide the proof construction
towards the desired algorithm. The facilities described in this chapter 
attempt to do the reverse: i.e. to try and generate the proof of correctness
from the program itself, given as argument to a specialized tactic.
This work is based on the PhD dissertation of 
Catherine Parent (see \cite{CPar95})

\asection{Developing certified programs: Motivations}
\label{program_proving}

We want to develop certified programs automatically proved by the
system. That is to say, instead of giving a specification, an
interactive proof and then extracting a program, the user gives the
program he wants to prove and the corresponding specification. Using
this information, an automatic proof is developed which solves the
``informative'' goals without the help of the user. When the proof is
finished, the extracted program is guaranteed to be correct and
corresponds to the one given by the user. The tactic uses the fact
that the extracted program is a skeleton of its corresponding proof.

\asection{Using {\tt Program}}
The user has to give two things: the specification (given as usual by
a goal) and the program (see section \ref{program-syntax}). Then, this program
is associated to the current goal (to know which specification it
corresponds to) and the user can use different tactics to develop an
automatic proof.

\asubsection{\tt Realizer \term.}
\tacindex{Realizer}
\label{Realizer}
This command attaches a program {\term} to the current goal. This is a
necessary step before applying the first time the tactic {\tt
Program}.  The syntax of programs is given in section \ref{program-syntax}.
If a program is already attached to the current subgoal, {\tt
Realizer} can be also used to change it.

\asubsection{\tt Show Program.}
\comindex{Show Program}\label{Show Program} 
The command \verb=Show Program= shows the program associated to the
current goal. The variant \verb=Show Program n= shows the program associated to
the nth subgoal.

\asubsection{\tt Program.}
\tacindex{Program}\label{Program} 
This tactics tries to build a proof of the current subgoal from the
program associated to the current goal. This tactic performs
\verb=Intros= then either one \verb=Apply= or one \verb=Elim=
depending on the syntax of the program. The \verb=Program= tactic
generates a list of subgoals which can be either logical or
informative. Subprograms are automatically attached to the informative
subgoals. 

When attached program are not automatically generated, an initial program
has to be given by {\tt Realizer}. 

\begin{ErrMsgs}
\item \errindex{No program associated to this subgoal}\\
You need to attach a program to the current goal by using {\tt Realizer}.
Perhaps, you already attached a program but a {\tt Restart} or an
{\tt Undo} has removed it.
\item \errindex{Type of program and informative extraction of goal do not coincide}
\item \errindex{Cannot attach a realizer to a logical goal}\\
The current goal is non informative (it lives in the world {\tt Prop}
of propositions or {\tt Type} of abstract sets) while it should lives
in the world {\tt Set} of computational objects.
\item \errindex{Perhaps a term of the Realizer is not an FW
    term}\texttt{ and you then have to replace it by its extraction}\\
Your program contains non informative subterms.
\end{ErrMsgs}

\begin{Variants}
\item{\tt Program\_all.}
  \tacindex{Program\_all}\label{Program_all}\\
  This tactic is equivalent to the composed tactic
  \verb=Repeat (Program OrElse Auto)=. It repeats the \verb=Program=
  tactic on every informative subgoal and tries the \verb=Auto= tactic
  on the logical subgoals. Note that the work of the \verb=Program=
  tactic is considered to be finished when all the informative subgoals
  have been solved. This implies that logical lemmas can stay at the end
  of the automatic proof which have to be solved by the user.
\item {\tt Program\_Expand}
  \tacindex{Program\_Expand}\label{Program_Expand}\\
  The \verb=Program_Expand= tactic transforms the current program into
  the same program with the head constant expanded. This tactic
  particularly allows the user to force a program to be reduced before
  each application of the \verb=Program= tactic.

  \begin{ErrMsgs}
  \item \errindex{Not reducible}\\
    The head of the program is not a constant or is an opaque constant.
    need to attach a program to the current goal by using {\tt Realizer}.
    Perhaps, you already attached a program but a {\tt Restart} or an
    {\tt Undo} has removed it.
  \end{ErrMsgs}
\end{Variants}

\asubsection{Hints for {\tt Program}}

\begin{description}
\item[Mutual inductive types] The \verb=Program= tactic can deal with
  mutual inductive types. But, this needs the use of
  annotations. Indeed, when associating a mutual fixpoint program to a
  specification, the specification is associated to the first (the
  outermost) function defined by the fixpoint. But, the specifications
  to be associated to the other functions cannot be automatically
  derived. They have to be explicitly given by the user as
  annotations. See section \ref{program-ex-mutual} for an example.
  
\item[Constants] The \verb=Program= tactic is very sensitive to the
  status of constants. Constants can be either opaque (their body
  cannot be viewed) or transparent. The best of way of doing is to
  leave constants opaque (this is the default). If it is needed after,
  it is best to use the \verb=Transparent= command {\bf after} having
  used the \verb=Program= tactic.
\end{description}

\asection{Syntax for programs}
\label{program-syntax}
\asubsection{Pure programs}
The language to express programs is called \real\footnote{It
  corresponds to \FW\ plus inductive definitions}. Programs are
explicitly typed\footnote{This information is not strictly needed but
  was useful for type checking in a first experiment.} like terms
extracted from proofs. Some extra expressions have been added to have
a simpler syntax.

This is the raw form of what we call pure programs. But, in fact, it
appeared that this simple type of programs is not sufficient. Indeed,
all the logical part useful for the proof is not contained in these
programs. That is why annotated programs are introduced.

\asubsection{Annotated programs}
The notion of annotation introduces in a program a logical assertion
that will be used for the proof. The aim of the \verb=Program= tactic
is to start from a specification and a program and to generate
subgoals either logical or associated with programs. However, to find
the good specification for subprograms is not at all trivial in
general.  For instance, if we have to find an invariant for a loop, or
a well founded order in a recursive call.

So, annotations add in a program the logical part which is needed for
the proof and which cannot be automatically retrieved. This allows the
system to do proofs it could not do otherwise.

For this, a particular syntax is needed which is the following: since
they are specifications, annotations follow the same internal syntax
as \Coq~terms. We indicate they are annotations by putting them
between \verb={= and \verb=}= and preceding them with \verb=:: ::=.
Since annotations are \Coq~terms, they can involve abstractions over
logical propositions that have to be declared. Annotated-$\lambda$
have to be written between \verb=[{= and \verb=}]=.
Annotated-$\lambda$ can be seen like usual $\lambda$-bindings but
concerning just annotations and not \Coq~programs.

\asubsection{Recursive Programs}
Programs can be recursively defined using the following syntax: \verb=<={\it
  type-of-the-result}\verb=> rec= \index{rec@{\tt rec}} {\it
  name-of-the-induction-hypothesis} \verb=:: :: {= {\it
    well-founded-order-of-the-recursion} \verb=}= and then the body of
the program (see section \ref{program-examples}) which must always begin with
an abstraction [x:A] where A is the type of the arguments of the
function (also on which the ordering relation acts).

\asubsection{Implicit arguments}

A synthesis of implicit arguments has been added in order to
allow the user to write a minimum of types in a program. Then, it is
possible not to write a type inside a program term. This type has then
to be automatically synthesized. For this, it is necessary to indicate
where the implicit type to be synthesized appears. The syntax is the
current one of implicit arguments in \Coq: the question mark
\verb+?+. 

This synthesis of implicit arguments is not possible everywhere in a
program. In fact, the synthesis is only available inside a
\verb+Match+, a \verb+Cases+ or a \verb+Fix+ construction (where
\verb+Fix+ is a syntax for defining fixpoints).

\asubsection{Grammar}
The grammar for programs is described in figure \ref{pgm-syntax}.

\begin{figure}
\begin{tabular}{lcl}
{\pg} & ::= & {\ident}\\
 & $|$ & {\tt ?} \\
 & $|$ & {\tt [} {\ident} {\tt :} {\pg} {\tt ]} {\pg} \\
 & $|$ & {\tt [} {\ident} {\tt ]} {\pg} \\
 & $|$ & {\tt (} {\ident} {\tt :} {\pg} {\tt )} {\pg} \\
 & $|$ & {\tt (} {\pgs} {\tt )} \\
 & $|$ & {\tt Match} {\pg} {\tt with} {\pgs} {\tt end} \\
 & $|$ & \verb=<={\pg}\verb=>={\tt Match} {\pg} {\tt with} {\pgs} {\tt end} \\
 & $|$ & {\tt Cases} {\pg} {\tt of} \sequence{\eqn} {|} {\tt end} \\
 & $|$ & \verb=<={\pg}\verb=>={\tt Cases} {\pg} {\tt of}
 \sequence{\eqn} {|} {\tt end} \\ 
 & $|$ & {\tt Fix} {\ident} \verb.{.\nelist{\fixpg}{with} \verb.}. \\
 & $|$ & {\tt Cofix} {\ident} \{{\ident} {\tt :} {\pg} {\tt :=} {\pg}
 {\tt with} {\ldots} {\tt with} {\ident} {\tt :} {\pg} {\tt :=} {\pg}\} \\
 & $|$ & {\pg} {\tt ::} {\tt ::} \{ {\term} \} \\
 & $|$ & {\tt [\{} {\ident} {\tt :} {\term} {\tt \}]} {\pg}  \\
 & $|$ & {\tt let}
  {\tt (} {\ident} {\tt ,} {\ldots} {\tt ,} {\ident} {\tt ,} {\dots}
  {\tt ,} {\ident} {\tt )} {\tt =} {\pg} {\tt in} {\pg} \\
% & $|$ & \verb=<={\pg}\verb=>={\tt let} {\tt (} {\ident} {\tt ,} {\ldots} {\tt
% ,} {\ident} {\tt :} {\pg} {\tt ;} {\ldots} {\tt ;} {\ident} {\tt ,}
% {\ldots} {\tt ,} {\ident} {\tt :} {\pg} {\tt )} {\tt =} {\pg} {\tt
% in} {\pg} \\ 
 & $|$ & \verb=<={\pg}\verb=>={\tt let} {\tt (} {\ident} {\tt ,}
 {\ldots} {\tt ,} {\ldots} {\tt ,} {\ident} {\tt )} {\tt =} {\pg} {\tt
 in} {\pg} \\ 
 & $|$ & {\tt if} {\pg} {\tt then} {\pg} {\tt else} {\pg} \\
 & $|$ & \verb=<={\pg}\verb=>={\tt if} {\pg} {\tt then} {\pg} {\tt
 else} {\pg} \\ 
 & $|$ & \verb=<={\pg}\verb=>={\tt rec} {\ident} {\tt ::} {\tt ::} \{ \term \}
  {\tt [} {\ident} {\tt :} {\pg} {\tt ]} {\pg} \\
  {\pgs} & ::= & \pg \\
 & $|$ & {\pg} {\pgs}\\
{\fixpg} & ::= & {\ident} {\tt [} \nelist{\typedidents}{;} {\tt ]} {\tt :} {\pg} {\tt :=} {\pg}  \\
         & $|$ & {\ident} {\tt /} {\num} {\tt :} {\pg} {\tt :=} {\pg} {\tt ::} {\tt ::} \{ {\term} \} \\
{\simplepattern}  & ::= & {\ident} \\
 & $|$ & \verb!(! \nelist{\ident}{} \verb!)! \\
{\eqn} & ::= &  {\simplepattern} ~\verb!=>! ~\pg \\
\end{tabular}
\caption{Syntax of annotated programs}
\label{pgm-syntax}
\end{figure}

As for {\Coq} terms (see section \ref{term}), {\tt (}{\pgs}{\tt )}
associates to the left. The syntax of {\term} is the one in section.
The infix annotation operator \verb!:: ::! binds more than the
abstraction and product constructions.
\ref{term}.

The reference to an identifier of the \Coq\ context (in particular a
constant) inside a program of the
language \real\ is a reference to its extracted contents.

\asection{Examples}
\label{program-examples}
\asubsection{Ackermann Function}
Let us give the specification of Ackermann's function. We want to
prove that for every $n$ and $m$, there exists a $p$ such that
$ack(n,m)=p$ with:

\begin{eqnarray*}
ack(0,n) & = & n+1 \\
ack(n+1,0) & = & ack(n,1) \\
ack(n+1,m+1) & = & ack(n,ack(n+1,m))
\end{eqnarray*}

An ML program following this specification can be:

\begin{verbatim}
let rec ack = function
        0  -> (function m -> Sm)
      | Sn -> (function  0  -> ack n 1
                       | Sm -> ack n (ack Sn m))
\end{verbatim}

Suppose we give the following definition in \Coq~of a ternary relation
\verb=(Ack n m p)= in a Prolog like form representing $p=ack(n,m)$:

\begin{coq_example*}
Inductive Ack : nat->nat->nat->Prop :=
     AckO : (n:nat)(Ack O n (S n))
   | AcknO : (n,p:nat)(Ack n (S O) p)->(Ack (S n) O p)
   | AckSS : (n,m,p,q:nat)(Ack (S n) m q)->(Ack n q p)
                  ->(Ack (S n) (S m) p).
\end{coq_example*}
Then the goal is to prove that $\forall n,m .\exists p.(Ack~n~m~p)$, so
the specification is:

\verb!(n,m:nat){p:nat|(Ack n m p)}!.
The associated {\real} program corresponding to the above ML program can be defined as a fixpoint:
\begin{coq_example*}
Fixpoint ack_func [n:nat] : nat -> nat :=
  Cases n of
      O    => [m:nat](S m)
  | (S n') => Fix ack_func2 {ack_func2 [m:nat] : nat :=
                 Cases m of
                   O      => (ack_func n' (S O))
                 | (S m') => (ack_func n' (ack_func2 m')) 
                 end} 
  end.
\end{coq_example*}
The program is associated by using \verb=Realizer ack_func=. The
program is automatically expanded. Each realizer which is a constant
is automatically expanded. Then, by repeating the \verb=Program=
tactic, three logical lemmas are generated and are easily solved by
using the property Ack0, Ackn0 and AckSS.
\begin{coq_eval}
Goal (n,m:nat){p:nat|(Ack n m p)}.
Realizer ack_func.
\end{coq_eval}
\begin{coq_example}
Repeat Program.
\end{coq_example}


\asubsection{Euclidean Division}
This example shows the use of {\bf recursive programs}. Let us
give the specification of the euclidean division algorithm. We want to
prove that for $a$ and $b$ ($b>0$), there exist $q$ and $r$ such that
$a=b*q+r$ and $b>r$.

An ML program following this specification can be:
\begin{verbatim}
let div b a = divrec a where rec divrec = function
        if (b<=a) then let (q,r) = divrec (a-b) in (Sq,r)
                  else (0,a)
\end{verbatim}
Suppose we give the following definition in \Coq~which describes what
has to be proved, ie, $\exists q \exists r.~(a=b*q+r \wedge ~b>r)$:
\begin{coq_eval}
Abort.
Require Arith.
\end{coq_eval}
\begin{coq_example*}
Inductive diveucl [a,b:nat] : Set 
        := divex : (q,r:nat)(a=(plus (mult q b) r))->(gt b r)
                       ->(diveucl a b).
\end{coq_example*}
The decidability of the ordering relation has to be proved first, by
giving the associated function of type \verb!nat->nat->bool!:
\begin{coq_example*}
Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
Realizer Fix le_gt_bool {le_gt_bool [n:nat] : nat -> bool := 
             Cases n of 
             | O => [m:nat]true
             | (S n') => [m:nat]Cases m of
                         | O => false
                         | (S m') => (le_gt_bool n' m')
                         end
             end}.
Program_all.
Save.
\end{coq_example*}
Then the specification is \verb!(b:nat)(gt b O)->(a:nat)(diveucl a b)!.
The associated program corresponding to the ML program will be:
\begin{coq_eval}
Definition lt := [n,m:nat](gt m n).
Theorem eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b).
\end{coq_eval}
\begin{coq_example*}
Realizer 
      [b:nat](<nat*nat>rec div :: :: { lt }
              [a:nat]if (le_gt_dec b a) 
                        then let (q,r) = (div (minus a b))
                                      in ((S q),r)
                        else (O,a)).
\end{coq_example*}
Where \verb=lt= is the well-founded ordering relation defined by:
\begin{coq_example}
Print lt.
\end{coq_example}
Note the syntax for recursive programs as explained before. The
\verb=rec= construction needs 4 arguments: the type result of the
function (\verb=nat*nat= because it returns two natural numbers)
between \verb=<= and \verb=>=, the name of the induction hypothesis
(which can be used for recursive calls), the ordering relation
\verb=lt= (as an annotation because it is a specification), and the
program itself which must begin with a $\lambda$-abstraction. The
specification of \verb=le_gt_dec= is known because it is a previous
lemma.
The term \verb!(le_gt_dec b a)! is seen by the \verb!Program! tactic
as a term of type \verb!bool! which satisfies the specification 
\verb!{(le a b)}+{(gt a b)}!. 
The tactics \verb=Program_all= or \verb=Program= can be used, and the
following logical lemmas are obtained:
\begin{coq_example}
Repeat Program.
\end{coq_example}
The subgoals 4, 5 and 6 are resolved by \verb=Auto= (if you use
\verb=Program_all= they don't appear, because \verb=Program_all= tries
to apply \verb=Auto=). The other ones have to be solved by the user.


\asubsection{Insertion sort}
This example shows the use of {\bf annotations}. Let us give the
specification of a sorting algorithm. We want to prove that for a
sorted list of natural numbers $l$ and a natural number $a$, we can
build another sorted list $l'$, containing all the elements of $l$
plus $a$.

An ML program implementing the insertion sort and following this
specification can be:
\begin{verbatim}
let sort a l = sortrec l where rec sortrec = function
        []    -> [a]
      | b::l' -> if a<b then a::b::l' else b::(sortrec l')
\end{verbatim}
Suppose we give the following definitions in \Coq:

First, the decidability of the ordering relation:
\begin{coq_eval}
Reset Initial.
Require Le.
Require Gt.
\end{coq_eval}
\begin{coq_example*}
Fixpoint inf_dec [n:nat] : nat -> bool :=
[m:nat]Cases n of
         O      => true
       | (S n') => Cases m of
                      O     => false 
                   | (S m') => (inf_dec n' m')
                   end 
       end.
\end{coq_example*}

The definition of the type \verb=list=:
\begin{coq_example*}
Inductive list : Set := nil : list | cons : nat -> list -> list.
\end{coq_example*}

We define the property for an element \verb=x= to be {\bf in} a list
\verb=l= as the smallest relation such that: $\forall a \forall
l~(In~x~l) \Ra (In~x~(a::l))$ and $\forall l~(In~x~(x::l))$.
\begin{coq_example*}
Inductive In [x:nat] : list->Prop
        := Inl  : (a:nat)(l:list)(In x l) -> (In x (cons a l))
        | Ineq : (l:list)(In x (cons x l)).
\end{coq_example*}

A list \verb=t'= is equivalent to a list \verb=t= with one added
element \verb=y= iff: $(\forall x~(In~x~t) \Ra (In~x~t'))$ and
$(In~y~t')$ and $\forall x~(In~x~t') \Ra ((In~x~t) \vee y=x)$. The
following definition implements this ternary conjunction.
\begin{coq_example*}
Inductive equiv [y:nat;t,t':list]: Prop :=
      equiv_cons : 
        ((x:nat)(In x t)->(In x t'))
        -> (In y t')
        ->((x:nat)(In x t')->((In x t)\/y=x))
        -> (equiv y t t').
\end{coq_example*}

Definition of the property of list to be sorted, still defined
inductively:
\begin{coq_example*}
Inductive sorted : list->Prop
        := sorted_nil  : (sorted nil)
        | sorted_trans : (a:nat)(sorted (cons a nil))
        | sorted_cons : (a,b:nat)(l:list)(sorted (cons b l)) -> (le a b) 
                         -> (sorted (cons a (cons b l))).
\end{coq_example*}
Then the specification is:\\
\verb!(a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}!.

The associated \real\ program corresponding to the ML program will be:
\begin{coq_eval}
Lemma toto : (a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}.
\end{coq_eval}
\begin{coq_example*}
Realizer
  Fix list_insert{list_insert [a:nat; l:list] : list := 
         Cases l of
         | nil => (cons a nil)
         | (cons b m) => 
                if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} } 
                then (cons b (list_insert a m))
                else (cons a (cons b m))
         end}.
\end{coq_example*}
% Realizer [a:nat][l:list]
%          Match l with
%           (cons a nil)
%           [b,m,H]if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} } 
%                  then (cons b H)
%                  else (cons a (cons b m))
%          end.
Note that we have defined \verb=inf_dec= as the program realizing the
decidability of the ordering relation on natural numbers. But, it has
no specification, so an annotation is needed to give this
specification. This specification is used and then the decidability of
the ordering relation on natural numbers has to be proved using the
index program.

Suppose \verb=Program_all= is used, a few logical
lemmas are obtained (which have to be solved by the user):
\begin{coq_example}
Program_all.
\end{coq_example}


\asubsection{Quicksort}
This example shows the use of {\bf programs using previous
programs}. Let us give the specification of Quicksort. We want to
prove that for a list of natural numbers $l$, we can build a sorted
list $l'$, which is a permutation of the previous one.

An ML program following this specification can be:
\begin{verbatim}
let rec quicksort l = function
   []   -> []
 | a::m -> let (l1,l2) = splitting a m in
                 let m1 = quicksort l1 and
                 let m2 = quicksort l2 in m1@[a]@m2
\end{verbatim}
Where \verb=splitting= is defined by:
\begin{verbatim}
let rec splitting a l = function
        []   -> ([],[])
      | b::m -> let (l1,l2) = splitting a m in
                 if a<b then (l1,b::l2)
                        else (b::l1,l2)
\end{verbatim}
Suppose we give the following definitions in \Coq:

Declaration of the ordering relation:
\begin{coq_eval}
Reset Initial.
Require List.
Require Gt.
\end{coq_eval}
\begin{coq_example*}
Variable   inf : A -> A -> Prop.
Definition sup  := [x,y:A]~(inf x y).
Hypothesis inf_sup : (x,y:A){(inf x y)}+{(sup x y)}.
\end{coq_example*}
Definition of the concatenation of two lists:
\begin{coq_eval}
Write State toto.
\end{coq_eval}
\begin{coq_example*}
Fixpoint app [l:list] : list -> list 
      := [m:list]Cases l of
                   nil => m 
                 | (cons a l1) => (cons a (app l1 m)) end.
\end{coq_example*}
\begin{coq_eval}
Restore State toto.
\end{coq_eval}
Definition of the permutation of two lists:
\begin{coq_eval}
Definition mil := [a:A][l,m:list](app l (cons a m)) : A->list->list->list.
Lemma mil_app : (a:A)(l,m,n:list)(mil a l (app m n))=(app (mil a l m) n).
        Intros.
        Unfold mil.
        Elim (ass_app l (cons a m) n).
        Auto.
Save.
\end{coq_eval}
\begin{coq_example*}
Inductive permut : list->list->Prop :=
    permut_nil  : (permut nil nil)
   |permut_tran : (l,m,n:list)(permut l m)->(permut m n)->(permut l n)
   |permut_cmil : (a:A)(l,m,n:list)
         (permut l (app m n))->(permut (cons a l) (mil a m n))
   |permut_milc : (a:A)(l,m,n:list)
         (permut (app m n) l)->(permut (mil a m n) (cons a l)).
\end{coq_example*}
\begin{coq_eval}
Hints Resolve permut_nil permut_cmil permut_milc.
Lemma permut_cons : (a:A)(l,m:list)(permut l m)->(permut (cons a l) (cons a m)).
        Intros.
        Change (permut (cons a l) (mil a nil m)).
        Auto.
Save.
Hints Resolve permut_cons.
Lemma permut_refl : (l:list)(permut l l).
        Induction l ; Auto.
Save.
Hints Resolve permut_refl.
Lemma permut_sym : (l,m:list)(permut l m)->(permut m l).
        Intros l m h1 ; Elim h1 ; Auto.
        Intros l0 m0 n h2 h3 h4 h5.
        Apply permut_tran with m0 ; Auto.
Save.
Hints Immediate permut_sym.
Lemma permut_app1 : (m1,n1,l:list)(permut m1 n1)->(permut (app l m1) (app l n1)).
        Intros ; Elim l ; Simpl ; Auto.
Save.
Hints Resolve permut_app1.
Lemma permut_app_mil : (a:A)(l1,m1,l2,m2,n2:list)
     (permut (app l1 m1) (app (app l2 m2) n2))
                -> (permut (app (cons a l1) m1) (app (mil a l2 m2) n2)).
        Intros ; Simpl.
        Elim (mil_app a l2 m2 n2).
        Apply permut_cmil.
        Elim (app_ass l2 m2 n2) ; Auto.
Save.
Hints Resolve permut_app_mil.
Lemma permut_app_app : (m1,m2,n1,n2 :list)
     (permut m1 n1)->(permut m2 n2)->(permut (app m1 m2) (app n1 n2)).
        Intros m1 m2 n1 n2 h1 h2.
        Elim h1 ; Intros.
        exact h2.
        Apply permut_tran with (app m n2) ; Auto.
        Apply permut_tran with (app m m2) ; Auto.
        Auto.
        Apply permut_sym ; Auto.
Save.
Hints Resolve permut_app_app.
Lemma permut_app : (m,m1,m2,n1,n2 :list)(permut m1 n1)->(permut m2 n2)->
     (permut m (app m1 m2))->(permut m (app n1 n2)).
        Intros.
        Apply permut_tran with (app m1 m2) ; Auto.
Save.
\end{coq_eval}
The definitions \verb=inf_list= and \verb=sup_list= allow to know if
an element is lower or greater than all the elements of a list:
\begin{coq_example*}
Section Rlist_.
Variable R : A->Prop.
Inductive Rlist  : list -> Prop :=
    Rnil : (Rlist nil)
  | Rcons : (x:A)(l:list)(R x)->(Rlist l)->(Rlist (cons x l)).
\end{coq_example*}
\begin{coq_eval}
Hints Resolve Rnil Rcons.
Lemma Rlist_app : (m,n:list)(Rlist m)->(Rlist n)->(Rlist (app m n)).
        Intros m n h1 h2 ; Elim h1 ; Simpl ; Auto.
Save.
Hints Resolve Rlist_app.
Section Rlist_cons_.
Variable a : A.
Variable l : list.
Hypothesis Rc : (Rlist (cons a l)).
Lemma Rlist_cons : (R a)/\(Rlist l).
    Inversion_clear Rc; Auto.
Save.
End Rlist_cons_.
Section Rlist_append.
Variable n,m : list.
Lemma Rlist_appd : (Rlist (app n m))->((Rlist n)/\(Rlist m)).
Elim n ; Simpl; Auto.
Intros a y h1 h2.
Elim (Rlist_cons a (app y m)) ; Auto.
Intros h3 h4; Elim h1 ; Auto.
Save.
End Rlist_append.
Hints Resolve Rlist_appd.
Lemma Rpermut : (m,n:list)(permut m n)->(Rlist m)->(Rlist n).
        Intros m n h1 ; Elim h1 ; Unfold mil ; Auto.
        Intros a l m0 n0 h2 h3 h4.
        Elim (Rlist_cons a l); Auto.
        Intros h5 h6; Elim (Rlist_appd m0 n0); Auto.
        Intros a l m0 n0 h2 h3 h4.
        Elim (Rlist_appd m0 (cons a n0)) ; Auto.
        Intros h5 h6; Elim (Rlist_cons a n0) ; Auto.
Save.
\end{coq_eval}
\begin{coq_example*}
End Rlist_.
Hints Resolve Rnil Rcons.
\end{coq_example*}
\begin{coq_eval}
Hints Resolve Rlist_app.
\end{coq_eval}
\begin{coq_example*}
Section Inf_Sup.
Hypothesis x : A.
Hypothesis l : list.
Definition inf_list := (Rlist (inf x) l).
Definition sup_list := (Rlist (sup x) l).
End Inf_Sup.
\end{coq_example*}
\begin{coq_eval}
Hints Unfold  inf_list sup_list.
\end{coq_eval}
Definition of the property of a list to be sorted:
\begin{coq_example*}
Inductive sort : list->Prop :=
     sort_nil : (sort nil)
   | sort_mil : (a:A)(l,m:list)(sup_list a l)->(inf_list a m)
        ->(sort l)->(sort m)->(sort (mil a l m)).
\end{coq_example*}
\begin{coq_eval}
Hints Resolve sort_nil sort_mil.
Lemma permutapp : (a0:A)(y,l1,l2:list)(permut y (app l1 l2))->(permut (cons a0 y) (app l1 (cons a0 l2))).
Intros.
exact (permut_cmil a0 y l1 l2 H).
Save.
Hints Resolve permutapp.
Lemma sortmil : (a:A)(x,x0,l1,l2:list)(sup_list a l1)->(inf_list a l2)->(sort x)->(sort x0)->(permut l1 x)->(permut l2 x0)->(sort (mil a x x0)).
Intros.
Apply sort_mil ; Auto.
Unfold sup_list ; Apply Rpermut with l1 ; Auto. 
Unfold inf_list ; Apply Rpermut with l2 ; Auto.
Save.
\end{coq_eval}

\noindent Then the goal to prove is 
$\forall l~\exists m~(sort~m) \wedge (permut~l~m)$ and the specification is 

\verb!(l:list){m:list|(sort m)&(permut l m)!.

\noindent Let us first prove a preliminary lemma. Let us define \verb=ltl= a
well-founded ordering relation.

\begin{coq_example*}
Definition ltl := [l,m:list](gt (length m) (length l)). 
\end{coq_example*}
\begin{coq_eval}
Hints Unfold ltl.
Lemma ltl_cons : (a,a0:A)(l1,y:list)(ltl l1 (cons a y))->(ltl l1 (cons a (cons a0 y))).
Unfold ltl; Simpl; Auto.
Save.
Hints Resolve ltl_cons.
Lemma ltl_cons_cons : (a,a0:A)(l2,y:list)(ltl l2 (cons a y))->(ltl (cons a0 l2) (cons a (cons a0 y))).
Unfold ltl; Simpl; Auto with arith..
Save.
Hints Resolve ltl_cons_cons.
Require Wf_nat.
\end{coq_eval}
Let us then give a definition of \verb=Splitting_spec= corresponding
to\\
$\exists l_1 \exists l_2.~(sup\_list~a~l_1) \wedge (inf\_list~a~l_2) 
\wedge (l \equiv l_1@l_2) \wedge (ltl~l_1~(a::l)) \wedge
(ltl~l2~(a::l))$ and a theorem on this definition.
\begin{coq_example*}
Inductive Splitting_spec [a:A; l:list] : Set :=
      Split_intro : (l1,l2:list)(sup_list a l1)->(inf_list a l2)
                    ->(permut l (app l1 l2))
                    ->(ltl l1 (cons a l))->(ltl l2 (cons a l))
                    ->(Splitting_spec a l).
\end{coq_example*}
\begin{coq_example*}
Theorem Splitting : (a:A)(l:list)(Splitting_spec a l).
Realizer 
  Fix split {split [a:A;l:list] : list*list := 
    Cases l of 
    | nil => (nil,nil)
    | (cons b m) => let (l1,l2) = (split a m) in
               if (inf_sup a b)
               then (* inf a b *) (l1,(cons b l2))
               else (* sup a b *) ((cons b l1),l2)
    end}.
Program_all.
Simpl; Auto.
Save.
\end{coq_example*}
% Realizer [a:A][l:list]
%     Match l with 
%     (* nil *) (nil,nil)
%   (* cons  *) [b,m,ll]let (l1,l2) = ll in
%                       if (inf_sup a b)
%                                    then (* inf a b *) (l1,(cons b l2))
%                                    else (* sup a b *) ((cons b l1),l2)
%     end.

The associated {\real} program to the specification we wanted to first
prove and corresponding to the ML program will be:
\begin{coq_example*}
Lemma Quicksort: (l:list){m:list|(sort m)&(permut l m)}.
Realizer <list>rec quick :: :: { ltl }
           [l:list]Cases l of 
              nil => nil
           | (cons a m) => let (l1,l2) = (Splitting a m) in
                                 (mil a (quick l1) (quick l2))
           end.
\end{coq_example*}
Then \verb=Program_all= gives the following logical lemmas (they have
to be resolved by the user):
\begin{coq_example}
Program_all.
\end{coq_example}
\begin{coq_eval}
Abort.
\end{coq_eval}

\asubsection{Mutual Inductive Types}
\label{program-ex-mutual}
This example shows the use of {\bf mutual inductive types} with
\verb=Program=. Let us give the specification of trees and forest, and
two predicate to say if a natural number is the size of a tree or a
forest. 

\begin{coq_example*}
Section TreeForest.

Variable A : Set.

Mutual Inductive 
     tree   : Set := node : A -> forest -> tree
with forest : Set := empty : forest 
                  | cons : tree -> forest -> forest.

Mutual Inductive Tree_Size : tree -> nat -> Prop :=
  Node_Size : (n:nat)(a:A)(f:forest)(Forest_Size f n)
               ->(Tree_Size (node a f) (S n))
with Forest_Size : forest -> nat -> Prop :=
  Empty_Size : (Forest_Size empty O)
| Cons_Size : (n,m:nat)(t:tree)(f:forest)
    (Tree_Size t n)
    ->(Forest_Size f m)
    ->(Forest_Size (cons t f) (plus n m)).

Hints Resolve Node_Size Empty_Size Cons_Size.
\end{coq_example*}

Then, let us associate the two mutually dependent functions to compute
the size of a forest and a tree to the the following specification:

\begin{coq_example*}
Theorem tree_size_prog : (t:tree){n:nat | (Tree_Size t n)}.

Realizer [t:tree]
(Fix tree_size{
  tree_size [t:tree] : nat := let (a,f) = t in (S (forest_size f))
  with forest_size /1 : forest -> nat 
    := ([f:forest]Cases f of
         empty => O
       | (cons t f') => (plus (tree_size t) (forest_size f'))
       end)
       :: :: {(f:forest) {n:nat | (Forest_Size f n)}}}
                   t).
\end{coq_example*}

It is necessary to add an annotation for the \verb=forest_size=
function. Indeed, the global specification corresponds to the
specification of the \verb=tree_size= function and the specification
of \verb=forest_size= cannot be automatically inferred from the
initial one.

Then, the \verb=Program_all= tactic can be applied:
\begin{coq_example}
Program_all.
Save.
\end{coq_example}

% $Id$ 

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