[Agda] Agda goes coinductive

[Dan Doel]

On Friday 06 June 2008, Ulf Norell wrote:
> On Fri, Jun 6, 2008 at 3:35 AM, Dan Doel <dan.doel at gmail.com> wrote:
> > > -- complaint: never != later never
> >
> >  map f (now v) != now (f v)
> >
> > Is this to be expected, or is it an oversight?
>
> This is the expected behaviour. When checking equality it's not safe to
> unfold corecursive functions. You can probably work around it by defining
> unfolding functions to force the unfolding. For instance,
>
> unfold : {a : Set} -> D a -> D a
> unfold (now x) = now x
> unfold (lated d) = later d
>
> You have unfold (map f (now v)) == now (f v).

That does work with 'map f (now v) = now (f v)' case, but it seems to cause 
trouble in the other case, and with never. Perhaps I'm just not seeing the 
solution though.

For instance:

  ...
  map-↓ (convergeLater pf) = ?0

    x = later (dx : D a)
    pf : dx ↓ v
    ?0 : unfold (map f (later dx)) ↓ f v
    map-↓ pf : unfold (map f dx) ↓ f v
    convergeLater (map-↓ pf) : later (unfold (map f dx)) ↓ f v

And I still get type errors. Similarly, I'm not sure where to put the unfold 
on diverge-never:

  diverge-never : unfold never ↑
  diverge-never = diverge diverge-never
    fails because now diverge-never : later never ↑
    and so diverge diverge-never : later (later never) ↑

I thought about adding a constructor to _↑

  codata _↑ {a : Set} : D a -> Set where
    diverge : {dx : D a} -> dx ↑ -> later dx ↑
    diverge-fold : {dx : D a} -> unfold dx ↑ -> dx ↑

But:

  diverge-never : never ↑
  diverge-never ~ diverge-fold (diverge diverge-never)

doesn't seem to work (which didn't surprise me, I suppose, as diverge-fold 
looks more inductive than coinductive), and the extra case requires me to 
rewrite tons of proofs. :)

I did notice with the extra constructor I can write:

  diverge-never : unfold never ↑
  diverge-never ~ diverge-fold (diverge-never)

Which doesn't seem right to me, but it nevertheless works. However, I've been 
as yet unable to get it to work with the map proof (and diverge-never : never 
↑ is also not an option).

Thanks for your help.

-- Dan