[Agda] How can we define a type of symmetric binary operations in Agda ?

[Dr. ÉRDI Gergő]

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)?

I'll have to see how awkward it is in practice to prove it, but any
commutative function

f : Nat -> Nat -> X

can be written as

f x y = h (min x y) (diff x y)

Which is of course also

h $ symIter (\b -> (b, 0)) (\(b,s) -> (b,su s)) x y

(Which is also a proof if symIter's completeness)
 On May 5, 2015 8:26 PM, "Dr. ERDI Gergo" <gergo at erdi.hu> wrote:

> On Tue, 5 May 2015, Conor McBride wrote:
>
>  Here's an old exercise of mine. Given
>>
>> data Nat : Set where
>> ze : Nat
>> su : Nat -> Nat
>>
>> symIter : {X : Set} -> (Nat -> X) -> (X -> X) -> Nat -> Nat -> X
>> symIter zen more ze          n  = zen n
>> symIter zen more m          ze  = zen m
>> symIter zen more (su m) (su n)  = more (symIter zen more m n)
>>
>> Then define max, min, addition and multiplication by instantiating zen and
>> more appropriately.
>>
>
> 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?
>
> https://gist.github.com/gergoerdi/46ad83513fd9db65c286
>
> 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
>
> symIter :: {X : Set} -> (A -> X) -> (X -> X) -> A -> A -> X
>
> ?
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150506/fae3ffd6/attachment.html