1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
|
\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$
|
