--- name: "prooftree" section: "1" platform: "linux" package: "prooftree" version: "0.13-2+b2" release: "Debian 12 (Bookworm)" platforms: ["linux"] url: "https://new.carta.tech/prooftree" --- # prooftree(1) proof-tree display for Proof General ## 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 *xpos*x*ypos*\[+*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 automatically updated, for instance, if an existential variable is instantiated. For additional sequent displays one can browse the instantiation history of the sequent using the forward and backward buttons. These additional windows can be *detached* from the proof tree. A detached display is neither automatically updated nor automatically deleted. ### 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* and *Show selected* items move the viewport of the proof tree such that the current proof goal, or, respectively, the selected node will be visible (if they exist). 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. There, 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 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 *Revert* button loads and applies the saved configuration. The *Cancel* and *OK* buttons close the dialog, but *Cancel* additionally resets the configuration to the state before the start of the dialog. To avoid opening partial file names, the *Log Proof General input* check box is deactivated when typing the log file name. ### 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** \>= 8.5, existential variables in **Prooftree** are severely broken because **Coq** does not provide the necessary information, see **Coq** bug 4504. In **Coq,** proofs must be started with command *Proof,* which is the recommended practice anyway (see Coq problem report 2776). In additional sequent displays, the information about existential variables is only shown for the latest version of the sequent and not for older versions in the instantiation history. The current communication protocol between **Proof General** and **Prooftree** does not permit more. ## 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 \