0
$\begingroup$

I am a beginner and trying to figure out how to work with finite sets and maps in Coq. I want to define an inductive type X with a single constructor that takes as an argument a finite set of elements of type X, for example:

Inductive X : Set := | constr : FinSet X -> X.

I am unsure which data structure to use for finite sets here. I looked into the std++ library but do not understand the data structure provided there: Set_ seems to require two types, A and C, and I do not know why the second type C is needed. Ideally I want a finite set constructor that takes one type as an argument (the type of elements), which is countable but not necessarily ordered. I am a beginner so I have a hard time reading Coq library files; can someone maybe post a code snippet? Thank you.

Improve this question
New contributor
anonymous is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
4
  • 1
    $\begingroup$ In stdpp the type you want to use is gset, defined in gmap.v. $\endgroup$
    – JoJoModding
    Commented Sep 2 at 16:53
  • $\begingroup$ @JoJoModding Thank you, I tried it but it does not work: Unable to satisfy the following constraints: In environment: X : Type ?EqDecision0 : "base.RelDecision eq" ?H : "countable.Countable X" It seems the issue is that by using gset inside an inductive definition, Coq does not automatically derive countability. $\endgroup$
    – anonymous
    Commented Sep 2 at 17:09
  • $\begingroup$ Ah, yes, it does not. That is unfortunate, but I don't think this can be fixed. $\endgroup$
    – JoJoModding
    Commented Sep 2 at 17:17
  • 1
    $\begingroup$ This is not a research-level question in theoretical computer science, so it does not belong here. But it does belong on proofassistants.stackexchange.com, so perhaps you should ask it there instead. $\endgroup$
    – Andrej Bauer
    Commented Sep 4 at 15:40

1 Answer 1

Reset to default
0
$\begingroup$

I usually use

Definition finite X : Prop := exists l, forall x : X, In x l.
Definition fin {X} (P : X -> Prop) := exists l, forall x, P x <-> In x l.

These ones have quite good properties.

Improve this answer
New contributor
Dominique Larchey-Wendling is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.