Finset and finmap are MathComp libraries defining finite sets of finite types and finite sets of choice types, respectively. Thus, it is not possible to create a finset-set of
nat, but it is possible to create a finmap-set of
nat, and it is possible to create both a finset-set and a finmap-set of
These libraries are similar in several ways, and knowing one brings you almost all the way to knowing the other. The main difference in notations is that finset notations use
":" to refer to set operations (eg
"A :|: B" for union), while finmap uses
"A `|` B"). The main difference in naming conventions is that finset uses
"set" where finmap uses
"fset". Make sure to at least skim the headers of each file before using it, and take particular note of the naming conventions described at the end of the finset header.
Some notes for finset:
- Some notions such as
\subsetare defined in fintype, which is a dependency of finset.
- Proving that two sets are equal is best accomplished through
setP(this translates equality to
x \in A <-> x \in B), unless there happens to already be a collection of lemmas that that let you reach your goal through direct rewriting.
A \subset Bis best accomplished through
subsetP, and similarly, a hypothesis that
A \subset Bwill probably be more useful under the
- Proving or manipulating statements of the form
[set _ | _]is best accomplished through
inEis useful to simplify expressions of the form
x \in X, where
Xincludes simplifyable set operations such as intersections, unions, etc. There are also views such as
setUPthat can be used in more or less the same contexts. Note that their names are easily guessable. Eg,
setUPis about union.
- Facts about operations with singletons, for example about
x |: X, can be found by searching for the operation about generic sets,
_ :|: _in this case. This is because
_ |: _is just a notation for
[set _] :|: _and often there are not specific lemmas for singletons (since their proofs would be the same as for their more generic counterparts).
- The notation for subset is now
- Continue using
inE. The views are named
- Same idea. Here notations for singletons are, eg,
_ |` _, which can be found by searching
_ `|` _.