Hello, I am trying to use the Coq.MSets functionality to make finite sets. Using it for types with no dependent parameters is easy enough, for instance:
Definition edge : Set := nat * nat.
Module Edge_OT := OrdersEx.PairOrderedType OrdersEx.Nat_as_OT OrdersEx.Nat_as_OT.
Module Edge_set := MSets.MSetList.Make Edge_OT.
Example a : Edge_set.t := (* something like this *)
Edge_set.union (Edge_set.singleton (0, 1)) (Edge_set.singleton (0, 2)).
However, I run into trouble when I try to do the same thing for a dependent type:
(* or equivalently, { value : nat | value < bound } *)
Inductive range_nat (bound : nat) :=
| range_nat_cons :
forall value : nat,
value < bound ->
range_nat bound.
Module Range_nat_as_OT
<: Orders.TotalOrder <: Equalities.DecidableType <: Orders.OrderedType
.
Parameter bound : nat.
Definition t := range_nat bound.
(* ...here I define/prove all necessary functions and properties... *)
End Range_nat_as_OT.
Now I can type Module Range_nat_set := MSets.MSetList.Make Range_nat_as_OT. but I cannot use Range_nat_set.t as a set type in other modules/function parameters (more specifically, I would like to have bound depend on the size of another data structure), because bound is a Parameter within the ordered type module and does not have a concrete value.
What I would love to do is Module Range_nat_set (bound : nat) := MSets.MSetList.Make (Range_nat_as_OT bound). but this does not work because you cannot parameterize a module over a term.
Is there a way in the standard library to get a set type over a dependent type? Or do I have to implement a finite set data structure (and all properties) myself…
Indeed, that is the problem, not MSets or any library: a plain Parameter declaration is synonym with an Axiom, OTOH you cannot parametrize a Module by an arbitrary term, the parameter must be a Module Type…
So, I am far from being an expert of Coq’s module system, but here is a basic scheme to write your own parametrized modules (called “functors”, i.e. module constructors):
(** Your library: **************** *)
Inductive range_nat (bound : nat) :=
| range_nat_cons :
forall value : nat,
value < bound ->
range_nat bound.
Module Type RangeNatSpec.
Parameter bound : nat.
End RangeNatSpec.
Module RangeNat (Spec : RangeNatSpec).
Include Spec.
Definition range := range_nat bound.
End RangeNat.
(** Now let's use it: **************** *)
Module Range10Spec <: RangeNatSpec.
Definition bound := 10.
End Range10Spec.
Module Range10 := RangeNat Range10Spec.
Import Range10.
Check eq_refl : bound = 10.
Check eq_refl : range = range_nat 10.
Thank you, that already definitely helps with understanding how modules are supposed to be used. However, I’m still not sure if there’s a way to define a function like the following, where the bound parameter really depends on a term and is not ever a constant:
Module Type GraphSpec.
Parameter g : graph.
End GraphSpec.
Module BoundByGraphSize (Spec : GraphSpec) <: RangeNatSpec.
Include Spec.
Definition bound := node_count g.
End GraphSize.
Module Impl (Spec : GraphSpec).
Include Spec.
Fixpoint bfs' (queue : (*not sure how to write this *)) := (* ...use g here... *).
End Impl.
and now I am forced to encapsulate everything that depends on a graph instance in a module of their own, and it becomes modules all the way down. I’d really like to avoid this and ultimately have a simple function definition without modules around it. I will never really have a concrete graph instance that I can implement a module for like above, since I am attempting to prove the correctness of certain algorithms and ultimately extract them.
Additionally, this approach will not work if I try to do a recursive call on a different g, say if I remove an edge but the number of nodes stays the same.
When a data structure uses modules you can’t escape it, sadly.
Instead, there are other data structure implementations without modules, such as stdpp’s fin_maps. These are not comparison-based (i.e., balanced trees), but there could be other implementations out there.
Why? What is the problem you are talking about? Of course one wouldn’t use code structuring with modules in place of definitions of dependent types: other than that, I don’t see the issue (the issue with modules)…
You can’t define a function that uses an MSet whose type depends on the function’s parameter. You are forced to define a functor, which is a second-class citizen in the language, unlike an actual Gallina term.
It shouldn’t be hard to write a DFS on a graph, but as soon as you need to define an order structure on the graph’s nodes to enable finite sets and maps, you have to put the graph in a module (or choose a representation where the type of graph nodes is unbundled from the graph).
Thank you all. I think I will look at a different finite set library like the stdpp library you mentioned, because it doesn’t seem possible to define my bfs function the way I want with MSets, and I also find working with modules like this rather unwieldy.