[Agda] Newbie question, book exercise problem.

[Andreas Abel]

On Nov 29, 2009, at 7:47 PM, Andreas Abel wrote:

>
> 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?


If you can answer the last question positively, please consult the  
attachment.  Basically, you need induction on xs and then equality  
reasoning.  The latter is greatly simplified by the module EqReasoning  
in the standard library, if you know the right incantations to set it  
up,
like local module opening and on the spot module specialization...

  .... where open Relation.Binary.EqReasoning (setoid (Vec _ _))

[To figure that out, took me longest...]

Cheers,

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