在 Agda 中，我如何证明 coductive list（又名 Stream）上的 uncons 之后的 cons 是身份？

Question

我正在通过https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html研究共导和共模式。我以为我理解文章代码，所以我决定研究以下命题。

cons-uncons-id : ? {A} (xs : Stream A) ? cons (uncons xs) ? xs

我以为这个命题和文章问题非常相似，也可以证明，但我不能很好地证明。 这是我写的代码。

我认为它可以改进，cons-uncons-id (tl xs)因为它的类型与 merge-split-id 非常相似，但 Agda 不接受它。

这是我自己想到的一个问题，所以我认为这是真的，但当然存在误解的可能性。然而，非利弊和利弊会恢复原状是很自然的。

如果你应该能够证明它而不会被误解，请告诉我你如何证明它。

你能解释一下为什么不能像merge-split-id一样证明吗？

问候，谢谢！

Answer 1

refl您只需要定制\xe2\x89\x88.

\n\n

refl-\xe2\x89\x88 : \xe2\x88\x80 {A} {xs : Stream A} \xe2\x86\x92 xs \xe2\x89\x88 xs\nhd-\xe2\x89\x88 refl-\xe2\x89\x88 = refl\ntl-\xe2\x89\x88 refl-\xe2\x89\x88 = refl-\xe2\x89\x88\n\ncons-uncons-id : \xe2\x88\x80 {A} (xs : Stream A) \xe2\x86\x92 cons (uncons xs) \xe2\x89\x88 xs\nhd-\xe2\x89\x88 (cons-uncons-id _ ) = refl\ntl-\xe2\x89\x88 (cons-uncons-id xs) = refl-\xe2\x89\x88\n

\n\n

不能使用与 with 相同的策略的原因merge-split-id是consanduncons函数不会在整个流中递归（即它们在第一个元素之后停止）。从某种意义上说，这实际上使cons-uncons-id引理更容易证明，因为您只需证明第一个元素相等，然后其余的就是自反性。

\n