10. Interactive Proof Assistants¶
10.1. Using an Interactive Proof Assistant to Discharge Goals¶
Instead of calling an automated theorem prover to discharge a goal, Why3 offers the possibility to call an interactive theorem prover instead. In that case, the interaction is decomposed into two distinct phases:
Edition of a proof script for the goal, typically inside a proof editor provided by the external interactive theorem prover;
Replay of an existing proof script.
An example of such an interaction is given in the tutorial section.
Some proof assistants offer more than one possible editor, e.g., a 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 Editors tab.
, under the10.2. Theory Realizations¶
Given a Why3 theory, one can use a proof assistant to make a realization of this theory, that is to provide definitions for some of its uninterpreted symbols and proofs for some of its axioms. This way, one can show the consistency of an axiomatized theory and/or make a connection to an existing library (of the proof assistant) to ease some proofs.
10.2.1. Generating a realization¶
Generating the skeleton for a theory is done by passing to the
realize
command a driver suitable for realizations, the names of the
theories to realize, and a target directory.
why3 realize -D path/to/drivers/prover-realize.drv
-T env_path.theory_name -o path/to/target/dir/
The theory is looked into the files from the environment, e.g., the standard
library. If the theory is stored in a different location, option why3 -L
should be used.
The name of the generated file is inferred from the theory name. If the target directory already contains a file with the same name, Why3 extracts all the parts that it assumes to be user-edited and merges them in the generated file.
Note that Why3 does not track dependencies between realizations and
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 Makefile
.
10.2.2. Using realizations inside proofs¶
If a theory has been realized, the Why3 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 realized_theory
meta
declaration in the corresponding theory section of the driver.
theory env_path.theory_name
meta "realized_theory" "env_path.theory_name", "optional_naming"
end
The first parameter is the theory name for Why3. The second 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.
10.2.3. Shipping libraries of realizations¶
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
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
realized_theory
meta declarations. The configuration file should
be as follows.
[main]
loadpath="path/to/theories"
[prover_modifiers]
name="Coq"
option="-R path/to/vo/files Logical_directory"
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))\""
This configuration file can be passed to Why3 thanks to the
why3 --extra-config
option.
10.3. Coq¶
This section describes the content of the Coq files generated by Why3 for both proof obligations and theory realizations. When reading a Coq script, Why3 is guided by the presence of empty lines to split the script, so the user should refrain from removing empty lines around generated blocks or adding empty lines inside them.
The header of the file contains all the library inclusions required by the driver file. Any user-made changes to this block will be lost when the file is regenerated by Why3. This part starts with
(* This file is generated by ... *)
.Abstract logic symbols are assumed with the vernacular directive
Parameter
. Axioms are assumed with theAxiom
directive. When regenerating a script, Why3 assumes that all such symbols have been generated by a previous run. As a consequence, the user should not introduce new symbols with these two directives, as they would be lost.Definitions of functions and inductive types in theories are printed in a block that starts with
(* Why3 assumption *)
. This comment should not be removed; otherwise Why3 will assume that the definition is a user-defined block.Proof obligations and symbols to be realized are introduced by
(* Why3 goal *)
. The user is supposed to fill the script after the statement. Why3 assumes that the user-made part extends up toQed
,Admitted
,Save
, orDefined
, whichever comes first. In the case of definitions, the original statement can be replaced by aNotation
directive, in order to ease the usage of predefined symbols. Why3 also recognizesVariable
andHypothesis
and preserves them; they should be used in conjunction with Coq’sSection
mechanism to realize theories that still need some abstract symbols and axioms.
Why3 preserves any block from the script that does not fall into one of the previous categories. Such blocks can be used to import other libraries than the ones from the prelude. They can also be used to state and prove auxiliary lemmas. Why3 tries to preserve the position of these user-defined blocks relatively to the generated ones.
Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, Why3 can easily be confused by some
terminating directive like Qed
that would be present in a comment.
10.4. Isabelle/HOL¶
When using Isabelle from Why3, files generated from Why3 theories and
goals are stored in a dedicated XML format. Those files should not be
edited. Instead, the proofs must be completed in a file with the same
name and extension .thy
. This is the file that is opened when using
the action in the Why3 IDE.
10.4.1. Installation¶
You need version Isabelle2018 or Isabelle2019. Former or later versions are not supported. We assume below that your version is 2019, please replace 2019 by 2018 otherwise.
Isabelle must be installed before compiling Why3. After compilation and installation of Why3, you must manually add the path
<Why3 lib dir>/isabelle
into either the user file
.isabelle/Isabelle2019/etc/components
or the system-wide file
<Isabelle install dir>/etc/components
10.4.2. Usage¶
The most convenient way to call Isabelle for discharging a Why3 goal is
to start the Isabelle/jedit interface in server mode. In this mode, one
must start the server once, before launching why3 ide
, using
isabelle why3_jedit
Then, inside a Why3 interactive session, any use of
will transfer the file to the already opened instance of jEdit. When the proof is completed, the user must send back the edited proof to Why3 IDE by closing the opened buffer, typically by hitting Control-w.10.4.3. Using Isabelle server¶
Starting from Isabelle version 2018, Why3 is able to exploit the server
features of Isabelle to speed up the processing of proofs in batch mode,
e.g., when replaying them from within Why3 IDE. Currently, when replaying
proofs using the isabelle why3 tool, an Isabelle process including a
rather heavyweight Java/Scala and PolyML runtime environment has to be
started, and a suitable heap image has to be loaded for each proof
obligation, which can take several seconds. To avoid this overhead, an
Isabelle server and a suitable session can be started once, and then
isabelle why3 can just connect to it and request the server to
process theories. In order to allow a tool such as Why3 IDE to use the
Isabelle server, it has to be started via the wrapper tool
isabelle use_server. For example, to process the proofs in
examples/logic/genealogy
using Why3 IDE and the Isabelle server, do the
following:
Start an Isabelle server using
isabelle server &
Start Why3 IDE using
isabelle use_server why3 ide genealogy
10.4.4. Realizations¶
Realizations must be designed in some .thy
as follows. The
realization file corresponding to some Why3 file f.why
should have
the following form.
theory Why3_f
imports Why3_Setup
begin
section {* realization of theory T *}
why3_open "f/T.xml"
why3_vc <some lemma>
<proof>
why3_vc <some other lemma> by proof
[...]
why3_end
See directory lib/isabelle
for examples.
10.5. PVS¶
10.5.1. Installation¶
You need version 6.0.
10.5.2. Usage¶
When a PVS file is regenerated, the old version is split into chunks,
according to blank lines. Chunks corresponding to Why3 declarations are
identified with a comment starting with % Why3
, e.g.,
% Why3 f
f(x: int) : int
Other chunks are considered to be user PVS declarations. Thus a comment
such as % Why3 f
must not be removed; otherwise, there will be two
declarations for f
in the next version of the file (one being
regenerated and another one considered to be a user-edited chunk).
10.5.3. Realization¶
The user is allowed to perform the following actions on a PVS realization:
give a definition to an uninterpreted symbol (type, function, or predicate symbol), by adding an equal sign (
=
) and a right-hand side to the definition. When the declaration is regenerated, the left-hand side is updated and the right-hand side is reprinted as is. In particular, the names of a function or predicate arguments should not be modified. In addition, theMACRO
keyword may be inserted and it will be kept in further generations.turn an axiom into a lemma, that is to replace the PVS keyword
AXIOM
with eitherLEMMA
orTHEOREM
.insert anything between generated declarations, such as a lemma, an extra definition for the purpose of a proof, an extra
IMPORTING
command, etc. Do not forget to surround these extra declarations with blank lines.
Why3 makes some effort to merge new declarations with old ones and with user chunks. If it happens that some chunks could not be merged, they are appended at the end of the file, in comments.