LP, the Larch Prover -- Proofs by cases

Conjectures can often be simplified by dividing a proof into cases. When a conjecture reduces to true in all cases, it is a theorem. Case analysis has two primary uses. If a conjecture is a theorem, a proof by cases may circumvent a lack of completeness in the rewrite rules. If a conjecture is not a theorem, an attempted proof by cases may simplify the conjecture and make it easier to understand why the proof is not succeeding.

The command prove F by cases F1, ..., Fn directs LP to prove a formula F by division into n cases defined by the formulas F1, ..., Fn (or into two cases, F1 and ~F1 if n = 1). The command resume by cases F1, ..., Fn directs LP to resume the proof of the current conjecture by division into cases.

A proof by cases involves n+1 subgoals. If n > 1, the first subgoal involves proving F1 \/ ... \/ Fn to show that the cases exhaust all possibilities. If n = 1, LP generates a default second case of ~F1, but does not generate a disjunction as the first subgoal. Then, for each case i, LP generates a subgoal F' and an additional hypothesis Fi' by substituting new constants for the free variables of Fi in both F and Fi. If an inconsistency results from adding a case hypothesis, that case is impossible and the subgoal is vacuously true. Otherwise the subgoal must be shown to follow from the axioms supplemented by the case hypothesis. The names of the case hypotheses have the form <simpleId>CaseHyp.<number>, where <simpleId> is the current value of the name-prefix setting.

In each case of a proof by cases, LP first adds the case hypothesis without using it to reduce the other rewrite rules in the system. Only if this action fails to reduce the desired conclusion to true does LP use the case hypothesis to reduce the other rewrite rules.