1 files changed, 0 insertions, 251 deletions
diff --git a/doc/Recursive-Definition.tex b/doc/Recursive-Definition.tex
deleted file mode 100755
index ba9423409..000000000
--- a/doc/Recursive-Definition.tex
+++ /dev/null
@@ -1,251 +0,0 @@
-\documentstyle[]{article}
-\input{title}
-
-\newcommand{\xx}{\noindent}
-\newcommand{\Coq}{\textsc{Coq}}
-
-\begin{document}
-
-\coverpage{Users friendly {\tt Recursive Definition}}{Pascal MANOURY}
-
-This command allows to define functions in
-the following syntax :
-\begin{verbatim}
-Recursive Definition f [X1:U1;..;Xk:Uk] : T1-> .. -> Tn -> T :=
- p11 .. p1n => t1
-...
-|pm1 .. pmn => tm.
-\end{verbatim}
-This definition schema must be understood as :
-\begin{itemize}
-\item {\tt f} is the name of the constant we want
-to define;
-\item {\tt (X1:U1)..(Xk:Uk) T1-> .. -> Tn -> T}
-is its intended type;
-\item {\tt  p11 .. p1n => t1 | ... |pm1 .. pmn => tm.}
-describe its beha\-viour in terms of patterns.
-We
-call the {\sl patterns clauses} this part of the {\tt Recursive Definition}.
-\end{itemize}
-The semantics of the {\tt Recursive Definition} 
-is to
-define the new constant {\tt f} as a term (say {\tt F}) of
-the intended type providing that {\tt F} has the intended
-computational behavior expressed in the {\sl patterns
-clauses}. Moreover, a {\tt Recursive Definition} states and
-proves all equational theorems corresponding to {\sl
-patterns clauses}. In other words, a {\tt Recursive Definition} is
-equivalent to :
-\begin{verbatim}
-Definition f : (X1:U1)..(Xk:Uk) T1-> .. -> Tn -> T := F.
-Theorem f_eq1 : (X1:U1)..(Xk:Uk)(x11:V11)..(x1l:V1l)(F X1 .. Xk p11 .. p1n)=t1.
-Intros; Unfold F; Simpl; Trivial. Save.
-...
-Theorem f_eqm : (X1:U1)..(Xk:Uk)(xm1:Vm1)..(xml:Vml)(F X1 .. Xk pm1 .. pmn)=tm.
-Intros; Unfold F; Simpl; Trivial. Save.
-\end{verbatim}
-For instance, one can write :
-\begin{coq_example}
-Recursive Definition Ack : nat -> nat -> nat :=
-  O m => (S m)
- |(S n) O => (Ack n (S O))
- |(S n) (S m) => (Ack n (Ack (S n) m)).
-\end{coq_example}
-
-Unfortunately, the problem of finding a term (of \Coq)
-satisfying a set of {\sl patterns clauses} does not always have a
-solution, as shown by the following example~:\\
-\centerline {\tt Recursive Definition fix :
-nat -> nat := n => (fix n).} 
-The point is that, in \Coq, any term {\tt F} of type {\tt
-nat -> nat} represents a function which always terminates
-and it is easy to see that the function {\tt fix} never
-terminates. This general property of \Coq's terms is called
-{\it strong normalization}.
-
-\xx
-The fact that a syntactically correct {\tt Recursive
-Definition} as the one of {\tt fix} does not correspond to any
-term in \Coq~ points out that we cannot content with the {\it
-syntactical level} of the declaration to obtain a term, but we
-have to lift up onto the {\it logical level} to ensure that
-the aimed function satisfies such a  strong property as
-termination. And here comes the difficulty, since the termination
-problem is known to be undecidable in general.
-
-\xx
-In fact, termination is the main logical property we
-have to face with. Then the main job of the {\tt Recursive
-Definition} is to build a proof of {\tt (X1:U1)..(Xk:Uk)
-T1-> .. -> Tn -> T} understood as a termination proof of the
-aimed function.\\
-Let's see how it works on the Ackermann's function example
-:
-\begin{coq_eval}
-Restore State Initial.
-\end{coq_eval}
-\begin{coq_example}
-Theorem Ack : nat -> nat -> nat.
-Intro n; Elim n.
-Intro m; exact (S m).
-Intros p Ack_n m; Elim m.
-exact (Ack_n (S O)).
-Intros q Ack_Sn_m; exact (Ack_n Ack_Sn_m).
-Save.
-\end{coq_example}
-One can check that the term {\tt Ack} ({\it eg} : the above
-proof of {\tt nat -> nat -> nat}) actually satisfies
-the intended {\sl patterns clauses} of Ackermann's
-function.
-
-\xx
-Such a proof is {\em automatically} synthesized by a
-{specialized strategy} which was originally designed for the
-\textsc{ProPre} programming language. It has been adapted for
-the \Coq's framework. For a short description of the \textsc{ProPre}
-programming language, we refer the reader to 
-\cite{MPSI}. For details 
-concerning the original proof search strategy, we refer the
-reader to \cite{MSAR}. For theoretical settings of the
-method involved in \textsc{ProPre}, we refer the reader to
-\cite{KRPA} and \cite{PARI}.
-
-\xx
-We list bellow some correct and incorrect usages of
-the {\tt Recursive Definition} feature. 
-
-\subsection*{Correct {\tt Recursive Definition}'s}
-\begin{coq_example*}
-Recursive Definition IfSet [X:Set] : bool -> X -> X -> X :=
-  true x y => x
- |false x y => y.
-Recursive Definition equal_nat : nat -> nat -> bool :=
-  O O => true
- |O (S m) => false
- |(S n) O => false
- |(S n) (S m) => (equal_nat n m).
-Recursive Definition less_equal : nat -> nat -> bool :=
-  O m => true
- |(S n) O => false
- |(S n) (S m) => (less_equal n m).
-Inductive Set bintree :=
-  Le : bintree
- |Br : nat -> bintree -> bintree -> bintree.
-Recursive Definition ins_bsr [n:nat] : bintree -> bintree :=
-  Le => (Br n Le Le)
- |(Br m a1 a2)
-  => (IfSet bintree (less_equal n m) (Br m (ins_bsr n a1) a2)
-         (Br m a1 (ins_bsr n a2))).
-Inductive list [X:Set] : Set :=
-  Nil : (list X)
- |Cons : X -> (list X) -> (list X).
-Recursive Definition append [X:Set;ys:(list X)] : (list X) -> (list X) :=
-  (Nil X) => ys
- |(Cons X x xs) => (Cons X x (append X ys xs)).
-Recursive Definition soml : (list nat) -> nat :=
-  (Nil nat) => O
- |(Cons nat O x) => (soml x)
- |(Cons nat (S n) x) => (S (soml (Cons nat n x))).
-Recursive Definition sorted_list : (list nat) -> Prop :=
-  (Nil nat) => True
- |(Cons nat n (Nil nat)) => True
-|(Cons nat n (Cons nat m x)) 
-  => (<bool>(less_equal n m)=true) /\ (sorted_list (Cons nat m x)).
-\end{coq_example*}
-
-\subsection*{Incorrect {\tt Recursive Definition}'s}
-\begin{coq_example}
-Recursive Definition equal_list : (list nat) -> (list nat) -> bool :=
-  (Nil nat) (Nil nat) => true
- |(Nil nat) (Cons nat n y) => false
- |(Cons nat n x) (Nil nat) => false
- |(Cons nat n x) (Cons nat n y) => (equal_list x y).
-\end{coq_example}
-As explains the error message, a same pattern variable can't be used
-more than one time.
-\begin{coq_example}
-Recursive Definition min : nat -> nat -> nat :=
-  O m => m
- |n O => n
- |(S n) (S m) => (S (min n m)).
-\end{coq_example}
-We do not allow the various left members of {\sl patterns clauses} to
-overlap.
-\begin{coq_example}
-Recursive Definition wrong_equal : nat -> nat -> bool :=
-  O O => true
- |(S n) (S m) => (wrong_equal n m).
-\end{coq_example}
-As we need to prove that the function is totally defined, we need an
-exhaustive pattern matching of the inputs.
-\begin{coq_example}
-Recursive Definition div2 : nat -> nat :=
-  O => O
- |(S O) => O
- |(S (S n)) => (S (div2 n)).
-\end{coq_example}
-The strategy makes use of structural induction to search a proof of
-{\tt nat -> nat}, then it can only accept arguments decreasing in one
-step ({\it eg} from {\tt (S n)} to {\tt n}) which is not the case
-here.
-\begin{coq_example}
-Recursive Definition wrong_fact : nat -> nat :=
- n => (IfSet nat (equal_nat n O) (S O) (mult n (wrong_fact (pred n)))).
-\end{coq_example}
-This error comes from the fact that the strategy doesn't recognize
-that the {\tt IfSet} is used as matching on naturals and that, when
-{\tt n} is not {\tt O}, {\tt (pred n)} is less than {\tt n}. Indeed,
-matching must be explicit and decreasing too.
-\begin{coq_example}
-Recursive Definition heap_merge : bintree -> bintree -> bintree :=
-  Le b => b
- |(Br n a1 a2) Le => (Br n a1 a2)
- |(Br n a1 a2) (Br m b1 b2)
-  => (IfSet bintree
-         (less_equal n m)
-         (Br n (heap_merge a1 a2) (Br m b1 b2))
-         (Br m (Br n a1 a2) (heap_merge  b1 b2))).
-\end{coq_example}
-This failure of the strategy is due to the fact than with simple
-structural induction one can't get any induction hypothesis for both
-inductive calls {\tt (heap\_merge a1 a2)} and {\tt (heap\_merge b1
-  b2)}.
-
-
-\begin{thebibliography}{9999}
-\bibitem{KRPA} J.L Krivine, M. Parigot
- {\it Programming with proofs} ; in SCT 87 (1987),
-Wendish-Rietz ; in EIK 26 (1990) pp 146-167.
-
-\bibitem{MPSI} P. Manoury, M. Parigot, M. Simonot {\it {\sf
-ProPre} : a programming language with proofs} ; in
-proceedings LPAR 92, LNAI 624.
-
-\bibitem{MSTH} P. Manoury and M. Simonot {\it Des preuves
-de totalit\'e de fonctions comme synth\`ese de
-programmes} ; Phd Thesis, Universit\'e Paris 7, December
-1992. 
-
-\bibitem{MSAR} P. Manoury and M. Simonot {\it
-Automatizing termination proof of recursively defined
-functions} ; to appear in TCS.
-
-\bibitem{PARI} M. Parigot {\it Recursive programming with
-proofs} ; in TCS 94 (1992) pp 335-356. 
-
-\bibitem{PAUL} C. Paulin-Mohring {\it Inductive
-Definitions in the System Coq - Rules and properties} ;
-proceedings TLCA 93, LNCS 664 (1993).
-
-\bibitem{WERN} B. Werner {\it Une th\'eorie des
-constructions inductives} ; Phd Thesis, Universit\'e Paris
-7, May 1994.
-
-\end{thebibliography}
-
-\end{document}
-
-
-
-
-% $Id$