Generalization and reuse of tactic proofs

A tactic proof is a tree-structured sequent proof where steps may be justified by tactic programs. We describe a prototype of a generic interactive theorem-proving system that supports the construction and manipulation of tactic proofs containing metavariables. The emphasis is on proof reuse. Examples of proof reuse are proof by analogy and reconstruction of partial proofs as part of recovering from errors in definitions or in proof strategies. Our reuse operations involve solving higherorder unification problems, and their effectiveness relies on a proof-generalization step that is done after a tactic is applied. The prototype is implemented in λProlog.