<div dir="ltr">Induction is not needed here:<div><br></div><div><span style="font-family:'courier new',monospace;font-size:13px">eq-succ : {n m : Nat} → n == m → succ n == succ m</span><br style="font-family:'courier new',monospace;font-size:13px"><span style="font-family:'courier new',monospace;font-size:13px">eq-succ (refl m) = refl (succ x)</span></div><div><span style="font-family:'courier new',monospace;font-size:13px"><br></span></div><div>I am not certain of the details, but I believe that the pattern <span style="font-family:'courier new',monospace;font-size:13px">(refl m)</span> makes it so you only need to prove <span style="font-size:13px;font-family:'courier new',monospace">succ m == succ m</span> because of unification.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 13, 2014 at 7:13 PM, Andrew Harris <span dir="ltr"><<a href="mailto:andrew.unit@gmail.com" target="_blank">andrew.unit@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hello,<br><br></div> 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:<br><br><span style="font-family:courier new,monospace">{- proof of eq-succ -}<br>eq-succ : {n m : Nat} → n == m → succ n == succ m<br>eq-succ (refl m) = natrec {(\k → (k + m) == (plus k m))} (refl m) (\i h → ((succ i) + m) == (plus (succ i) m)) m<br><br></span></div><span style="font-family:courier new,monospace"><font face="arial,helvetica,sans-serif">But this does not typecheck</font>, I get the error:<br><br>Set !=< (succ i + m) == plus (succ i) m of type Set₁<br>when checking that the expression (succ i + m) == plus (succ i) m<br>has type (succ i + m) == plus (succ i) m<br><br></span></div><span style="font-family:courier new,monospace"><font face="arial,helvetica,sans-serif">I'm stuck -- I don't quite understand what I'm supposed to create an element of Set_1 that has a signature of </font></span><span style="font-family:courier new,monospace">(succ i + m) == plus (succ i) m, <span style="font-family:arial,helvetica,sans-serif">(if that's what I'm supposed to do). Any hints would be appreciated!</span><span class="HOEnZb"><font color="#888888"><br></font></span></span><span class="HOEnZb"><font color="#888888"><div><div><div><br></div><div>-andrew<br></div></div></div></font></span></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>