From 6cf8d80ac0a9869d97373d6813441eabebce8980 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Feb 2006 13:58:10 +0000
Subject: Nettoyage de l'archive doc et restructuration avant intégration à
 l'archive principale de Coq et publication des sources (HH)

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

(limited to 'doc/Program.tex')

diff --git a/doc/Program.tex b/doc/Program.tex
deleted file mode 100644
index aa900ecb90..0000000000
--- a/doc/Program.tex
+++ /dev/null
@@ -1,850 +0,0 @@
-\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: 
-- 
cgit v1.2.3

