代码之家 › 专栏 › 技术社区 › Lodewijk Bogaards

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

idris

2

Lodewijk Bogaards · 技术社区 · 8 年前

我正在学习IDRIS,我有一个小小的难题。

我正在做IDRIS类型驱动开发书籍第8.3章的练习2。关键是要实现 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 只有当我不说出证据的名字时才有效?

谢谢您!

1 回复 | 直到 8 年前

1

2

xash 8 年前

重要的区别在于 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) . 另一方面,在你的版本中, ?孔 是 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 ,idris可以统一 x 和 y ,因为 雷弗 是的构造函数 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