The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I guess that by "Resource" in your mail you meant "thing" (or the reverse, the point being that they identify the same thing), that in the example you have in mind, the constructors of thing really need S, and that you meant FSet (or MSet) and not WSet (which I have never heard of).

If these assumptions are correct, then you could use parameterized modules:

Module Type GroupModule.
  Parameter Group : Type.
  (* Put here some stuff you want about your Group types *)
End GroupModule.

Module ThingMod (G : GroupModule).
  Definition t := Resource G.Group.
  Function eq (x y : Resource G.Group) : Prop := …
End ThingMod.

Then you can define a functor from GroupModule to FSet with something like:

Module FSetGroup (G : GroupModule).
  Module T := ThingMod(G).
  Module GroupSet := FSet.Create(T).
End FSetGroup.

Not sure of the name of the FSet constructor FSet.Create, as I am not really used to modules (Coq Record/Class is often way more convenient). In general, I think twice before defining/using a module/functor in Coq.


You can also do a

Module ThingMod.
  Definition t := forall (S : Group), Resource S.
  Function eq (x y: forall (S : Group), Resource S): Prop :=
   (...)
End ThingMod.

But that is probably not what you want, as the elements will be functions from Group to Resources built on that Group.

2014-04-17 18:05 GMT+02:00 Jaap Boender <jaapb AT kerguelen.org>:

Hello all,

I'm trying to implement a calculus in Coq, which involves the following
inductive type (minimalised a bit, but this is the idea):

Parameter Atom: Type.
Parameter Group: Type
Inductive thing (S: Group): Type :=
  nd_atom: Atom -> thing S
| nd_impl: thing S -> thing S -> thing S
| nd_and: thing S -> thing S -> thing S
| nd_or: thing S -> thing S -> thing S.

I'd now like to create sets of 'thing'  using FSets, so I've put thing in a
module, which contains things like

Module ThingMod.
  Definition t := Resource.
  Function eq {S: Group} (x y: Resource S): Prop :=
   (...)
End ThingMod.

and now I'm trying to define a WSet based on this module, but I'm running into
a problem: my ThingMod.t is not  a Type, but a Group -> Type. That's not
surprising, but what I've been wrestling with: is there a way to lift this
Group parameter to the module level? I'd like to be able to define sets that
are parametrised by S, such that the elements of these sets are all of type
'thing S' - but I haven't been able to find how. Am I overlooking something
really basic, or is this just not possible? Or should I do this differently?
Any help would be appreciated.

thanks,

  Jaap

--
.../Sedrikov\...