stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-09-06T14:07:30Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/567Stronger sorted unique lemmas2024-09-06T14:07:30ZRobbert KrebbersStronger sorted unique lemmasAdd lemmas `Sorted_unique'` and `StronglySorted_unique'` that only require anti symmetry for the elements that are in the list.Add lemmas `Sorted_unique'` and `StronglySorted_unique'` that only require anti symmetry for the elements that are in the list.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/565Draft: Add law `map_fold_foldr` to `FinMap` interface.2024-09-02T19:36:56ZRobbert KrebbersDraft: Add law `map_fold_foldr` to `FinMap` interface.See the discussion at https://mattermost.mpi-sws.org/iris/pl/dmdsga9stjgebfwwnjmike56do
This rule expresses a form of "parametricity": it says that regardless of `A`, `B`, `f`, and `b`, the function `map_fold f b m` will always travers...See the discussion at https://mattermost.mpi-sws.org/iris/pl/dmdsga9stjgebfwwnjmike56do
This rule expresses a form of "parametricity": it says that regardless of `A`, `B`, `f`, and `b`, the function `map_fold f b m` will always traverse the map `m` in the same order. Namely the order of converting the map into a list.
This law holds for all instances of `FinMap` we currently have, and I think without weird non-constructive axioms (that allow one to define non-parametric functions) it is impossible to define a `FinMap` instance that does *not* satisfy this law.
/cc @johannes @ivanbakelhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/564Generalize `map_relation` and `map_included` / Add `map_Forall2`.2024-09-03T10:26:40ZRobbert KrebbersGeneralize `map_relation` and `map_included` / Add `map_Forall2`.`map_Forall` and the big ops in Iris also take the key, so this makes `map_relation` consistent with that.
This also allowed me to add `map_Forall2` (defined using `map_relation`) in a way that is consistent with `map_Forall`.
This cha...`map_Forall` and the big ops in Iris also take the key, so this makes `map_relation` consistent with that.
This also allowed me to add `map_Forall2` (defined using `map_relation`) in a way that is consistent with `map_Forall`.
This change is not backwards compatible, but I expect little breakage. `map_relation` is mostly used internally to define `(⊆)`, `map_disjoint`, `map_agree`. And aside from a `Decision` instance there is very little theory about `map_relation`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/563Add lemma `fmap_insert_inv`.2024-08-30T09:02:59ZRobbert KrebbersAdd lemma `fmap_insert_inv`.For other operations (empty, singleton) we have a similar lemma. This one is missing.
I had to move some things around in the file, and re-proved `map_fmap_singleton_inv` using the new lemma.For other operations (empty, singleton) we have a similar lemma. This one is missing.
I had to move some things around in the file, and re-proved `map_fmap_singleton_inv` using the new lemma.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/562Add lower bound lemma for finite sets2024-08-30T09:47:45ZLennard Gähergaeher@mpi-sws.orgAdd lower bound lemma for finite setsForked off from the discussion here: https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/38#note_104108
This adds a variant of `minimal_exists` which does not require the set to be non-empty, but in return also does not guarant...Forked off from the discussion here: https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/38#note_104108
This adds a variant of `minimal_exists` which does not require the set to be non-empty, but in return also does not guarantee that the element is part of the set.
I'm not sure what the best naming for this lemma is. Maybe it should be called `infimum_exists` instead of `lower_bound_exists`? Should it be prefixed by `set`, like many other lemmas in the file for which it is not directly clear it's related to sets? (and should `minimal_exists` be prefixed accordingly?)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/561Allow `map_imap` to be used in nested recursive fixpoints.2024-08-27T19:24:27ZRobbert KrebbersAllow `map_imap` to be used in nested recursive fixpoints.See the test file for an example.
I expect this change to be backwards compatible. Since the definition of `map_imap` is awful, I don't expect anyone to use it directly (i.e., perform `unfold map_imap` in proofs), but rather use `map_lo...See the test file for an example.
I expect this change to be backwards compatible. Since the definition of `map_imap` is awful, I don't expect anyone to use it directly (i.e., perform `unfold map_imap` in proofs), but rather use `map_lookup_imap` or other lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/560Rename `X_length` into `length_X`.2024-08-16T08:44:34ZRobbert KrebbersRename `X_length` into `length_X`.This follows https://github.com/coq/coq/pull/18564
This closes #213
We didn't include our own copies of `app_length` and `seq_length`, but used those from the standard library. To make sure we can use them (without deprecation warnings...This follows https://github.com/coq/coq/pull/18564
This closes #213
We didn't include our own copies of `app_length` and `seq_length`, but used those from the standard library. To make sure we can use them (without deprecation warnings) until support for Coq 8.19 is dropped, I included our own copies for the transition period. This was also suggested by @tchajed in #213.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/559Use gmake for BSD systems2024-07-31T17:00:23ZYiyun LiuUse gmake for BSD systemsThis PR modifies the `make-package` script so it runs on systems whose default `make` executable is BSD Make rather than GNU Make. It checks the os type and decides whether to run `gmake` or `make`. This is exactly how `opam` determines ...This PR modifies the `make-package` script so it runs on systems whose default `make` executable is BSD Make rather than GNU Make. It checks the os type and decides whether to run `gmake` or `make`. This is exactly how `opam` determines which `make` executable to use.
I also changed the script to use `sh` instead of `bash` because `make-package` doesn't seem to depend on bash-specific features and sh has a more standard path.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/558docs: quick typo fixes2024-07-19T19:16:21ZSanjit Bhatdocs: quick typo fixeshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/557docs(gmap): add galina escaping2024-07-19T13:47:03ZSanjit Bhatdocs(gmap): add galina escapingThis fixes #211. I checked this locally with coqdoc.This fixes #211. I checked this locally with coqdoc.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/556Fix convention in gitlab config.2024-06-17T08:34:27ZRodolphe LepigreFix convention in gitlab config.Something I messed up in the dune MR.Something I messed up in the dune MR.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses2024-09-10T15:14:47ZMichael SammlerDon't constraint template polymorphic universes of list and option redefining `MBind` and related typeclassesThis is an idea how to fix https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and #207 . Since `M` never appears unapplied, it should not introduce the universe constraints. Note that the universe of `gmap` and `gset` and similar remain c...This is an idea how to fix https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and #207 . Since `M` never appears unapplied, it should not introduce the universe constraints. Note that the universe of `gmap` and `gset` and similar remain constrained due to the `MonadSet` and `FinMap` typeclasses.
In particular, with
```
Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
Global Instance x : MBind list.
Admitted.
Print Universes.
```
one gets the contraint `list.u0 = MBind.u0`.
But with
```
Class MBind' (A MA MB : Type) := mbind : (A → MB) → MA → MB.
Notation MBind M := (∀ A B, MBind' A (M A) (M B)).
Global Instance x : MBind list.
Admitted.
Print Universes.
```
one only gets the constraints
```
x.u0 <= list.u0
x.u0 <= MBind'.u0
x.u0 <= MBind'.u1
x.u1 <= list.u0
x.u1 <= MBind'.u2
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/554Prepare for https://github.com/coq/coq/pull/190592024-06-04T14:19:04ZPierre RouxPrepare for https://github.com/coq/coq/pull/19059Prepare for next version number bump in Coq.
Could you please encode the test in the other direction to avoid having to do that kind of PR again for next Coq version (no hurry, this can be done in the next six months).Prepare for next version number bump in Coq.
Could you please encode the test in the other direction to avoid having to do that kind of PR again for next Coq version (no hurry, this can be done in the next six months).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/553Misc lemma for sets and `gset_to_gmap`2024-07-16T12:44:14ZLéo StefanescoMisc lemma for sets and `gset_to_gmap`Upstreamed from the Aneris project.Upstreamed from the Aneris project.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/552Allow compiling the packages with dune.2024-06-17T08:17:58ZRodolphe LepigreAllow compiling the packages with dune.This MR adds support for the dune build system (documentation available [here](https://dune.readthedocs.io/en/stable/reference/index.html)), so it is basically an updated version of https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/...This MR adds support for the dune build system (documentation available [here](https://dune.readthedocs.io/en/stable/reference/index.html)), so it is basically an updated version of https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/387 (CC @Blaisorblade).
Dune still has many rough edges for projects involving Coq (mostly, it lacks features), but it is still very useful. The main goal of this MR is to allow including stdpp in dune workspaces, which basically allow one to compile (parts of) all involved projects with a single `dune build` invocation, which is convenient to make changes to several packages at once without having to install the packages at the start of the dependency chain (which does not scale). Another large advantage of compiling with dune is caching, but that is more relevant if you have large projects.
What is included in this MR is:
- Compilation of the packages only (no tests).
- Compilation with dune (via `make dune`) as part of a new CI job.
What is not included in this MR, but could be worked on in subsequent MRs if there is interest:
- Generate the `_CoqProject` file depending on how the repo is being used (normal build: use current `_CoqProject`, dune build: use slightly different `_CoqProject`, dune workspace build: no `_CoqProject` since it can get in the way). Note that `dune` technically does not need a `_CoqProject` since editors could invoke `dune coq top` instead of `coqtop`, but they currently don't by default.
- Letting dune generate and manage (also install) the opam packages, which would require making `dune` a hard dependency, but would simplify the infrastructure significantly (no need for patching up `_CoqProject` with a script).
- Port the tests to dune cram tests, which could also simplify the infrastructure, but currently requires a slightly more verbose setup.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/551Strengthen `map_disjoint_difference_{l,r}` and make them consistent with the lemmas for sets.2024-08-14T15:44:55ZRobbert KrebbersStrengthen `map_disjoint_difference_{l,r}` and make them consistent with the lemmas for sets.This closes #208, if m2 = m3 the precondition is vacuously true.This closes #208, if m2 = m3 the precondition is vacuously true.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/550Explicitly Require Coq Vector in vector.v (for coq/coq#18936)2024-04-19T16:29:09ZAndres ErbsenExplicitly Require Coq Vector in vector.v (for coq/coq#18936)For https://github.com/coq/coq/pull/18936
I think previously stdpp vector.v pulled in stdlib Vector.v through NArith, Ndigits, and ByteVector.For https://github.com/coq/coq/pull/18936
I think previously stdpp vector.v pulled in stdlib Vector.v through NArith, Ndigits, and ByteVector.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/549Adapt to https://github.com/coq/coq/pull/189282024-04-16T12:04:57ZPierre RouxAdapt to https://github.com/coq/coq/pull/18928Adapt output tests to upstream PR on Coq https://github.com/coq/coq/pull/18928Adapt output tests to upstream PR on Coq https://github.com/coq/coq/pull/18928https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/548prepare changelog for release2024-04-12T09:26:24ZRalf Jungjung@mpi-sws.orgprepare changelog for releasehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/547always add Proof. after Restart.2024-04-03T15:44:05ZRalf Jungjung@mpi-sws.orgalways add Proof. after Restart.We did this in Iris, we should also do it here.We did this in Iris, we should also do it here.