[Agda] Newbie question, book exercise problem.

[Paul Graphov]

Hello!

I'm new to Agda and dependent types at all.
Now I am reading "Dependently typed programming in Agda" by Ulf Norell.
I got stuck with exercise 2.2.b

Here it is:

(Nat, Fin and Vec are as usual)

_!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A
[]        ! ()
(x :: xs) ! fzero    = x
(x :: xs) ! (fsuc i) = xs ! i

tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero} f = []
tabulate {suc n} f = f fzero :: tabulate (f ◦ fsuc)

Prove that they are indeed each other’s inverses.

lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! xs = {! !}

I figured out the proof on the paper but can't translate it to Agda code...

Thanks.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091129/ad6d73b7/attachment.html