[Agda] Newbie question, book exercise problem.

Andreas Abel andreas.abel at ifi.lmu.de
Wed Dec 2 19:43:43 CET 2009


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/


More information about the Agda mailing list