3
\aauthor{Matthieu Sozeau}
7
\em The status of \Program\ is experimental.
10
We present here the new \Program\ tactic commands, used to build certified
11
\Coq\ programs, elaborating them from their algorithmic skeleton and a
12
rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction
13
(see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular
14
functional programming language whilst using as rich a specification as
15
desired and proving that the code meets the specification using the whole \Coq{} proof
16
apparatus. This is done using a technique originating from the
17
``Predicate subtyping'' mechanism of \PVS \cite{Rushby98}, which generates type-checking
18
conditions while typing a term constrained to a particular type.
19
Here we insert existential variables in the term, which must be filled
20
with proofs to get a complete \Coq\ term. \Program\ replaces the
21
\Program\ tactic by Catherine Parent \cite{Parent95b} which had a similar goal but is no longer
24
The languages available as input are currently restricted to \Coq's term
25
language, but may be extended to \ocaml{}, \textsc{Haskell} and others
26
in the future. We use the same syntax as \Coq\ and permit to use implicit
27
arguments and the existing coercion mechanism.
28
Input terms and types are typed in an extended system (\Russell) and
29
interpreted into \Coq\ terms. The interpretation process may produce
30
some proof obligations which need to be resolved to create the final term.
32
\asection{Elaborating programs}
33
The main difference from \Coq\ is that an object in a type $T : \Set$
34
can be considered as an object of type $\{ x : T~|~P\}$ for any
35
wellformed $P : \Prop$.
36
If we go from $T$ to the subset of $T$ verifying property $P$, we must
37
prove that the object under consideration verifies it. \Russell\ will
38
generate an obligation for every such coercion. In the other direction,
39
\Russell\ will automatically insert a projection.
41
Another distinction is the treatment of pattern-matching. Apart from the
42
following differences, it is equivalent to the standard {\tt match}
43
operation (see Section~\ref{Caseexpr}).
45
\item Generation of equalities. A {\tt match} expression is always
46
generalized by the corresponding equality. As an example,
55
will be first rewrote to:
57
(match x as y return (x = y -> _) with
58
| 0 => fun H : x = 0 -> t
59
| S n => fun H : x = S n -> u
63
This permits to get the proper equalities in the context of proof
64
obligations inside clauses, without which reasoning is very limited.
66
\item Generation of inequalities. If a pattern intersects with a
67
previous one, an inequality is added in the context of the second
68
branch. See for example the definition of {\tt div2} below, where the second
69
branch is typed in a context where $\forall p, \_ <> S (S p)$.
71
\item Coercion. If the object being matched is coercible to an inductive
72
type, the corresponding coercion will be automatically inserted. This also
73
works with the previous mechanism.
76
If you do specify a {\tt return} or {\tt in} clause the typechecker will
77
fall back directly to \Coq's usual typing of dependent pattern-matching.
79
The next two commands are similar to their standard counterparts
80
Definition (see Section~\ref{Simpl-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
81
they define constants. However, they may require the user to prove some
82
goals to construct the final definitions.
84
\subsection{\tt Program Definition {\ident} := {\term}.
85
\comindex{Program Definition}\label{ProgramDefinition}}
87
This command types the value {\term} in \Russell\ and generate proof
88
obligations. Once solved using the commands shown below, it binds the final
89
\Coq\ term to the name {\ident} in the environment.
92
\item \errindex{{\ident} already exists}
96
\item {\tt Program Definition {\ident} {\tt :}{\term$_1$} :=
98
It interprets the type {\term$_1$}, potentially generating proof
99
obligations to be resolved. Once done with them, we have a \Coq\ type
100
{\term$_1'$}. It then checks that the type of the interpretation of
101
{\term$_2$} is coercible to {\term$_1'$}, and registers {\ident} as
102
being of type {\term$_1'$} once the set of obligations generated
103
during the interpretation of {\term$_2$} and the aforementioned
104
coercion derivation are solved.
105
\item {\tt Program Definition {\ident} {\binder$_1$}\ldots{\binder$_n$}
106
{\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
107
This is equivalent to \\
108
{\tt Program Definition\,{\ident}\,{\tt :\,forall} %
109
{\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}} \\
110
\qquad {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
115
\item \errindex{In environment {\dots} the term: {\term$_2$} does not have type
117
\texttt{Actually, it has type {\term$_3$}}.
120
\SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
122
\subsection{\tt Program Fixpoint {\ident} {\params} {\tt \{order\}} : type := \term
123
\comindex{Program Fixpoint}
124
\label{ProgramFixpoint}}
126
The structural fixpoint operator behaves just like the one of Coq
127
(see Section~\ref{Fixpoint}), except it may also generate obligations.
128
It works with mutually recursive definitions too.
131
Require Import Program.
132
Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
134
| S (S p) => S (div2 p)
139
Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are
140
automatically generated by the pattern-matching compilation algorithm).
145
One can use a well-founded order or a measure as termination orders using the syntax:
148
Require Import Arith.
149
Require Import Program.
152
Definition id (n : nat) := n.
153
Program Fixpoint div2 (n : nat) {measure id n} :
154
{ x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
156
| S (S p) => S (div2 p)
161
The \verb|measure| keyword expects a measure function into the naturals, whereas
162
\verb|wf| expects a relation.
165
When defining structurally recursive functions, the
166
generated obligations should have the prototype of the currently defined functional
167
in their context. In this case, the obligations should be transparent
168
(e.g. using Defined) so that the guardedness condition on
169
recursive calls can be checked by the
170
kernel's type-checker. There is an optimization in the generation of
171
obligations which gets rid of the hypothesis corresponding to the
172
functionnal when it is not necessary, so that the obligation can be
173
declared opaque (e.g. using Qed). However, as soon as it appears in the
174
context, the proof of the obligation is \emph{required} to be declared transparent.
176
No such problems arise when using measures or well-founded recursion.
178
An important point about well-founded and measure-based functions is the following:
179
The recursive prototype of a function of type
180
{\binder$_1$}\ldots{\binder$_n$} \{ {\tt measure m \binder$_i$} \}:{\type$_1$},
182
\verb|{|{\binder$_i'$ \verb$|$ {\tt m} $x_i'$ < {\tt m} $x_i$}\verb|}|\ldots{\binder$_n$},{\type$_1$}.
183
So any arguments appearing before the recursive one are ignored for the
184
recursive calls, hence they are constant.
186
\subsection{\tt Program Lemma {\ident} : type.
187
\comindex{Program Lemma}
188
\label{ProgramLemma}}
190
The \Russell\ language can also be used to type statements of logical
191
properties. It will generate obligations, try to solve them
192
automatically and fail if some unsolved obligations remain.
193
In this case, one can first define the lemma's
194
statement using {\tt Program Definition} and use it as the goal afterwards.
195
Otherwise the proof will be started with the elobarted version as a goal.
196
The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt
197
Hypothesis}, {\tt Axiom} etc...
199
\section{Solving obligations}
200
The following commands are available to manipulate obligations. The
201
optional identifier is used when multiple functions have unsolved
202
obligations (e.g. when defining mutually recursive blocks). The optional
203
tactic is replaced by the default one if not specified.
206
\item {\tt Obligation Tactic := \tacexpr}\comindex{Obligation Tactic}
207
Sets the default obligation
208
solving tactic applied to all obligations automatically, whether to
209
solve them or when starting to prove one, e.g. using {\tt Next}.
210
\item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining
212
\item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of
213
obligation {\tt num}.
214
\item {\tt Next Obligation [of \ident]}\comindex{Next Obligation} Start the proof of the next
216
\item {\tt Solve Obligations [of \ident] [using
217
\tacexpr]}\comindex{Solve Obligations}
219
each obligation of \ident using the given tactic or the default one.
220
\item {\tt Solve All Obligations [using \tacexpr]} Tries to solve
221
each obligation of every program using the given tactic or the default
222
one (useful for mutually recursive definitions).
223
\item {\tt Admit Obligations [of \ident]}\comindex{Admit Obligations}
224
Admits all obligations (does not work with structurally recursive programs).
225
\item {\tt Preterm [of \ident]}\comindex{Preterm}
226
Shows the term that will be fed to
227
the kernel once the obligations are solved. Useful for debugging.
228
\item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations}
229
Control whether all obligations should be declared as transparent (the
230
default), or if the system should infer which obligations can be declared opaque.
233
The module {\tt Coq.Program.Tactics} defines the default tactic for solving
234
obligations called {\tt program\_simpl}. Importing
235
{\tt Coq.Program.Program} also adds some useful notations, as documented in the file itself.
237
\section{Frequently Asked Questions
241
\item {Ill-formed recursive definitions}
242
This error can happen when one tries to define a
243
function by structural recursion on a subset object, which means the Coq
246
\verb$Program Fixpoint f (x : A | P) := match x with A b => f b end.$
248
Supposing $b : A$, the argument at the recursive call to f is not a
249
direct subterm of x as b is wrapped inside an exist constructor to build
250
an object of type \verb${x : A | P}$. Hence the definition is rejected
251
by the guardedness condition checker. However you can do
252
wellfounded recursion on subset objects like this:
255
Program Fixpoint f (x : A | P) { measure size } :=
256
match x with A b => f b end.
259
You will then just have to prove that the measure decreases at each recursive
260
call. There are three drawbacks though:
262
\item You have to define the measure yourself;
263
\item The reduction is a little more involved, although it works
264
using lazy evaluation;
265
\item Mutual recursion on the underlying inductive type isn't possible
266
anymore, but nested mutual recursion is always possible.
272
%%% TeX-master: "Reference-Manual"
273
%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
added
removed
doc/refman/Program.tex
