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

Question

I'm doing some development in Idris and I've being getting into the following problem. Say we have 3 vectors:

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

and say we also have

samelen : len = len'

Finally, we also have the following equalities:

xsys : xs = ys

yszs : ys = zs

In the first equality, we have an equality for the type Vect len a while in the second for Vect len' a. Now we want to establish:

xsza : xs = zs

I've been having a hard time making this work. In particular, trans needs equality between the same types, but that is not the case here. How can transitivity be used here to achieve xsza?

HTNW HTNW · Accepted Answer · 2019-04-19T01:40:13

Why, sure:

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

I think it's important to know that this basically has to be a function. You cannot use the sameLen proof to replace len with len' in the types of things that are already in scope. That is, if your type signatures were all top level, Idris could never be convinced that zs : Vect len a. You have to use an auxiliary function. In the above function, len' is matched to len, justified by matching the Refl, before the zs variable is introduced. You might argue that's clearly false, as zs comes before the Refl argument, but, since Idris is a total language, the compiler is allowed to make life easier for you by implicitly reordering the abstraction and the matching and all that jazz. In effect, right before the Refl is matched, before zs is introduced, the goal type is (zs : Vect len' A) -> xs = ys -> ys = zs -> xs = zs, but the match rewrites that to (zs : Vect len A) -> ?etc, and zs is introduced with a nicer type.

Do note that the len = len' thing is really just not necessary, though. This works:

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

Or even

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

1 Answers