<div dir="ltr">If anyone's interested, here'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"><<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>></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't this exactly the same as defining a function in terms of min(x,y) and abs(x-y)? </p>
<p dir="ltr">I'll have to see how awkward it is in practice to prove it, but any commutative function</p>
<p dir="ltr">f : Nat -> Nat -> 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 -> (b, 0)) (\(b,s) -> (b,su s)) x y</p>
<p dir="ltr">(Which is also a proof if symIter's completeness)<br>
</p><div class="HOEnZb"><div class="h5">
<div class="gmail_quote">On May 5, 2015 8:26 PM, "Dr. ERDI Gergo" <<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>> 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's an old exercise of mine. Given<br>
<br>
data Nat : Set where<br>
ze : Nat<br>
su : Nat -> Nat<br>
<br>
symIter : {X : Set} -> (Nat -> X) -> (X -> X) -> Nat -> Nat -> 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've done this exercise now. Multiplication is the odd one out that was tricky to implement; I wonder if there'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} -> (A -> X) -> (X -> X) -> A -> A -> X<br>
<br>
?<br>
</blockquote></div>
</div></div></blockquote></div><br></div>