Prover Structure

Harpoon is structured in a hierarchical fashion: the prover maintains a number of sessions, each contains a number of theorems, each of which contains a number of subgoals. A theorem with no subgoals remaining is complete, and similarly, a session with no theorems remaining is complete.

Session

Harpoon organizes a set of mutually inductive theorems into a session. Often, there is only one session at a time in Harpoon, but more than one simultaneous session is possible. For example, you might want to start a second session if you decide to prove a lemma while in the middle of another proof.

Changing sessions

One can switch between theorems by using the select command. Selecting a theorem belonging to another session will cause a session switch, which is a somewhat delicate process.

In order to prevent incomplete theorems in different sessions from referring to each other, all theorems belonging to other sessions are not in scope. When switching sessions, the theorems in the active session are moved out of scope, and the theorems in the destination session are brought into scope. Crucially, this is to prevent undesirable circularities between theorems.

It is important to be aware of this limitation, as it means that lemmas must be proven before they can be used.

Session configuration wizard

The series of interactive prompts that appear when Harpoon is started is called the session configuration wizard. This wizard appears when there are no sessions in the prover, and unless there were incomplete proofs in the loaded signature, there will be no sessions when Harpoon starts.

The wizard prompts for three things about each theorem:

1. The name of the theorem. This is how the theorem is referred to for induction hypotheses, and how other theorems can refer to this theorem.
2. The statement of the theorem. This is a Beluga computational type. (See Contextual LF.)
3. The induction order of the theorem. Non-inductive theorems can simply leave this blank. Inductive theorems specify the order numerically, by giving the position of the parameter to induct on. Only explicit parameters are counted, and counting proceeds from left to right.

Note

Implicit context quantifiers are not counted for the numeric induction order. That is, in

(g : ctx) [g |- oft M A] -> [g |- step M M'] -> [g |- oft M' A]

the position of the parameter of type [g |- step M M'] is still 2.

For example, here is how one might configure a type preservation proof for the simply-typed lambda calculus.

Name of theorem: tps
Statement of theorem: [|- oft M A] -> [|- step M M'] -> [|- oft M' A]
Induction order: 2

Once a theorem is configured, the wizard will repeat so you can configure additional theorems to be proven mutually. To end the wizard, use an empty theorem name or the special name :quit. Ending the wizard without configuring any theorems will abort the creation of the new session. If there are no other sessions in Harpoon, then Harpoon will exit.

Loading goals from a file

Harpoon proofs are recorded into signature files as a proof script. This is a structured language whose core constructs close resembles the syntax of Proof tactics, which the following section in this document will describe. In a signature file, a proof named foo is declared as follows.

proof foo : tau = P;

where tau is a computation type and P is the body of the proof.

However, when a proof script is saved back using session commands, this P contains some subgoals left. When harpoon loads a signature file with such incomplete proofs, harpoon will load the proofs into a session so that a user doesn’t need to repeat the session wizard. It is still possible to open the session wizard using session commands in a case when a user want to use it to start a new proof.

Subgoal

Proofs are developed by applying a tactic to a subgoal. If the tactic is successful, the subgoal it is applied to is solved and removed from its theorem. New subgoals may be introduced by the tactic. These subgoals are understood as children of the subgoal that was eliminated.

Subgoal prompt

To apply a tactic, one types the corresponding command into the subgoal prompt. This prompt is the main point of interaction with Harpoon. Consider this example subgoal prompt from the beginning of a type preservation proof for the simply-typed lambda calculus.

intros
Meta-context:
  M : ( |- tm) (not in scope)
  A : ( |- tp) (not in scope)
  M' : ( |- tm) (not in scope)
Computational context:
  x : [ |- oft M A]
  x1 : [ |- step M M']

-------------------------------
[ |- oft M' A]

>

The subgoal prompt shows the prover state at the subgoal. This state contains three key pieces of information.

1. The subgoal label. Every subgoal in Harpoon is identified by a subgoal label. This label indicates where in the proof this subgoal is located. In the example, the label is intros at the very top, and demonstrates that this subgoal is right after having introduced the assumptions of the theorem.
2. The contexts. Harpoon uses Beluga’s indexed type system in which one distinguishes between metavariables and computational variables. Metavariables belong to the meta-context and computational variables belong to the computational context. Notice that the metavariables in the example are all marked (not in scope). This annotation is presented for implicit parameters: recall that in the statement of the theorem, the parameters M, A and M' appeared free.
3. The goal. Below the line, the type of the subgoal appears. As tactics are applied and new subgoals are introduced, one can expect the goal type to change. Broadly speaking, one’s objective is to construct a term of this type.

Administrative tactics

There are a number of tactics in Harpoon that do not contribute directly to the development of the proof, but are used to manipulate the state of the prover. To distinguish these from the proof tactics, we call these administrative tactics. Despite not contributing to the development of the proof, administrative tactics are nonetheless entered into the subgoal prompt.

See here for the complete list of administrative tactics.