Zippy -- Generic White-Box Proof Search with Zippers

TL;DR

Zippy tackles the challenge of rigid and hard-to-extend proof automation by offering a generic, white-box framework for tree-based proof search that is largely independent of concrete representations. It builds on alternating zippers, arrows, monads, and lenses to separate navigation, effects, and data manipulation, enabling extensibility and analysability in Isabelle/ML. The paper presents an abstract navigation specification, automatic generation of alternating zippers, and an extensible data-slot framework, along with an Isabelle/ML implementation and example instantiations. This approach aims to enable flexible, inspectable automation in interactive theorem proving, with potential to port or inspire AESOP-like strategies within Isabelle and beyond.

Abstract

We present a framework for tree-based proof search, called Zippy. Unlike existing proof search tools, Zippy is largely independent of concrete search tree representations, search-algorithms, states and effects. It is designed to create analysable and navigable proof searches that are open to customisation and extensions by users. Zippy is founded on concepts from functional programming theory, particularly zippers, arrows, monads, and lenses. We implemented the framework in Isabelle's metaprogramming language Isabelle/ML.

Figures (4)

• Figure 1: A step-by-step best-first proof search, from top-left to bottom-right. Goal nodes are solid and rule nodes are dashed, containing a rule ($\lor L$, Assm, $\land I$, etc.) to expand their parent and a success probability. Selected rules nodes are bold and red. The resulting proof is bold and blue.
• Figure 2: Step-wise abstraction of a search tree, from left to right. First, the nodes' data is abstracted. For this, node types $\vv{\mathsf{\alpha}}\,\mathsf{N}_{i}=\vv{\mathsf{\alpha}}\,\mathsf{NC}_{i}\times\vv{\mathsf{\alpha}}\,\mathsf{NN}_{i}$ are introduced. Polymorphic type arguments are omitted in the figure. Second, for each $i$, a container type $\vv{\mathsf{\alpha}}\,\mathsf{CO}_{i}$ is introduced, containing nodes of type $\vv{\mathsf{\alpha}}\,\mathsf{N}_{i}$. These containers are drawn dotted. Each $\vv{\mathsf{\alpha}}\,\mathsf{NN}_{i}$ is then set to point to a follow-up container. The last figure shows the resulting model, parametrised by a number $n$ and arbitrary container and content types for each $1\leq i\leq n$.
• Figure 3: Zipper navigation in a tree-shaped container, using the move sequence $[\mathsf{zip},\mathsf{down},\mathsf{down},\mathsf{right},\mathsf{up},\mathsf{unzip}]$. Focused parts are bold and red, containers are dotted, and nodes are solid. Initially, the whole container is in focus. We move to the root using $\mathsf{zip}$. Using $\mathsf{down}$, we move to its first child. This is once repeated. Then we move to the node's right sibling using $\mathsf{right}$. Using $\mathsf{up}$ moves to the node's parent. Finally, $\mathsf{unzip}$ moves the focus to the container.
• Figure 4: Navigation in a linked zipper, from top-left to bottom-right, using the move sequence $[\mathsf{Z}_{1}.\mathsf{zip}$, $\mathsf{down}_{1}$, $\mathsf{Z}_{2}.\mathsf{right}$, $\mathsf{up}_{2}$, $\mathsf{Z}_{1}.\mathsf{unzip}]$. Focused parts are bold and red, containers are dotted, and nodes are solid. Edges inside of containers are dashed. Initially, the container $\vv{\mathsf{\alpha}}\,\mathsf{CO}_{1}$ is in focus. Using $\mathsf{Z}_{1}.\mathsf{zip}$, we move to its node. Using $\mathsf{down}_{1}$, we move to the children's container's root. Using $\mathsf{Z}_{2}.\mathsf{right}$, we move to the node's right sibling. Using $\mathsf{up}_{2}$, we move to the container's parent. Finally, $\mathsf{Z}_{1}.\mathsf{unzip}$ moves the focus to the container.

Theorems & Definitions (10)

• Definition 1: Nodes
• Definition 2: Moves
• Definition 3: Zippers
• Definition 4: Linked Zippers
• Definition 5: Alternating Zippers
• Definition 6: Alternating Zipper Product
• Example 7
• Example 8
• Example 9
• Example 10