.. _chap.itp: 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 `. 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 :: /isabelle into either the user file :: .isabelle/Isabelle2019/etc/components or the system-wide file :: /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 why3_vc 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.