Как доказать ((x :: xs) = (y :: ys)) с учетом (x = y) & (xs = ys)

Я изучаю Идрис, и у меня есть небольшой вопрос для новичков.

Я выполняю упражнение 2 из главы 8.3 книги по разработке с использованием Idris. Дело в том, чтобы реализовать DecEq для вашего собственного Vector. Вот как далеко я зашел:

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 elem
  (::) : elem -> Vect n elem -> Vect (S n) elem

headUnequal : {xs : Vect n a} -> {ys : Vect n a} -> (contra : (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl

tailsUnequal : {xs : Vect n a} -> {ys : Vect n a} -> (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailsUnequal contra Refl = contra Refl

headAndTailEq : {xs : Vect n a} -> {ys : Vect n a} -> (xEqY : x = y) -> (xsEqYs : xs = ys) -> ((x :: xs) = (y :: ys))
headAndTailEq xEqY xsEqYs = ?hole

implementation DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes xEqY => case decEq xs ys of
        No xsNeqYs => No $ tailsUnequal xsNeqYs
        Yes xsEqYs => Yes $ headAndTailEq xEqY xsEqYs

Как залить ?hole?

Я видел решение на https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter8/Exercises/ex_8_3.idr. Обладая этими знаниями, я могу заставить свое решение работать:

implementation DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes Refl => case decEq xs ys of
        No xsNeqYs => No $ tailsUnequal xsNeqYs
        Yes Refl => Yes Refl

Но, честно говоря, почему это работает? Почему окончательный Yes Refl работает только в том случае, если я не назову доказательства?

Спасибо!


idris
person Lodewijk Bogaards    schedule 29.07.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Важное различие заключается в сопоставлении значений в case-блоках, а не в именовании доказательств. Если вы осмотрите первый case с

  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes Refl => ?hole

вы увидите, что ?hole требуется только Dec (x :: xs = x :: ys). С другой стороны, в вашей версии ?hole это Dec (x :: xs = y :: ys):

  decEq (x :: xs) (y :: ys) =
    case decEq x y of
      No xNeqY => No $ headUnequal xNeqY
      Yes xEqY => ?hole

Вот xEqY : x = y. Идрис не имеет специального понимания =, поэтому это просто означает, что существует значение xEqY, имеющее тип x = y (и дальнейшая проверка того, что xEqY может быть, не проводится). Если вы сопоставите Refl, Идрис может объединить x и y, потому что Refl является конструктором для x = x - значения одинаковы. Таким образом, вы получите больше информации с сопоставлением с образцом; вместо непрозрачного имени переменной вы получите конкретное значение. Практическое правило: всегда сопоставляйте шаблон, пока в правой части не будет достаточно информации.

Благодаря этому ваше доказательство также может быть легко реализовано:

headAndTailEq : {xs : Vect n a} -> {ys : Vect n a} -> (xEqY : x = y) -> (xsEqYs : xs = ys) -> ((x :: xs) = (y :: ys))
headAndTailEq Refl Refl = Refl
person xash    schedule 29.07.2018
comment
Большое спасибо! Я предположил, что, поскольку у = только один конструктор, эффект будет таким же. - person Lodewijk Bogaards; 29.07.2018
comment
Наличие только одного конструктора не гарантирует, что вы действительно сможете создать значение. 3 = 5 - допустимый тип, но вы не можете создать для него значение с помощью Refl. - person Markus; 01.08.2018
comment
Но в Yes xEqY уже есть значение, поэтому оно должно быть Yes Refl. Так что я предполагаю, что это можно было сделать вывод, хотя я не думал обо всех последствиях. - person xash; 01.08.2018