Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery

Abstract

We present a succinct account of dynamic rippling, a technique used to guide the automation of inductive proofs. This simplifies termination proofs for rippling and hence facilitates extending the technique in ways that preserve termination. We illustrate this by extending rippling with a terminating version of middle-out reasoning for lemma speculation. This supports automatic speculation of schematic lemmas which are incrementally instantiated by unification as the rippling proof progresses. Middle-out reasoning and lemma speculation have been implemented in higher-order logic and evaluated on typical libraries of formalised mathematics. This reveals that, when applied, the technique often finds the needed lemmas to complete the proof, but it is not as frequently applicable as initially expected. In comparison, we show that theory formation methods, combined with simpler proof methods, offer an effective alternative.