Agda Type-Checking и Commutativity/Associativity of +

Так как _+_ -Operation для Nat обычно определяется рекурсивно в первом аргументе, его очевидно нетривиально для проверки типа, чтобы знать, что i + 0 == i. Тем не менее, я часто сталкиваюсь с этой проблемой при записи функций на Vectors с фиксированным размером.

Один пример: как определить функцию 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} -case в приведенном выше swap -Definition):

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

Итак, мой вопрос: как научить Агда, что m == m + zero? И как написать такую функцию swap в Agda?

Ответ 1

Преподавание Агда, что 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

(оба из которых могут быть определены без доказательства теоремы), Агда с радостью примет это определение без всякой суеты:

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