<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">&lt;<a href="mailto:dan.krejsa@gmail.com" target="_blank">dan.krejsa@gmail.com</a>&gt;</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 : ℕ} -&gt; (p : n ≡ m) -&gt; (a : A) -&gt; (v : Vec A n)<br>     -&gt; 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) -&gt;  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">&lt;<a href="mailto:dan.krejsa@gmail.com" target="_blank">dan.krejsa@gmail.com</a>&gt;</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&#39;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) -&gt; 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) -&gt; 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) -&gt; 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 &#39;cast&#39; to convert the type of fromList (toList v)<br><br>transport : ∀ {i j} {A : Set i} (B : A -&gt; Set j) {x y : A} -&gt; x ≡ y -&gt; B x -&gt; B y<br>



transport B refl = id<br><br>transLen : ∀ {i} {A : Set i} {n m : ℕ} -&gt; n ≡ m -&gt; Vec A n -&gt; Vec A m<br>transLen {A = A} n≡m v = transport (λ l -&gt; Vec A l) n≡m v<br><br>v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -&gt;  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&#39;t get much further since Agda does not want to case on &#39;eq&#39; as a pattern<br>variable turning it into refl.<br>



<br></div><div>My guess is there&#39;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&#39;m presently both new &amp; 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>