Two key problems in inductive theorem proving are proposing lemmas and generalizations. A prover's divergence often suggests to the user an appropriate lemma or generalization that will enable the proof to go through without divergence. As a simple example, consider the theorem,
This is part of a simple program verification problem [11]. Addition and doubling are defined recursively by means of the rewrite rules,
where represents the successor of
(that is,
).
I have adopted the PROLOG convention of writing meta-variables
like
and
in upper case.
The theorem prover SPIKE [5]
fails to prove this theorem.
The proof attempt begins with a simple
one step induction on . The base case is
trivial. In the step case,
the induction hypothesis is,
And the induction conclusion is,
To ease presentation,
variables in this paper are, as here, sometimes renamed
from those introduced by SPIKE. This has no effect
on the results as the prover and divergence
critic both alpha convert variable names where necessary.
Rewriting the induction conclusion with the
recursive definitions of
and + gives,
The outermost successor functions on either
side of the equality are now cancelled,
The prover then fertilizes with the induction hypothesis
on the left hand side,
This equation cannot be simplified further so
another induction is performed. Unfortunately,
this generates the diverging sequence of subgoals,
The problem is that the prover repeatedly tries an induction
on but is unable to simplify the successor functions that this introduces
on the first argument position of
+. The proof will go through without divergence if
we have the rewrite rule,
This rule ``ripples'' accumulating successor functions
off the first argument position of
+. This rewrite rule is derived from
the lemma,
This is the commuted version of the recursive definition
of addition and is, coincidently, a generalization
of the first subgoal. This lemma can be proved without
divergence as the induction variable,
occurs just in the second
argument position of +.
In this paper I describe a simple ``divergence critic'', a computer program which attempts to automate this process. The divergence critic identifies when a proof attempt is diverging by means of a ``difference matching'' procedure. The critic then proposes lemmas and generalizations which hopefully allow the proof to go through without divergence. Although the critic is designed to work with the prover SPIKE, it should also work with other induction provers [19]. SPIKE is a rewrite based theorem prover for first order conditional theories. It contains powerful rules for case analysis, simplification and implicit induction using the notion of a test set. Unfortunately, as is the case with other inductive theorem provers, its attempts to prove many theorems diverge without an appropriate generalization or the addition of a suitable lemma.
In Section 2, I describe difference matching and rippling, the two key ideas at the heart of the divergence critic. I then outline how difference matching identifies the accumulating term structure which is causing divergence (Section 3). In Section 4 and 6, I show how lemmas are speculated which ``ripple'' this term structure out of the way. In Section 5, I describe the heuristics used in generalizing these lemmas. Finally, implementation and results are described in Sections 7 and 8.