blob: ab00fbfe37e97069795c9d859de95eb92a84f7d3 (
plain)
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
|
\achapter{\protect{Miscellaneous extensions}}
%HEVEA\cutname{miscellaneous.html}
\asection{Program derivation}
Coq comes with an extension called {\tt Derive}, which supports
program derivation. Typically in the style of Bird and Meertens or
derivations of program refinements. To use the {\tt Derive} extension
it must first be required with {\tt Require Coq.Derive.Derive}. When
the extension is loaded, it provides the following command.
\subsection[\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$]
{\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$\comindex{Derive}}
The name $\ident_1$ can appear in \term. This command opens a new
proof presenting the user with a goal for \term{} in which the name
$\ident_1$ is bound to a existential variables {\tt ?x} (formally,
there are other goals standing for the existential variables but they
are shelved, as described in Section~\ref{shelve}).
When the proof ends two constants are defined:
\begin{itemize}
\item The first one is name $\ident_1$ and is defined as the proof of
the shelved goal (which is also the value of {\tt ?x}). It is
always transparent.
\item The second one is name $\ident_2$. It has type {\tt \term}, and
its body is the proof of the initially visible goal. It is opaque if
the proof ends with {\tt Qed}, and transparent if the proof ends
with {\tt Defined}.
\end{itemize}
\Example
\begin{coq_example*}
Require Coq.derive.Derive.
Require Import Coq.Numbers.Natural.Peano.NPeano.
Section P.
Variables (n m k:nat).
\end{coq_example*}
\begin{coq_example}
Derive p SuchThat ((k*n)+(k*m) = p) As h.
Proof.
rewrite <- Nat.mul_add_distr_l.
subst p.
reflexivity.
\end{coq_example}
\begin{coq_example*}
Qed.
End P.
\end{coq_example*}
\begin{coq_example}
Print p.
Check h.
\end{coq_example}
Any property can be used as \term, not only an equation. In
particular, it could be an order relation specifying some form of
program refinement or a non-executable property from which deriving a
program is convenient.
|
