itp.tex 4.64 KB
Newer Older
1
\chapter{Interactive Proof Assistants}
2
%HEVEA\cutname{itp.html}
3

4
% ... We then provide specific information about some ITPs.
5

6 7 8 9 10 11 12 13 14 15 16 17 18 19
\section{Using an Interactive Proof Assistant to Discharge Goals}

Instead of calling an automated theorem prover to discharge a goal,
\why offers the possibility to call an interactive theorem prover
instead. In that case, the interaction is decomposed into two distinct
phases:
\begin{itemize}
\item Edition of a proof script for the goal, typically inside a proof editor
  provided by the external interactive theorem prover;
\item Replay of an existing proof script.
\end{itemize}
An example of such an interaction is given in the tutorial
section~\ref{sec:gui}.

20
Some proof assistants offer more than one possible editor, \eg a
21 22 23
choice between the use of a dedicated editor and the use of the Emacs
editor and the ProofGeneral mode. Selection of the preferred mode can
be made in \texttt{why3ide} preferences, under the ``Editors'' tab.
24

25 26
\section{Theory Realizations}
\label{sec:realizations}
27

28 29 30
Given a \why theory, one can use a proof assistant to make a
\emph{realization} of this theory, that is to provide definitions for
some of its uninterpreted symbols and proofs for some of its
31
axioms. This way, one can show the consistency of an axiomatized
32 33
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
34
%Currently, realizations are supported for the proof assistants Coq and PVS.
35

36
\subsection{Generating a realization}
37

38 39
Generating the skeleton for a theory is done by passing to the
\texttt{realize} command a driver suitable for realizations, the names of
40
the theories to realize, and a target directory.
41
\index{realize@\texttt{realize}}
42 43

\begin{verbatim}
44 45
why3 realize -D path/to/drivers/prover-realize.drv
             -T env_path.theory_name -o path/to/target/dir/
46
\end{verbatim}
47 48
\index{driver@\verb+--driver+}
\index{theory@\verb+--theory+}
49

50 51 52 53
The theory is looked into the files from the environment, \eg the standard
library. If the theory is stored in a different location, option \texttt{-L}
should be used.

54 55
The name of the generated file is inferred from the theory name. If the
target directory already contains a file with the same name, \why
56
extracts all the parts that it assumes to be user-edited and merges them in
57 58
the generated file.

59
Note that \why does not track dependencies between realizations and
60 61 62 63
theories, so a realization will become outdated if the corresponding
theory is modified.
It is up to the user to handle such dependencies, for instance using a
\texttt{Makefile}.
64

65
\subsection{Using realizations inside proofs}
66

67 68 69 70 71
If a theory has been realized, the \why printer for the corresponding prover
will no longer output declarations for that theory but instead simply put
a directive to load the realization. In order to tell the printer
that a given theory is realized, one has to add a meta declaration in the
corresponding theory section of the driver.
72 73
\index{driver file}

74 75
\begin{verbatim}
theory env_path.theory_name
76
  meta "realized_theory" "env_path.theory_name", "optional_naming"
77 78
end
\end{verbatim}
79

80
The first parameter is the theory name for \why. The second
81 82 83
parameter, if not empty, provides a name to be used inside generated
scripts to point to the realization, in case the default name is not
suitable for the interactive prover.
84
\index{realized_theory@\verb+realized_theory+}
85

86
\subsection{Shipping libraries of realizations}
87 88 89

While modifying an existing driver file might be sufficient for local
use, it does not scale well when the realizations are to be shipped to
90 91 92
other users. Instead, one should create two additional files: a
configuration file that indicates how to modify paths, provers, and
editors, and a driver file that contains only the needed
93
\verb+meta "realized_theory"+ declarations. The configuration file should be as
94
follows.
95
\index{configuration file}
96 97 98 99 100

\begin{verbatim}
[main]
loadpath="path/to/theories"

101 102
[prover_modifiers]
name="Coq"
103
option="-R path/to/vo/files Logical_directory"
104 105 106 107 108 109 110 111
driver="path/to/file/with/meta.drv"

[editor_modifiers coqide]
option="-R path/to/vo/files Logical_directory"

[editor_modifiers proofgeneral-coq]
option="--eval \"(setq coq-load-path (cons '(\\\"path/to/vo/files\\\" \
  \\\"Logical_directory\\\") coq-load-path))\""
112 113
\end{verbatim}

114 115
This configuration file can be passed to \why thanks to the
\verb+--extra-config+ option.
116
\index{extra-config@\verb+--extra-config+}
117 118 119 120
\index{prover_modifiers@\verb+prover_modifiers+}
\index{editor_modifiers@\verb+editor_modifiers+}
\index{option@\verb+option+}
\index{driver@\verb+driver+}
121 122


123 124 125 126 127 128 129
\input{./coq.tex}

\input{./isabelle.tex}

\input{./pvs.tex}


130 131 132 133 134
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: