The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Hello everyone.

We are building a small algebra library for working with semigroups, semirings and related structures.
Very often, the morphisms of those structures can be seen as having those structures themselves, e.g.


the morphisms between two semigroups can be given a semigroup structure by defining its operation as
f * g = x -> (f x) * (g x).

Right now we are taking advantage of this to define multi-argument morphisms in

a simple way using type classes. As an exemple, consider morphisms between setoids A and B
(noted A =>> B), i.e. maps between their underlying types that preserve the setoid equality. In our
implementation, members of this type are records of two fields: a regular function of type A -> B and
a proof that it preserves setoid equality. We declare a instance of the setoid class for A =>> B by letting
f == g <-> forall a, f a == g a. With this, we can state
that a function of two arguments preserves equality
for both arguments by saying it has type A =>> B =>> C.

The nice thing about this is that we are then able to get rewriting in functions of many arguments without

having to declare new morphisms to the rewriting system. The problem with it, however, is that 
it is very awkward to actually define these objects, because we must define several intermediate ones.
If we try to define the composition of two maps, with type (B =>> C) =>> (A =>> B) =>> A =>> C,
we must first define F : (B =>> C) -> (A =>> B) -> A =>> C, then show that for every f we can build
a (A =>> B) =>> A =>> C from (F f), then define F' : (B =>> C) -> (A =>> B) =>> A =>> C, and finally
show that F' preserves equality and from that get the desired result. Put another way, for each morphism
arrow we have a definition and one lemma to prove. If we have another kind of morphism built on top of
setoid morphisms (e.g., semigroup morphisms), the definitions will get even harder.

What I wanted to do then is to find a uniform way of easily defining these morphisms for arbitrary
structures. It could be a function that would build a big proposition combining the properties
required by each arrow and ask me to prove that proposition, or a tactic, or maybe another
way of defining those properties that would still make them easy to combine and give rewriting without
much pain. Does anyone know of such a way?

Thank you, and sorry for the lengthy message!


-- 
Arthur Azevedo de Amorim