stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-09-11T16:58:43Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/574Unsilence deprecation warning regarding list lemmas.2024-09-11T16:58:43ZRobbert KrebbersUnsilence deprecation warning regarding list lemmas.I think having our own (direct) version of this two line proof (instead of going via an equivalent to a stdlib def) is less problematic than missing out on other deprecation warnings.I think having our own (direct) version of this two line proof (instead of going via an equivalent to a stdlib def) is less problematic than missing out on other deprecation warnings.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417Add `set_fold_union_strong` and similarly for map2024-09-10T18:08:55ZRobbert KrebbersAdd `set_fold_union_strong` and similarly for map[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativit...[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativity/commutativity for the elements in the sets.
Interestingly, the already existing "disjoint" versions of the lemma can be derived.
The proofs are pretty long/tricky, so I tried to add some comments what's going on.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/570Better use of modules / less global polution for strings2024-09-10T18:02:24ZRobbert KrebbersBetter use of modules / less global polution for stringsSee CHANGELOG for detailsSee CHANGELOG for detailshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/573Make `foldr_cons_permute` lemmas consistent.2024-09-10T16:05:07ZRobbert KrebbersMake `foldr_cons_permute` lemmas consistent.See CHANGELOG.
Addressing issue pointed out in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417#note_85025See CHANGELOG.
Addressing issue pointed out in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417#note_85025https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/569Add `map_Forall2_dom`.2024-09-10T12:47:30ZRobbert KrebbersAdd `map_Forall2_dom`.I didn't add a CHANGELOG, because there is already "Add `map_Forall2` and some basic lemmas about it".I didn't add a CHANGELOG, because there is already "Add `map_Forall2` and some basic lemmas about it".https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/572numbers.v: Don't Qed Decision instances2024-09-08T07:00:12ZPaolo G. Giarrussonumbers.v: Don't Qed Decision instancesNoticed from a `compute_done` failure.
Also, use `abstract` to still hide proof-irrelevant terms from computation.Noticed from a `compute_done` failure.
Also, use `abstract` to still hide proof-irrelevant terms from computation.https://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/568Notation for string literals in `stdpp_scope`.2024-09-06T13:26:07ZRobbert KrebbersNotation for string literals in `stdpp_scope`.This removes a giant hack (`Global Open Scope list_scope` in the old `strings` file) and fixes some parsing issues (`=?` not working after importing strings, see test case).This removes a giant hack (`Global Open Scope list_scope` in the old `strings` file) and fixes some parsing issues (`=?` not working after importing strings, see test case).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/566Stronger induction principle for `map_fold`.2024-09-04T22:07:35ZRobbert KrebbersStronger induction principle for `map_fold`.(Based on a proposal by @johannes, see https://mattermost.mpi-sws.org/iris/pl/uosw3r3xx7dhmgz9o4xy7joxpe)
The new induction principle is:
```coq
map_fold_ind {A} (P : M A → Prop) :
P ∅ →
(∀ i x m,
m !! i = None →
...(Based on a proposal by @johannes, see https://mattermost.mpi-sws.org/iris/pl/uosw3r3xx7dhmgz9o4xy7joxpe)
The new induction principle is:
```coq
map_fold_ind {A} (P : M A → Prop) :
P ∅ →
(∀ i x m,
m !! i = None →
(∀ B (f : K → A → B → B) b,
map_fold f b (<[i:=x]> m) = f i x (map_fold f b m)) →
P m →
P (<[i:=x]> m)) →
∀ m, P m;
```
This induction scheme is like `map_ind`, but it gives an equality for `map_fold` for the current element (`i`/`x`) without any conditions on `f`. This is sound because all uses of `fold` and the induction principle traverse the map in the same way.
- The new scheme implies `map_fold_foldr` from !565
- It also implies the proposed rule `map_to_list_cons_inv` by @johannes in https://mattermost.mpi-sws.org/iris/pl/drduhw8etirftc7bkwdjhj57fr
- I think the new `map_fold_ind` is more usable than the old one since you can just do `induction m as .. using map_fold_ind`. You do not need to `revert` and manually `apply` the scheme. Hence I renamed the old scheme into `map_fold_weak_ind`, which should discourage one from using it.
- Additional bonus: Using the new scheme we can easily prove `map_fold_comm_acc(_strong)?` without needless side-conditions, making it consistent with the versions of sets and multisets.https://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/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/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/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/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/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/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.