[Agda] Newbie question, book exercise problem.

[Andreas Abel]

On Nov 29, 2009, at 2:50 PM, Paul Graphov wrote:
> 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...

Can you be more specific?  What does your paper proof look like and at  
which point does its implementation fail?  Or do you just want to see  
a solution?

Cheers,
Andreas

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41