agda - 在 Agda 中，我如何证明在 uncons over coinductive list（aka Stream）之后的 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 不接受它。

这是我自己想到的一个问题，所以我觉得是对的，当然也有误解的可能。但是，uncons 和 cons 会按原样返回是很自然的。

如果您应该能够在不被误解的情况下证明它，请告诉我您如何证明它。

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

问候，谢谢！

标签： agdatheorem-provingcoinduction

Answer 1