LP, the Larch Prover — The prove command

The prove command initiates the proof of a conjecture.

Syntax

<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