How can i prove that cons after uncons over coinductive list(a.k.a Stream) are identity, in Agda?

Question

I'm studying coinductive and copatterns through https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html . I thought I understood the article code, so I decided to work on the following proposition.

cons-uncons-id : ∀ {A} (xs : Stream A) → cons (uncons xs) ≈ xs

I thought this proposition was very similar to the article problem and could be proved as well, but I can't prove it well. Here is the code I write.

I thought it could be refined with cons-uncons-id (tl xs) because the type is very similar to merge-split-id, but Agda doesn't accept it.

This is a problem I thought of myself, so I think it's true, but of course there is a possibility of misunderstanding. However, it is natural that uncons and cons will return as they are.

If you should be able to prove it without being misunderstood, please tell me how you can prove it.

Can you explain why you can't prove it in the same way as merge-split-id?

Regards, thank you!

Answer 1

You just need a custom refl for ≈.

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-≈

The reason you can't use the same strategy as with merge-split-id is that the cons and uncons functions don't recurse down the whole stream (i.e. they stop after the first element). This actually makes the cons-uncons-id lemma easier to prove, in a sense, since you only have to prove the first elements are equal, and then the rest is reflexivity.