stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-03-24T15:55:51Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/458Add NoDup_bind, vec_enum, vec_finite (new version with proper branch)2023-03-24T15:55:51ZRobbert KrebbersAdd NoDup_bind, vec_enum, vec_finite (new version with proper branch)Follow up of !451, but with a branch where I can push.Follow up of !451, but with a branch where I can push.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/457Add `by` parameter to `multiset_solver`2023-03-20T11:12:29ZRobbert KrebbersAdd `by` parameter to `multiset_solver`The tactics `naive_solver` and `set_solver` have a `by` parameter to specify the tactic that is used on the leafs. This MR adds such a parameter to `multiset_solver` too, and similar to `naive_solver`/`set_solver` lets it default to `eau...The tactics `naive_solver` and `set_solver` have a `by` parameter to specify the tactic that is used on the leafs. This MR adds such a parameter to `multiset_solver` too, and similar to `naive_solver`/`set_solver` lets it default to `eauto`.
I cannot easily come up with useful test cases where we need the full power of `eauto`. Either just `fast_done` is sufficient (e.g., if the goal is an equality, see `test_goal_{1,2}` and `gmultiset_singleton_subseteq`) or you need `eauto` with some hints (see `test_goal_3`). Nonetheless, I think it makes sense to be consistent with `naive_solver`/`set_solver` to avoid issues such as !420.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/456Add set_omap to finite sets2023-03-24T16:50:23ZDorian LesbreAdd set_omap to finite setsAdd `omap`-like function to finite sets, aka OCaml's `filter_map` operation.
I needed it to destruct a set of `X + Y` into a set of `X` and a set of `Y`.
Also add a few lemmas to reason about it.Add `omap`-like function to finite sets, aka OCaml's `filter_map` operation.
I needed it to destruct a set of `X + Y` into a set of `X` and a set of `Y`.
Also add a few lemmas to reason about it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/455Various tweaks to lists, maps, sets2023-03-21T16:36:03ZRobbert KrebbersVarious tweaks to lists, maps, setsWhile reviewing !442 and !441 I ran into a bunch of stuff that should be improved:
- Add `subset_proper`.
- Add `list_eq_prefix_length` and `list_eq_suffix_length`. **The version for `prefix` is also part of !441, but the version for `s...While reviewing !442 and !441 I ran into a bunch of stuff that should be improved:
- Add `subset_proper`.
- Add `list_eq_prefix_length` and `list_eq_suffix_length`. **The version for `prefix` is also part of !441, but the version for `suffix` was missing there.**
- Add `set_equiv_subseteq_size` and `set_eq_subseteq_size`. **Similar to the prior lemmas, but now for set equality. These are not part of !441 and !442.**
- Add `dom_subseteq_size`, `dom_subset_size`, `map_eq_subseteq_dom`. **The last lemma is part of !442, but the version in this MR is stronger since it requires `Set_` instead of `FinSet`)**
- Add `map_eq_subseteq_size`, `map_subseteq_size`, `map_subset_size`. **These lemmas are also part of !442, but the statement and naming are made consistent with similar lemmas for sets, and the proof have been shortened.**
- Add `Permutation_submseteq_length` to replace `Permutation_alt`, `submseteq_Permutation_length_le` and `submseteq_Permutation_length_eq`. **This makes the statement and naming consistent with the new lemmas for prefix/suffix/sets/maps**
- Simplify proofs of map induction principles; remove `map_to_list_length`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/454Rename `map_preimage` into `map_preimg` (to be consistent with `dom`).2023-03-19T19:47:33ZRobbert KrebbersRename `map_preimage` into `map_preimg` (to be consistent with `dom`).For the domain of a map we use `dom`, not `domain`.
So it makes sense to also use `img` instead of `image`. In !444 we already do that for the proper image, so let's do too for the pre-image.For the domain of a map we use `dom`, not `domain`.
So it makes sense to also use `img` instead of `image`. In !444 we already do that for the proper image, so let's do too for the pre-image.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/453Improve `bijective_finite`.2023-03-19T18:21:39ZRobbert KrebbersImprove `bijective_finite`.Make the statement stronger by no longer requiring an inverse.
Make the implementation more efficient by not filtering duplicates.Make the statement stronger by no longer requiring an inverse.
Make the implementation more efficient by not filtering duplicates.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/452Add scalar multiplication for multisets.2023-03-19T20:27:14ZRobbert KrebbersAdd scalar multiplication for multisets.The operation `n *: X` multiplies the multiplicity of each element `x ∈ X` with `n`
This MR:
- Introduces a type class `ScalarMul N A := N → A → A` with associated notations for scalar multiplication. The notation `*:` is taken from ss...The operation `n *: X` multiplies the multiplicity of each element `x ∈ X` with `n`
This MR:
- Introduces a type class `ScalarMul N A := N → A → A` with associated notations for scalar multiplication. The notation `*:` is taken from ssreflect, see https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnotations.v
- Provides an instance `ScalarMul nat (gmultiset A)`.
- Provides a bunch of lemmas for `*:` on multisets
- Extends `multiset_solver` and adds a couple of tests.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/451Add NoDup_bind, vec_enum, vec_finite.2023-03-24T15:55:44ZHerman BergwerfAdd NoDup_bind, vec_enum, vec_finite.This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can `vec_finite` be used to simplify the proof of `list_finite`?This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can `vec_finite` be used to simplify the proof of `list_finite`?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/450Cancellation for multiplication on `nat`.2023-03-08T09:24:17ZRobbert KrebbersCancellation for multiplication on `nat`.Coq's stdlib has these lemmas for `Z`, but those for `nat` are missing. We use the naming scheme of Coq's stdlib.Coq's stdlib has these lemmas for `Z`, but those for `nat` are missing. We use the naming scheme of Coq's stdlib.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/449Rename `option_union_Some` → `union_Some`2023-03-21T16:45:56ZRobbert KrebbersRename `option_union_Some` → `union_Some`See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/432#note_87085
This removes `option_` if there's already something else in the name to disambiguate, here that is `_Some`.
We could also prefix everything with `o...See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/432#note_87085
This removes `option_` if there's already something else in the name to disambiguate, here that is `_Some`.
We could also prefix everything with `option_`, but that would require more changes. For better or worse, I think this MR matches the consensus we also have for lists, maps, sets (e.g., having `lookup_app_Some` instead of `list_lookup_app_Some`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/448Alternative definition of `no_new_unsolved_evars` tactic2023-03-17T19:59:52ZRobbert KrebbersAlternative definition of `no_new_unsolved_evars` tacticFollowing a suggestion by @jung in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/429/diffs#note_86725
@jung Could you run CI on all reverse dependencies to see if this indeed does not break anything?
Todo:
- [ ] Also improve...Following a suggestion by @jung in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/429/diffs#note_86725
@jung Could you run CI on all reverse dependencies to see if this indeed does not break anything?
Todo:
- [ ] Also improve naming to make sure this tactic either solves or fails.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/447Add link to style guide2023-03-18T17:53:38ZDorian LesbreAdd link to style guideI couldn't find any styling instruction for my first MR, so I figured mentioning the style guide in the README could be a good ideaI couldn't find any styling instruction for my first MR, so I figured mentioning the style guide in the README could be a good ideahttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/446Remove curry/uncurry workaround for Coq ≤ 8.13.2023-02-13T17:40:07ZRobbert KrebbersRemove curry/uncurry workaround for Coq ≤ 8.13.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/445Add locality for `Hint Rewrite`.2023-02-13T22:16:08ZRobbert KrebbersAdd locality for `Hint Rewrite`.We can do this since we dropped support for Coq 8.13.
For `natmap`, the apply to internal lemmas and should thus be `Local`.
For the bit files, it appears the rewrites are used in a tactic that is used externally. Hence they should be ...We can do this since we dropped support for Coq 8.13.
For `natmap`, the apply to internal lemmas and should thus be `Local`.
For the bit files, it appears the rewrites are used in a tactic that is used externally. Hence they should be `Global`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/444Add images (codomains) to finite maps2023-03-20T12:31:01ZDorian LesbreAdd images (codomains) to finite mapsSimple axiomatization of finite map images (also called codomains). This is strongly inspired by the implementation of `dom`.
It doesn't contain nearly as much lemmas though, mainly because results on the image are generally much weaker...Simple axiomatization of finite map images (also called codomains). This is strongly inspired by the implementation of `dom`.
It doesn't contain nearly as much lemmas though, mainly because results on the image are generally much weaker than
those on the domain, so just using the definition seems simple then providing overly complex lemmas.
Disclaimers: I'm not exactly an expert in Coq but eager to learn more. If you find that my coding style and proofs are ugly,
inefficient, impractical or not in keeping with recommended guidelines feel free to let me know.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/443avoid deprecated Proof <term>.2023-02-01T19:49:19ZRalf Jungjung@mpi-sws.orgavoid deprecated Proof <term>.I didn't even know this was a thing, and it seems the Coq devs [consider it deprecated](https://github.com/coq/coq/pull/12450) and won't fix the issues it has (it doesn't properly work in ProofGeneral).I didn't even know this was a thing, and it seems the Coq devs [consider it deprecated](https://github.com/coq/coq/pull/12450) and won't fix the issues it has (it doesn't properly work in ProofGeneral).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/442miscellaneous map lemmas2023-03-24T15:49:54ZRalf Jungjung@mpi-sws.orgmiscellaneous map lemmassome of these are from Perennialsome of these are from Perennialhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/441Add some list lemmas2023-03-24T15:54:25ZRalf Jungjung@mpi-sws.orgAdd some list lemmasThis fixes some inconsistencies and gaps that I noticed while working on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439, and ports some list lemmas from Perennial.This fixes some inconsistencies and gaps that I noticed while working on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439, and ports some list lemmas from Perennial.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/440drop support for Coq 8.12 and 8.132023-02-04T18:18:47ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.12 and 8.13Dropping 8.12 is needed for `Zify.zify_pre_hook` in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439.
I also propose we document an official support policy of supporting always at least the last 3 stable Coq releases. Looking ...Dropping 8.12 is needed for `Zify.zify_pre_hook` in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439.
I also propose we document an official support policy of supporting always at least the last 3 stable Coq releases. Looking at how we dropped old Coq versions in the past, I think this was always true. Most releases of std++ supported 4 or even 5 Coq versions, but 1.2.0 and 1.2.1 only supported 3 versions. However I feel like more than 3 releases shouldn't really be needed: right now this means the oldest Coq we support, Coq 8.14, is more than 14 months old.
Because we are dropping Coq versions anyway, and to test at least with 1 sample the impact of this policy, I suggest we also drop Coq 8.13, so we are down to the minimal set of 3 supported Coq versions.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439add basic list functionality with Z-based indexing2023-03-23T22:10:13ZRalf Jungjung@mpi-sws.orgadd basic list functionality with Z-based indexingThis starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g...This starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g. the interactions with `Forall3`, `subseteq`, `submseteq`, `filter`, `mask` are missing. Also there are more operations that would need a Z-based version, such as `lookup_total`, `alter`, `delete`, `inserts`, `find`, `imap`, `imap2`, `resize`, `rotate`, `rotate_take`, `sublist_lookup`, `sublist_alter`. There are also some tactics that will not handle these new operations and so might need adjustments or Z-based tactics: `solve_length`, `simplify_list_eq`.
Still I think this is a useful start that can serve as a foundation for later extensions. :)
Blocked on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/441.