[Agda] Re: Data.Vec toList - fromList isomorphism

[Dan Krejsa]

Hi,

I figured out a proof for v-l-v using a lemma transLenSuc,

-----
transLenSuc :  ∀ {i} {A : Set i} {n m : ℕ} -> (p : n ≡ m) -> (a : A) -> (v
: Vec A n)
     -> transLen (cong ℕ.suc p) (a ∷ v) ≡ a ∷ transLen p v
transLenSuc refl a v = refl

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v)
(fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) = trans (transLenSuc (lentoList v) x (fromList (toList v)))
(cong (_∷_ x) (v-l-v v))
-----

but the approach still seems kind of awkard, so suggestions still
appreciated.

- Dan



On Sat, Jul 19, 2014 at 4:37 PM, Dan Krejsa <dan.krejsa at gmail.com> wrote:

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