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?

I don't see a single example in there.

Why do you say it always returns 0 or 1 ?

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

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

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

not sure how to use coq's multiset this way

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

The SingletonBag and the union allows adding an element.

multiplicity is the count you're looking for.

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

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

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.

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.

No problem :-)

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

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

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

I mean including those external libraries

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`

I am total beginner here, what does `Coq Platform`

mean is there a coq specific package manager ?

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

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

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

understood! thanks alot.

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`

?

Ivan Eric has marked this topic as resolved.

walker has marked this topic as unresolved.

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`

.

Previous discussion with references on finite multisets.

Last updated: Jan 29 2023 at 01:02 UTC