1 files changed, 251 insertions, 0 deletions
diff --git a/doc/Recursive-Definition.tex b/doc/Recursive-Definition.tex
new file mode 100755
index 000000000..77774d9fa
--- /dev/null
+++ b/doc/Recursive-Definition.tex
@@ -0,0 +1,251 @@
+\documentstyle[]{article}
+\input{title}
+
+\newcommand{\xx}{\noindent}
+\newcommand{\Coq}{{\sf 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
+{\sf ProPre} programming language. It has been adapted for
+the \Coq's framework. For a short description of the {\sf
+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 {\sf 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$