Search code examples
equalityidris

Pair equality on components

I would like to define a function of the following type

pairEquality :
     (a, b : (obj1, obj2))
  -> (fst a) = (fst b)
  -> (snd a) = (snd b)
  -> a = b

but I am a bit at loss with the implementation.

I know I can write

pairEquality' :
     a1 = b1
  -> a2 = b2
  -> (a1, a2) = (b1, b2)

but that doesn't seem to compile where I need to use it (that's another question: what's the big difference between the two functions?)

Solution

  • The first implementation is pretty straight-forward. Once you split the tuples to get pairEquality (a, b) (x, y) prf1 prf2 = ?t and inspect the the hole, you already see, that the compiler infers that prf1 : a = x, prf2: b = y, alas:

    pairEquality :
     (a, b : (obj1, obj2))
  -> (fst a) = (fst b)
  -> (snd a) = (snd b)
  -> a = b
pairEquality (x, y) (x, y) Refl Refl = Refl

    In pairEquality you de-construct the tuples and in pairEquality' you construct the tuples. Latter is usually a better approach, and I guess you can change something in your caller function so it can be used.