Initial revision

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 850 insertions, 0 deletions

diff --git a/doc/Program.tex b/doc/Program.tex
new file mode 100644
index 000000000..9fd6080b8
--- /dev/null
+++ b/doc/Program.tex
@@ -0,0 +1,850 @@
+\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}
+Restore State 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}
+Restore State 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}
+Save 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: