代码之家 › 专栏 › 技术社区 › Attila Karoly

构造有用引理

isabelle

2

Attila Karoly · 技术社区 · 6 年前

在教程中 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\u-app引理:

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

仅仅是直觉和实践,就像在纸和笔的证明中一样,使人能够看到子目标1.是如何被简化的,并产生了一个类似rev\u应用程序的引理?我根本不知道这个引理是怎么暗示自己的。

1 回复 | 直到 6 年前

1

4

larsrh 6 年前

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

例如,主引理描述了 rev / 版次 财产。但是,子目标需要 app . 这就是为什么你需要一个关于这两个的引理。

不幸的是,剩下的只能用“人类的创造力”来形容:看到这一点 rev(app xs ys) = app (rev ys) (rev xs) 是合理的财产 版次 / .

例如,在自动检测这些属性方面有各种各样的研究 IsaHipster