类型中具有相同长度但不同长度表达式的向量之间的相等性

Question

我在伊德里斯做了一些开发，我遇到了以下问题。假设我们有3个向量：

xs : Vect len  a
ys : Vect len  a
zs : Vect len' a

并说我们也有

samelen : len = len' 

最后，我们还有以下等式：

xsys : xs = ys

yszs : ys = zs

在第一个相等中，我们在Vect len'a的第二个类型中具有Vect len类型的相等性。现在我们要建立：

xsza : xs = zs

我一直很难做这项工作。特别是，trans需要相同类型之间的相等，但这不是这种情况。如何使用传递性来实现xsza？

Answer 1

为什么，当然：

xszs : {A : Type} -> {len, len' : Nat} ->
       (xs, ys : Vect len A) -> (zs : Vect len' A) ->
       len = len' ->
       xs = ys -> ys = zs ->
       xs = zs
xszs {A} {len} {len'=len} xs ys zs Refl = trans

我认为重要的是要知道这基本上必须是一个功能。您不能使用sameLen证明将len替换为已经在范围内的事物类型的len'。也就是说，如果你的类型签名都是顶级，那么伊德里斯永远不会相信zs : Vect len a。你必须使用辅助功能。在上面的函数中，len'与len相匹配，在引入Refl变量之前通过匹配zs来证明。您可能认为这显然是错误的，因为zs出现在Refl论证之前，但是，由于Idris是一种完整的语言，编译器可以通过隐式重新排序抽象和匹配以及所有爵士乐来让生活更轻松。实际上，在Refl匹配之前，在引入zs之前，目标类型是(zs : Vect len' A) -> xs = ys -> ys = zs -> xs = zs，但是匹配将其重写为(zs : Vect len A) -> ?etc，并且zs以更好的类型引入。

请注意，len = len'事情确实没有必要。这有效：

xszs : {A : Type} -> {len, len' : Nat} ->
       (xs, ys : Vect len A) -> (zs : Vect len' A) ->
       xs = ys -> ys = zs -> xs = zs
xszs {A} {len} {len'=len} xs xs xs Refl Refl = Refl

甚至

xszs : {A : Type} -> {len, len' : Nat} ->
       (xs, ys : Vect len A) -> (zs : Vect len' A) ->
       xs = ys -> ys = zs -> xs = zs
xszs xs ys zs = trans