The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Hello,

I am not entirely sure it answers your question but I have made a short developpement with multiple argument functions for reason which seem very similar to yours. It is done for sets (setoids) but the methodology seems general enough. 

It defines a type [ A1 ; ... ; An ] --> B for any list [ A1 ; ... ; An ]. The easiest way to realise that is to have a good product on your structure (cartesian product on sets, tensor product on monoids) and then fold it over the list and build a unary function that way. But it's not necessarily entirely satisfactory, or idiomatic. In this case it is defined as the type of curried functions    A1 -> ... -> An -> B which respect an appropriate morphism predicate. 
Note that this way, I cannot define the first projection as a coercion to Funclass, therefore I have to manage it somewhat manually. One might consider defining function so that they are at least unary ( something in the line of  [ A1 ; A2 ; ... ; An ] -> B for any list [ A2 ; ... ; An ] ) to retrieve the coercion.

Here comes the developpement, with real bits of unicode in it :

Delimit Scope set_scope with set.
Open Local Scope set_scope.

Class set :=
  carrier : Type ;
  equality : relation carrier ;
  equality_correction :> Equivalence equality
.
Coercion carrier : set >->Sortclass.
Notation  " a ≡ b " := (equality a b) (at level 70, no associativity) : set_scope.
Notation Local 𝕊 := set.

Fixpoint fcarrier (T:list 𝕊) (G:𝕊) : Type :=
    match T with
    | A::Γ => A -> (fcarrier Γ G)
    |  nil  => G
    end
 .

Fixpoint fsig (T:list 𝕊) (G:𝕊) : relation (fcarrier  T G) :=
  match T with
  | A::Γ => ( @equality A ==> (fsig Γ G) )%signature
  |  nil  =>   @equality G
  end
.

Class is_function (T:list 𝕊) (G:𝕊) (f:fcarrier T G) :=
  is_well_defined : Morphism (fsig T G) f
.
Instance partial (A:𝕊) (T:list 𝕊) (G:𝕊) (f:fcarrier (A::T) G) (_ : is_function _ _ f)(x:A)
                          : is_function T G (f x).
  intros until 0; intro ff; intro.
  apply is_well_defined.
  reflexivity.
Qed.

Class function (T:list 𝕊) (G:𝕊) :=
  procedure : fcarrier T G ;
  well_defined :> is_function _ _ procedure
.

2009/4/28 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