我想在agda中写一个反向向量函数，但遇到了以下的障碍。
Goal: Vec Nat (suc n)
Have: Vec Nat (n +N 1)
如果我没理解错的话，这些值并不是绝对相等的。 这里是反向函数。
vReverse : {X : Set} {n : Nat} → Vec X n → Vec X n
vReverse [] = []
vReverse (x ,- x₁) = {!(vReverse x₁) +V (x ,- [])!}
如果possibilbe，我如何克服这个问题，而不重构代码。 如果有必要重构，一般来说，如何才能先期避免这些陷阱？ 下面是剩下的代码。
data Nat : Set where
zero : Nat
suc : Nat -> Nat -- recursive data type
{-# BUILTIN NATURAL Nat #-}
_+N_ : Nat -> Nat -> Nat
zero +N y = y
suc x +N y = suc (x +N y) -- there are other choices
data Vec (X : Set) : Nat -> Set where -- like lists, but length-indexed
[] : Vec X zero
_,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_ -- the "cons" operator associates to the right
_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V xs = xs
(x ,- xs) +V [] = x ,- xs +V []
(x ,- xs) +V x₁ ,- ys = x ,- xs +V x₁ ,- ys
我们的想法是，你可以将一个类型为 P x 类型的元素。P y 只要你能证明 x ≡ y. 让我一步步引导你完成这个过程。这是你提供的基本代码，我没有按照你的要求进行重构。
data Nat : Set where
zero : Nat
suc : Nat -> Nat -- recursive data type
{-# BUILTIN NATURAL Nat #-}
_+N_ : Nat -> Nat -> Nat
zero +N y = y
suc x +N y = suc (x +N y) -- there are other choices
infixl 5 _+N_
data Vec (X : Set) : Nat -> Set where -- like lists, but length-indexed
[] : Vec X zero
_,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_ -- the "cons" operator associates to the right
但是，你的连接函数是不正确的，它没有终止，所以这里是更正的版本。
_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V vs = vs
(x ,- xs) +V vs = x ,- (xs +V vs)
为什么我们在这个函数中不需要做任何替换，是因为 suc n + m 在定义上等于 suc (n + m).
既然你已经定义了你自己的本体和你自己的加法，我假设你想自己重新定义一切。根据这个假设，你需要定义命题平等，具体做法如下。
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
infix 1 _≡_
根据这个定义，我们可以定义这个答案前言中提到的替换， 以及你问题的评论中提到的替换。
subst : ∀ {a b} {A : Set a} {x y : A} (P : A → Set b) → x ≡ y → P x → P y
subst _ refl p = p
在你的逆向函数中，问题在于： n + 1 在定义上不等于 suc n. 这就是为什么我们需要一个属性来建立这个事实，然后我们可以将其反馈给我们的替换机制。这个证明需要我们定义的命题平等的一致性，如下所示。
cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong _ refl = refl
n+1≡sn : ∀ {n} → n +N 1 ≡ suc n
n+1≡sn {zero} = refl
n+1≡sn {suc _} = cong suc n+1≡sn
我们现在有了所有必要的元素来写你的... vReverse 函数。
vReverse : ∀ {X n} → Vec X n → Vec X n
vReverse [] = []
vReverse (x ,- x₁) = subst (Vec _) n+1≡sn ((vReverse x₁) +V (x ,- []))
更进一步，你可以用同样的方法来建立通常的反向函数，这样更有效率（线性复杂度）。我冒昧的为你做了这个，因为它显示了更多的例子来使用 subst.
n+sm≡sn+m : ∀ {n m} → n +N suc m ≡ suc (n +N m)
n+sm≡sn+m {zero} = refl
n+sm≡sn+m {suc _} = cong suc n+sm≡sn+m
reverse-better-aux : ∀ {X n m} → Vec X n → Vec X m → Vec X (n +N m)
reverse-better-aux [] v₂ = v₂
reverse-better-aux (x ,- v₁) v₂ = subst (Vec _) n+sm≡sn+m (reverse-better-aux v₁ (x ,- v₂))
n+0≡n : ∀ {n} → n +N 0 ≡ n
n+0≡n {zero} = refl
n+0≡n {suc _} = cong suc n+0≡n
reverse-better : ∀ {X n} → Vec X n → Vec X n
reverse-better v = subst (Vec _) n+0≡n (reverse-better-aux v [])