\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$