Thank you guys,<div><br></div><div>There is one thing that is not clear to me yet. Actually "cong (λ xs → x ∷ xs) (lem-tab-! xs)" gives Agda proof that</div><div>x <span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">∷ tabulate(_!_ xs) </span><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">≡ x </span><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">∷ xs</span><br>
<br></div><div>but how Agda knows that </div><div>tabulate(_!_ (x ∷ xs)) is the same as x <span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">∷ tabulate(_!_ xs) ?</span></div>
<div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; "><br></span></div><div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">When I remove the whole cong expression and replace it with {! !} ant then try to </span></div>
<div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">reduce tabulate(_!_ (x ∷ xs)) to normal form (C-c C-n) it gives "x ∷ tabulate ((λ {.x} → _!_ (x ∷ xs)) ∘ fsuc)"</span></div>
<div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; "><br></span></div><div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">How to know that it can evaluate it to "x ∷ tabulate(_!_ xs)"?</span></div>
<div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; "><br></span></div><div><span class="Apple-style-span" style="font-family: arial, sans-serif; font-size: 13px; border-collapse: collapse; ">Thanks.</span></div>
<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;">
Julian is correct that in this case the EqReasoning is not necessary. If you look at the justifications I use in this equality chain<br>
<br>
begin<br>
tabulate (_!_ (x ∷ xs))<br>
≡⟨ refl ⟩<br>
(x ∷ xs) ! zero ∷ tabulate (λ i → (x ∷ xs) ! (suc i))<br>
≡⟨ refl ⟩<br>
x ∷ tabulate (λ i → xs ! i)<br>
≡⟨ cong (λ xs → x ∷ xs) (lem-tab-! xs) ⟩<br>
x ∷ xs<br>
∎<br>
<br>
the first two steps are justified by "refl" which means they do not need a justification, they follow by computation (unfolding of definitions). Only the last step needs a non-trivial justification, a call to the induction hypothesis at position x ∷ _. "cong" has the role of telling which subterm should be rewritten by the induction hypothesis.<br>
<br>
Since there is only one non-trivial step, the equality chain can be collapsed into Julian's single-step proof. Equality chains are made for reasoning involving transitivity. I, however, find then also nice to document the proof in a human-readable way. Instead of doing the calculation on paper, I did it directly in Agda, using EqReasoning as notation.<br>
<br>
Cheers,<br><font color="#888888">
Andreas</font><div><div></div><div class="h5"><br>
<br>
On Nov 30, 2009, at 9:53 AM, Julian Beaumont wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
It's worth pointing out that you can do this fairly simply without<br>
using EqReasoning. The downside is that the proof is generally less<br>
readable. Agda will reduce all functions using the definitions as much<br>
as possible for you. In the inductive case this means the goal is<br>
simplified to proving x :: tabulate (_!_ xs) == x :: xs. This may be<br>
proven trivially using cong and a recursive call to lem-tab-!.<br>
<br>
cong : {A B : Set} {x y : A} (f : A -> B) -> x == y -> f x == f y<br>
cong f refl = refl<br>
<br>
lem-tab-! [] = refl<br>
lem-tab-! (x :: xs) = cong {! !} {! !} -- you should be able to fill<br>
in the blanks easily enough.<br>
<br>
In this case the version without EqReasoning is fairly readable and<br>
easy to understand, however, for more complicated equational proofs<br>
you definately want to be using EqReasoning.<br>
<br>
On Mon, Nov 30, 2009 at 4:10 PM, Paul Graphov <<a href="mailto:graphov@gmail.com" target="_blank">graphov@gmail.com</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
It's much more complicated than I expected...<br>
Thanks a lot!<br>
2009/11/30 Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
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<br>
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<br>
code...<br>
<br>
Can you be more specific? What does your paper proof look like and at<br>
which point does its implementation fail? Or do you just want to see a<br>
solution?<br>
<br>
<br>
If you can answer the last question positively, please consult the<br>
attachment. Basically, you need induction on xs and then equality<br>
reasoning. The latter is greatly simplified by the module EqReasoning in<br>
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>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</blockquote>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><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>
</div></div></blockquote></div><br></div>