[Agda] yet another grinding reload

[Conor McBride]

Hi folks

Many apologies that I can't make it to AIM this time around,
but let me wish you all every success.

If you're stuck for a code sprint, you could always figure
out why the attached files behave quite so badly!

Let me tell you a bit about them.

PrimTypes defines a collection of primitive types, being 0, 1, 2,
Pi, Sigma, and the inductive and coinductive variants of
Petersson-Synek trees.

It's imported by Model which constructs an inductive-recursive
universe of the same, carefully split into prop-like and set-like
regions (much in the manner of Epigram 2). Coinductive relations
are like coinductive families of sets, but instead of having a
Hancock-Setzer state-indexed set of Commands, they have a
Disneyland predicate of vapid Cheerfulness, to be maintained,
whatever Response the world may deliver.

Next, ObsEq imports both and delivers the definition of
observational equality for this universe, targetting the
prop-like fragment. (I haven't rebuilt coercion yet, but I will.)
Equality for coinductive types is a coinductive relation, of course.

Last, Thm is my attempt to show that each coinductive process is
equal to its one-step unfolding. I abstracted out the recursive
"unfold" just in case it was too enthusiastic in doing so. You'll
see that the file has one shed to go---the coalgebra which
establishes the bisimulation. Loading the file and committing that
refinement takes a while: it's done in less than half a minute on
my pathetic-but-thin computer. However (you guessed it) loading
the completed proof just does not want to happen.

Probably I should tell it to have more stack: can anyone remind
me how to do that?

But it might also be worth trying to figure out what the reason
for the discrepancy is. I'm sure it's known that it's a problem,
but is it known what problem it is? As the perpetrator of
Epigram 1, I can hardly point a finger without three pointing
back. I do, however, wonder what can possibly be going on in
there...

Good luck!

Conor



-------------- next part --------------
A non-text attachment was scrubbed...
Name: PrimTypes.agda
Type: application/octet-stream
Size: 2132 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100322/c34a3546/PrimTypes.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Model.agda
Type: application/octet-stream
Size: 1522 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100322/c34a3546/Model.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ObsEq.agda
Type: application/octet-stream
Size: 2755 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100322/c34a3546/ObsEq.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Thm.agda
Type: application/octet-stream
Size: 2327 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100322/c34a3546/Thm.obj
-------------- next part --------------