Publikation
Tactics for Hierarchical Proofs
David Aspinall; Ewen Denney; Christoph Lüth
In: Mathematics in Computer Science, Vol. 3, Pages 309-330, Birkhäuser, 3/2010.
Zusammenfassung
There is something of a discontinuity at the heart of popular tactical
theorem provers. Low-level, fully-checked mechanical proofs are large
trees consisting of primitive logical inferences. Meanwhile, high-level
human inputs are lexically structured formal texts which include tactics
describing search procedures. The proof checking process maps from the
high-level to low-level, but after that, explicit connections are usually
lost. The lack of connection can make it difficult to understand the proof
trees produced by successful tactic proofs, and difficult to debug faulty
tactic proofs.
We propose the use of hierarchical proofs, also known as hiproofs, to help
bridge these levels. Hiproofs superimpose a labelled hierarchical nesting
on an ordinary proof tree, abstracting from the underlying logic. The
labels and nesting are used to describe the organisation of the proof,
typically relating to its construction process.
In this paper we introduce a foundational tactic language Hitac which
constructs hiproofs in a generic setting. Hitac programs can be evaluated
using a big-step or a small-step operational semantics. The big-step
semantics captures the intended meaning, whereas the small-step semantics
is closer to possible implementations and provides a unified notion of
proof state. We prove that the semantics are equivalent and construct
valid proofs. We also explain how to detect terms which are stuck in the
small-step semantics, and how these suggest interaction points with
debugging tools. Finally we show some typical examples of tactics,
constructed using tactical combinators, in our language.