Парное равенство на компонентах

Question

Я хотел бы определить функцию следующего типа

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

, но я немного растерялся с реализацией.

Я знаю, что могу написать

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

но, похоже, это не компилируется там, где мне нужно его использовать (это другой вопрос: в чем большая разница между двумя функциями?)

Answer 1

Первая реализация довольно проста.Как только вы разделите кортежи, чтобы получить pairEquality (a, b) (x, y) prf1 prf2 = ?t и осмотрите дыру, вы уже видите, что компилятор делает вывод, что prf1 : a = x, prf2: b = y, увы:

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

В pairEquality вы де-строить кортежи и в pairEquality' вы создаете кортежи.Последний подход, как правило, лучше, и я думаю, что вы можете что-то изменить в своей функции вызывающей стороны, чтобы ее можно было использовать.

Answer 2

Я действительно обнаружил, что могу определить pairEquality в терминах pairEquality' как

pairEquality :
     (a, b : (obj1, obj2))
  -> (fst a) = (fst b)
  -> (snd a) = (snd b)
  -> a = b
pairEquality (a1, a2) (b1, b2) = pairEquality' {a1} {a2} {b1} {b2}