Agda类型检查和+的交换性/关联性 [英] Agda Type-Checking and Commutativity / Associativity of +

问题描述

由于 _ + _ < - code> Nat 的操作通常在第一个参数中递归定义， - 类型检查器知道 i + 0 == i 。但是，当我在固定大小的向量上编写函数时，我经常遇到这个问题。

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

  swap：{A：Set} {mn：Nat}  - > Vec A（n + m） - > Vec A（m + n）
  

将第一个 n


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



  swap 0 xs = xs 
 swap n（x：xs）= swap（n-1）（xs ++ [x]）
  
 
 
 
  swap：{A：Set} {mn：Nat}  - > Vec A（n + m） - > Vec A（m + n）
 swap {_} {_} {zero} xs = xs 
 swap {_} {_} {suc i}（x :: xs）= swap {_} {_} {i}（xs ++（x :: []））
  
检查器失败，并显示消息（与上面的 swap  -Definition）中的 {zero}  -case有关）：  
 
 
  .m！= .m +类型为Nat 
的零检查表达式xs的类型为Vec .A （.m + zero）
  
所以，我的问题：如何教Agda， 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）
  
然后我们可以通过 rewrite 关键字告诉Agda使用此证明：
  swap：{A：Set} {mn：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 
取：{A：Set} {m：Nat}  - > （n：Nat） - > Vec A（n + m） - > Vec A n 
  
（这两个都可以在没有任何定理证明的情况下定义），Agda会高兴地接受这个没有任何大惊小怪的定义： 
 
 
  swap：{A：Set} {mn：Nat}  - > Vec A（n + m） - > Vec A（m + n）
 swap {_} {_} {n} xs = drop n xs ++ take n xs 
  
 
Since the _+_-Operation for Nat is usually defined recursively in the first argument, its obviously non-trivial for the type-checker to know that i + 0 == i. However, I frequently run into this issue when I write functions on fixed-size Vectors.


One example: How can I define an Agda-function 
swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)
which puts the first n values at the end of the vector?

Since a simple solution in Haskell would be 
swap 0 xs     = xs
swap n (x:xs) = swap (n-1) (xs ++ [x])
I tried it analogously in Agda like this: 
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 :: []))
But the type checker fails with the message (which relates to the the {zero}-case in the above swap-Definition): 
.m != .m + zero of type Nat
when checking that the expression xs has type Vec .A (.m + zero)
So, my question: How to teach Agda, that m == m + zero? And how to write such a swap Function in Agda?
解决方案
Teaching Agda that m == m + zero isn't too hard. For example, using the standard type for equality proofs, we can write this proof:
rightIdentity : (n : Nat) -> n + 0 == n
rightIdentity zero = refl
rightIdentity (suc n) = cong suc (rightIdentity n)
We can then tell Agda to use this proof using the rewrite keyword:
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) = ?
However, providing the necessary proofs for the second equation is a lot more difficult. In general, it's a much better idea to try to make the structure of your computations match the structure of your types. That way, you can get away with a lot less theorem proving (or none in this case).

For example, assuming we have 
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
(both of which can be defined without any theorem proving), Agda will happily accept this definition without any fuss:
swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)
swap {_} {_} {n} xs = drop n xs ++ take n xs


                        
这篇关于Agda类型检查和+的交换性/关联性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！