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

[Conor McBride]

Just popping up briefly...

On 5 May 2015, at 10:27, Andreas Abel <abela at chalmers.se> wrote:

> Looks like you want a higher inductive type...
> 
> On 05.05.2015 08:27, Dr. ÉRDI Gergő wrote:
>> What about creating them such that they are symmetric by construction?

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)

First, show that

  symIter zen more

is always commutative.

Then define max, min, addition and multiplication by instantiating zen and
more appropriately.

The key to not seeing more than you should is to change your means of
looking.

All the best

Conor


>> If we had quotient types, one could easily make an "unordered pair"
>> type, and make unary relations over that.
>> 
>> Are there any useful tricks to do something similar in Agda?
>> 
>> On May 1, 2015 3:07 PM, "Andreas Abel" <abela at chalmers.se
>> <mailto:abela at chalmers.se>> wrote:
>> 
>>    You can create a record with two fields, one is your binary
>>    operation, the other the proof of symmetry.
>> 
>>    record SymBinOp : Set where
>>       field
>>         _⊙_ : BinaryOperation
>>         proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x
>> 
>>    That's it!
>> 
>>    On 30.04.2015 17:35, Sergey Kirgizov wrote:
>> 
>>        Hello,
>> 
>>        I don't  understand how  we can  define in Agda  a type  of
>>        "Symmetric
>>        Binary Relation". Can you help me?
>>        Imagine I have something like:
>> 
>>        =======================================================
>> 
>>        {-
>>            At first we reaname  Set
>> 
>>        {-
>>            First, we define a polymorphic idenity
>>        -}
>>        data _==_ {A : 𝓤} (a : A) : A → 𝓤 where
>>            definition-of-idenity : a == a
>>        infix 30 _==_
>> 
>>        {-
>>           Next we define the finite set Ω = {A,B,C}
>>        -}
>>        data Ω : 𝓤 where
>>            A B C : Ω
>> 
>>        {-
>>           We add a type "Binary operation"
>>        -}
>>        BinaryOperation = Ω → Ω → Ω
>> 
>>        {-
>>           I can actually define an example of Binary operation.
>>        -}
>>        _⊙_ : BinaryOperation
>>        x ⊙ x' = A
>>        infix 40 _⊙_
>> 
>>        {-
>>           And then I can proove that ⊙ is Symmetric
>>        -}
>>        proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x
>>        proof-of-symmetry = λ x y → definition-of-idenity
>> 
>> 
>>        ========================================================
>> 
>>        How we  can define a  type "Symmetric Binary Operation"?
>>          Having this
>>        type we will be able to define ⊙ as
>> 
>>        _⊙_ : SymmetricBinaryOperation
>>        x ⊙ y = A
>> 
>>        and proof that ⊙ is symmetric will no be required.
>> 
>> 
>>        Best regards,
>>        Sergey
>>        _______________________________________________
>>        Agda mailing list
>>        Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>        https://lists.chalmers.se/mailman/listinfo/agda
>> 
>> 
>> 
>>    --
>>    Andreas Abel  <><      Du bist der geliebte Mensch.
>> 
>>    Department of Computer Science and Engineering
>>    Chalmers and Gothenburg University, Sweden
>> 
>>    andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>>    http://www2.tcs.ifi.lmu.de/~abel/
>>    _______________________________________________
>>    Agda mailing list
>>    Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>    https://lists.chalmers.se/mailman/listinfo/agda
>> 
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
> 
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda