[Agda] Newbie question, book exercise problem.

[Andreas Abel]

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