1PROOFTREE(1) User Manuals PROOFTREE(1)
2
6 prooftree - proof-tree display for Proof General
7
9 prooftree [Options...]
10
12 Prooftree visualizes proof trees during proof development with Proof
13 General. Currently it only works for Coq, though adding support for
14 other proof assistants should be relatively easy.
15 To start a proof-tree display, hit the Prooftree icon in the Proof Gen‐
17 eral tool-bar or select the menu entry Proof-General -> Start/Stop
18 Prooftree or type C-c C-d (which runs proof-tree-external-display-tog‐
19 gle). Inside a proof, this will immediately start a proof-tree display
20 for the current proof. Outside a proof, Proof General remembers to
21 start the proof-tree display for the next proof.
22 Under normal circumstances Prooftree is started by Proof General as an
24 Emacs subprocess. The user interacts with Prooftree only through the
25 graphical user interface. A substantial part of the proof-tree visual‐
26 ization task is done by Proof General. Therefore not only the
27 Prooftree command line arguments but also other aspects can only be
28 configured inside Proof General, see Proof General Customization below.
29
31 -help Print synopsis and exit.
32 -config
34 Open the configuration dialog on startup (if you want to change
35 the configuration without starting Proof General).
36 -geometry spec
38 Sets the X geometry of the main window. spec is a standard X
39 geometry string in the form xposxypos[+xoff[+yoff]].
40 -tee file
42 Write all input to file (usually for debugging purposes).
43 -debug Provide more details on errors.
45 -help-dialog
47 Open the help dialog on startup. Mainly useful for proofreading
48 the help text.
49
51 Prooftree opens one window for each proof that it is requested to dis‐
52 play. This window contains the proof-tree graph and a small display
53 for sequents and proof commands.
54 Colors
56 The branches in the proof-tree graph are colored according to their
57 state. Prooftree distinguishes between the following states.
58 current (blue by default)
60 The current branch is the branch from the root of the proof tree
61 to the current goal.
62 unproven (default foreground color)
64 A branch is unproven if it contains open proof goals.
65 proved incomplete (cyan by default)
67 An incompletely proved branch has its proof finished, but some
68 of the existential variables that have been introduced in this
69 branch are not (yet) instantiated.
70 proved partially (dark green by default)
72 In a partially proved branch all existential variables of the
73 branch itself are instantiated, but some of those instantiations
74 contain existential variables that are not (yet) instantiated.
75 proved complete (green by default)
77 A branch is proved complete if all its existential variables are
78 instantiated with terms that themselves do not contain any exis‐
79 tential variables.
80 cheated (red by default)
82 A cheated branch contains a cheating proof command, such as
83 admit
84 The colors as well as many other Prooftree parameters can be changed in
86 the Prooftree Configuration Dialog (see below).
87 Navigation
89 When the proof tree grows large one can navigate by a variety of means.
90 In addition to scroll bars and the usual keys one can move the proof
91 tree by dragging with mouse button 1 pressed. By default, dragging
92 moves the viewport (i.e., the proof tree underneath moves in the oppo‐
93 site direction). After setting a negative value for Drag acceleration
94 in the Prooftree Configuration Dialog, dragging will move the proof
95 tree instead (i.e, the proof tree moves in the same direction as the
96 mouse).
97 Sequent Display
99 The sequent display below the proof tree normally shows the ancestor
100 sequent of the current goal. With a single left mouse click one can
101 display any goal or proof command in the sequent display. A single
102 click outside the proof tree will switch back to default behavior. The
103 initial size of the sequent display can be set in the Prooftree Config‐
104 uration Dialog. A value of 0 hides the sequent display.
105 Tool Tips
107 Abbreviated proof commands and sequents are shown in full as tool tips
108 when the mouse pointer rests over them. Both, the tool tips for abbre‐
109 viated proof commands and for sequents can be independently switched
110 off in the Prooftree Configuration Dialog. The length at which proof
111 commands are abbreviated can be configured as well.
112 Additional Displays
114 A double click or a shift-click displays any goal or proof command in
115 an additional window. These additional windows are automatically
116 updated, for instance, if an existential variable is instantiated. For
117 additional sequent displays one can browse the instantiation history of
118 the sequent using the forward and backward buttons. These additional
119 windows can be detached from the proof tree. A detached display is nei‐
120 ther automatically updated nor automatically deleted.
121 Existential Variables
123 Prooftree keeps track of existential variables, whether they have been
124 instantiated and whether they depend on some other, not (yet) instanti‐
125 ated existential. It uses different colors for proved branches that
126 contain non-instantiated existential variables and branches that only
127 depend on some not instantiated existential. The list of currently not
128 (yet) instantiated existential variables is appended to proof commands
129 and sequents in tool-tips and the other displays.
130 The Existential Variable Dialog displays a table with all existential
132 variables of the current proof and their dependencies. Each line of the
133 table contains a button that marks the proof command that introduced
134 this variable (with yellow background, by default) and, if present, the
135 proof command that instantiated this variable (with orange background,
136 by default).
137 Main Menu
139 The Menu button displays the main menu. The Clone item clones the cur‐
140 rent proof tree in an additional window. This additional window contin‐
141 ues to display a snapshot of the cloned proof tree, no matter what hap‐
142 pens with the original proof.
143 The Show current and Show selected items move the viewport of the proof
145 tree such that the current proof goal, or, respectively, the selected
146 node will be visible (if they exist).
147 The Exit item terminates Prooftree and closes all proof-tree displays.
149 The remaining three items display, respectively, the Prooftree Configu‐
151 ration Dialog, and the Help and About windows.
152 Context Menu
154 A right click displays the Context Menu, which contains additional
155 items.
156 The item Undo to point is active over sequent nodes in the proof tree.
158 There, it sends an retract or undo request to Proof General that
159 retracts the scripting buffer up to that sequent.
160 The items Insert command and Insert subproof are active over proof com‐
162 mands. They sent, respectively, the selected proof command or all proof
163 commands in the selected subtree, to Proof General, which inserts them
164 at point.
165
167 Prooftree Configuration Dialog
168 The Save button stores the current configuration (as marshaled OCaml
169 record) in ~/.prooftree, which will overwrite the built-in default con‐
170 figuration for the following Prooftree runs. The Revert button loads
171 and applies the saved configuration. The Cancel and OK buttons close
172 the dialog, but Cancel additionally resets the configuration to the
173 state before the start of the dialog. To avoid opening partial file
174 names, the Log Proof General input check box is deactivated when typing
175 the log file name.
176 Proof General Customization
178 The location of the Prooftree executable and the command line arguments
179 are in the customization group proof-tree. Prover specific points,
180 such as the regular expressions for navigation and cheating commands
181 are in the customization group proof-tree-internals. To visit a cus‐
182 tomization group, type M-x customize-group followed by the name of the
183 customization group inside Proof General.
184
186 For Coq >= 8.5, existential variables in Prooftree are severely broken
187 because Coq does not provide the necessary information, see Coq bug
188 4504.
189 In Coq, proofs must be started with command Proof, which is the recom‐
191 mended practice anyway (see Coq problem report 2776).
192 In additional sequent displays, the information about existential vari‐
194 ables is only shown for the latest version of the sequent and not for
195 older versions in the instantiation history. The current communication
196 protocol between Proof General and Prooftree does not permit more.
197
199 This version of Prooftree requires Coq 8.4beta or better and Proof Gen‐
200 eral 4.3pre130327 or better.
201
203 ~/.prooftree
204 Saved Prooftree configuration. Is loaded at application start-up
205 for overwriting the built-in default configuration. Must contain
206 a marshaled OCaml configuration record.
207
209 The Prooftree web page, http://askra.de/software/prooftree/
210 The Proof General Adapting Manual
213 contains information about adapting Prooftree for a new proof
214 assistant (see http://proofgeneral.inf.ed.ac.uk/adaptingman-lat‐
215 est.html).
216
218 Prooftree has been inspired by the proof tree display of PVS.
219
221 Hendrik Tews <prooftree at askra.de>
222PROOFTREE August 2011 PROOFTREE(1)