[Agda] Tentative guidelines for working with coinductive types

[Nils Anders Danielsson]

On 2009-01-15 01:21, Dan Doel wrote:
> On Wednesday 14 January 2009 4:51:09 pm Noam Zeilberger wrote:
>
>>   infeq : inf ≈ inf
>>   infeq = seq infeq'
>>     where infeq' ~ ♯ infeq
>>
>> but this doesn't typecheck, because "(ss .T._.inf') != (♭ (♯ inf))
>> of type CoNat".
>
> precisely this works fine for me.

Yes, this works, but you cannot prove that inf is equal to (what looks
like) its own unfolding by using the obvious corecursive proof:

   infeq : inf ≈ ss (♯ inf)
   infeq = seq infeq'
     where infeq' ~ ♯ infeq

   ⇒ ♯ ss .T._.inf' != .T._.inf'

A simple workaround is to replace the corecursive call with reflexivity:

   infeq : inf ≈ ss (♯ inf)
   infeq = seq infeq'
     where infeq' ~ ♯ refl inf

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.