证明展开的聚变定律

Question

我正在阅读 Jeremy Gibbons 在 origami programming 上的文章，但在练习 3.7 中遇到了困难，该练习要求读者证明列表展开的融合定律：

unfoldL p f g . h = unfoldL p' f' g'

如果

p . h = p'
f . h = f'
g . h = h . g'

函数unfoldL，用于列表展开，定义如下：

unfoldL :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a
unfoldL p f g b = if p b then Nil else Cons (f b) (unfoldL p f g (g b))

这是我目前的证明尝试：

(unfoldL p f g . h) b
=   { composition }
unfoldL p f g (h b)
=   { unfoldL }
if p (h b) then Nil else Cons (f (h b)) (unfoldL p f g (g (h b)))
=   { composition }
if (p . h) b then Nil else Cons ((f . h) b) (unfoldL p f g ((g . h) b))
=   { assumptions }
if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
=   { composition }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
=   { ??? }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
=   { unFoldL }
unFoldL p' f' g'

我不确定如何证明标有??? 的步骤。我可能应该对b 上的功能应用程序进行某种归纳？相关问题：有哪些很好的资源可以解释和激发各种归纳技术，例如结构归纳？

Answer 1

经过一番谷歌搜索后，我找到了由同一位 Jeremy Gibbons（和 Graham Hutton）撰写的论文，该论文提出了proof methods for corecursive programs； 这篇文章包括一个关于互模拟和共归纳的部分，这是@luqui 在接受的答案中使用的证明技术。 第 6 节使用展开的普遍性质证明了聚变定律。 为了完整起见，我复制了下面的证明。

---

unfoldL的通用属性：

h = unfoldL p f g
<=>
∀ b . h b = if p b then Nil else Cons (f b) (h (g b))

聚变定律的证明：

unfoldL p f g . h = unfoldL p' f' g'
<=> { universal property }
∀ b . (unfoldL p f g . h) b = if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
<=> { composition }
∀ b . unfoldL p f g (h b) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { unfoldL }
∀ b . if p (h b) then Nil else Cons (p (h b)) (unfoldL p f g (g (h b))) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { composition }
∀ b . if (p . h) b then Nil else Cons (p . h) b (unfoldL p f g ((g . h) b)) = if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
<=  { assumptions }
(p . h = p') ^ (f . h = f') ^ (g . h = h . g')

Answer 2

我没有读过 Gibbons 的文章，他可能还依赖其他技术，但这是我所知道的。

您正在寻找某种归纳，这是一种很好的直觉，因为您需要的内容与您要证明的内容非常相似。但你实际上需要在这里共归纳。这是因为unfoldL 可以生成无限列表。在正式的类型系统中，您很少能证明两个无限结构是“相等的”——正式的相等性太强而无法证明大多数结果。相反，我们证明bisimilarity，这在非正式情况下也可能是平等的。

双相似性在理论上很棘手，我不会深入探讨（部分原因是我不完全理解基础），但在实践中使用它并不太难。基本上，要证明两个列表是双相似的，您可以证明它们要么都是Nil，要么都是Cons，具有相同的头部并且它们的尾部是双相似的，并且您可以在以下情况下使用协推假设证明尾巴的双相似性（但不是其他地方）。

所以对你来说，我们通过共归纳证明对于所有b（因为我们需要对不同的bs 使用共归纳假设）：

(unfoldL p f g . h) b ~~ unfoldL p' f' g' b

到目前为止我们已经

(unfoldL p f g . h) b
= { your reasoning }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))

通过p' b上的案例分析，如果p' b为True则

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is True }
Nil
~~ { reflexivity }
Nil
= { p' b is True }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }
unfoldL p' f' g'

;如果p' b 为 False 则

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is False }
Cons (f' b) ((unfoldL p f g . h) (g' b))
*** ~~ { bisimilarity Cons rule, coinductive hypothesis } ***
Cons (f' b) (unfoldL p' f' g' (g' b))
= { p' b is False }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }

标有*** 的行是关键行。首先，请注意它是~~ 而不是=。此外，我们被允许仅在Cons 构造函数下使用共归纳假设。如果允许我们在其他任何地方使用它，那么我们就可以证明任何两个列表都是相似的。