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

[Wouter Swierstra]

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:

  data _==_ {A : Set} (x : A) : {b : Set} -> b -> Set where
    Refl : x == x

Now you can finish the proof as follows:

  decEqBool : (b1 : bool) -> (b2 : bool) -> Maybe (b1 == b2)
  decEqBool tt tt = Just Refl
  decEqBool ff ff = Just Refl
  decEqBool _ _ = Nothing

  fooeq : {b1 b2 : BOOL} -> (x1 : foo b1) -> (x2 : foo b2) -> Maybe  
(x1 == x2)
  fooeq (FOO b1) (FOO b2)   with decEqBool b1 b2
  fooeq (FOO b1) (FOO .b1)  | Just Refl = Just Refl
  fooeq (FOO b1) (FOO b2)   | Nothing = Nothing

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,

   Wouter