I tried looking for a multiset data structure in coq but I could't find exactly what I am looking for, I found this:
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-stdpp). Then Require-Import the files from the respective namespaces
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.
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
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
to_nat functions that would let you prove that
term is countable from a bijection with
Previous discussion with references on finite multisets.
Last updated: Jan 29 2023 at 01:02 UTC