[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