[Agda] Proving _!_ is inverse of tabulate...

[Jason Dusek]

  This is a homework problem from a well known tutorial; so I am
  just going to ask for a clue.

  We would like to show that tabulating the operation of
  indexing into a vector over the range of indices of the vector
  is the identity. Some signatures:

    _!_      : {n : ℕ}{A : Set} → Vec A n → Fin n → A
    tabulate : {n : ℕ}{A : Set} → (Fin n → A) → Vec A n

  In the case where n : ℕ ≡ 0, I can just use refl; tabulating
  an empty vector is the empty vector. In the non-empty case I
  am vexed because I would like prove it like this:

 .  Show that the heads of the vector and its tabulation (bound
    via `with') are equal.

 .  Recurse to find equality of the tails.

  I am not sure how to do this in practice, though; I end up
  with two statements of refl-ness. Calling the vector and its
  tabulation x ∷ xs and y ∷ ys, respectively, I have:

    x ≡ y
    xs ≡ ys

  But I need some transitivity to show that x ∷ xs ≡ y ∷ ys and
  I am honestly not sure how to do it.

  Of course, I welcome any discussion of alternate approaches to
  this problem.

--
Jason Dusek
()  ascii ribbon campaign - against html e-mail
/\  www.asciiribbon.org   - against proprietary attachments