blob: c85270895716db27312e1ec26b4de395e2053bba (
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
|
\achapter{\protect{Miscellaneous extensions}}
\asection{Program derivation}
Coq comes with an extension called {\tt Derive}, which supports
program derivation. Typically in the style of Bird and Meertens. 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$ From \term$_1$ Upto \term$_2$ As \ident$_2$]
{\tt Derive \ident$_1$ From \term$_1$ Upto \term$_2$ As \ident$_2$\comindex{Derive}}
This commands opens a new proof with two goals. The first one has, as
conclusion, the type of $\term_1$, but is shelved (see
Section~\ref{shelve}). The visible goal has type {\tt \term$_2$
\term$_1$ ?x} where {\tt ?x} is the existential variable
corresponding to the shelved goal.
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$_1$
\term$_2$ \ident$_1$}, 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 Coq.Numbers.Natural.Peano.NPeano.
Section P.
Variables (n m k:nat).
\end{coq_example*}
\begin{coq_example}
Derive p From ((k*n)+(k*m)) Upto eq As h.
Proof.
rewrite <- Mult.mult_plus_distr_l.
reflexivity.
\end{coq_example}
\begin{coq_example*}
Qed.
End P.
\end{coq_example*}
\begin{coq_example}
Print p.
Check h.
\end{coq_example}
As $\term_2$ does not need to be a symmetric relation, the
{\tt Derive} extension may also be used for program refinement.
|
