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

[Ulf Norell]

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/20140720/b8e0e207/attachment-0001.html