proof tree example

Proof tree visualization for Proof General

Prooftree is a program for proof-tree visualization during interactive proof development in a theorem prover. It is currently being developed for Coq and Proof General. Prooftree helps against getting lost between different subgoals in interactive proof development. It clearly shows where the current subgoal comes from and thus helps in developing the right plan for solving it.

Prooftree uses different colors for the already proven subgoals, the current branch in the proof and the still open subgoals. Sequent texts are not displayed in the proof tree itself, but they are shown as a tool-tip when the mouse rests over a sequent symbol. Long proof commands are abbreviated in the tree display, but show up in full length as tool-tip. Both, sequents and proof commands, can be shown in the display below the tree (on single click) or in a separate window (on double or shift-click).

Prooftree can mark the proof command that introduced a certain existential variable and thus help to locate the problem when Coq says No more subgoals but non-instantiated existential variables.

Currently, prooftree does only work for Coq proofs. Adding support for a different proof assistant should not be too hard, see the Proof General Adapting manual. Please drop me a line, if you would like to help with another proof assistant.

Recent Changes

2013-05-17: Prooftree 0.12 released
2013-01-21: Prooftree 0.11 released

For older items visit the list of all changes.

Status

proof tree example

Ready to be used. Prooftree requires Proof General >= 4.3pre130327 and Coq version 8.4beta or greater.

Implemented Features

Download

Binary versions: [Debian Wheezy i386] [Debian Wheezy amd64]

Sources: [prooftree-0.12.tar.gz]

Versions before 0.8 required patched versions of Proof General and Coq and were therefore distributed as a bundle of Prooftree, Proof General and the Coq patches.

Previous versions: 0.11, 0.10, 0.9, 0.8, 2011-11-01, 2011-10-04, 2011-08-11, 2011-06-14, 2011-04-21, 2011-04-20, 2011-04-18.

Requirements and Installation

Prooftree is implemented in Ocaml and Gtk (using version 2.20) with the LablGtk2 bindings. For compilation you therefore need Ocaml, Gtk and LablGtk installed. For Debian the packages ocaml-nox and liblablgtk2-ocaml-dev suffice (but the package ocaml-native-compilers is strongly recommended for binary compilation). For Proof General you need Emacs version 23 (debian package emacs23).

Because prooftree needs very recent versions of Proof General and Coq you probably have to install those from source as well. See the page on the development version of Proof General and the page on Coq 8.4 for details.

The communication protocol between Prooftree and Proof General changes now and then. Therefore, only certain versions of Prooftree and Proof General are compatible with each other, see the following table.

Prooftree version Proof General version communication protocol
0.11 - latest >= 4.3pre130327 version 3
0.9, 0.10 4.2; 4.2pre120110 - 4.3pre130111 version 2
0.8 4.2pre120104 version 1

Usage and Documentation

Proof-tree display is initially off. To display a proof tree hit the proof tree icon icon in the toolbar or select the menu entry Proof-General -> Start/Stop Prooftree or type C-c C-d. If you are inside a proof, Proof General will immediately display a window with the proof tree of the current proof. Otherwise it will remember to start the proof-tree display for the next proof.

Displaying the proof tree of an already started proof requires to retract and redo all proof steps done so far. This should be almost unnoticeable, except for the time it takes.

For comprehensive documentation see the Prooftree help window or the Prooftree man page.

The Proof General Users Manual contains a section about Prooftree with the most essential information. Information about supporting a new proof assistant is contained in the Proof General Adapting Manual.

Technology

Prooftree is controlled by Proof General and thus an Emacs subprocess. Proof General does a light analysis of the output of the proof assistant and sends appropriate commands to prooftree. To avoid synchronization trouble, the communication between Proof General and prooftree is (almost) one way: Proof General sends display commands to Prooftree and Prooftree never requests anything from Proof General. To achieve this, Proof General maintains some state for prooftree. For instance, Proof General keeps a mapping of existential variables to goals in which they occur. This mapping helps to decide which goals must be updated inside prooftree when some existential variable gets instantiated.

Drawing a proof tree is just a matter of digging up the right functions for drawing circles and lines inside a drawing area. For Coq proof trees it is, however, a bit more complicated than that.

Credits

Prooftree is more or less a reimplementation of the graphical proof display of Pvs. The Pvs version is implemented in Tcl/Tk and controlled directly by the Pvs prover process. Therefore, for Pvs, one can start the proof display in the middle of a proof, without the need of rerunning the proof. The Pvs proof display has some performance problems for very large proofs. For a comparison, see this screen shot.

proof tree example

last changed on 17 May 2013 by Hendrik