<div dir="ltr"><div><div><div>Hi,<br><br></div>I figured out a proof for v-l-v using a lemma transLenSuc,<br><br>-----<br>transLenSuc : ∀ {i} {A : Set i} {n m : ℕ} -> (p : n ≡ m) -> (a : A) -> (v : Vec A n)<br> -> transLen (cong ℕ.suc p) (a ∷ v) ≡ a ∷ transLen p v<br>
transLenSuc refl a v = refl<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) = trans (transLenSuc (lentoList v) x (fromList (toList v))) (cong (_∷_ x) (v-l-v v))<br>
-----<br><br></div>but the approach still seems kind of awkard, so suggestions still appreciated.<br></div><br>- Dan<br><br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sat, Jul 19, 2014 at 4:37 PM, Dan Krejsa <span dir="ltr"><<a href="mailto:dan.krejsa@gmail.com" target="_blank">dan.krejsa@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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?<span class="HOEnZb"><font color="#888888"><br><br></font></span></div><span class="HOEnZb"><font color="#888888"><div>
- Dan<br></div></font></span></div>
</blockquote></div><br></div>