walker (Mar 20 2022 at 17:16): 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?
walker (Mar 20 2022 at 17:16):I don't see a single example in there.
Julien Puydt (Mar 20 2022 at 17:17):Why do you say it always returns 0 or 1 ?
Julien Puydt (Mar 20 2022 at 17:18):(look at munion -- you'll see it can return much more)
walker (Mar 20 2022 at 17:18):I am trying to find a multiset without the need to implement one
walker (Mar 20 2022 at 17:18):(a set where elements can be repeated) that is all.
walker (Mar 20 2022 at 17:19):not sure how to use coq's multiset this way
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
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.
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.
walker (Mar 20 2022 at 17:22):may I ask, what are things named in such strange way ?
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.
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.
Julien Puydt (Mar 20 2022 at 17:24):No problem :-)
Karl Palmskog (Mar 20 2022 at 18:13):also multisets here: https://github.com/math-comp/finmap/blob/master/multiset.v
Karl Palmskog (Mar 20 2022 at 18:13):and here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/gmultiset.v
walker (Mar 20 2022 at 20:09):what will be the best way to include those files If I ever decided to use them ?
walker (Mar 20 2022 at 20:11):I mean including those external libraries
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
walker (Mar 20 2022 at 20:37):I am total beginner here, what does Coq Platform mean is there a coq specific package manager ?
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
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
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
walker (Mar 20 2022 at 21:10):understood! thanks alot.
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 ?
Notification Bot (Mar 21 2022 at 02:56):Ivan Eric has marked this topic as resolved.
Notification Bot (Mar 21 2022 at 07:58):walker has marked this topic as unresolved.
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.
Olivier Laurent (Mar 21 2022 at 10:15):Previous discussion with references on finite multisets.
Last updated: Oct 13 2024 at 01:02 UTC