LP, the Larch Prover — The box and diamond commands

A [] (box) or a <> (diamond) appearing as the first nonblank characters of an input line begins a checkable comment, which LP uses to ensure that replayed proofs do not diverge from the way users expect them to proceed.

Syntax

<diamond-command> ::= <> <character>*
<box-command>     ::= [] <character>*

Examples

<> induction step
[] induction step

Usage

LP generates []'s and <>'s in the history and script files. Users generally copy the <> and [] annotations supplied by LP into their command files rather than attempt to generate these annotations themselves. LP generates a <> whenever it introduces a subgoal in a proof, and it generates a [] whenever it finishes the proof of a subgoal or of a conjecture. After a successful proof, the number of []'s in the history and script file equals the number of prove commands plus the number of <>'s.

LP checks <>'s and []'s when it executes commands from a .lp file and the box-checking setting is on. Whenever it generates a <> or a [], LP checks that the next nonblank line in the .lp file contains a corresponding <> or [] command. The special LP prompts <>? and []? indicate that LP expects a confirming <> or [] in the .lp file. LP prints an error message if the confirming <> or [] is missing, or if an unexpected <> or [] appears in the .lp file.

Regardless of whether box-checking is on or off, LP does not copy <> and [] commands from its input to the history or to a script file. Instead, it puts into the history and script file the <> and [] commands that it produces as it creates and discharges subgoals. Thus, the history and the script file will be annotated in a way that correctly reflects the actual progress of the proof.