<div>It's much more complicated than I expected...</div><div>Thanks a lot!</div><br><div class="gmail_quote">2009/11/30 Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Here is the file...<br>
<br>
<br><br>
<br>
On Nov 29, 2009, at 9:53 PM, Paul Graphov wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Yes, I am trying to do induction on xs, [] case is trivial but y::y' is not for me.<br>
On paper I just substitute y::x' in the definition of (_!_) and tabulate.<br>
<br>
EqReasoning looks quite difficult for me but I'll take a look, thanks.<br>
<br>
And yes, I can answer positively. But I don't see any attachment.<br>
<br>
Thanks!<br>
<br>
2009/11/29 Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>><br>
<br>
On Nov 29, 2009, at 7:47 PM, Andreas Abel wrote:<br>
<br>
<br>
On Nov 29, 2009, at 2:50 PM, Paul Graphov wrote:<br>
Now I am reading "Dependently typed programming in Agda" by Ulf Norell.<br>
I got stuck with exercise 2.2.b<br>
<br>
Here it is:<br>
<br>
(Nat, Fin and Vec are as usual)<br>
<br>
_!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A<br>
[] ! ()<br>
(x :: xs) ! fzero = x<br>
(x :: xs) ! (fsuc i) = xs ! i<br>
<br>
tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n<br>
tabulate {zero} f = []<br>
tabulate {suc n} f = f fzero :: tabulate (f ◦ fsuc)<br>
<br>
Prove that they are indeed each other’s inverses.<br>
<br>
lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs<br>
lem-tab-! xs = {! !}<br>
<br>
I figured out the proof on the paper but can't translate it to Agda code...<br>
<br>
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?<br>
<br>
<br>
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,<br>
like local module opening and on the spot module specialization...<br>
<br>
.... where open Relation.Binary.EqReasoning (setoid (Vec _ _))<br>
<br>
[To figure that out, took me longest...]<br>
<br>
Cheers,<br>
<br>
<br>
Andreas ABEL<br>
INRIA, Projet Pi.R2<br>
23, avenue d'Italie<br>
F-75013 Paris<br>
Tel: +33.1.39.63.59.41<br>
<br>
<br>
<br>
<br>
</blockquote>
<br>
Andreas ABEL<br>
INRIA, Projet Pi.R2<br>
23, avenue d'Italie<br>
F-75013 Paris<br>
Tel: +33.1.39.63.59.41<br>
<br>
<br>
<br>
<br></blockquote></div><br>