5

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!

いとうかつとし
  • 95
  • 4

1 Answers1

4

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.

oisdk
  • 9,763
  • 4
  • 18
  • 36
  • 2
    Really? I think the holes have different types. For `cons-uncons-id`, it should be `tl xs ≈ tl xs`, for `merge-split-id`, the hole should be `merge (split (tl xs)) ≈ tl xs`. The key here is that in the second one `merge` and `split` are still present in the equation. I'll update the answer with some more detail – oisdk Nov 25 '19 at 13:35
  • In my environment, for cons-uncons-id, it should be ```tl (cons (uncons xs)) ≈ tl xs```, for merge-split-id, the hale should be ```tl (merge (split xs)) ≈ tl xs```. Am I using something wrong? Here is the screen shot of my emacs at C-cC-l. https://twitter.com/cutsea110/status/1199081389020213249/photo/1 – いとうかつとし Nov 25 '19 at 21:44
  • Again, I check **C-c C-,** command, for merge-split-id, the hale should be ```merge (proj₂ (split xs) , tl (proj₁ (split xs))) ≈ tl xs``` , for cons-uncons-id, the hole should be ```proj₂ (uncons xs) ≈ tl xs```. There are something difference. :-) – いとうかつとし Nov 26 '19 at 01:58
  • 1
    Yeah, the type Agda is giving you there is a little unhelpful, but not wrong. You have do some execution in your head: `proj₂ (uncons xs)` evaluates to `tl xs`. Anyway, that's what makes the two types different: neither `uncons` nor `cons` is present in the type of the output proof (after you've normalised), so it doesn't require you to recurse in the proof unlike `merge-split-id`. – oisdk Nov 26 '19 at 12:37
  • I'm a little surprised because I have never experienced that Goal displayed by loading with **C-c C-l** and Goal displayed by **C-c C-,** with hole. I understand that there is a difference anyway and I understand what you say. Thank you. – いとうかつとし Nov 26 '19 at 14:48