[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