Thanks again, now it is clear!<br><br><div class="gmail_quote">2009/12/2 Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;</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 &quot;cong (λ xs → x ∷ xs) (lem-tab-! xs)&quot; 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 &quot;x ∷ tabulate ((λ {.x} → _!_ (x ∷ xs)) ∘ fsuc)&quot;<br>
<br>
How to know that it can evaluate it to &quot;x ∷ tabulate(_!_ xs)&quot;?<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 -&gt; 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 -&gt; ((_!_ (x ∷ xs)) ∘ fsuc) i)<br>
<br>
which is<br>
<br>
  tabulate (\ i -&gt; (x :: xs) ! (fsuc i))<br>
<br>
by definition of tabulate, reducing to<br>
<br>
  tabulate (\ i -&gt; 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 &lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a> &lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;&gt;<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 &quot;refl&quot; 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 ∷ _. &quot;cong&quot; 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&#39;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&#39;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 -&gt; B) -&gt; x == y -&gt; 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 &lt;<a href="mailto:graphov@gmail.com" target="_blank">graphov@gmail.com</a><br></div></div><div class="im">
        &lt;mailto:<a href="mailto:graphov@gmail.com" target="_blank">graphov@gmail.com</a>&gt;&gt; wrote:<br>
<br>
            It&#39;s much more complicated than I expected...<br>
            Thanks a lot!<br>
            2009/11/30 Andreas Abel &lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br></div>
            &lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;&gt;<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&#39; is<br>
                    not for me.<br>
                    On paper I just substitute y::x&#39; in the definition<br>
                    of (_!_) and tabulate.<br>
<br>
                    EqReasoning looks quite difficult for me but I&#39;ll<br>
                    take a look, thanks.<br>
<br>
                    And yes, I can answer positively. But I don&#39;t see<br>
                    any attachment.<br>
<br>
                    Thanks!<br>
<br>
                    2009/11/29 Andreas Abel &lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br></div>
                    &lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;&gt;<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 &quot;Dependently typed programming in<br>
                    Agda&quot; 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} -&gt; Vec A n -&gt; Fin n -&gt; A<br>
                    []        ! ()<br>
                    (x :: xs) ! fzero    = x<br>
                    (x :: xs) ! (fsuc i) = xs ! i<br>
<br>
                    tabulate : {n : Nat}{A : Set} -&gt; (Fin n -&gt; A) -&gt; 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) -&gt; tabulate<br>
                    (_!_ xs) == xs<br>
                    lem-tab-! xs = {! !}<br>
<br>
                    I figured out the proof on the paper but can&#39;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&#39;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  &lt;&gt;&lt;      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>