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

Question

我试图在伊莎贝尔身上证明以下内容:

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

如何获取h和b的实例化值？

Answer 1

有时可以达到此目的的一种方法是陈述一个示意性引理:

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

像simp或rule这样的方法可以在证明过程中实例化原理图变量(统一的结果)。如果您能够完成证明，那么您只需查看生成的引理即可了解最终的实例化是什么。

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

在这种特定情况下，Isabelle 能够毫无问题地实例化 ?b，但无法通过统一确定 ?h。一般来说，具有函数类型的原理图变量处理起来要困难得多。

最后，我做了类似曼努埃尔建议的事情:首先，用普通变量陈述一个引理(引理“map f xs =foldr h xs b”)。然后看看归纳证明在哪里陷入困境，并逐步完善该陈述，直到它可被证明。