[Agda] Newbie question, book exercise problem.

Paul Graphov graphov at gmail.com
Fri Dec 4 22:13:34 CET 2009


Thanks again, now it is clear!

2009/12/2 Andreas Abel <andreas.abel at ifi.lmu.de>

> Paul Graphov a écrit :
>
>  Thank you guys,
>>
>> There is one thing that is not clear to me yet. Actually "cong (λ xs → x ∷
>> xs) (lem-tab-! xs)" gives Agda proof that
>> x ∷ tabulate(_!_ xs) ≡ x ∷ xs
>>
>> but how Agda knows that tabulate(_!_ (x ∷ xs)) is the same as x ∷
>> tabulate(_!_ xs) ?
>>
>> 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)"
>>
>> How to know that it can evaluate it to "x ∷ tabulate(_!_ xs)"?
>>
>
> Agda has eta-equality built in so you can always replace a term t by its
> eta-expansion
>
>  \ x -> t x   (where x is a fresh variable)
>
> Agda does not distinguish between these two. So
>
>  tabulate ((_!_ (x ∷ xs)) ∘ fsuc)
>
> is the same as
>
>  tabulate (\ i -> ((_!_ (x ∷ xs)) ∘ fsuc) i)
>
> which is
>
>  tabulate (\ i -> (x :: xs) ! (fsuc i))
>
> by definition of tabulate, reducing to
>
>  tabulate (\ i -> xs ! i)
>
> eta-reducing to
>
>  tabulate (_!_ xs)
>
> This step is actually documented in my proof (justified by the second
> refl).
>
> Cheers,
> Andreas
>
>
>  2009/11/30 Andreas Abel <andreas.abel at ifi.lmu.de <mailto:
>> andreas.abel at ifi.lmu.de>>
>>
>>
>>    Julian is correct that in this case the EqReasoning is not
>>    necessary.  If you look at the justifications I use in this equality
>>    chain
>>
>>     begin
>>       tabulate (_!_ (x ∷ xs))
>>     ≡⟨ refl ⟩
>>       (x ∷ xs) ! zero ∷ tabulate (λ i → (x ∷ xs) ! (suc i))
>>     ≡⟨ refl ⟩
>>       x ∷ tabulate (λ i → xs ! i)
>>     ≡⟨ cong (λ xs → x ∷ xs) (lem-tab-! xs) ⟩
>>       x ∷ xs
>>>>
>>    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.
>>
>>    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.
>>
>>    Cheers,
>>    Andreas
>>
>>
>>    On Nov 30, 2009, at 9:53 AM, Julian Beaumont wrote:
>>
>>        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
>>        <mailto: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
>>            <mailto: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
>>                    <mailto: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  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> http://www.tcs.informatik.uni-muenchen.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091205/e6257192/attachment.html


More information about the Agda mailing list