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
