论文标题
对精益的新手友好的归纳策略
A Novice-Friendly Induction Tactic for Lean
论文作者
论文摘要
在基于依赖类型理论（例如COQ和LEAN）的定理掠夺中，归纳是一种基本的证明方法，而归纳策略在证明脚本中无所不在。然而，现有的归纳策略的人体工程学并不理想：它们不能可靠地支持归纳谓词和关系；它们有时会产生过度特异性或不必要的复杂诱导假设。他们偶尔为他们引入的假设选择令人困惑的名字。 本文描述了一种在LEAN 3中实施的新的归纳策略，该策略解决了这些问题。该策略特别适合教育使用，但专家还应该发现它比现有的归纳策略更方便。此外，该策略是针对精益3的元编程框架的中等复杂的案例研究。该论文描述了实施过程中遇到的一些困难，并提出了对框架的改进。
In theorem provers based on dependent type theory such as Coq and Lean, induction is a fundamental proof method and induction tactics are omnipresent in proof scripts. Yet the ergonomics of existing induction tactics are not ideal: they do not reliably support inductive predicates and relations; they sometimes generate overly specific or unnecessarily complex induction hypotheses; and they occasionally choose confusing names for the hypotheses they introduce. This paper describes a new induction tactic, implemented in Lean 3, which addresses these issues. The tactic is particularly suitable for educational use, but experts should also find it more convenient than existing induction tactics. In addition, the tactic serves as a moderately complex case study for the metaprogramming framework of Lean 3. The paper describes some difficulties encountered during the implementation and suggests improvements to the framework.
