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

[Dan Krejsa]

Hi,

The _=v=_ version of equality that I introduced, and the awkward 'transfer'
use, turn
out not to be needed if one maps between List A and Σ ℕ (λ n -> Vec A n):

listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)
listToVec [] = ℕ.zero , []
listToVec (x ∷ l) = let (n , v) = listToVec l in ℕ.suc n , x ∷ v

vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A
vecToList (.ℕ.zero , []) = []
vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)

L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l
L-V-L [] = refl
L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)

V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec
(vecToList v) ≡ v
V-L-V (.ℕ.zero , []) = refl
V-L-V (ℕ.suc n  , x ∷ v) with listToVec (vecToList (n , v)) | V-L-V (n , v)
V-L-V (ℕ.suc n , x ∷ v) | .n , .v | refl = refl

Figuring out how to get the equality working on the Σ type was a bit tricky
for me.

- Dan



On Sun, Jul 20, 2014 at 12:44 PM, Dan Krejsa <dan.krejsa at gmail.com> wrote:

> Thanks, Ulf!
>
> In my actual application I'm using (Fin n -> A) to represent the vectors
> (since I want
> to look at permutations / bijections of Fin n), but I may take a similar
> approach to
> what you do above.
>
> Also, I'll take a look at agda-prelude.
> The main awkwardness I think is the need to resort to 'transport' at all,
> but
> maybe that's unavoidable if I'm trying to get a propositional equality (at
> least pointwise for Fin n -> A) rather than being content with something
> like VecEq.
>
> - Dan
>
> P.S. It may also help to extend the toList / fromList mappings to
> non-dependent
> mappings between (List A) and Σ ℕ (λ n -> Vec A n), and maybe hide the
> nasty 'transport' inside an appropriate equality operator on Σ ℕ (λ n ->
> Vec A n),
> maybe something like this:
>
> listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)
> listToVec [] = ℕ.zero , []
> listToVec (x ∷ l) =
>     let (n , v) = listToVec l
>     in ℕ.suc n , x ∷ v
>
> vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A
> vecToList (.0 , []) = []
> vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)
>
> L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l
> L-V-L [] = refl
> L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)
>
> infix 2 _=v=_
>
> _=v=_ : ∀ {i} {A : Set i} -> (v w : Σ ℕ (λ n -> Vec A n)) -> Set i
> _=v=_ {A = A} (n , v) (m , w) = Σ (n ≡ m) (λ n≡m -> transport (Vec A) n≡m
> v ≡ w)
>
> _∷'_ : ∀ {i} {A : Set i} -> A ->  Σ ℕ (λ n -> Vec A n) ->  Σ ℕ (λ n -> Vec
> A n)
> x ∷' (n , v) = ℕ.suc n , x ∷ v
>
> =v=cons : ∀ {i} {A : Set i} {v w : Σ ℕ (λ n -> Vec A n)} (a : A) -> v =v=
> w -> a ∷' v =v= a ∷' w
> =v=cons {v = n , v} {.n , w} a (refl , tv=w) = refl , cong (_∷_ a) tv=w
>
> V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec
> (vecToList v) =v= v
> V-L-V (.0 , []) = refl , refl
> V-L-V (ℕ.suc n  , x ∷ v) = =v=cons x (V-L-V (n , v))
>
>
>
>
>
> On Sun, Jul 20, 2014 at 1:19 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
>
>> 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).
>>
>> open import Prelude
>>
>> -- Heterogenous equality on vectors --
>>
>> VecEq : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) → Set a
>> VecEq []       []       = ⊤′
>> VecEq []       (x ∷ ys) = ⊥′
>> VecEq (x ∷ xs) []       = ⊥′
>> VecEq (x ∷ xs) (y ∷ ys) = x ≡ y × VecEq xs ys
>>
>> -- If vectors are equal then the lengths are equal
>> vecEq-len : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) →
>>               VecEq xs ys → n ≡ m
>> vecEq-len [] [] heq = refl
>> vecEq-len [] (x ∷ ys) ()
>> vecEq-len (x ∷ xs) [] ()
>> vecEq-len (_ ∷ xs) (_ ∷ ys) (_ , heq) =
>>   cong suc (vecEq-len xs ys heq)
>>
>> -- VecEq xs ys implies transport xs ≡ ys
>> vecEq-≡ : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) (n=m : n
>> ≡ m) →
>>             VecEq xs ys → transport (Vec A) n=m xs ≡ ys
>> vecEq-≡ [] [] refl heq = refl
>> vecEq-≡ (x ∷ xs) (.x ∷ ys) refl (refl , heq) =
>>   cong (_∷_ x) (vecEq-≡ xs ys refl heq)
>>
>> -- Vec to List round-trip --
>>
>> -- This proof is super-easy
>> v-l-v′ : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
>>            VecEq (listToVec (vecToList xs)) xs
>> v-l-v′ []       = _
>> v-l-v′ (x ∷ xs) = refl , v-l-v′ xs
>>
>> -- We can get the original theorem from the VecEq lemmas
>> lentoList : ∀ {a} {A : Set a} {n} (xs : Vec A n) → length (vecToList xs)
>> ≡ n
>> lentoList xs = vecEq-len (listToVec (vecToList xs)) xs (v-l-v′ xs)
>>
>> v-l-v : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
>>         transport (Vec A) (lentoList xs) (listToVec (vecToList xs)) ≡ xs
>> v-l-v xs = vecEq-≡ (listToVec (vecToList xs)) xs (lentoList xs) (v-l-v′
>> xs)
>>
>> / Ulf
>>
>> [1] https://github.com/UlfNorell/agda-prelude
>>
>>
>> On Sun, Jul 20, 2014 at 3:22 AM, Dan Krejsa <dan.krejsa at gmail.com> wrote:
>>
>>> 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
>>>>
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140721/b7fe4eed/attachment.html