LP, the Larch Prover -- Hints on managing proofs


Prove as you would program. Design your proofs. Modularize them. Think about their computational complexity.

Be careful not to let variables disappear too quickly in a proof. Once they are gone, you cannot do a proof by induction. Start your inductions before starting proofs by cases, the => method, the <=> method, or the if method.

Splitting a conjecture into separate conjuncts (using the /\ proof method) early in a proof often leads to repeating work on multiple conjuncts, for example, doing the same case analysis several times.

To keep lemmas and theorems from disappearing (because they normalize to true), make them immune. Typing either of the commands

set immunity on                          prove ... by explicit-commands
prove ... by explicit-commands           make immune conjecture
set immunity off                         resume by ...
resume by ...
when you begin the proof of a conjecture immunizes that conjecture (i.e., causes it to be immune once it becomes a theorem), but nothing else. Similarly, the commands
set immunity ancestor
instantiate ... in ...
set immunity off
help keep instantiations from disappearing when they are special cases of other facts.

When a proof gets stuck:

In the course of a proof, you may lose track of your place in the subgoal tree. This happens most often if LP has just discharged several subgoals in succession without user intervention and/or it has automatically introduced subgoals. The display, resume, and history commands can be used to help find your place.

Because LP automatically internormalizes facts, you may find that what you consider to be the information content of some user-supplied assertion has been ``spread out'' over several facts in the current logical system in a way that may not be easy to understand, particularly if the system contains dozens or hundreds of facts. Similarly, you may sometimes notice that LP is reducing (or has reduced) some expression in some way that you don't understand. The command show normal-form E, where E is the expression being mysteriously reduced, or where E is the original form of one side of a formula, will often be enlightening in such cases. Setting the trace-level up to 6 will show which rewrite rules are applied in the normalization.