Capturing Hiproofs in HOL Light

TL;DR

This paper introduces two methods, tactic recording and proof recording, for capturing hierarchical proof trees (hiproofs) in HOL Light, along with tools for visualization, enhancing proof structure understanding.

Contribution

It presents two novel, complementary approaches for capturing hiproofs in HOL Light, including implementations and visualization tools, improving proof analysis and explanation.

Findings

Implemented tactic recording method with Tactician

Developed proof recording approach with HipCam

Produced web-based visualization of hierarchical proofs

Abstract

Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used to abstract away from details, or to label particular portions to explain their purpose. In this paper we present two complementary methods for capturing hiproofs in HOL Light, along with a tool to produce web-based visualisations. The first method uses tactic recording, by modifying tactics to record their arguments and construct a hierarchical tree; this allows a tactic proof script to be modified. The second method uses proof recording, which extends the HOL Light kernel to record hierachical proof trees alongside theorems. This method is less invasive, but requires care to manage the size of the recorded objects. We have implemented both methods, resulting in two systems: Tactician and HipCam.