How can I make use of cong and injective with indexed vectors in Idris?

user_2904322 0
Viewed 20

cong and injective allow you to apply and unapply functions to equalities:

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

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

Both of these fail for indexed vectors with different lengths, for obvious reasons.

How can I prove that two equal vectors have the same length? I.e.

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

I can't just do

sameLen pf = cong length pf

because length on xs has type Vect n a -> Nat and length on ys has type Vect m b -> Nat. (In fact, I'm not even sure how to prove the same thing for two regular Lists, due to the differing type arguments, never mind with the added indices).

Going the other way, how would I prove something like

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

Again, I can't just do

unwrap pf = injective pf

due to the differing types of T (one with m and one with n). And even if I had a proof m=n, how could I use that to convince Idris that the two applications of T are the same?

theorem-proving idris vector
1 Answers

Got the answer from the Idris Discord - if you pattern match on Refl then it unifies a and b automatically:

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
user_29043220
Related