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

[Dr. ÉRDI Gergő]

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)`.

https://gist.github.com/gergoerdi/f0288a2f060400ceb13c

On Wed, May 6, 2015 at 11:51 AM, Dr. ÉRDI Gergő <gergo at erdi.hu> wrote:

> 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/20150507/cdbfcc3a/attachment.html