构建有用的引理

Posted 2023-03-28

【中文标题】构建有用的引理

【英文标题】：Constructing useful lemmas

【发布时间】：2018-10-10 14:09:22

【问题描述】：

在教程Isabelle/HOL 中的编程和证明中，有一步一步的解释了将列表反转两次产生原始列表的证明（2.2.4 证明过程）。

theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induction xs)
apply(auto)

按照自动步骤，子目标仍然存在：

1. V x1 xs.
     rev (rev xs) = xs =⇒
     rev (app (rev xs) (Cons x1 Nil)) = Cons x1 xs

然后作者说“为了进一步简化这个子目标，引理建议自己。”，并在下面介绍 rev_app 引理：

lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"

是否只是直觉和实践，就像在纸笔证明中一样，可以让人们看到子目标 1. 可以如何简化并提出像 rev_app 这样的引理？我根本无法识别这个引理是如何暗示自己的。

【参考方案1】：

对于不熟悉形式证明开发的人来说，这确实很棘手。随着时间的推移，人们将学习许多启发式方法来提出潜在的引理。

在这种情况下（纯等式推理），启发式通常通过查看子目标的相关常数来工作。

例如，主要引理描述了rev/rev 属性。然而，子目标需要一些关于rev/app 的信息。这就是告诉您您需要关于这两者的引理。

不幸的是，剩下的只能被描述为“人类的聪明才智”：看到rev(app xs ys) = app (rev ys) (rev xs) 是rev/app 的合理属性。

关于自动检测这些属性有各种研究，例如IsaHipster。

【讨论】：

解释 Tobias Nipkow，使用证明助手不会消除数学推理中的直觉。直觉很重要，虽然没有它也可以使用证明助手，但我怀疑一个人会走得很远。形式推理（有或没有计算机）的作用不是消除数学中的直觉，而是消除必须信任一个人的直觉的需要。您使用直觉来提出您的证明，然后将其形式化，然后您可以合理地确定它确实是正确的。

等式推理的另一个小提示：当你的目标涉及两个这样的函数时，你通常需要将它们关联起来的辅助事实，在等式的情况下，你可能需要一些关于它们如何通勤的引理.对于某些固定功能f 和g，有一个像f (g x) 或f (g x) (g y) 这样的子术语是相当常见的情况。您希望简化器做的通常的事情是推入f，或者以某种方式“取消”f 和g。