Thanks again, now it is clear!<br><br><div class="gmail_quote">2009/12/2 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;">
Paul Graphov a écrit :<div class="im"><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Thank you guys,<br>
<br>
There is one thing that is not clear to me yet. Actually "cong (λ xs → x ∷ xs) (lem-tab-! xs)" gives Agda proof that<br>
x ∷ tabulate(_!_ xs) ≡ x ∷ xs<br>
<br>
but how Agda knows that tabulate(_!_ (x ∷ xs)) is the same as x ∷ tabulate(_!_ xs) ?<br>
<br>
When I remove the whole cong expression and replace it with {! !} ant then try to reduce tabulate(_!_ (x ∷ xs)) to normal form (C-c C-n) it gives "x ∷ tabulate ((λ {.x} → _!_ (x ∷ xs)) ∘ fsuc)"<br>
<br>
How to know that it can evaluate it to "x ∷ tabulate(_!_ xs)"?<br>
</blockquote>
<br></div>
Agda has eta-equality built in so you can always replace a term t by its eta-expansion<br>
<br>
\ x -> t x (where x is a fresh variable)<br>
<br>
Agda does not distinguish between these two. So<br>
<br>
tabulate ((_!_ (x ∷ xs)) ∘ fsuc)<br>
<br>
is the same as<br>
<br>
tabulate (\ i -> ((_!_ (x ∷ xs)) ∘ fsuc) i)<br>
<br>
which is<br>
<br>
tabulate (\ i -> (x :: xs) ! (fsuc i))<br>
<br>
by definition of tabulate, reducing to<br>
<br>
tabulate (\ i -> xs ! i)<br>
<br>
eta-reducing to<br>
<br>
tabulate (_!_ xs)<br>
<br>
This step is actually documented in my proof (justified by the second refl).<br>
<br>
Cheers,<br>
Andreas<br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
2009/11/30 Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a> <mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>>><div>
<div></div><div class="h5"><br>
<br>
Julian is correct that in this case the EqReasoning is not<br>
necessary. If you look at the justifications I use in this equality<br>
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<br>
need a justification, they follow by computation (unfolding of<br>
definitions). Only the last step needs a non-trivial justification,<br>
a call to the induction hypothesis at position x ∷ _. "cong" has the<br>
role of telling which subterm should be rewritten by the induction<br>
hypothesis.<br>
<br>
Since there is only one non-trivial step, the equality chain can be<br>
collapsed into Julian's single-step proof. Equality chains are made<br>
for reasoning involving transitivity. I, however, find then also<br>
nice to document the proof in a human-readable way. Instead of<br>
doing the calculation on paper, I did it directly in Agda, using<br>
EqReasoning as notation.<br>
<br>
Cheers,<br>
Andreas<br>
<br>
<br>
On Nov 30, 2009, at 9:53 AM, Julian Beaumont wrote:<br>
<br>
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<br>
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><br></div></div><div class="im">
<mailto:<a href="mailto:graphov@gmail.com" target="_blank">graphov@gmail.com</a>>> wrote:<br>
<br>
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></div>
<mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>>><div class="im"><br>
<br>
<br>
Here is the file...<br>
<br>
<br>
<br>
<br>
On Nov 29, 2009, at 9:53 PM, Paul Graphov wrote:<br>
<br>
Yes, I am trying to do induction on xs, [] case is<br>
trivial but y::y' is<br>
not for me.<br>
On paper I just substitute y::x' in the definition<br>
of (_!_) and tabulate.<br>
<br>
EqReasoning looks quite difficult for me but I'll<br>
take a look, thanks.<br>
<br>
And yes, I can answer positively. But I don't see<br>
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></div>
<mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>>><div><div></div><div class="h5"><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<br>
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<br>
(_!_ xs) == xs<br>
lem-tab-! xs = {! !}<br>
<br>
I figured out the proof on the paper but can't<br>
translate it to Agda<br>
code...<br>
<br>
Can you be more specific? What does your paper<br>
proof look like and at<br>
which point does its implementation fail? Or do you<br>
just want to see a<br>
solution?<br>
<br>
<br>
If you can answer the last question positively,<br>
please consult the<br>
attachment. Basically, you need induction on xs and<br>
then equality<br>
reasoning. The latter is greatly simplified by the<br>
module EqReasoning in<br>
the standard library, if you know the right<br>
incantations to set it up,<br>
like local module opening and on the spot module<br>
specialization...<br>
<br>
.... where open Relation.Binary.EqReasoning (setoid<br>
(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>
<br>
</div></div></blockquote>
<br>
-- <br><div><div></div><div class="h5">
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
<a href="http://www.tcs.informatik.uni-muenchen.de/~abel/" target="_blank">http://www.tcs.informatik.uni-muenchen.de/~abel/</a><br>
</div></div></blockquote></div><br>