<div dir="ltr"><div>@andreas and kyle,</div><div><br></div><div>Thanks -- it seems like the following definition type-checks:<br><br>{- proof of eq-succ -}<br>eq-succ : {n m : Nat} → n == m → succ n == succ m<br>eq-succ (refl m) = refl (succ m)<br><br></div><div>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":<br><br>eq-plus-req : (n m : Nat) → (n + m) == (plus n m)<br>eq-plus-req n m = natrec (refl m) (\k' ih → eq-succ ih) n<br><br></div><div>(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):<br><br>Refuse to construct infinite term by instantiating _58 to succ<br>(_n_58 n m k')<br>when checking that the expression eq-succ ih has type<br>_n_58 n m (succ k') == _m_59 n m (succ k')<br></div><div><br></div>@mateusz and silvio,<div class="gmail_extra"><br></div><div class="gmail_extra">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...<br><br>-andrew<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 14, 2014 at 5:55 AM, <span dir="ltr"><<a href="mailto:silvio@cs.ioc.ee" target="_blank">silvio@cs.ioc.ee</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi All,<span><br>
<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Hello,<br>
<br>
I'm trying to follow along in the very good paper "Dependent Types At<br>
Work" written by Ana Bove and Peter Dybjer. I'm stuck at trying to prove<br>
"eq-succ", which is one of the exercises in Section 4.4. The closest I can<br>
make it is the following:<br>
</blockquote></blockquote>
<br></span>
CUT<br>
<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span>
<br>
This is probably a stupid question considering I haven't looked at the<br></span>
cited work, but what's wrong with just ?cong suc??<br>
<br>
--<br>
Mateusz K.<br>
</blockquote>
<br>
I agree with Mateusz. This is actually how I did it when I was doing the same exercise.<br>
<br>
Best regards,<br>
<br>
Silvio<div><div><br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>