[Agda] Agda goes coinductive

[Dan Doel]

On Saturday 07 June 2008, Nils Anders Danielsson wrote:
> 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:

Well, this is the sort of thing I was looking for, I suppose. I was able to 
rewrite things in this way so that I can complete proofs *and* keep the 
termination/productivity checker happy. For instance, here's the mapD 
convergence proof:

---- snip ----

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

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-now : {a b : Set}
          {v : a}
          (x : D a)
          (f : a -> b) ->
          destruct x == now v ->
          destruct (mapD f x) == now (f v)
map-now {a} {b} {v} (now .v) f refl = refl 
map-now (later dv) f ()

map-later : {a b : Set}
            (v : a)
            (x  : D a)
            {dx : D a}
            (f : a -> b) ->
            destruct x == later dx ->
            destruct (mapD f x) == later (mapD f dx)
map-later v (now v')    f ()
map-later v (later dx) f refl = refl 

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} (converge-now .v eq) = converge-now (f v) 
(map-now x f eq )
map-converge {a} {b} {x} {v} {f} (converge-later eq pfc)
             = converge-later (map-later v x f eq) (map-converge pfc)

---- snip ----

The never divergence proof failed the productivity checker in my scheme, but 
works fine in this one:

---- snip ----

diverge-never : {a : Set} -> Diverge (never {a})
diverge-never ~ diverge never refl diverge-never

---- snip ----

And this theorem failed the termination checker, but works under this scheme:

---- snip ----

race : {a : Set} (x y : D a) -> D a
race (now v)    y           ~ now v
race (later dv) (now v)     ~ now v
race (later dv) (later dv') ~ later (race dv dv')

data _||_ (P Q : Set) : Set where
  pfl : P -> P || Q
  pfr : Q -> P || Q

race-converge : {a : Set} {x y : D a} {v : a} ->
                Converge (race x y) v -> Converge x v || Converge y v
race-converge {a} {now .v} {y} {v} (converge-now .v refl)
  = pfl (converge-now v refl) 
race-converge {a} {later dv} {now .v} {v} (converge-now .v refl)
  = pfr (converge-now v refl)
race-converge {a} {later dv} {later dv'} {v} (converge-now .v ())
race-converge {a} {now v} (converge-later () pfc)
race-converge {a} {later dv} {now v} (converge-later () pfc)
race-converge {a} {later dv} {later dv'} (converge-later refl pfc) with 
race-converge pfc
...           | pfl pfx = pfl (converge-later refl pfx)
...           | pfr pfy = pfr (converge-later refl pfy)

> 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.

Yeah, I think I agree. As a visible side effect, there's an explosion of cases 
in proofs with the equalities. That race-convergence proof has 3 cases (+ 2 
with cases) in my original, but there are 6 (+2) in the above, because of the 
required matches with the absurd pattern. The equality shuffling in 
map-converge isn't a lot of fun either (maybe I could rewrite it to be all 
one function, but I suspect there'd be a similar introduction of lots of 
absurd patterns).

In the inductive case, Agda manages to get a lot done without both tedium and 
extensive automation. Hopefully the same will be true in the coinductive case 
(as an aside, when I started getting frustrated translating the proofs in the 
paper into Agda, I went and looked at the Coq code referenced in the paper; 
it was pretty much no help to me. Perhaps that's just because I don't know 
Coq, but it also seemed that most of the proofs were lists of stuff for the 
proof assistant to do automatically, which seems to me less illuminating as 
to what's actually happening in the proof than when I write such things in 
Agda).

Cheers.

-- Dan Doel