考虑以下树和子树的愚蠢 Isabelle 定义:
datatype tree = Leaf int
| Node tree tree
fun children :: "tree ⇒ tree set" where
"children (Leaf _) = {}" |
"children (Node a b) = {a, b}"
lemma children_decreasing_size:
assumes "c ∈ children t"
shows "size c < size t"
using assms
by (induction t, auto)
function subtrees :: "tree ⇒ tree set" where
"subtrees t = { s | c s. c ∈ children t ∧ s ∈ subtrees c }"
by auto
termination
apply (relation "measure size", simp)
子树
的终止证明在这一点上卡住了,尽管递归调用只对子树进行,根据有根据的 size
关系(如微不足道的引理所示)。
证明状态如下:
goal (1 subgoal):
1. ⋀t x xa xb. (xa, t) ∈ measure size
当然,这是不可能证明的,因为 xa
是 t
的 child 的信息丢失了。我做错什么了吗?我能做些什么来保存证明吗?我注意到我可以使用列表而不是集合来制定相同的定义:
fun children_list :: "tree ⇒ tree list" where
"children_list (Leaf _) = []" |
"children_list (Node a b) = [a, b]"
function subtrees_list :: "tree ⇒ tree list" where
"subtrees_list t = concat (map subtrees_list (children_list t))"
by auto
termination
apply (relation "measure size", simp)
并获得信息量更大、可证明的终止目标:
goal (1 subgoal):
1. ⋀t x.
x ∈ set (children_list t) ⟹
(x, t) ∈ measure size
这是 Isabelle 中的一些限制,我应该通过不使用集合来解决这个问题吗?
最佳答案
在 subtrees
的集合理解中对 c : children t
的限制不会出现在终止证明义务中,因为函数包先验地不知道任何事情关于 &
。可以使用一致性规则来实现这一点。在这种情况下,您可以在本地将 conj_cong
声明为 [fundef_cong]
以实质上模拟从左到右的评估顺序(尽管 HOL 中没有评估这样的东西) .例如,
context notes conj_cong[fundef_cong] begin
fun subtrees :: ...
termination ...
end
上下文 block 确保声明 conj_cong[fundef_cong]
仅对该函数定义有效。
带有列表的版本可以工作,因为它使用函数 map
,默认情况下有一个同余规则。如果您对集合使用了单子(monad)绑定(bind)操作(而不是集合理解),那么集合也应该如此。
关于isabelle - 使用集合理解的函数的终止证明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/33379349/