walker (Sep 20 2022 at 09:36): walker (Sep 20 2022 at 09:36):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.
Paolo Giarrusso (Sep 20 2022 at 10:01):set_solver handles such things for stdpp sets
Alexander Gryzlov (Sep 20 2022 at 13:49):https://coq.inria.fr/library/Coq.MSets.MSetDecide.html seems to extend fsetdec tactic to Msets
walker (Sep 20 2022 at 16:03):That is perfect, I found stdpp not easy to work with
walker (Sep 21 2022 at 14:15):@Alexander Gryzlov is there a tutorail on how to use fsetdec, I started at the implementation yesterday long enough with no results.
walker (Sep 21 2022 at 14:17):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).
Paolo Giarrusso (Sep 21 2022 at 17:31):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.
Paolo Giarrusso (Sep 21 2022 at 17:32):autorewrite can be extended with propositional equalities if desired (but its performance isn't great, for Coq-specific reasons)
Paolo Giarrusso (Sep 21 2022 at 17:33):data structures where simpl works well (nat, list, fin and vector) are generally more the exception than the rule
Alexander Gryzlov (Sep 21 2022 at 20:25):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.
walker (Sep 21 2022 at 20:27):noted, thanks a lot.
Last updated: Apr 19 2024 at 11:02 UTC