Stream: Coq users

Topic: Multi Sets in coq


view this post on Zulip walker (Mar 20 2022 at 17:16):

I tried looking for a multiset data structure in coq but I could't find exactly what I am looking for, I found this:

https://coq.inria.fr/library/Coq.Sets.Multiset.html

But the data structure looks strange instead of being a normal array it is function that returns 0 or 1, I can imagine how this would work as set, like it would return 1 if the element exists, or zero otherwise, but I cannot see how can we extend this set or perform normal operations on it?

view this post on Zulip walker (Mar 20 2022 at 17:16):

I don't see a single example in there.

view this post on Zulip Julien Puydt (Mar 20 2022 at 17:17):

Why do you say it always returns 0 or 1 ?

view this post on Zulip Julien Puydt (Mar 20 2022 at 17:18):

(look at munion -- you'll see it can return much more)

view this post on Zulip walker (Mar 20 2022 at 17:18):

I am trying to find a multiset without the need to implement one

view this post on Zulip walker (Mar 20 2022 at 17:18):

(a set where elements can be repeated) that is all.

view this post on Zulip walker (Mar 20 2022 at 17:19):

not sure how to use coq's multiset this way

view this post on Zulip walker (Mar 20 2022 at 17:19):

the operation I am looking for are contains, add, remove and maybe maybe .. count. I cannot figure out how the standard library implementation support those

view this post on Zulip Julien Puydt (Mar 20 2022 at 17:20):

The SingletonBag and the union allows adding an element.

multiplicity is the count you're looking for.

view this post on Zulip Julien Puydt (Mar 20 2022 at 17:21):

For contains, it's just multiplicity > 0 ; for remove... that one I don't see in the file you point to.

view this post on Zulip walker (Mar 20 2022 at 17:22):

may I ask, what are things named in such strange way ?

view this post on Zulip Julien Puydt (Mar 20 2022 at 17:23):

But it should be pretty straightforward to implement a mdifference similar to munion.

The names looks pretty right. I would say you expected computer science words and mathematical words are used.

view this post on Zulip walker (Mar 20 2022 at 17:24):

yes coming from cs background the names looks fancy but hard to understand. Alright, I will try to see how can I implement stuff and come back with more questions, thanks.

view this post on Zulip Julien Puydt (Mar 20 2022 at 17:24):

No problem :-)

view this post on Zulip Karl Palmskog (Mar 20 2022 at 18:13):

also multisets here: https://github.com/math-comp/finmap/blob/master/multiset.v

view this post on Zulip Karl Palmskog (Mar 20 2022 at 18:13):

and here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/gmultiset.v

view this post on Zulip walker (Mar 20 2022 at 20:09):

what will be the best way to include those files If I ever decided to use them ?

view this post on Zulip walker (Mar 20 2022 at 20:11):

I mean including those external libraries

view this post on Zulip Karl Palmskog (Mar 20 2022 at 20:17):

use Coq's opam or the Coq Platform, where they are both included (packages coq-mathcomp-finmap and coq-stdpp). Then Require-Import the files from the respective namespaces mathcomp.finmap/stdpp

view this post on Zulip walker (Mar 20 2022 at 20:37):

I am total beginner here, what does Coq Platform mean is there a coq specific package manager ?

view this post on Zulip Karl Palmskog (Mar 20 2022 at 20:51):

the Coq Platform is a distribution of Coq together with many packages in addition to the standard library (which is small by comparison): https://github.com/coq/platform

view this post on Zulip Karl Palmskog (Mar 20 2022 at 20:52):

it's the recommended way to install Coq for beginners since there are binary installers that install both Coq and packages

view this post on Zulip Karl Palmskog (Mar 20 2022 at 20:56):

the "Coq package manager" is the OCaml package manager, opam, which is the foundation of the Coq Platform, but also usable independently of the Platform for Coq

view this post on Zulip walker (Mar 20 2022 at 21:10):

understood! thanks alot.

view this post on Zulip walker (Mar 21 2022 at 00:21):

I tried using iris's multiset but I am totally lost here!

I am basially following an implementation of some type theory book for untyped lambda calculus:

Require Import Coq.Strings.String.
Require Import stdpp.gmultiset.

Inductive term : Type  :=
| Var (v: string)
| App (t1: term) (t2: term)
| Lambda (x: string) (t: term).

Fixpoint subterm_model (t: term) : (gmultiset term). Admitted.

Generates error

Unable to satisfy the following constraints:
In environment:
t : term

?EqDecision0 : "EqDecision term"

?H : "Countable term"

I have rough understanding of what is missing, that is equality needs to be decidable and term should be countable (I cannot even understand the output of Print Countable Is there an easy to follow examples for using gmultiset ?

view this post on Zulip Notification Bot (Mar 21 2022 at 02:56):

Ivan Eric has marked this topic as resolved.

view this post on Zulip Notification Bot (Mar 21 2022 at 07:58):

walker has marked this topic as unresolved.

view this post on Zulip Andrew Hirsch (Mar 21 2022 at 10:05):

It looks to me (I'm no expert in std++) that Countable is asking that you are able to encode elements of term as bitstrings, and that you can decode bitstrings into term. It looks like the file Positive_as_OT contains of_nat and to_nat functions that would let you prove that term is countable from a bijection with Nat.

view this post on Zulip Olivier Laurent (Mar 21 2022 at 10:15):

Previous discussion with references on finite multisets.


Last updated: Jan 29 2023 at 01:02 UTC