functional-programming - 如何提取 Isabelle 中的实例化变量？

Question

我试图在 Isabelle 中证明以下内容：

theorem map_fold: "∃h b. (map f xs)  = foldr h xs b"
apply (induction xs)
apply auto
done

如何获得hand的实例化值b？

Answer 1

有时为此目的有效的一种方法是陈述一个示意性引理：

schematic_lemma "map f xs = foldr ?h xs ?b"
apply (induct xs)
apply simp
...

类似simp或rule可以在证明期间实例化示意图变量的方法（统一的结果）。如果您能够完成证明，那么您只需查看生成的引理即可了解最终的实例化是什么。

请注意，示意图变量可能有点棘手：有时simp会以一种使当前目标可以轻松证明的方式实例化示意图变量，但同时使其他子目标无法解决。

在这种特定情况下，Isabelle 可以毫无问题地实例化 ?b，但无法通过统一确定 ?h。通常，具有函数类型的示意图变量更难处理。

最后，我做了 Manuel 建议的事情：首先，用普通变量 ( lemma "map f xs = foldr h xs b") 陈述一个引理。然后看看归纳证明在哪里卡住了，并逐步完善陈述，直到它可以证明。

Answer 2

一种方法是使用SOME：

h := SOME h. ∃b. map f xs = foldr h xs b
b := SOME b. map f xs = foldr h xs b

使用您的map_fold定理和一些摆弄someI_ex，您可以证明通过这些定义，map f xs = foldr h xs b确实成立。

但是，虽然这在逻辑上为您提供了 and 的值h，b但我希望您不会对它们非常满意，因为您实际上并没有看到hand是什么b；而且也没有办法（逻辑上）这样做。

在某些情况下，您还可以制定一个定理，说明“存在f,xs使得不存在h,b存在map f xs = foldr h xs b”并让 nitpick 为该陈述找到反例，但这种情况对于 nitpick 来说太复杂了，因为它必须找到一个函数在一个无限域上，它依赖于无限域上的另一个函数。

我认为没有办法让您真正获得存在证人h，并b摆脱您证明为具体价值的定理。您只需通过检查归纳案例自己找到它们，并发现它们是h = λx xs. f x # xs和b = []。

这是迄今为止最简单的解决方案。

更新：证明提取

今天重读这个帖子时，我真的记得 Isabelle 中确实存在证明提取。它需要为所有定理计算显式证明项，因此您需要从 Isabelle 开始isabelle jedit -l HOL-Proofs。然后你可以这样做：

theorem map_fold: "∃h b. (map f xs)  = foldr h xs b"
  by (induction xs) auto

extract map_fold

map_fold这为您定义了一个类型的常量('a ⇒ 'b) ⇒ 'a list ⇒ ('a ⇒ 'b list ⇒ 'b list) × 'b list，即给定一个映射函数和一个列表，它为您提供了函数和您必须放入的初始状态foldr才能获得相同的结果。您可以使用 . 查看定义thm map_fold_def。稍微简化一下，它看起来像这样：

map_fold f xs = 
    rec_list (λx xa. default, []) (λx xa H. (λa b. f a # map f xa, default)) xs

这有点难以阅读，但您可以看到[]和f a # map f xa。

不幸的是，证明术语变得相当大，所以我怀疑这对于玩具示例之外的任何东西都有多大用处。