<div dir="ltr">A good rule of thumb is that if you want to prove something about a function (like hermes),<div>the proof should follow the same recursion pattern as the function.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 6, 2015 at 7:34 PM, Dmytro Starosud <span dir="ltr"><<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@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>If you get stuck using pattern matching on first argument try to split using another...<br></div><br>Cheers,<br>Dmytro<br><br>P.S. actually theorem proving is undecidable in general:-D so you shouldn't except to get all the knowledge required for this in one go (and even in many;)).<br></div><div>I would suggest you first just try to repeat some existing profs to become familiar with this process.<br><br></div><br><br><br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">2015-04-06 12:25 GMT+03:00 Serge Leblanc <span dir="ltr"><<a href="mailto:33dbqnxpy7if@gmail.com" target="_blank">33dbqnxpy7if@gmail.com</a>></span>:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
<div bgcolor="#FFFFFF" text="#000000">
<div>Thanks Dmytro, is trivial when x = 0,
but I have more difficulty when x > 0.<br>
<br>
<small><span>hermes≡hermes' : (x y : ℕ) → hermes x y ≡ hermes' x y<br></span>
hermes≡hermes' zero y = refl (suc y)<br>
hermes≡hermes' (suc x) y = { }0 {- ?0 : hermes (suc x) y ≡
hermes' (suc x) y -}</small><span><br>
<br>
<br>
On 2015-04-05 14:06, Dmytro Starosud wrote:<br>
</span></div><span>
<blockquote type="cite">
<div>
<div>
<div>
<div>
<div>Hello Serge,<br>
<br>
</div>
Now try to partially apply corresponding functions to the
arguments you've got after pattern matching.<br>
</div>
I.e. Think what would you get <span style="font-family:monospace,monospace">hermes x y</span>
if <span style="font-family:monospace,monospace">x</span>
were <span style="font-family:monospace,monospace">zero</span>.<br>
</div>
And the same for <span style="font-family:monospace,monospace">fold</span>.<br>
<br>
</div>
You can use _ for the right hand side and compile your file to
see what you need to place there.<br>
<br>
</div>
Hope this will help.</blockquote>
<br>
<br>
</span><span><div>-- <br>
Serge Leblanc
<hr>
gpg --keyserver hkp://<a href="http://keyserver.ubuntu.com:11371" target="_blank">keyserver.ubuntu.com:11371</a> --recv-keys
0x67B17A3F
<br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
</span></div>
<br></div></div><span class="">_______________________________________________<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/mailman/listinfo/agda</a><br>
<br></span></blockquote></div><br></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>