[Agda] Newbie question, book exercise problem.

[Paul Graphov]

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)"?

Thanks.

2009/11/30 Andreas Abel <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> wrote:
>>
>>> It's much more complicated than I expected...
>>> Thanks a lot!
>>> 2009/11/30 Andreas Abel <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>
>>>>>
>>>>> 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
>>>> INRIA, Projet Pi.R2
>>>> 23, avenue d'Italie
>>>> F-75013 Paris
>>>> Tel: +33.1.39.63.59.41
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>>  _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
> Andreas ABEL
> INRIA, Projet Pi.R2
> 23, avenue d'Italie
> F-75013 Paris
> Tel: +33.1.39.63.59.41
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091202/1eb1ac18/attachment.html