Равенство между векторами одинаковой длины, но с разной длиной выражения в типе - PullRequest
Новая
       26

Равенство между векторами одинаковой длины, но с разной длиной выражения в типе

3 голосов
/ 19 апреля 2019

Я занимаюсь разработкой в ​​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?

1 Ответ

3 голосов
/ 19 апреля 2019

Почему, конечно: 

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
...