[Agda] Agda goes coinductive

[Dan Doel]

On Friday 06 June 2008, Dan Doel wrote:
> 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.

In case anyone's interested in this, after much working, I managed to work out 
a strategy that seems to be working. I hope it's all right if I reproduce a 
little code, as I rewrote things into a small example from the main file I'm 
working in, and things are a bit different:

---- snip ----

module Partial where

codata D (a : Set) : Set where
  now   : (v : a)    -> D a
  later : (dv : D a) -> D a

data Converge {a : Set} : D a -> a -> Set where
  converge-now   : (v : a) -> Converge (now v) v
  converge-later : {x : D a} {v : a} -> Converge x v -> Converge (later x) v

codata Diverge {a : Set} : D a -> Set where
  diverge : (x : D a) -> Diverge x -> Diverge (later x)

unfold : {a : Set} -> D a -> D a
unfold (now x)    = now x
unfold (later dx) = later dx

never : {a : Set} ->  D a
never ~ later never

data _==_ {a : Set} (x : a) : a -> Set where
  refl : x == x

==-unfold : {a : Set} (x : D a) -> unfold x == x
==-unfold (now v)    = refl 
==-unfold (later dv) = refl

==-resp : {a : Set}{x y : a} (f : a -> Set) -> x == y -> f x -> f y
==-resp f refl fx = fx

mapD : {a b : Set} -> (a -> b) -> D a -> D b
mapD f (now v)    ~ now (f v)
mapD f (later dv) ~ later (mapD f dv)

---- snip ----

so far nothing too special. Now to prove the theorem about map:

---- snip ----

mutual
  map-converge₁ : {a b : Set}{x : D a}{v : a}{f : a -> b} ->
                  Converge x v -> Converge (unfold (mapD f x)) (f v)
  map-converge₁ {a}{b}{.(now v)}{v}{f}(converge-now .v) = converge-now (f v)
  map-converge₁ (converge-later pf) = converge-later (map-converge pf)

  map-converge : {a b : Set}{x : D a}{v : a}{f : a -> b} ->
                 Converge x v -> Converge (mapD f x) (f v)
  map-converge {a}{b}{x}{v}{f} pf = ==-resp
                                      (\t -> Converge t (f v))
                                      (==-unfold (mapD f x))
                                      (map-converge₁ pf)

---- snip ----

So, to prove a theorem, you prove a theorem about an expression containing 
unfold, and use the fact that 'unfold x == x' to turn it into the theorem you 
actually want (I had tried this before, and thought it didn't work, but I 
guess I was doing something wrong).

This approach works for the divergence of never as well:

---- snip ----

mutual
  diverge-never₁ : {a : Set} -> Diverge (unfold (never {a}))
  diverge-never₁ ~ diverge never diverge-never

  diverge-never : {a : Set} -> Diverge (never {a})
  diverge-never ~ ==-resp Diverge (==-unfold never) diverge-never₁

---- snip ----

However, this does not pass the productivity checker, so things aren't 
necessarily hunky-dory. Hopefully going along this route should allow me to 
translate most of the proofs from General Recursion via Coinductive Types, 
though (I've a lot of it translated, but struggled near the end, as most 
proofs there run into this).

Thanks for your time.

-- Dan