# LP, the Larch Prover -- The prove command

The *prove command* initiates the proof of a conjecture.
`<prove-command> ::= ``prove` <assertion> [ `by` <proof-method> ]

## Examples

`prove e \in {e}
prove i * (j + k) = (i * j) + (i * k) by induction on i
prove sort Set generated by {}, insert
`

## Usage

The `prove` command initiates an attempt to prove a conjectured assertion
using the specified method. If no method is specified, LP uses the one
determined by the current value of the proof-methods setting. LP
assigns a name to the conjecture using the current
name-prefix setting, unless the assertion begins with
`:`<simpleId>`:`, in which case LP uses that identifier as the
name-prefix for the assertion. If and when the proof of a conjecture succeeds,
LP adds the conjecture to its logical system and uses it as if it had been
asserted by the assert command. The activity and
immunity of the conjecture, however, are determined when it is
introduced by a `prove` command, not when it is proved; these attributes can
be changed using the make command.
LP maintains a stack of *proof contexts* for conjectures whose proofs are
not yet complete. Each proof context consists of a conjecture, a
logical system of facts available for the proof, and
values for the local settings that govern
the proof. The conjecture in the topmost proof context on the stack is known
as the *current conjecture*.

The `prove` command pushes a new proof context on top of the stack. Certain
proof methods create *subgoals* for proving a conjecture. LP associates a
separate proof context with each subgoal, and it adds appropriate additional
facts, called *hypotheses*, to the logical system in that proof context.

The user can cancel the proof of a conjecture with the cancel command,
which pops the stack of proof contexts. Or the user can resume the proof of
the current conjecture with the resume command (for example, to
specify a new method of proof or after proving a lemma). Whenever a proof
succeeds or is canceled, LP pops the stack of proof contexts, restores its
logical system and settings to those in effect before work began on the
conjecture (thereby discarding any lemmas proved while working on the
conjecture), adds the conjecture to the system if it was proved, and resumes
work on the new current conjecture. As soon as LP can establish the current
conjecture, it terminates any forward inference mechanisms (such as
internormalization of the rewriting system or the computation of critical-pair
equations) that may be in progress.

## See also