[Agda] basic question about induction/recursion & pattern-matching

[Ulf Norell]

On Tue, Sep 9, 2008 at 8:06 PM, Wouter Swierstra <wss at cs.nott.ac.uk> wrote:

> Hi Noam,
>
> I'm not an expert, but I imagine it's quite hard to prove fooeq with the
> standard definition of equality. I think this is where you really need the
> heterogeneous definition:
>
> I suspect this is the best you can do. I'm sure someone else more qualified
> than myself (Ulf? Conor?) can say plenty more on the subject. Hope this
> helps,
>

I'm not sure how to measure which is the best way to do this, but here's
another solution which doesn't resort to heterogenous equality. :-)

Observe that while the pattern FOO b doesn't make sense for the second
argument, everything would work if you where allowed to match on the b as
well. Unfortunately Agda require all the case splits leading up to a pattern
to make sense. The answer, naturally, is a view:

 data fooView : {B : BOOL} -> foo B -> Set where
   FOOtt : fooView (FOO tt)
   FOOff : fooView (FOO ff)

 view : {B : BOOL}(x : foo B) -> fooView x
 view (FOO tt) = FOOtt
 view (FOO ff) = FOOff

The fooView allows you to pattern match on the a foo B as being either FOO
tt or FOO ff, which is exactly what we need for the equality function:

 fooeq : {B : BOOL} -> (x1 x2 : foo B) -> Maybe (x1 ≡ x2)
 fooeq x1 x2 with view x1 | view x2
 fooeq .(FOO tt) .(FOO tt) | FOOtt | FOOtt = just refl
 fooeq .(FOO ff) .(FOO ff) | FOOff | FOOff = just refl

The coverage checker happily accepts that the off diagonal cases cannot
happen.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080909/38b9b9a1/attachment.html