Profound 0.3 Alpha

Profound is an experiment in subformula linking as an interaction method. Its theoretical basis is found in this document:

K. Chaudhuri. Subformula Linking as an Interaction Method. Conference on Interactive Theorem Proving (ITP-04), Rennes, France. LNCS 7998, pp. 386–401. July 2013. ©Springer

0. Download

Profound is developed on GitHub. The 0.3 alpha release can be downloaded as a tar.gz or as a zip file. You can also follow the development by cloning the repository:

git clone https://github.com/chaudhuri/profound.git

Please note that this is alpha quality software that is under active development.

1. Building Prerequisites

You will need OCaml (version 3.12.1 or later) and the following packages:

Batteries Included (version 2.0 or later)

Findlib

LablGTK2

Menhir

Consider using OPAM and a recent version (4.00.0+) of OCaml and the most recent versions of the above libraries. Until I add Profound to the main OPAM repository, you can get it with a local OPAM repository as follows (not recomended for novices).

$ wget http://kaustuv.chaudhuri.info/uncat/opam-kc.tar.gz && tar -C ~ -xf opam-kc.tar.gz
$ opam repo add opam-kc ~/opam-kc
$ opam install profound

This command will install all the dependencies for you.

You will also need a LaTeX distribution (eg. TeXLive) that contains AMS Math and dvipng.

It will probably only work on a Linux system.

2. Building

There is nothing to configure.

Just run make.

It will produce the binary ./profound.native.

3. Invoking

Use the --help option for a quick overview of all options.

Theorem in the command line

$  ./profound.native  "a | ~a"

Theorem read from a file

$  echo "a | ~a" > a.p
$  ./profound.native -i a.p

4. User Interface

Profound has a very minimalistic user interface.

The main theorem is displayed centered in the window.

The only other widget is a small status bar that sometimes displays hints or error messages.

Navigation in the subformula tree is done with the cursor keys (Up, Down, Left and Right). The current selected subformula is indicated in braces {}.

To start navigating, you will have to descend at least once (with the Down key).

Hit Shift-Up to stop navigating subformulas, i.e., to go all the way back to the top.

4.2. Linking

The primary operation that the user is expected to perform is linking.

To initiate a link (technical term: mark a source), press the Return or Enter keys. This will turn the current selection blue. Any subformula of the theorem can be a source – not just the atoms.

To complete a link (technical term: mark a sink), navigate to another subformula that is ancestrally joined to the source via a par or a ?. Then hit Return or Enter again. Any suitable subformula can be a sink, not just atoms.

When a link completes, the source and sink interact hereditarily, with all ties broken in favor of the sink having outermost scope. Intuitively, the source is “brought to” the sink.

4.3. History

The proof state is presented as a linear timeline with the present shown in the middle in a large font, and the past and future below and above the present.

Whenever a link is resolved or the current theorem is rewritten, the previous state of the theorem is prepended to the past.

To go back to an earlier form, hit Ctrl-Z.

Going back in history shows the known future above the theorem line. You can return to any of the futures in the current timeline by hitting Ctrl-Y.

Note that any rule application that modifies the text of the theorem will alter the current timeline and therefore will remove the futures from the earlier timeline. (There is currently no way to restore a lost timeline – after a number of experiments, I came to the conclusion that allowing too much branching in time adds only confusion.)

By default only the three most recent past and future states are shown. You can change this with the -hist-lines command line parameter, and dynamically using the + and - keys.

4.4. Saving and quitting

To quit, hit Ctrl-Q.

If the input came from a file, the current state of the proof is saved on quitting. When working on the same file again, the previous state is restored, including the full undo and redo histories.

A save can also be forced at any time using Ctrl-S.

4.5. Other interactions

On any subformula

Delete rewrites it to 0. Note that 0 \plus A and A \plus 0 will be rewritten to A eagerly when ascending out of the current context.

If the current subformula is a ?-formula and has no marks in any subformula, then:

Shift-Return / Shift-Enter contracts it, i.e., it rewrites ?A to ?A \par ?A.
Shift-Delete applies weakening to it, i.e., it rewrites ?A to \bot.
? applies dereliction to it, i.e. it rewrites ? A to A.

If the current subformula is an existential, then:

Shift-Return opens a dialog box asking for a witness to substitute for the variable. Witnesses are allowed to use any of the variables in scope of the existential – these will be captured. All free identifiers in the witness terms are assumed to be signature constants, and are displayed in a different (sans-serif) font.

4.6. Concrete syntax

Formulas in theorems use the following concrete syntax:

Atomic formulas: first-order predicates. Example: p(f(x), g(x, y))
Negated atoms: \lnot or ~. Example: ~ p(f(x), g(x, y))
Tensor: \tensor or *. Examples: a \tensor b, a * b
One (unit of Tensor): \one or 1
Plus: \plus or +. Examples: a \plus b, a + b
Zero (unit of Plus): \zero or 0
Par: \par or |. Examples: a \par b, a | b
Bottom (unit of Par): \bot or #F
With: \with or &. Examples: a \with b, a & b
Top (unit of With): \top or #T
Bang: !. Example: !a
Why-not: ?. Example: ?a
Universal quantification: \A with comma-separated variables terminated by a .. Example: \A x, y. p(x, f(y)).
Existential quantification: \E with comma-separated variables terminated by a .. Example: \E x, y. p(x, f(y)).

Identifiers must match the regexp [A-Za-z][A-Za-z0-9_]*

Some example theorems can be found in the examples/ subdirectory.