Previous Up Next

Chapter 8  Interactive Proof Assistants

8.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:

An example of such an interaction is given in the tutorial section 1.2.

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 why3ide preferences, under the “Editors” tab.

8.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.

8.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 -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.

8.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 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.

8.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 meta "realized_theory" 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 --extra-config option.

8.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.

  1. 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 ... *).
  2. Abstract logic symbols are assumed with the vernacular directive Parameter. Axioms are assumed with the Axiom 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.
  3. 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.
  4. 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 to Qed, Admitted, Save, or Defined, whichever comes first. In the case of definitions, the original statement can be replaced by a Notation directive, in order to ease the usage of predefined symbols. Why3 also recognizes Variable and Hypothesis and preserves them; they should be used in conjunction with Coq’s Section 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.

8.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 “Edit” action in why3 ide.

8.4.1  Installation

You need version Isabelle2017 or Isabelle2018. Former versions are not supported. We assume below that your version is 2018, please replace 2018 by 2017 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/Isabelle2018/etc/components

or the system-wide file

<Isabelle install dir>/etc/components

8.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 ide session, any use of “Edit” 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 Ctrl-w.

8.4.3  Using Isabelle 2018 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:

  1. Start an Isabelle server using
       isabelle server &
    
  2. Start Why3 IDE using
       isabelle use_server why3 ide genealogy
    

8.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.

8.5  PVS

8.5.1  Installation

You need version 6.0.

8.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).

8.5.3  Realization

The user is allowed to perform the following actions on a PVS realization:

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.


Previous Up Next