[Agda] simple question

[Andrew Harris]

@andreas and kyle,

Thanks -- it seems like the following definition type-checks:

{- proof of eq-succ -}
eq-succ : {n m : Nat} → n == m → succ n == succ m
eq-succ (refl m) = refl (succ m)

However, the exercise is to define this eq-succ function above that is to
be used in a proof of the equivalence of + versus "plus":

eq-plus-req : (n m : Nat) → (n + m) == (plus n m)
eq-plus-req n m = natrec (refl m) (\k' ih → eq-succ ih) n

(this function definition is provided in the paper).  However, this
function no longer typechecks, I think it has something to do with the
definition of eq-succ above.  In the paper, it says explicitly that the
eq-succ can be proved using "natrec" -- that's why I was trying to define
it with natrec in my original question.  I certainly do think that the
definition you suggested makes more sense to me but I'm wondering why it
causes eq-plus-req not to typecheck (here is the error I get):

Refuse to construct infinite term by instantiating _58 to succ
(_n_58 n m k')
when checking that the expression eq-succ ih has type
_n_58 n m (succ k') == _m_59 n m (succ k')

@mateusz and silvio,

Thanks for this suggestion.  I will investigate what "cong suc" means -- I
certainly don't know currently.  It is not something that I have seen
discussed in the previous sections of the paper that I'm reading.  And this
paper is serving as my introduction to Agda...

-andrew

On Tue, Oct 14, 2014 at 5:55 AM, <silvio at cs.ioc.ee> wrote:

> Hi All,
>
>  Hello,
>>>
>>>    I'm trying to follow along in the very good paper "Dependent Types At
>>> Work" written by Ana Bove and Peter Dybjer.  I'm stuck at trying to prove
>>> "eq-succ", which is one of the exercises in Section 4.4.  The closest I
>>> can
>>> make it is the following:
>>>
>>
> CUT
>
>
>> This is probably a stupid question considering I haven't looked at the
>> cited work, but what's wrong with just ?cong suc??
>>
>> --
>> Mateusz K.
>>
>
> I agree with Mateusz. This is actually how I did it when I was doing the
> same exercise.
>
> Best regards,
>
> Silvio
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141014/1ba22093/attachment.html