The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2016-06-27 2:32 GMT+02:00 Saulo Araujo <saulo2 AT gmail.com>:

Hi,

I am starting to study modules in Coq and I have a doubt regarding modules and sigma types. I have defined the module signature TotalMap, which is very similar to the one found in the book Interactive Theorem Proving and Software Development:

Module Type TotalMap.

Parameter Key: Set.

Parameter Value: Set.

Parameter TotalMap: Set.

Parameter get: TotalMap -> Key -> Value.

Parameter put: TotalMap -> Key -> Value -> TotalMap.

Axiom putMapsKeyToValue: forall (p: TotalMap) (k: Key) (v: Value), get (put p k v) k = v.

Axiom putRetainsOtherMappings: forall (p: TotalMap) (k1 k2: Key) (v: Value), k1 <> k2 -> get (put p k1 v) k2 = get p k2.

End TotalMap.

Now, I want to create an implementation called CompleteBinaryLeafTree, in which the parameter Key is the sigma-type {ds: list bool | length ds = n}, where n is a nat. I have tried to declare CompleteBinaryLeafTree as below:

Module CompleteBinaryLeafTree: TotalMap with Definition Key := {ds: list bool | length ds = n}.

but, of course, Coq complains about not knowing what is n.

I also have tried to declare CompleteBinaryLeafTree as a functor from nat to TotalMap:

Module CompleteBinaryLeafTree (n: nat): TotalMap with Definition Key := {ds: list bool | length ds = n}.

But Coq complains that nat is not a module.

I had success creating an "articial" module signature called NatContainer:

Module Type NatContainer.

Parameter n: nat.

End NatContainer.

and declaring CompleteBinaryLeafTree as a functor from NatContainer to TotalMap:

​​

Module CompleteBinaryLeafTree (c: NatContainer): TotalMap with Definition Key := {ds: list bool | length ds = c.n}.

Is there a "less artificial" way of creating an implementation of TotalMap, in which Key is the sigma-type {ds: list bool | length ds = c.n}?

Sincerely,

Saulo Araujo

​The first thing is to wonder if you really need modules.

Modules in Coq are often more cumbersome than raw records (or type classes), and can almost always be replaced by them.

If you really need them (for instance, because you use a library not designed to support other things than modules)​

 

​,

then you can try to make CompleteBinaryLeafTree live in a world where nat is already defined.

Something like

Parameter n:nat.​

​

​

Module CompleteBinaryLeafTree : TotalMap with Definition Key := {ds: list bool | length ds = n}.​

should work (but your n will be fixed, you cannot have various CompleteBinaryLeafTree with different values of n).