Case Analysis
We often fail to prove something by reduction just because OBJ does not have a rewrite rule for some necessary fact, e.g., about the data values involved in the problem. In such a case, we can go off "to the side" to prove the result (in the form of an equation), assert it, and then use it to complete the reduction. Such an auxiliary result is called a lemma.

Sometimes it is easier to prove a result by breaking the proof (or a part of it) into `cases.' For example, in trying to prove a sentence of the form 

    ( n) (n > 0 => Q(n)),
it might be easier to prove the following two cases separately, 
    ( n) (n > 0 and n even => Q(n))
    ( n) (n > 0 and n odd  => Q(n)),
than to prove the assertion in its original form. In general, there may be many different ways to break a condition like n>0 into cases. Another is 
    ( n) (n = 1 => Q(n))
    ( n) (n > 1 => Q(n)).

Examples like these suggest that cases are predicates P1,...,PN such that P1 and ... and PN and P are equivalent, where the sentence to be proved has the form ( X) P => Q; and they further suggest that a proof by case analysis consists of proving ( X) Pi => Q for i=1,...,N.

The rule for case analysis is then as follows:

    A  (P => Q) ---> A  (Pi => Q) for i=1,...,N and
                       A  (P => P1 and ... and PN) .
[Next] [Prev] [Home] [BHome]
26 December 1996