我正在通过 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)来改进它，因为该类型与合并拆分 id 非常相似，但 Agda 不接受它。
这是我自己想到的问题，所以我认为这是真的，但当然有误解的可能。 但是，缺点和缺点自然会恢复原样。
如果你应该能够证明它而不会被误解，请告诉我你如何证明它。
你能解释一下为什么你不能用与合并-拆分-id 相同的方式证明它吗？
问候，谢谢！
您只需要一个自定义refl即可≈。
refl-≈ : ∀ {A} {xs : Stream A} → xs ≈ xs
hd-≈ refl-≈ = refl
tl-≈ refl-≈ = refl-≈
cons-uncons-id : ∀ {A} (xs : Stream A) → cons (uncons xs) ≈ xs
hd-≈ (cons-uncons-id _ ) = refl
tl-≈ (cons-uncons-id xs) = refl-≈
您不能使用与merge-split-id相同的策略的原因是cons和uncons函数不会递归整个流(即它们在第一个元素之后停止(。从某种意义上说，这实际上使cons-uncons-id引理更容易证明，因为你只需要证明第一个元素是相等的，然后其余的就是反身性。