Idris：关于向量连接的证明

Question

假设我有以下 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 代表 "phantom type"，我正在考虑的向量的隐式类型。我也明白go是库函数reverse定义的where子句中定义的函数名。

问题

How can I continue the proof? Is my inductive strategy sound? Is there a better one?

上下文

这出现在我的一个玩具项目中，我试图在其中定义任意张量；具体来说，这似乎是定义 "full index contraction" 所必需的。我会详细说明一下：

我定义张量的方式大致等同于

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

应该"iterate contractProduct as much as possible (that is, r times)"；等效地，可以将其定义为 tensorProduct 由尽可能多的 contractIndex 组成（同样，该数量应该是 r）。

我把所有这些都包括在内是因为不证明上面的 lemma 就可以更容易地解决这个问题：如果是这样的话，我也会完全满意。我只是觉得上面的 "shorter" 版本可能更容易处理，因为我很确定我自己能够找出缺失的部分。

我使用的 idris 版本是 1.3.2-git:PRE（当从命令行调用时 repl 是这么说的）。

编辑: 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" 版本，我们称它为 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 证明以进行此类型检查：我做错了什么吗？

Answer 1

序曲 Data.Vect.reverse 很难推理，因为据我所知 go 辅助函数不会在类型检查器中解析。通常的方法是在类型级别定义一个更简单的 reverse 而不需要 rewrite 。 :

%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

如您所见，这个定义足够简单，无需进一步工作即可解决这个等价引理。因此，您可能只匹配 fullIndexContraction 中的 reverse ns，如本例所示：

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

Idris：关于向量连接的证明

Idris: proof about concatenation of vectors

vector

tensor

proof

idris