Algebraic Foundations of Proof Refinement

TL;DR

This paper introduces Dependent LCF, a framework for proof refinement that handles dependencies between subgoals and distinguishes rules from tactics, enhancing proof assistant capabilities.

Contribution

It presents a general apparatus for dependent proof refinement and introduces a naturality-based distinction between refinement rules and tactics.

Findings

Framework implemented in RedPRL proof assistant.

Supports dependency of subgoal statements on other proofs.

Enhances algorithmic proof refinement methods.

Abstract

We contribute a general apparatus for dependent tactic-based proof refinement in the LCF tradition, in which the statements of subgoals may express a dependency on the proofs of other subgoals; this form of dependency is extremely useful and can serve as an algorithmic alternative to extensions of LCF based on non-local instantiation of schematic variables. Additionally, we introduce a novel behavioral distinction between refinement rules and tactics based on naturality. Our framework, called Dependent LCF, is already deployed in the nascent RedPRL proof assistant for computational cubical type theory.