如何证明 ((x :: xs) = (y :: ys)) 给定 (x = y) & (xs = ys)

Question

我正在学习 Idris，但我有一些菜鸟问题。

我正在使用 Idris 进行类型驱动开发一书第 8.3 章的练习 2。重点是为您自己的 Vector 实施 DecEq。这是我的进展：

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 只有在我不命名证明时才有效？

谢谢！

Answer 1

重要的区别是 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。 Idris 对 = 没有特别的理解，所以这只是意味着，有一个值 xEqY 具有 x = y 类型（并且没有进一步检查 xEqY 是什么可能）。如果匹配 Refl，Idris 可以统一 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

如何证明 ((x :: xs) = (y :: ys)) 给定 (x = y) & (xs = ys)

How to prove ((x :: xs) = (y :: ys)) given (x = y) & (xs = ys)

idris