+的检查和交换性/关联性

由于Nat的_+_ -Operation通常是在第一个参数中递归定义的，因此它对于知道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 :: []))

但类型检查器会失败，并显示消息（与上面的swap的{zero} -case相关的定义）：

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

所以，我的问题：如何教阿格达，那m == m + zero ？ 以及如何在Agda中编写这样的swap函数？

---

教Agda， m == m + zero不是太难。 例如，使用标准类型进行相等证明，我们可以写出这个证明：

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

然后，我们可以告诉Agda使用rewrite关键字使用此证明：

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

链接地址: http://www.djcxy.com/p/43345.html

上一篇: Checking and Commutativity / Associativity of +

下一篇: What is the combinatory logic equivalent of intuitionistic type theory?