Version 1.4.1

[why3.git] / doc / itp.rst

Interactive Proof Assistants
============================

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 :ref:`tutorial section <sec.gui>`.

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 :menuselection:`File --> Preferences`, under the :guilabel:`Editors` tab.

.. _sec.realizations:

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.

Generating a realization
~~~~~~~~~~~~~~~~~~~~~~~~

Generating the skeleton for a theory is done by passing to the
:why3:tool:`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 :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 :file:`Makefile`.

.. index:: driver file

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 :why3:meta:`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.

.. index:: configuration file

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
:why3:meta:`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
:option:`why3 --extra-config` option.

.. index:: Coq proof assistant, proof assistant; Coq
.. _sec.coq:

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

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

.. index:: Isabelle proof assistant, proof assistant; Isabelle
.. _sec.isabelle:

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 :menuselection:`Tools --> Edit` action in the Why3 IDE.

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

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:tool:`why3 ide`, using

::

    isabelle why3_jedit

Then, inside a Why3 interactive session, any use
of :menuselection:`Tools --> Edit` will transfer the file to the already
opened instance of :program:`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 :kbd:`Control-w`.

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 :program:`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
:program:`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
:program:`isabelle use_server`. For example, to process the proofs in
:file:`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

Realizations
~~~~~~~~~~~~

Realizations must be designed in some :file:`.thy` as follows. The
realization file corresponding to some Why3 file :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 :file:`lib/isabelle` for examples.

.. index:: PVS proof assistant, proof assistant; PVS
.. _sec.pvs:

PVS
---

Installation
~~~~~~~~~~~~

You need version 6.0.

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

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, the ``MACRO`` 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 either ``LEMMA`` or ``THEOREM``.

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