Highly automated theorem provers like Dafny allow users to prove simple properties with little effort, making it easy to quickly sketch proofs. The drawback is that such provers leave users with little control about the proof search, meaning that the small changes inherent to the iterative process of writing a proof often lead to unpredictable variations in verification time, and eventually hard-to-diagnose proof failures. This sometimes turns the boon of high automation into a curse, as instead of breaking early and showing unsolved goals to the user like in Coq, proofs tend to gradually become unstable until their verification time explodes. At this point, the absence of a proof context to investigate often leaves the user to a painful debugging session. In this paper, we show how to use Dafny modules to encode Coq-like induction principles to dramatically improve the stability and maintainability of proofs about inductive data structures.

翻译：像Dafny这样高度自动化的定理证明器能让用户以很小的代价证明简单性质，便于快速构建证明草图。其不足之处在于，这类证明器使用户难以掌控证明搜索过程，这意味着迭代式证明写作中固有的微小改动，往往会导致验证时间的不可预测波动，最终引发难以诊断的证明失败。这有时会将高自动化带来的裨益转变为诅咒：与Coq中提前中断并展示未解决目标不同，Dafny中的证明往往逐渐变得不稳定，直至验证时间呈爆炸式增长。此时，由于缺乏可供调查的证明上下文，用户常常陷入痛苦的调试过程。本文展示了如何利用Dafny模块对Coq式归纳原理进行编码，从而显著提高关于归纳数据结构的证明的稳定性和可维护性。