Bridging Syntax and Semantics of Lean Expressions in E-Graphs

交互式定理证明器，如Isabelle/HOL、Coq和Lean，具有表达能力强的语言，可以形式化一般的数学对象和证明。在这个背景下，一个重要的目标是减少证明定理所需的时间和精力。提高证明自动化的效率是实现这一目标的重要手段。我们通过使用等式饱和实现了Lean中的等式推理的早期原型。为了实现这一目标，我们需要弥合Lean表达语义和等式饱和中的语法驱动的等价类图之间的差距。这涉及到处理绑定变量、隐式类型和Lean的定义等价性，后者比语法等价性更为一般，涉及到诸如$\alpha$-等价、$\beta$-约简和$\eta$-约简等概念。在本篇扩展摘要中，我们强调了我们如何尝试弥合这一差距，以及仍需解决的挑战。值得注意的是，虽然我们的技术部分不完全正确，但由于Lean的证明检查机制，最终的证明自动化仍然是正确的。

如何通过等式饱和来改进交互式定理证明器的证明自动化？这是一个新问题吗？

本文通过使用等式饱和来实现早期原型的证明自动化，以改进Lean中的等式推理。作者需要解决Lean表达语义和等式饱和中的语法驱动的等式图之间的差距，包括处理绑定变量、隐式类型以及Lean的定义等价性。这种定义等价性比语法等价性更为通用，包括诸如α-等价性、β-规约和η-规约等概念。虽然技术上是部分不完整的，但由于Lean的证明检查，所以得到的证明自动化仍然是完备的。相比于当前领域的研究，本文的思路是新颖的。

本文的亮点包括实现了证明自动化的早期原型，使用了等式饱和的方法来改进证明自动化，解决了Lean表达语义和等式饱和中的语法驱动的等式图之间的差距。作者提到了技术上的局限性，但是由于Lean的证明检查，得到的证明自动化仍然是完备的。本文没有提供数据集和代码，但值得进一步研究。

最近的相关研究包括使用等式饱和来改进定理证明器的证明自动化的研究，例如使用等式饱和来自动化化简和优化程序的研究。