[Agda] Agda goes coinductive

[Nils Anders Danielsson]

On Sat, Jun 7, 2008 at 7:38 AM, Dan Doel <dan.doel at gmail.com> wrote:
>
> 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

This is not strictly necessary. If you define your predicates in terms
of destructors (basically Anton's case) instead of indexing on
constructor applications then you can avoid this use of unfolding
functions:

  module Partial where

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

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

  destruct : forall {a} -> D a -> D' a
  destruct (now v)    = now v
  destruct (later dv) = later dv

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

  codata Diverge {a : Set} : D a -> Set where
    diverge : (x : D a) {x' : D a} ->
              destruct x == later x' ->
              Diverge x' -> Diverge x -- <-- Just a simple variable.

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

  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)

  map-diverge : {a b : Set} {x : D a} (f : a -> b) ->
                Diverge x -> Diverge (mapD f x)
  map-diverge f (diverge (now v)   ()   _)
  map-diverge f (diverge (later x) refl d) ~
    diverge (mapD f (later x)) refl (map-diverge f d)

However, I am not really fond of this programming style. The defining
feature of Agda is dependent pattern matching over inductive families,
and using destructors and explicit equalities feels like a step
backwards. I hope that we can find an elegant system which allows
dependent pattern matching over coinductive families.

-- 
/NAD