We present a sound and complete focusing calculus for the core of the logic behind the proof assistant Beluga as well as an overview of its implementation as a tactic in Beluga's interactive proof environment Harpoon. The focusing calculus is designed to construct uniform proofs over contextual LF and its meta-logic in Beluga: a dependently-typed first-order logic with recursive definitions. The implemented tactic is intended to complete straightforward sub-cases in proofs allowing users to focus only on the interesting aspects of their proofs, leaving tedious simple cases to Beluga's theorem prover. We demonstrate the effectiveness of our work by using the tactic to simplify proving weak-head normalization for the simply-typed lambda-calculus.

翻译：我们提出了一种针对证明助手Beluga背后逻辑核心的完备且可靠的主焦演算，并概述了其在Beluga交互式证明环境Harpoon中作为策略的实现。该主焦演算旨在为上下文LF及其在Beluga中的元逻辑（一个带有递归定义的依赖类型一阶逻辑）构建统一证明。所实现的策略旨在补全证明中直接明了的子情况，使用户只需关注其证明中感兴趣的部分，而将繁琐的简单情况交由Beluga的定理证明器处理。我们通过使用该策略简化简单类型λ演算的弱头规范化证明，展示了工作的有效性。