Previous Up Next

Chapter 9  Interactive Proof Assistants

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

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

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

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

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

9.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 parts 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 part will be lost when the file is regenerated by Why3. This part ends at the first empty line.
  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 user-made.
  4. Finally, 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 already defined 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.

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.

9.3.1  Coq Tactic

Why3 provides a Coq tactic to call external theorem provers as oracles.

Installation

You need Coq version 8.4 or greater. If this is the case, Why3’s configuration detects it, then compiles and installs the Coq tactic. The Coq tactic is installed in

why3-lib-dir/coq-tactic/

where why3-lib-dir is Why3’s library directory, as reported by why3 --print-libdir. This directory is automatically added to Coq’s load path if you are calling Coq via Why3 (from why3 ide, why3 replay, etc.). If you are calling Coq by yourself, you need to add this directory to Coq’s load path, either using Coq’s command line option -I or by adding

Add LoadPath "why3-lib-dir/coq-tactic/".

to your ~/.coqrc resource file.

Usage

The Coq tactic is called why3 and is used as follows:

why3 "prover-name" [timelimit n].

The string prover-name identifies one of the automated theorem provers supported by Why3, as reported by why3 --list-provers (interactive provers excluded). The current goal is then translated to Why3’s logic and the prover is called. If it reports the goal to be valid, then Coq’s admit tactic is used to assume the goal. The prover is called with a time limit in seconds as given by Why3’s configuration file (see Section 10.3). A different value may be given using the timelimit keyword.

Error messages.

The following errors may be reported by the Coq tactic.

Not a first order goal
  The Coq goal could not be translated to Why3’s logic.
Timeout
  There was no answer from the prover within the given time limit.
Don’t know
  The prover stopped without validating the goal.
Invalid
  The prover stopped, reporting the goal to be invalid.
Failure
  The prover failed. Depending on the message that follows, you may want to file a bug report, either to the Why3 developers or to the prover developers.

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

9.4.1  Installation

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

or the system-wide file

<Isabelle install dir>/etc/components

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

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

9.5  PVS

9.5.1  Installation

You need version 6.0.

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

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