stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-10-30T15:15:54Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/579Update to version 1.11.02024-10-30T15:15:54ZJesper BengtsonUpdate to version 1.11.0https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/576Add cartesian products to all concrete set types2024-10-30T10:12:55ZThibaut PéramiAdd cartesian products to all concrete set typesThis adds a set Cartesian product on:
- `list`
- `gset`
- `propset`
- `boolset`
- `listset`
With the notation `A × B` at level 37. The notation is left associative so that `lA × lB × lC : list (A * B * C)`. This includes corresponding ...This adds a set Cartesian product on:
- `list`
- `gset`
- `propset`
- `boolset`
- `listset`
With the notation `A × B` at level 37. The notation is left associative so that `lA × lB × lC : list (A * B * C)`. This includes corresponding specification lemmas and `SetUnfoldElemOf` instances. I only did a set level specification. There is no lemma in this MR describing the order for the Cartesian product on lists (the only one of those types where order is relevant)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/578make levels consistent between propset notation and singleton notation2024-10-30T09:00:40ZRalf Jungjung@mpi-sws.orgmake levels consistent between propset notation and singleton notationThis fixes the last remaining occurrences of the "incompatible prefix" warning when building with `coq.dev`. `{[ x ]}` does not set a level for `x` so I guess it makes sense that we have to do the same here.
Cc @tperami @blaisorbladeThis fixes the last remaining occurrences of the "incompatible prefix" warning when building with `coq.dev`. `{[ x ]}` does not set a level for `x` so I guess it makes sense that we have to do the same here.
Cc @tperami @blaisorbladehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/577Add `gmultiset_map` and associated lemmas2024-10-21T09:28:32ZMarijn van Wezelmarijn.vanwezel@ru.nlAdd `gmultiset_map` and associated lemmasThis merge request adds a definition for mapping over a `gmultiset`, `gmultiset_map`, similar to `set_map` for (regular) finite sets.
I struggled with finding a correct location for the definition and associated lemmas in `gmultiset.v`....This merge request adds a definition for mapping over a `gmultiset`, `gmultiset_map`, similar to `set_map` for (regular) finite sets.
I struggled with finding a correct location for the definition and associated lemmas in `gmultiset.v`. I am open to any suggestions to improve the placement.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/575Enable `map_Forall2` to be used in nested inductive relations2024-10-02T14:18:11ZRobbert KrebbersEnable `map_Forall2` to be used in nested inductive relationsThis MR allows definitions like the following, whereas they were previously rejected by the positivity checker:
```coq
Inductive gtest_rel `{Countable K} : relation (gtest K) :=
| GTest_rel ts1 ts2 :
map_Forall2 (λ _, gtest_rel) ...This MR allows definitions like the following, whereas they were previously rejected by the positivity checker:
```coq
Inductive gtest_rel `{Countable K} : relation (gtest K) :=
| GTest_rel ts1 ts2 :
map_Forall2 (λ _, gtest_rel) ts1 ts2 → gtest_rel (GTest ts1) (GTest ts2).
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/564Generalize `map_relation` and `map_included` / Add `map_Forall2`.2024-09-29T17:16:20ZRobbert 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/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/533Allow pattern and type annotations in propset notation2024-09-11T16:23:21ZThibaut PéramiAllow pattern and type annotations in propset notationThis allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break...This allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break if someone adds a binary infix `|` notation downstream, In which case this will be parsed as a singleton of whatever the result of the `|` operation is. This was already the case before, so anyone that did that already broke the original `propset` notationhttps://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/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.