I am trying to define (1,2,3) as a set of elements in coq. I can define it using list as (1 :: (2 :: (3 :: nil))). Is there any way to define set in coq without using list.
3 Answers
The are basically four possible choices to be made when defining sets in Coq depending on your constraints on the base type of the set and computation needs:
If the base type doesn't have decidable equality, it is common to use:
Definition Set A := A -> Prop Definition cup A B := fun x => A x /\ B x. ...basically, Coq's Ensembles. This representation cannot "compute", as we can't even decide if two elements are equal.
If the base data type has decidable equality, then there are two choices depending if extensionality is wanted:
Extensionality means that two sets are equal in Coq's logic iff they have the same elements, formally:
forall (A B : set T), (A = B) <-> (forall x, x \in A <-> x \in B).If extensionality is wanted, sets should be represented by a canonically-sorted duplicate-free structure, usually a list. A good example is Cyril's Cohen finmap library. This representation however is very inefficient for computing as re-sorting is needed every time a set is modified.
If extensionality is not needed (usually a bad idea if proofs are wanted), you can use representations based on binary trees such as Coq's MSet, which are similar to standard Functional Programming set implementations and can work efficiently.
Finally, when the base type is finite, the set of all sets is a finite type too. The best example of this approach is IMO math-comp's finset, which encodes finite sets as the space of finitely supported membership functions, which is extensional, and forms a complete lattice.
-
-
2A bit informally, the reason is because of the extensional representation. A
{fset T}needs to be "sorted" every time is modified. On top of that, the "sorting" function is extremely inefficient as it will enumerate all possible lists until it gets the desired one. This helps to avoid having to equipTwith an order relation, as choice is guaranteed to be extensional on the predicate (in this case, the library picks the first list satisfying, P x := perm_eq x (undup s) IIRC), which implies extensionality. Commented Apr 14, 2016 at 3:45 -
Regarding your last bullet (base finite type) are you aware of any more lightweight implementations besides
finset? It is a part ofsslreflectwhich is a heavy dependency, which in addition comes with it's own language....– krokodilCommented Mar 28, 2017 at 3:10 -
Well, you have Robbert Krebbers' gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp , but I am not sure it is more "lightweight" , YMMV. ssreflect is surprisingly lightweight for the power it packs. Commented Mar 28, 2017 at 13:21
The standard library of coq provides the following finite set modules:
Coq.MSetsabstracts away the implementation details of the set. For instance, there is an implementation that uses AVL trees and another based onlists.Coq.FSetsabstracts away the implementation details of the set; it is a previous version ofMSets.Coq.Lists.ListSetis an encoding of lists as sets, which I am including for the sake of completeness
Here is an example on how to define a set with FSets:
Require Import Coq.Structures.OrderedTypeEx.
Require Import Coq.FSets.FSetAVL.
Module NSet := FSetAVL.Make Nat_as_OT.
(* Creates a set with only element 3 inside: *)
Check (NSet.add 3 NSet.empty).
There are many encodings of sets in Coq (lists, function, trees, ...) which can be finite or not. You should have a look at Coq's standard library. For example the 'simplest' set definition I know is this one
T -> Prop.