[Agda] Re: Agda beats Coq (was: Termination proof in partiality monad)

[Dan Doel]

On Thursday 20 November 2008 7:05:24 am Edsko de Vries wrote:
> I don't know Agda very well, but there is some magic going on in fix-
> fac-ind! I tried to port your development to Coq, and most of it is
> easy, but I get stuck in that proof. I think Agda is doing something
> behind the scenes that is not obvious to me how to replicate in Coq.
> For the curious, I have attached my Coq development. I'd be very
> interested to see how this proof can be translated.

I think this has to do with your using the same type definitions as the ones in 
Capretta's paper. I'll expand on that a lot below, but I had problems 
replicating some proofs in that paper in Agda (the proof of divergence of 
never comes to mind first). Basically, I think Coq proofs using the rewrite 
tactic with unfold were problematic, and while inserting explicit unfolds may 
fix individual problems, a reworking of the approach seems to solve the 
systemic problem that explicit unfolds are a symptom of.

> Also, you cheated a little and removed the use of bind in the
> definition of faq ;-)

Yes, however, I just tried a definition with bind, and the proof is exactly the 
same. Note that neither proof makes use of map-D-↓ in the Convergence module. 
I thought I'd need it, but apparently I don't. So, similarly, I don't need 
>>=-↓ in the version with bind, and everything just works as-is somehow. :)

> (** (Incomplete) Coq translation of Dan Doel's proof of convergence of
> faq *)

Here's the thing: I don't know coq, but it looks like you haven't actually 
translated your proof types and such to the versions that actually allowed me 
to prove the theorem. So, it's somewhat unsurprising if using the definitions 
in Capretta's paper (for instance) isn't working, because it doesn't work in 
Agda, either. :)

The scheme that did yield a proof is based on mails from Anton Setzer, who I 
suspect would say that codata as found in Agda and Coq gives you poor 
intuition about how to work with coinductive data. Instead you want to think 
in terms of coalgebras. So, rather than:

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

Which looks like you have constructors, what you want is something more like:

  -- For any a:Set, D a is the terminal coalgebra where the observation is
  -- of type B -> a + B
  D : Set -> Set

  observe : {a : Set} -> D a -> a + D a

Importantly, a value of type D a is not either (now a) or (later a). The only 
operation on it is "observe" (which was the star operation in my code), which 
yields either a regular value, or another D a. Alternately, you could type 
observe like so:

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

  observe : {a : Set} -> D a -> D' a

Which is how "now" and "later" enter the picture; they're not constructors of 
D like they appear with codata, they're observations you can make of an opaque 
D a.

Now, one area this leads is that it no longer makes sense to write something 
like:

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

because "now" and "later" are not constructors for D a, and D as are just 
opaque, and the only equality you get is dx = dx. So, rather, you need to 
break up your convergence type into something that observes the value, and 
proofs for each observation:

  Converge : {a : Set} -> D a -> a -> Set
  Converge dx v with observe dx
  ... | now x    = x == v
  ... | later dx = ConvergeLater dx v

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

Of course, my == is named ConvergeNow. The other tricky part with this 
formalism is defining functions, where you essentially write things like (I'm 
not sure I totally grok this part of Setzer's mails):

  f : {a : Set} -> D a -> D a
  observe (f dx) = observe (expr-in-dx)

Where you're saying that observations on (f dx) are the observations on expr-
in-dx.

Now, the important point is that although this is not analogous to codata, we 
can mimic it with codata, and it works well, because being precise about the 
separation between coinductive values and observations thereof means that all 
the unfolding that needs to happen to make types check automatically happens 
because of the observations we need to make. As you can see, in my proofs 
above, I did just that. There are two sticky points. First, you need a codata 
definition for your opaque type, and need to give your observation function in 
terms of pattern matching on it:

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

  observe : {a : Set} -> D a -> a + D a
  observe (now a)    = inl a
  observe (later da) = inr da

(I hope that isn't too confusing; now and later are now part of the definition 
of the 'opaque' coinductive type, and the observations are now in terms of a 
standard sum type.) And instead of the funky coinductive function definitions 
above, we do the following:

  f : {a : Set} -> D a -> D a
  f dx with observe dx
  ... | inl x    ~ now (expr-in-x)
  ... | inr dx' ~ later (expr-in-dx')

So you make an observation, wrap it in the corresponding coconstructor for D, 
and work with the stuff the observation gave you. The proof types look roughly 
the same as the ones I gave above.

Now, I don't know how well all of this translates to Coq. However, Mr. 
Setzer's way of looking at things in terms of coalgebras and such seems to 
Just Work in a way that the straight-forward codata stuff in Agda (and Coq) 
don't (although it is a bit more verbose; perhaps someone will come up with a 
brilliant syntax for this stuff, though). It may be possible to stick in some 
unfolds in strategic places in codata-based proofs and have them work, but I 
have trouble figuring out where exactly to stick them.

In any case, hopefully that gives some insight into how my proofs are working.

Cheers,
-- Dan