Ответ 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