<div dir="ltr">If anyone&#39;s interested, here&#39;s a proof that `symIter` is complete. It uses `Data.Nat._+_` but just to make my life a bit easier; it could as well use `symIter id (suc ∘ suc)`.<div><br></div><div><a href="https://gist.github.com/gergoerdi/f0288a2f060400ceb13c">https://gist.github.com/gergoerdi/f0288a2f060400ceb13c</a><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 6, 2015 at 11:51 AM, Dr. ÉRDI Gergő <span dir="ltr">&lt;<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">Hang on a sec, in retrospect, isn&#39;t this exactly the same as defining a function in terms of min(x,y) and abs(x-y)? </p>
<p dir="ltr">I&#39;ll have to see how awkward it is in practice to prove it, but any commutative function</p>
<p dir="ltr">f : Nat -&gt; Nat -&gt; X</p>
<p dir="ltr">can be written as</p>
<p dir="ltr">f x y = h (min x y) (diff x y)</p>
<p dir="ltr">Which is of course also</p>
<p dir="ltr">h $ symIter (\b -&gt; (b, 0)) (\(b,s) -&gt; (b,su s)) x y</p>
<p dir="ltr">(Which is also a proof if symIter&#39;s completeness)<br>
</p><div class="HOEnZb"><div class="h5">
<div class="gmail_quote">On May 5, 2015 8:26 PM, &quot;Dr. ERDI Gergo&quot; &lt;<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>&gt; wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Tue, 5 May 2015, Conor McBride wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Here&#39;s an old exercise of mine. Given<br>
<br>
data Nat : Set where<br>
ze : Nat<br>
su : Nat -&gt; Nat<br>
<br>
symIter : {X : Set} -&gt; (Nat -&gt; X) -&gt; (X -&gt; X) -&gt; Nat -&gt; Nat -&gt; X<br>
symIter zen more ze          n  = zen n<br>
symIter zen more m          ze  = zen m<br>
symIter zen more (su m) (su n)  = more (symIter zen more m n)<br>
<br>
Then define max, min, addition and multiplication by instantiating zen and<br>
more appropriately.<br>
</blockquote>
<br>
OK, I&#39;ve done this exercise now. Multiplication is the odd one out that was tricky to implement; I wonder if there&#39;s a more straightforward way than mine?<br>
<br>
<a href="https://gist.github.com/gergoerdi/46ad83513fd9db65c286" target="_blank">https://gist.github.com/gergoerdi/46ad83513fd9db65c286</a><br>
<br>
Now the real question is, what is the general, (semi-)mechanizable way of going from (some description of) an argument type A to the definition of<br>
<br>
symIter :: {X : Set} -&gt; (A -&gt; X) -&gt; (X -&gt; X) -&gt; A -&gt; A -&gt; X<br>
<br>
?<br>
</blockquote></div>
</div></div></blockquote></div><br></div>