[Agda] Tentative guidelines for working with coinductive types

[Nils Anders Danielsson]

On 2009-01-15 02:23, Nils Anders Danielsson wrote:

> Let us now see if we can prove that ones is equal to its own unfolding
> (almost) with the simple corecursive proof that did not work for "inf"
> in another message in this thread:
> 
>   eq : ones ≈ 1 ∷ ♯ ones
>   eq = 1 ∷ eq′
>     where
>     eq′ : ∞ (♭ rec ≈ ♭ (♯ones))
>     ♭ eq′ = ?

As an aside I'd like to note that we can avoid the problems with this
proof by stating the goal differently:

   tail : Stream ℕ → Stream ℕ
   tail (x ∷ xs) = ♭ xs

   eq : tail ones ≈ ones
   eq = 1 ∷ eq′
     where eq′ ~ ♯ eq

This works just as well with destructors as with constructors:

   record _≈_ {A} (xs ys : Stream A) : Set where
     field
       head-eq : head xs ≡ head ys
       tail-eq : ∞ (♭ (tail xs) ≈ ♭ (tail ys))

   eq : ♭ (tail ones) ≈ ones
   eq = record { head-eq = refl
               ; tail-eq = eq′
               }
     where eq′ ~ ♯ eq

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.