Stream: Coq users

Topic: Is there ready to uses lemmas for MsetAVL.


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 20 2022 at 10:01):

set_solver handles such things for stdpp sets

view this post on Zulip Alexander Gryzlov (Sep 20 2022 at 13:49):

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

view this post on Zulip walker (Sep 20 2022 at 16:03):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip walker (Sep 21 2022 at 20:27):

noted, thanks a lot.


Last updated: Jan 28 2023 at 07:30 UTC