递归函数导致 Isabelle 中的简化循环

Question

我有以下两个伊莎贝尔定义：

fun remove_left :: "cmd ⇒ cmd × cmd option" where
"remove_left (Comp c d) = (case remove_left c of
  (head, Some c') ⇒ (head, Some (Comp c' d)) |
  (head, None) ⇒ (head, Some d)
)" |
"remove_left c = (c, None)"

function pop_flatten :: "cmd ⇒ cmd" where
"pop_flatten c = (case remove_left c of
  (h, Some c') ⇒ Comp h (pop_flatten c') |
  (h, None) ⇒ h
)"
by pat_completeness auto
termination by(relation "measure size"; simp; metis remove_left_decreases)

（作为练习，我正在证明各种版本的程序扁平化例程是相同的。）

简化器似乎无法处理这个问题。例如，当我尝试以下明显错误的引理时：

lemma "pop_flatten c = Skip"
  apply(simp)

简化器立即进入循环。 simp_trace 显示它不断应用 pop_flatten 的定义。我怀疑 case 表达式引入了简化器认为是全新的术语 c'，因此它再次展开定义。我不确定如何解决这个问题，我不想改变我的定义。我尝试删除 pop_flatten 的简单规则如下：

declare pop_flatten.simps [simp del]

但是现在我通常会做的几个证明步骤

by simp

显然不再起作用了。我对 cmd 的定义是标准的，只是一个跳过，顺序组合，if 和 while。我在这里遇到的简化器中是否确实存在边缘情况，或者我的定义在某些我没有看到的方面是错误的？

Answer 1

这导致无限循环并不特别令人惊讶：

pop_flatten.simps

规则的左侧立即再次适用于其右侧，因此几乎可以保证无限重写循环。

出于这个原因，如果您只使用一个不受条件或模式匹配保护的方程式进行递归定义，最好立即从 simp 集中删除

.simps

规则（正如您所做的那样） .

如果你确实想应用它，你可以使用

apply (subst pop_flatten.simps)

以非常有针对性的方式应用它一次，或者你可以将它限制为你想要应用它的特定值，例如

apply (simp add: pop_flatten.simps[of c])

.

Answer 2

为了完整起见，根据 Manuel 的建议，我最终做的是重写

pop_flatten

以在先决条件中拆分案例，如下所示：

function pop_flatten' :: "cmd ⇒ cmd" where
"snd (remove_left c) = None ⟹ pop_flatten' c = fst (remove_left c)" |
"snd (remove_left c) ≠ None ⟹ pop_flatten' c = Comp (fst (remove_left c)) (pop_flatten' (the (snd (remove_left c))))"
by simp auto
termination
  apply(relation "measure size")
   apply(simp)
  apply(simp add: remove_left_decreases)
  by (metis option.sel prod.collapse remove_left_decreases)

我不太清楚，但我怀疑这对简化器更好，因为展开现在由

⟹

条件保护。显然，简化器 is 允许穿透

case of

构造（？），因此这是我的错误假设。

然后我使用这个版本修正了我的引理，这一切都变得非常简单，因为我可以使用

simp

而不是必须替换自定义设计术语，最后（在证明

pop_flatten

和

pop_flatten'

相等之后）在那里替换了

simp

-不友好的版本以获得最终的引理。我想这并不总是一个选项，但由于我的功能非常简单，所以我不必更改任何其他内容。

（非常感谢 Manuel！）