假设我有以下idris源代码：
module Source
import Data.Vect
--in order to avoid compiler confusion between Prelude.List.(++), Prelude.String.(++) and Data.Vect.(++)
infixl 0 +++
(+++) : Vect n a -> Vect m a -> Vect (n+m) a
v +++ w = v ++ w
--NB: further down in the question I'll assume this definition isn't needed because the compiler
-- will have enough context to disambiguate between these and figure out that Data.Vect.(++)
-- is the "correct" one to use.
lemma : reverse (n :: ns) +++ (n :: ns) = reverse ns +++ (n :: n :: ns)
lemma {ns = []} = Refl
lemma {ns = n' :: ns} = ?lemma_rhs
如图所示，lemma的基本情况为Refl。但是我似乎找不到找到证明归纳的方法：repl“ just”吐出以下内容
*source> :t lemma_rhs
phTy : Type
n1 : phTy
len : Nat
ns : Vect len phTy
n : phTy
-----------------------------------------
lemma_rhs : Data.Vect.reverse, go phTy
(S (S len))
(n :: n1 :: ns)
[n1, n]
ns ++
n :: n1 :: ns =
Data.Vect.reverse, go phTy (S len) (n1 :: ns) [n1] ns ++
n :: n :: n1 :: ns
我了解phTy代表“幻像类型”，即我正在考虑的向量的隐式类型。我也理解go是在库函数where的定义的reverse子句中定义的函数的名称。
问题
我如何继续证明？我的归纳策略是否合理？有更好的吗？
Context
这是在我的一个玩具项目中出现的，我尝试定义任意张量；特别是，这似乎是定义“全指数收缩”所必需的。我将对此进行详细说明：
我定义张量的方式大致等同于
data Tensor : (rank : Nat) -> (shape : Vector rank Nat) -> Type where
Scalar : a -> Tensor Z [] a
Vector : Vect n (Tensor rank shape a) -> Tensor (S rank) (n :: shape) a
对其余的源代码进行了处理（因为它不相关，并且到目前为止，它已经很长而且没有兴趣了，所以我能够定义以下函数）
contractIndex : Num a =>
Tensor (r1 + (2 + r2)) (s1 ++ (n :: n :: s2)) a ->
Tensor (r1 + r2) (s1 ++ s2) a
tensorProduct : Num a =>
Tensor r1 s1 a ->
Tensor r2 s2 a ->
Tensor (r1 + r2) (s1 ++ s2) a
contractProduct : Num a =>
Tensor (S r1) s1 a ->
Tensor (S r2) ((last s1) :: s2) a ->
Tensor (r1 + r2) ((take r1 s1) ++ s2) a
并且我正在研究另外一个
fullIndexContraction : Num a =>
Tensor r (reverse ns) a ->
Tensor r ns a ->
Tensor 0 [] a
fullIndexContraction {r = Z} {ns = []} t s = t * s
fullIndexContraction {r = S r} {ns = n :: ns} t s = ?rhs
应该“尽可能地重复contractProduct次（即r次）”；同样，可以将其定义为由尽可能多的tensorProduct组成的contractIndex（同样，该量应为r）。
我将所有这些信息都包括在内，因为在不证明上述lemma的情况下解决该问题可能会更容易：如果是这种情况，我也将感到非常满意。我只是以为上面的“较短”版本可能会更容易处理，因为我敢肯定自己将自己找出缺失的部分。
我正在使用的idris版本是1.3.2-git:PRE（这是从命令行调用时repl所说的内容。
Edit：xash的答案几乎涵盖了所有内容，并且我能够编写以下函数
nreverse_id : (k : Nat) -> nreverse k = k
contractAllIndices : Num a =>
Tensor (nreverse k + k) (reverse ns ++ ns) a ->
Tensor Z [] a
contractAllProduct : Num a =>
Tensor (nreverse k) (reverse ns) a ->
Tensor k ns a ->
Tensor Z []
我还写了reverse的“花哨”版本，我们称它为fancy_reverse，它会自动将其结果重写为nreverse k = k。所以我试图编写一个签名中没有nreverse的函数，例如
fancy_reverse : Vect n a -> Vect n a
fancy_reverse {n} xs =
rewrite sym $ nreverse_id n in
reverse xs
contract : Num a =>
{auto eql : fancy_reverse ns1 = ns2} ->
Tensor k ns1 a ->
Tensor k ns2 a ->
Tensor Z [] a
contract {eql} {k} {ns1} {ns2} t s =
flip contractAllProduct s $
rewrite sym $ nreverse_id k in
?rhs
现在，rhs的推断类型为Tensor (nreverse k) (reverse ns2)，并且在范围上我有k = nreverse k的重写规则，但是我似乎无法将我的头放在如何重写隐式eql证明上，以使这种类型的检查：我做错了吗？
前奏Data.Vect.reverse很难理解，因为AFAIK go辅助函数不会在类型检查器中解析。通常的方法是为自己定义一个更轻松的reverse，它在类型级别上不需要rewrite。 Like here for example：
%hide Data.Vect.reverse
nreverse : Nat -> Nat
nreverse Z = Z
nreverse (S n) = nreverse n + 1
reverse : Vect n a -> Vect (nreverse n) a
reverse [] = []
reverse (x :: xs) = reverse xs ++ [x]
lemma : {xs : Vect n a} -> reverse (x :: xs) = reverse xs ++ [x]
lemma = Refl
如您所见，这个定义很简单，无需进一步的工作即可解决这个等效引理。因此，您可以像在此示例中一样，只匹配reverse ns中的fullIndexContraction：
data Foo : Vect n Nat -> Type where
MkFoo : (x : Vect n Nat) -> Foo x
foo : Foo a -> Foo (reverse a) -> Nat
foo (MkFoo []) (MkFoo []) = Z
foo (MkFoo $ x::xs) (MkFoo $ reverse xs ++ [x]) =
x + foo (MkFoo xs) (MkFoo $ reverse xs)
[您的评论：首先，有时必须使用len = nreverse len，但是如果您在类型级别上具有rewrite（通过通常的n + 1 = 1 + n恶作剧），您将遇到相同的问题（即使没有更复杂的证明，但这只是一个猜测。）
vectAppendAssociative实际上足够：
lemma2 : Main.reverse (n :: ns1) ++ ns2 = Main.reverse ns1 ++ (n :: ns2)
lemma2 {n} {ns1} {ns2} = sym $ vectAppendAssociative (reverse ns1) [n] ns2