Доказательство закона слияния для разворачивания

Я не читал статью Гиббонса, и могут быть другие методы, на которые он опирается, но вот что я знаю.

Это хорошая интуиция, что вы ищете какую-то индукцию, потому что то, что вам нужно, очень похоже на то, что вы пытаетесь доказать. Но здесь действительно нужна коиндукция. Это потому, что unfoldL может создавать бесконечные списки. В системах формальных типов очень редко можно доказать, что две бесконечные структуры «равны» — формальное равенство слишком сильно, чтобы доказать большинство результатов. Вместо этого мы доказываем биподобие, которое в неформальных обстоятельствах могло бы также быть равенством.

Бисимилярность теоретически сложна, и я не буду вдаваться в нее (отчасти потому, что не до конца понимаю ее основы), но работать с ней на практике не так уж сложно. По сути, чтобы доказать, что два списка биподобны, вы доказываете, что они либо оба Nil, либо что они оба Cons с одной и той же головой, а их хвосты биподобны, и вы можете использовать гипотезу коиндукции при доказательстве биподобности списков. хвосты (но не где-либо еще).

Итак, мы доказываем методом коиндукции, что для всех b (поскольку нам нужно использовать гипотезу коиндукции для разных b):

(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 верно, то

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. Если бы нам разрешили использовать его где-нибудь еще, мы могли бы доказать, что любые два списка биподобны.

Погуглив, я нашел статью того же Джереми Гиббонса (и Грэма Хаттона), в которой представлен методы подтверждения для корекурсивных программ; статья включает раздел о бисимуляции и коиндукции, методе доказательства, использованном @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')