<div dir="ltr"><div>Hi,</div><div><br></div><div>It's pretty clear that the toList and fromList functions in Data.Vec are in some<br>sense inverses. One direction is easy to show:<br><br>l-v-l : ∀ {i} {A : Set i} (l : List A) -> toList (fromList l) ≡ l<br>
l-v-l [] = refl<br>l-v-l (x ∷ l) = cong (λ xs → x ∷ xs) (l-v-l l)<br><br></div><div>In the other direction my first naive attempt <br><br>v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> fromList (toList v) ≡ v<br>v-l-v v = ?<br>
<br></div><div>fails with Agda complaining about (fromList (toList v) ≡ v) since equality is<br>homogeneous and <br><br> fromList (toList v)<br><br>has type<br><br> Vec A (length (toList v))<br><br>which is not judgementally equal to the type of v, which is (Vec A n), <br>
although that equality is easy to show propositionally:<br><br>lentoList : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> length (toList v) ≡ n<br>lentoList [] = refl<br>lentoList (x ∷ v) = cong ℕ.suc (lentoList v)<br><br>
</div><div>My next attempt was to try to use the equality (lentoList v) as a 'cast' to convert the type of fromList (toList v)<br><br>transport : ∀ {i j} {A : Set i} (B : A -> Set j) {x y : A} -> x ≡ y -> B x -> B y<br>
transport B refl = id<br><br>transLen : ∀ {i} {A : Set i} {n m : ℕ} -> n ≡ m -> Vec A n -> Vec A m<br>transLen {A = A} n≡m v = transport (λ l -> Vec A l) n≡m v<br><br>v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> transLen (lentoList v) (fromList (toList v)) ≡ v<br>
v-l-v [] = refl<br>v-l-v (x ∷ v) with lentoList v<br>... | eq = {! !}<br><br></div><div>but I didn't get much further since Agda does not want to case on 'eq' as a pattern<br>variable turning it into refl.<br>
<br></div><div>My guess is there's probably a standard way around this sort of problem, or<br></div><div>a better way to express that (fromList ∘ toList) is pointwise the same as the identity.<br></div><div>But I'm presently both new & rusty enough not to think of it, having done just a bit of<br>
</div><div>Agda proving in the past and having been away from it for a while...<br></div><div><br></div><div>Any hints?<br><br></div><div>- Dan<br></div></div>