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 `bool`

.

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 `"`"`

(eg `"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
`\subset`

are 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. - Proving
`A \subset B`

is best accomplished through`subsetP`

, and similarly, a hypothesis that`A \subset B`

will probably be more useful under the`subsetP`

view. - Proving or manipulating statements of the form
`[set _ | _]`

is best accomplished through`imsetP`

. `inE`

is useful to simplify expressions of the form`x \in X`

, where`X`

includes simplifyable set operations such as intersections, unions, etc. There are also views such as`setUP`

that can be used in more or less the same contexts. Note that their names are easily guessable. Eg,`setUP`

is 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).

Finmap equivalents:

- The notation for subset is now
`"`<=`"`

instead of`"\subset"`

- Use
`fsetP`

- Use
`fsubsetP`

- Use
`imfsetP`

- Continue using
`inE`

. The views are named`fsetUP`

, etc. - Same idea. Here notations for singletons are, eg,
`_ |` _`

, which can be found by searching`_ `|` _`

.