<div dir="ltr">Hi,<br><div><br>The _=v=_ version of equality that I introduced, and the awkward 'transfer' use, turn<br>out not to be needed if one maps between List A and Σ ℕ (λ n -> Vec A n):<br><br>listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)<br>
listToVec [] = ℕ.zero , []<br>listToVec (x ∷ l) = let (n , v) = listToVec l in ℕ.suc n , x ∷ v<br><br>vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A<br>vecToList (.ℕ.zero , []) = []<br>vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)<br>
<br>L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l<br>L-V-L [] = refl<br>L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)<br><br>V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec (vecToList v) ≡ v<br>
V-L-V (.ℕ.zero , []) = refl<br>V-L-V (ℕ.suc n , x ∷ v) with listToVec (vecToList (n , v)) | V-L-V (n , v)<br>V-L-V (ℕ.suc n , x ∷ v) | .n , .v | refl = refl<br><br></div><div>Figuring out how to get the equality working on the Σ type was a bit tricky for me.<br>
</div><div><br>- Dan<br><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jul 20, 2014 at 12:44 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><div><div><div><div><div>Thanks, Ulf!<br><br></div>In my actual application I'm using (Fin n -> A) to represent the vectors (since I want<br>
to look at permutations / bijections of Fin n), but I may take a similar approach to<br>
what you do above.<br><br>Also, I'll take a look at agda-prelude.<br></div>The main awkwardness I think is the need to resort to 'transport' at all, but<br>maybe that's unavoidable if I'm trying to get a propositional equality (at<br>
least pointwise for Fin n -> A) rather than being content with something like VecEq.<br><br></div>- Dan<br><br></div>P.S. It may also help to extend the toList / fromList mappings to non-dependent<br>mappings between (List A) and Σ ℕ (λ n -> Vec A n), and maybe hide the<br>
</div>nasty 'transport' inside an appropriate equality operator on Σ ℕ (λ n -> Vec A n),<br></div>maybe something like this:<br><br>listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)<br>listToVec [] = ℕ.zero , []<br>
listToVec (x ∷ l) =<br> let (n , v) = listToVec l<br> in ℕ.suc n , x ∷ v<br><br>vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A<br>vecToList (.0 , []) = []<br>vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)<br>
<br>L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l<br>L-V-L [] = refl<br>L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)<br><br>infix 2 _=v=_<br><br>_=v=_ : ∀ {i} {A : Set i} -> (v w : Σ ℕ (λ n -> Vec A n)) -> Set i<br>
_=v=_ {A = A} (n , v) (m , w) = Σ (n ≡ m) (λ n≡m -> transport (Vec A) n≡m v ≡ w)<br><br>_∷'_ : ∀ {i} {A : Set i} -> A -> Σ ℕ (λ n -> Vec A n) -> Σ ℕ (λ n -> Vec A n)<br>x ∷' (n , v) = ℕ.suc n , x ∷ v<br>
<br>=v=cons : ∀ {i} {A : Set i} {v w : Σ ℕ (λ n -> Vec A n)} (a : A) -> v =v= w -> a ∷' v =v= a ∷' w<br>=v=cons {v = n , v} {.n , w} a (refl , tv=w) = refl , cong (_∷_ a) tv=w<br><br>V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec (vecToList v) =v= v<br>
V-L-V (.0 , []) = refl , refl<br>V-L-V (ℕ.suc n , x ∷ v) = =v=cons x (V-L-V (n , v))<div><div class="h5"><br><br><div><div><div><br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jul 20, 2014 at 1:19 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><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" target="_blank">https://github.com/UlfNorell/agda-prelude</a></div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote"><div><div>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>
</div></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div><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><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><font color="#888888"><br></font></span></div><span><font color="#888888"><br>- Dan<br>
<br></font></span></div><div><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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);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></div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
</blockquote></div><br></div></div></div></div></div></div>
</blockquote></div><br></div>