[Agda] Newbie question, book exercise problem.

[Paul Graphov]

It's much more complicated than I expected...
Thanks a lot!

2009/11/30 Andreas Abel <andreas.abel at ifi.lmu.de>

> Here is the file...
>
>
>
>
> On Nov 29, 2009, at 9:53 PM, Paul Graphov wrote:
>
>  Yes, I am trying to do induction on xs, [] case is trivial but y::y' is
>> not for me.
>> On paper I just substitute y::x' in the definition of (_!_) and tabulate.
>>
>> EqReasoning looks quite difficult for me but I'll take a look, thanks.
>>
>> And yes, I can answer positively. But I don't see any attachment.
>>
>> Thanks!
>>
>> 2009/11/29 Andreas Abel <andreas.abel at ifi.lmu.de>
>>
>> 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
>>
>>
>>
>>
>>
> Andreas ABEL
> INRIA, Projet Pi.R2
> 23, avenue d'Italie
> F-75013 Paris
> Tel: +33.1.39.63.59.41
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091130/010f5216/attachment.html