[Agda] Tentative guidelines for working with coinductive types

[Dan Doel]

On Wednesday 14 January 2009 3:36:17 pm Noam Zeilberger wrote:
> This is a nice design pattern.  I was having trouble getting Agda to
> accept some proofs about an equality relation ≡ for a little
> coinductively defined language, and following these principles almost
> all of the proofs went through easily.  The remaining problem seems to
> be the weakness of Agda's definitional equality.  For example, I
> define a cyclic term Ω in the syntax of the language, and then want to
> prove that Ω ≡ Ω.  Well, I can prove reflexivity in general by
> recursion on terms, but I'm having trouble proving Ω ≡ Ω directly.
> (If this doesn't make any sense, I can try to come up with a small
> example.)

The thing is, equality on coinductive types is extensional. For a given type, 
you can define a type of bisimulations for that type, which was given 
previously for Colists as _≈_. You can then add a rule for extensional 
equality that looks like:

    ext-≈ : {A : Set} {xs ys : Colist A} -> xs ≈ ys -> xs ≡ ys

But, there's no way to prove xs ≡ ys through the definitional equality 
(excepting things like force from the original message, possibly), because 
Agda's equality is intensional (which has its reasons; type theories with 
extensional equality have traditionally been undecidable, which can be 
undesirable, although Observational Type Theory promises a decidable 
extensional theory).

Similarly, there's no way to prove via Agda's definitional equality the 
following rule for extensional equality:

    ext-→ : {A B : Set} {f g : A -> B} -> (forall x -> f x ≡ g x) -> f ≡ g

Despite that being a sensible rule. That's just the nature of equality in a 
type theory like Agda, although it bites most severely in the case of 
coinductive types, where you can't feasibly prove much of anything equal (as 
in the ≡ type) without adding postulates.

So, the short answer is that you shouldn't be trying to prove Ω ≡ Ω, you 
should be trying to demonstrate that the two are bisimilar, and adding an 
axiom (I suppose) if you really need the former.

-- Dan