如何在 Idris 中使用带索引向量的 cong 和单射？答案

【问题标题】：How can I make use of cong and injective with indexed vectors in Idris?如何在 Idris 中使用带索引向量的 cong 和单射？
【发布时间】：2022-01-13 14:12:11
【问题描述】：

cong 和 injective 允许您对等式应用和取消应用函数：

cong : (f : a -> b) -> x = y -> f x = f y

injective : Injective f => f x = f y -> x = y

对于不同长度的索引向量，这两种方法都失败了，原因很明显。

如何证明两个相等的向量具有相同的长度？即

sameLen : {xs : Vect n a} -> {ys : Vect m b} -> xs = ys -> n = m

我做不到

sameLen pf = cong length pf

因为xs 上的length 具有Vect n a -> Nat 类型，而ys 上的length 具有Vect m b -> Nat 类型。（事实上，由于类型参数不同，我什至不确定如何为两个常规 Lists 证明相同的事情，更不用说添加索引了）。

换个方式，我怎么证明这样的事情

data Rose a = V a | T (Vect n (Rose a))
Injective T where
    injective Refl = Refl
unwrap : {xs : Vect n (Rose a)} -> {ys : Vect m (Rose b)} -> T xs = T ys -> xs = ys

再说一遍，我不能这样做

unwrap pf = injective pf

由于T 的类型不同（一种带有m，一种带有n）。而且即使我有一个证明m=n，我怎么能用它来说服伊德里斯T 的两个应用程序是一样的？

【问题讨论】：

标签： vector idris theorem-proving

【解决方案1】：

从 Idris Discord 中得到答案 - 如果您在 Refl 上进行模式匹配，那么它会自动统一 a 和 b：

sameLen : {xs : List a} -> {ys : List b} -> xs = ys -> length xs = length ys
sameLen Refl = Refl

sameLen' : {xs : Vect n a} -> {ys : Vect m b} -> xs = ys -> n = m
sameLen' Refl = Refl

【讨论】：