<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&#39;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">2015-04-06 12:25 GMT+03:00 Serge Leblanc <span dir="ltr">&lt;<a href="mailto:33dbqnxpy7if@gmail.com" target="_blank">33dbqnxpy7if@gmail.com</a>&gt;</span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div bgcolor="#FFFFFF" text="#000000">
    <div>Thanks Dmytro, is trivial when x = 0,
      but I have more difficulty when x &gt; 0.<br>
      <br>
      <small><span class="">hermes≡hermes&#39; : (x y : ℕ) → hermes x y ≡ hermes&#39; x y<br></span>
        hermes≡hermes&#39; zero y = refl (suc y)<br>
        hermes≡hermes&#39; (suc x) y = { }0   {- ?0 : hermes (suc x) y ≡
        hermes&#39; (suc x) y -}</small><span class=""><br>
      <br>
      <br>
      On 2015-04-05 14:06, Dmytro Starosud wrote:<br>
    </span></div><span class="">
    <blockquote type="cite">
      <div>
        <div>
          <div>
            <div>
              <div>Hello Serge,<br>
                <br>
              </div>
              Now try to partially apply corresponding functions to the
              arguments you&#39;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 class=""><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>_______________________________________________<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>