prooftree(1)
NAME
prooftree - proof-tree display for Proof General
SYNOPSIS
prooftree [Options...]
DESCRIPTION
Prooftree visualizes proof trees during proof development with Proof General. Currently it only works for Coq, though adding support for other proof assistants should be relatively easy. To start a proof-tree display, hit the Prooftree icon in the Proof General tool-bar or select the menu entry Proof-General -> Start/Stop Prooftree or type C-c C-d (which runs proof-tree-external-display- toggle). Inside a proof, this will immediately start a proof-tree display for the current proof. Outside a proof, Proof General remembers to start the proof-tree display for the next proof. Under normal circumstances Prooftree is started by Proof General as an Emacs subprocess. The user interacts with Prooftree only through the graphical user interface. A substantial part of the proof-tree visualization task is done by Proof General. Therefore not only the Prooftree command line arguments but also other aspects can only be configured inside Proof General, see Proof General Customization below.
OPTIONS
-help Print synopsis and exit.
-config
Open the configuration dialog on startup (if you want to change
the configuration without starting Proof General).
-geometry spec
Sets the X geometry of the main window. spec is a standard X
geometry string in the form xposxypos[+xoff[+yoff]].
-tee file
Write all input to file (usually for debugging purposes).
-debug Provide more details on errors.
-help-dialog
Open the help dialog on startup. Mainly useful for proofreading
the help text.
MAIN PROOF DISPLAY
Prooftree opens one window for each proof that it is requested to
display. This window contains the proof-tree graph and a small display
for sequents and proof commands.
Colors
The branches in the proof-tree graph are colored according to their
state. Prooftree distinguishes between the following states.
current (blue by default)
The current branch is the branch from the root of the proof tree
to the current goal.
unproven (default foreground color)
A branch is unproven if it contains open proof goals.
proved incomplete (cyan by default)
An incompletely proved branch has its proof finished, but some
of the existential variables that have been introduced in this
branch are not (yet) instantiated.
proved partially (dark green by default)
In a partially proved branch all existential variables of the
branch itself are instantiated, but some of those instantiations
contain existential variables that are not (yet) instantiated.
proved complete (green by default)
A branch is proved complete if all its existential variables are
instantiated with terms that themselves do not contain any
existential variables.
cheated (red by default)
A cheated branch contains a cheating proof command, such as
admit
The colors as well as many other Prooftree parameters can be changed in
the Prooftree Configuration Dialog (see below).
Navigation
When the proof tree grows large one can navigate by a variety of means.
In addition to scroll bars and the usual keys one can move the proof
tree by dragging with mouse button 1 pressed. By default, dragging
moves the viewport (i.e., the proof tree underneath moves in the
opposite direction). After setting a negative value for Drag
acceleration in the Prooftree Configuration Dialog, dragging will move
the proof tree instead (i.e, the proof tree moves in the same direction
as the mouse).
Sequent Display
The sequent display below the proof tree normally shows the ancestor
sequent of the current goal. With a single left mouse click one can
display any goal or proof command in the sequent display. A single
click outside the proof tree will switch back to default behavior. The
initial size of the sequent display can be set in the Prooftree
Configuration Dialog. A value of 0 hides the sequent display.
Tool Tips
Abbreviated proof commands and sequents are shown in full as tool tips
when the mouse pointer rests over them. Both, the tool tips for
abbreviated proof commands and for sequents can be independently
switched off in the Prooftree Configuration Dialog. The length at
which proof commands are abbreviated can be configured as well.
Additional Displays
A double click or a shift-click displays any goal or proof command in
an additional window. These additional windows are deleted when the
main proof-tree window disappears, unless their Sticky button is
pressed.
Existential Variables
Prooftree keeps track of existential variables, whether they have been
instantiated and whether they depend on some other, not (yet)
instantiated existential. It uses different colors for proved branches
that contain non-instantiated existential variables and branches that
only depend on some not instantiated existential. The list of
currently not (yet) instantiated existential variables is appended to
proof commands and sequents in tool-tips and the other displays.
The Existential Variable Dialog displays a table with all existential
variables of the current proof and their dependencies. Each line of the
table contains a button that marks the proof command that introduced
this variable (with yellow background, by default) and, if present, the
proof command that instantiated this variable (with orange background,
by default).
Main Menu
The Menu button displays the main menu. The Clone item clones the
current proof tree in an additional window. This additional window
continues to display a snapshot of the cloned proof tree, no matter
what happens with the original proof.
The Show current item moves the viewport to the proof tree such that
the current proof goal (if there is any) will be visible.
The Exit item terminates Prooftree and closes all proof-tree displays.
The remaining three items display, respectively, the Prooftree
Configuration Dialog, and the Help and About windows.
Context Menu
A right click displays the Context Menu, which contains additional
items.
The item Undo to point is active over sequent nodes in the proof tree.
Then it sends an retract or undo request to Proof General that retracts
the scripting buffer up to that sequent.
The items Insert command and Insert subproof are active over proof
commands. They sent, respectively, the selected proof command or all
proof commands in the selected subtree, to Proof General, which inserts
them at point.
CONFIGURATION
Prooftree Configuration Dialog Changes in the configuration dialog take only effect when the Apply or OK button is pressed. The Save button stores the current configuration (as marshaled OCaml record) in ~/.prooftree, which will overwrite the built-in default configuration for the following Prooftree runs. The Restore button loads and applies the saved configuration. Proof General Customization The location of the Prooftree executable and the command line arguments are in the customization group proof-tree. Prover specific points, such as the regular expressions for navigation and cheating commands are in the customization group proof-tree-internals. To visit a customization group, type M-x customize-group followed by the name of the customization group inside Proof General.
LIMITATIONS
For Coq, proofs must be started with command Proof, which is the recommended practice anyway (see Coq problem report 2776).
PREREQUISITES
This version of Prooftree requires Coq 8.4beta or better and Proof General 4.3pre130327 or better.
FILES
~/.prooftree
Saved Prooftree configuration. Is loaded at application start-up
for overwriting the built-in default configuration. Must contain
a marshaled OCaml configuration record.
SEE ALSO
The Prooftree web page, http://askra.de/software/prooftree/
The Proof General Adapting Manual
contains information about adapting Prooftree for a new proof
assistant (see http://proofgeneral.inf.ed.ac.uk/adaptingman-
latest.html).
CREDITS
Prooftree has been inspired by the proof tree display of PVS.
AUTHOR
Hendrik Tews <prooftree at askra.de>
Opportunity
Personal Opportunity - Free software gives you access to billions of dollars of software at no cost. Use this software for your business, personal use or to develop a profitable skill. Access to source code provides access to a level of capabilities/information that companies protect though copyrights. Open source is a core component of the Internet and it is available to you. Leverage the billions of dollars in resources and capabilities to build a career, establish a business or change the world. The potential is endless for those who understand the opportunity.
Business Opportunity - Goldman Sachs, IBM and countless large corporations are leveraging open source to reduce costs, develop products and increase their bottom lines. Learn what these companies know about open source and how open source can give you the advantage.
Free Software
Free Software provides computer programs and capabilities at no cost but more importantly, it provides the freedom to run, edit, contribute to, and share the software. The importance of free software is a matter of access, not price. Software at no cost is a benefit but ownership rights to the software and source code is far more significant.
Free Office Software - The Libre Office suite provides top desktop productivity tools for free. This includes, a word processor, spreadsheet, presentation engine, drawing and flowcharting, database and math applications. Libre Office is available for Linux or Windows.
Free Books
The Free Books Library is a collection of thousands of the most popular public domain books in an online readable format. The collection includes great classical literature and more recent works where the U.S. copyright has expired. These books are yours to read and use without restrictions.
Source Code - Want to change a program or know how it works? Open Source provides the source code for its programs so that anyone can use, modify or learn how to write those programs themselves. Visit the GNU source code repositories to download the source.
Education
Study at Harvard, Stanford or MIT - Open edX provides free online courses from Harvard, MIT, Columbia, UC Berkeley and other top Universities. Hundreds of courses for almost all major subjects and course levels. Open edx also offers some paid courses and selected certifications.
Linux Manual Pages - A man or manual page is a form of software documentation found on Linux/Unix operating systems. Topics covered include computer programs (including library and system calls), formal standards and conventions, and even abstract concepts.
