agda - 在 Agda 中，我如何证明联合归纳列表(a.k.a 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

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

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

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

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

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

问候，谢谢!

Answer 1

您只需要一个定制 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引理在某种意义上更容易证明，因为你只需要证明第一个元素是相等的，然后剩下的就是自反性。