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

[Sergey Kirgizov]

On Tue, May 05, 2015 at 10:35:00AM +0100, Conor McBride wrote:
> 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.

Indeed  "symIter"  is  a  beautiful  solution  for  defining  symetric
operations over finite  and denumerable sets.

Do I understand correctly that it will work only with finite and denumerable sets?
Imaginde, for example that we have defined Real numbers in Agda.
Than, we cannot directly use symIter in order to define x:Real + y:Real.

_+_ : Real → Real → Real
_+_ = symIter ? ??

Can we write something like symIter but without using Nat ?

Best
Sergey

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