itp.tex 4.64 KB
Newer Older
1 2 3 4

\chapter{Interactive Proof Assistants}


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

7 8 9 10 11 12 13 14 15 16 17 18 19 20
\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}.

Piotr Trojanek's avatar
Piotr Trojanek committed
21
Some proof assistants offer more than one possible editor, \eg a
22 23 24
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.
25

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

29 30 31
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
32
axioms. This way, one can show the consistency of an axiomatized
33 34
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
35
%Currently, realizations are supported for the proof assistants Coq and PVS.
36

37
\subsection{Generating a realization}
38

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

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

Guillaume Melquiond's avatar
Guillaume Melquiond committed
51 52 53 54
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.

55 56
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
57
extracts all the parts that it assumes to be user-edited and merges them in
58 59
the generated file.

60
Note that \why does not track dependencies between realizations and
61 62 63 64
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}.
65

66
\subsection{Using realizations inside proofs}
67

68 69 70 71 72
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.
73 74
\index{driver file}

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

81
The first parameter is the theory name for \why. The second
82 83 84
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.
85
\index{realized_theory@\verb+realized_theory+}
86

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

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
91 92 93
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
94
\verb+meta "realized_theory"+ declarations. The configuration file should be as
95
follows.
96
\index{configuration file}
97 98 99 100 101

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

102 103
[prover_modifiers]
name="Coq"
104
option="-R path/to/vo/files Logical_directory"
105 106 107 108 109 110 111 112
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))\""
113 114
\end{verbatim}

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


124 125
\input{./coq.tex}

126 127
\input{./coq_tactic.tex}

128 129 130 131 132
\input{./isabelle.tex}

\input{./pvs.tex}


133 134 135 136 137
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: