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

[AndrásKovács]

Dan Krejsa <dan.krejsa at ...> writes:

> 
> 
> Hi,
> 
> It's pretty clear that the toList and fromList functions in Data.Vec are
in somesense inverses.  One direction is easy to show:l-v-l : ∀ {i} {A : Set
i} (l : List A) -> toList (fromList l) ≡ l
> l-v-l [] = refll-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) ≡ vv-l-v v = ?
> 
> fails with Agda complaining about (fromList (toList v) ≡ v) since equality
ishomogeneous 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) ≡ nlentoList [] =
refllentoList (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 = idtransLen : ∀ {i} {A : Set i} {n m : ℕ} -> n ≡ m ->
Vec A n -> Vec A mtransLen {A = A} n≡m v = transport (λ l -> Vec A l) n≡m
vv-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v)
(fromList (toList v)) ≡ v
> v-l-v [] = reflv-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 patternvariable 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 ...
> https://lists.chalmers.se/mailman/listinfo/agda
> 

I ran into this issue a few times, and my preferred method is to use an
augmented "cong" for heterogeneous equality, which also works in the case
when the function argument has an  indexed type, and the indices are not
patently equal:


open import Relation.Binary.HeterogeneousEquality hiding (cong)

hcong-ix1 :
   ∀ {i c p}
   {I : Set i}
   {C : I → Set c}
   (P : ∀ i → (x : C i) → Set p)
   {i i' : I}  
   {x : C i} {y : C i'}
   (f : ∀ {i} → (x : C i) → P i x) 
   → i ≡ i'
   → x ≅ y 
   → f x ≅ f y
hcong-ix1 P f refl refl = refl

length-lem : ∀ {a}{A : Set a} n (xs : Vec A n) → length (toList xs) ≡ n
length-lem zero [] = refl
length-lem (suc n) (x ∷ xs) = cong suc (length-lem n xs) 

v-l-v : ∀ {a}{A : Set a}{n} (v : Vec A n) → fromList (toList v) ≅ v 
v-l-v [] = refl
v-l-v {A = A}(x ∷ xs) = hcong-ix1 (λ i _ → Vec A (suc i)) (_∷_ x)
(length-lem _ xs) (v-l-v xs)


There is an analogously extended version of the heterogeneous subst, which
I've found useful. It has a simpler definition though, because the
heterogeneous equality already implies equality of types (and type indices):

hsubst' : 
  ∀ {c p}
  {C1 C2 : Set c} 
  {x : C1} {y : C2}
  (P : {C : Set c} -> C -> Set p)
  -> x ≅ y
  -> P x
  -> P y
hsubst' _ refl x = x