实现“平等的Vect”与DecEq

我试图执行以下操作：实现“平等的Vect”与DecEq

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

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

来源

2017-04-04 Kevin Meredith

您应该删除'vectEqual'的最后两个子句，因为它们不会出现，因为两个矢量具有相同的长度。 – Lee

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

Just (Yes prf) => vectEqual xxs yys

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

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)

请注意，此函数的返回类型有点奇怪，因为您使用的是Nothing enco de Dec已经提供使用No构造函数的故障情况，因此您永远不会返回Just (No _)。

来源

2017-04-04 13:23:59 Lee

实现“平等的Vect”与DecEq

回答

相关问题