[Agda] Data.Vec toList - fromList isomorphism

[Dan Krejsa]

Hi,

It's pretty clear that the toList and fromList functions in Data.Vec are in
some
sense inverses.  One direction is easy to show:

l-v-l : ∀ {i} {A : Set i} (l : List A) -> toList (fromList l) ≡ l
l-v-l [] = refl
l-v-l (x ∷ l) = cong (λ xs → x ∷ xs) (l-v-l l)

In the other direction my first naive attempt

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> fromList (toList v) ≡ v
v-l-v v = ?

fails with Agda complaining about (fromList (toList v) ≡ v) since equality
is
homogeneous and

   fromList (toList v)

has type

  Vec A (length (toList v))

which is not judgementally equal to the type of v, which is (Vec A n),
although that equality is easy to show propositionally:

lentoList : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> length (toList v) ≡ n
lentoList [] = refl
lentoList (x ∷ v) = cong ℕ.suc (lentoList v)

My next attempt was to try to use the equality (lentoList v) as a 'cast' to
convert the type of fromList (toList v)

transport : ∀ {i j} {A : Set i} (B : A -> Set j) {x y : A} -> x ≡ y -> B x
-> B y
transport B refl = id

transLen : ∀ {i} {A : Set i} {n m : ℕ} -> n ≡ m -> Vec A n -> Vec A m
transLen {A = A} n≡m v = transport (λ l -> Vec A l) n≡m v

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v)
(fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) with lentoList v
... | eq = {! !}

but I didn't get much further since Agda does not want to case on 'eq' as a
pattern
variable turning it into refl.

My guess is there's probably a standard way around this sort of problem, or
a better way to express that (fromList ∘ toList) is pointwise the same as
the identity.
But I'm presently both new & rusty enough not to think of it, having done
just a bit of
Agda proving in the past and having been away from it for a while...

Any hints?

- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140719/39d05285/attachment.html