用 DecEq 实现 'equal Vect'

Question

我尝试执行以下操作：

headEqual : DecEq a => (x : a) -> (y : a) -> Maybe (Dec (x = y))
headEqual x y = case decEq x y of
                  Yes Refl  => Just (Yes Refl)
                  No contra => Nothing

vectEqual : DecEq a => (xs : Vect n a) -> (ys : Vect n a) -> Maybe (Dec (xs = ys))
vectEqual []         []         = Just (Yes Refl)
vectEqual (x :: xxs) (y :: yys) = case headEqual x y of
                                  Just (Yes prf) => vectEqual xxs yys
                                  No contra      => Nothing
vectEqual (x :: xxs) []         = Nothing
vectEqual []         (y :: yys) = Nothing

但是编译失败：

*section3> :r
Type checking ./section3.idr
section3.idr:45:63-66:
When checking right hand side of Main.case block in vectEqual at section3.idr:44:40 with expected type
        Maybe (Dec (x :: xxs = y :: yys))

When checking argument xs to Main.vectEqual:
        Unifying len and S len would lead to infinite value
Holes: Main.y, Main.vectEqual

我不明白这个编译时错误。有人可以解释一下吗？

Answer 1

对于非空情况，您需要两个证明 - 一个证明头部相等，一个证明尾部相等。然后，您需要将这些证明合并为一个输入向量。在：

Just (Yes prf) => vectEqual xxs yys

当您需要整个列表的证明时，您正在尝试 return 尾部的证明。您需要检查递归调用的结果以构建证明，例如

vectEqual : DecEq a => (xs : Vect n a) -> (ys : Vect n a) -> Maybe (Dec (xs = ys))
vectEqual [] [] = Just (Yes Refl)
vectEqual (x :: xs) (y :: ys) = case decEq x y of
  Yes hd_prf => case vectEqual xs ys of
    Just (Yes tl_prf) => ?combine_proofs
    _ => Nothing
  No contra => Nothing

如果您在 repl 中加载上述定义，您将看到 hd_prf 和 tl_prf 的类型：

hd_prf : x = y
tl_prf : xs = ys

你可以使用rewrite构造(x :: xs) = (y :: ys)

所需的证明

Just (Yes tl_prf) => rewrite hd_prf in rewrite tl_prf in Just (Yes Refl)

请注意，此函数的 return 类型有点奇怪，因为您使用 Nothing 来编码 Dec 已经使用 No 构造函数提供的失败案例, 所以你永远不会 return Just (No _).

用 DecEq 实现 'equal Vect'

Implementing 'equal Vect' with DecEq

equality

idris