一句话：提出 Mtac2，为 Coq 提供支持反向推理的类型化策略编程语言，可在策略定义期静态排除多类错误。
Coq 的 Ltac 与 OCaml 策略编程虽支持自定义证明自动化，但无法为策略本身提供静态保证，导致大型策略开发难以维护。已有的 Mtac 虽引入类型化元编程，但缺少直接操纵证明状态、进行反向推理这一策略语言的核心能力。本文提出 Mtac2，在 Mtac 的类型化元编程基础上加入 Ltac 风格的反向推理策略编程，并引入新特性“类型化反向推理”（typed backward reasoning），从而在策略定义阶段静态排除若干类原本难以发现的错误。作者通过将大型 Coq 开发 Iris Proof Mode 中的多个策略从 Ltac 移植到 Mtac2，验证了其类型化策略的实用性。
Coq supports a range of built-in tactics, which are engineered primarily to support backward reasoning . Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemmas to break the goal into subgoals until all subgoals have been solved. Additionally, it provides support for tactic programming via OCaml and Ltac, so that users can roll their own custom proof automation routines. Unfortunately, though, these tactic languages share a significant weakness. They do not offer the tactic programmer any static guarantees about the soundness of their custom tactics, making large tactic developments difficult to maintain. To address this limitation, Ziliani et al. previously proposed Mtac , a new typed approach to custom proof automation in Coq which provides the static guarantees that OCaml and Ltac are missing. However, despite its name, Mtac is really more of a metaprogramming language than it is a full-blown tactic language: it misses an essential feature of tactic programming, namely the ability to directly manipulate Coq’s proof state and perform backward reasoning on it. In this paper, we present Mtac2 , a next-generation version of Mtac that combines its support for typed metaprogramming with additional support for the programming of backward-reasoning tactics in the style of Ltac. In so doing, Mtac2 introduces a novel feature in tactic programming languages—what we call typed backward reasoning . With this feature, Mtac2 is capable of statically ruling out several classes of errors that would otherwise remain undetected at tactic definition time. We demonstrate the utility of Mtac2’s typed tactics by porting several tactics from a large Coq development, the Iris Proof Mode, from Ltac to Mtac2.
@article{paperbot302,
title = {Mtac2: typed tactics for backward reasoning in Coq},
author = {Jan-Oliver Kaiser and Beta Ziliani and Robbert Krebbers and Yann Régis-Gianas and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236773}
}