4 - A formal account of rippling

Summary

As explained in Section 1.1.4, rippling is a heuristic that reflects a common pattern of reasoning found in theorem-proving: one wants to prove a goal using a given, and rewriting is used to transform the goal to the point where the given can be used. As noted in Chapter 2, there are various complications, such as multiple goals and givens and universally quantified givens with corresponding sinks. However, the general pattern is the same and can be codified by methods used in proof-planning.

To mechanize this common pattern of reasoning, rippling generalizes rewriting, so that semantic information is used to guide proof construction. The user has expectations (encoded by the proof-plan methods) about how the proof should proceed, namely that differences between the goal and the givens should be minimized. Annotations provide a kind of abstraction that is used to minimize these differences. Under this abstraction, the identity of the different symbols is ignored and one just differentiates whether they belong to the skeleton or not. Rippling constitutes an extension of rewriting that uses these annotations to drive proofs forward in a goal-directed way. Differences are monotonically decreased and rippling terminates with success or failure depending on whether the givens can be used or not.

In this chapter we consider how the concepts described above can be formalized. There is no one best formalization, so we keep our discussion abstract, when possible, and first discuss what properties are desired.