Agda类型检查和+的交换/相关性

Question

由于_+_-Operation for 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}与上面的swap-Definition 中的-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