For instance at bare minimum, I am looking for something that

reduces `union empty (singleton x)`

to `singleton x`

directly (and be equally rich to the List API in coq)

At best I would love to see some automatic solver that solves things like

`Subset (singleton x) (union empty (singleton x))`

or `Subset empty (union empty (singleton x))`

automatically the way lia works.

Intitively I know that those are easily solvable for finite sets, so I imagine someone already did it somewhere in coq but I cannot find it in the documentation.

set_solver handles such things for stdpp sets

https://coq.inria.fr/library/Coq.MSets.MSetDecide.html seems to extend `fsetdec`

tactic to Msets

That is perfect, I found stdpp not easy to work with

@Alexander Gryzlov is there a tutorail on how to use fsetdec, I started at the implementation yesterday long enough with no results.

Also I am curious why Msets do not simplify.

For instance I imagined that `union (singleton x) empty`

will be reduce via a `simpl`

to `singleton x`

, but it didn't, which makes me wonder if computations on Msets are not easy to perform (especially when transpiling coq code to something else).

I haven't run the code, but I'll note those are distinct questions: `union (singleton x) empty`

is not an "actual computation" in the sense you mean — it has a free variable. `simpl`

only ever applies some _definitional_ equalities; an equality that requires a case-split on a sum to prove is already guaranteed to not be definitional.

`autorewrite`

can be extended with propositional equalities if desired (but its performance isn't great, for Coq-specific reasons)

data structures where `simpl`

works well (`nat`

, `list`

, `fin`

and `vector`

) are generally more the exception than the rule

walker said:

Alexander Gryzlov is there a tutorail on how to use fsetdec, I started at the implementation yesterday long enough with no results.

I haven't seen a proper tutorial, but e.g. https://github.com/fasapa/nominalsets/blob/main/theories/Atom/MSetNotin.v has a bunch of MSet-related lemmas that are solvable by it.

noted, thanks a lot.

Last updated: Jan 28 2023 at 07:30 UTC