[Agda] Newbie question, book exercise problem.

[Julian Beaumont]

It's worth pointing out that you can do this fairly simply without
using EqReasoning. The downside is that the proof is generally less
readable. Agda will reduce all functions using the definitions as much
as possible for you. In the inductive case this means the goal is
simplified to proving x :: tabulate (_!_ xs) == x :: xs. This may be
proven trivially using cong and a recursive call to lem-tab-!.

cong : {A B : Set} {x y : A} (f : A -> B) -> x == y -> f x == f y
cong f refl = refl

lem-tab-! [] = refl
lem-tab-! (x :: xs) = cong {! !} {! !} -- you should be able to fill
in the blanks easily enough.

In this case the version without EqReasoning is fairly readable and
easy to understand, however, for more complicated equational proofs
you definately want to be using EqReasoning.

On Mon, Nov 30, 2009 at 4:10 PM, Paul Graphov <graphov at gmail.com> wrote:
> 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
>>
>>
>>
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>