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

[gallais at ensl.org]

Hi Jason,

Have you tried to destruct the proofs of [x == y] and [xs == ys] ?

Cheers,

--
guillaume



On 8 April 2011 08:12, Jason Dusek <jason.dusek at gmail.com> wrote:
>  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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>