<div dir="ltr">Not sure if you find this less awkward, but here is a different, slightly less ad-hoc, approach (using my prelude library [1] rather than the standard library).<div><br></div><div><div><font face="courier new, monospace">open import Prelude</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- Heterogenous equality on vectors --</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">VecEq : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) → Set a</font></div>
<div><font face="courier new, monospace">VecEq [] [] = ⊤′</font></div><div><font face="courier new, monospace">VecEq [] (x ∷ ys) = ⊥′</font></div><div><font face="courier new, monospace">VecEq (x ∷ xs) [] = ⊥′</font></div>
<div><font face="courier new, monospace">VecEq (x ∷ xs) (y ∷ ys) = x ≡ y × VecEq xs ys</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- If vectors are equal then the lengths are equal</font></div>
<div><font face="courier new, monospace">vecEq-len : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) →</font></div><div><font face="courier new, monospace"> VecEq xs ys → n ≡ m</font></div><div><font face="courier new, monospace">vecEq-len [] [] heq = refl</font></div>
<div><font face="courier new, monospace">vecEq-len [] (x ∷ ys) ()</font></div><div><font face="courier new, monospace">vecEq-len (x ∷ xs) [] ()</font></div><div><font face="courier new, monospace">vecEq-len (_ ∷ xs) (_ ∷ ys) (_ , heq) =</font></div>
<div><font face="courier new, monospace"> cong suc (vecEq-len xs ys heq)</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- VecEq xs ys implies transport xs ≡ ys</font></div>
<div><font face="courier new, monospace">vecEq-≡ : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) (n=m : n ≡ m) →</font></div><div><font face="courier new, monospace"> VecEq xs ys → transport (Vec A) n=m xs ≡ ys</font></div>
<div><font face="courier new, monospace">vecEq-≡ [] [] refl heq = refl</font></div><div><font face="courier new, monospace">vecEq-≡ (x ∷ xs) (.x ∷ ys) refl (refl , heq) =</font></div><div><font face="courier new, monospace"> cong (_∷_ x) (vecEq-≡ xs ys refl heq)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- Vec to List round-trip --</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- This proof is super-easy</font></div>
<div><font face="courier new, monospace">v-l-v′ : ∀ {a} {A : Set a} {n} (xs : Vec A n) →</font></div><div><font face="courier new, monospace"> VecEq (listToVec (vecToList xs)) xs</font></div><div><font face="courier new, monospace">v-l-v′ [] = _</font></div>
<div><font face="courier new, monospace">v-l-v′ (x ∷ xs) = refl , v-l-v′ xs</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- We can get the original theorem from the VecEq lemmas</font></div>
<div><font face="courier new, monospace">lentoList : ∀ {a} {A : Set a} {n} (xs : Vec A n) → length (vecToList xs) ≡ n</font></div><div><font face="courier new, monospace">lentoList xs = vecEq-len (listToVec (vecToList xs)) xs (v-l-v′ xs)</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">v-l-v : ∀ {a} {A : Set a} {n} (xs : Vec A n) →</font></div><div><font face="courier new, monospace"> transport (Vec A) (lentoList xs) (listToVec (vecToList xs)) ≡ xs</font></div>
<div><font face="courier new, monospace">v-l-v xs = vecEq-≡ (listToVec (vecToList xs)) xs (lentoList xs) (v-l-v′ xs)</font></div></div><div><br></div><div>/ Ulf</div><div><br></div><div>[1] <a href="https://github.com/UlfNorell/agda-prelude">https://github.com/UlfNorell/agda-prelude</a></div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jul 20, 2014 at 3:22 AM, 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><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<div class=""><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></div>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.<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><br>- Dan<br>
<br></font></span></div><div class="HOEnZb"><div class="h5"><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><font color="#888888"><br><br></font></span></div><span><font color="#888888"><div>
- Dan<br></div></font></span></div>
</blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>