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:

Be skeptical. Don't be too sure your conjecture is a theorem.
If the conjecture is a conditional, conjunction, implication, or logical equivalence, try the corresponding proof method.
Try computing critical pairs between hypotheses and other rewrite rules, for example, by typing the command critical-pairs *Hyp with *.
Use a proof by cases to find out what is going on. Case on repeated subterms of the conjecture, on the antecedent of an implication in a rewrite rule, or on the test in an if in a rewrite rule.
Display the hypotheses (by typing display *Hyp) and check whether any that you expected to see are missing or are not oriented in the way you expected.
Look for a useful lemma to prove. See if replacing a repeated subterm in a subgoal by a variable results in a more general fact that you know to be true.

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.

display *Hyp is an easy way to find your place in nested case analyses.
display proof-status displays the entire proof stack; display conjectures names displays the named conjectures.
resume shows just the current conjecture (normalized, if the proof-methods setting includes normalization).
history 20 (or some other number) displays an indented history, including LP-generated box and diamond commands.

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.