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

Question

我正在 Idris 中进行一些开发，但遇到了以下问题。假设我们有 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' a 的等式。现在我们要建立：

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'。也就是说，如果你的类型签名都是顶级的，Idris 永远不会相信 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

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

Equality between vectors with same length but different length expression in type

equality

idris

dependent-type