haskell - Agda 类型检查和交换性/+ 的关联性

Question

由于_+_ -Nat 的操作通常在第一个参数中以递归方式定义，对于类型检查器来说，知道 i + 0 == i 显然不是微不足道的。 .但是，当我在固定大小的向量上编写函数时，我经常遇到这个问题。

一个例子:我如何定义一个 Agda 函数

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)

其中第一个 n向量末尾的值？

由于 Haskell 中的一个简单解决方案是

swap 0 xs     = xs
swap n (x:xs) = swap (n-1) (xs ++ [x])

我在 Agda 中类似地尝试过，如下所示:

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {_} {zero} xs          = xs 
swap {_} {_} {suc i} (x :: xs)  = swap {_} {_} {i} (xs ++ (x :: []))

但是类型检查器失败并显示消息(与上述 {zero} -Definition 中的 swap -case 相关):

.m != .m + zero of type Nat
when checking that the expression xs has type Vec .A (.m + zero)

所以，我的问题是:如何教 Agda，m == m + zero ?以及如何写这样的swap在 Agda 中的功能？

Answer 1

教 Agda m == m + zero不是太难。例如，使用等式证明的标准类型，我们可以写出这样的证明:

rightIdentity : (n : Nat) -> n + 0 == n
rightIdentity zero = refl
rightIdentity (suc n) = cong suc (rightIdentity n)

然后我们可以使用 rewrite 告诉 Agda 使用这个证明。关键词:

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {m} {zero} xs rewrite rightIdentity m = xs 
swap {_} {_} {suc i} (x :: xs) = ?

然而，为第二个等式提供必要的证明要困难得多。一般来说，尝试 是一个更好的主意。使您的计算结构与您的类型结构匹配 .这样，您就可以少做定理证明(或者在这种情况下没有)。

例如，假设我们有

drop : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A m
take : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A n

(这两者都可以在没有任何定理证明的情况下定义)，Agda 很乐意接受这个定义，而不用大惊小怪:

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)
swap {_} {_} {n} xs = drop n xs ++ take n xs