For instance at bare minimum, I am looking for something that
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
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 (
vector) are generally more the exception than the rule
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