stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-03-20T11:12:29Zhttps://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/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/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/438Stop mentioning Coq bug fixed in Coq >= 8.132023-02-13T17:39:26ZPaolo G. GiarrussoStop mentioning Coq bug fixed in Coq >= 8.13This should wait till stdpp drops support for Coq 8.12, but that's soon IIUC.This should wait till stdpp drops support for Coq 8.12, but that's soon IIUC.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/434Use high cost for `Decision` instances for `True` and `False`.2022-12-16T12:52:29ZRobbert KrebbersUse high cost for `Decision` instances for `True` and `False`.This fixes issue #165.
What happens is that it needs to solve `Decision (@elem_of ... ?instance x xs)` where `?instance` is an evar representing an unresolved type class. Now instead of solving `?instance` first, Coq applies `False_dec`...This fixes issue #165.
What happens is that it needs to solve `Decision (@elem_of ... ?instance x xs)` where `?instance` is an evar representing an unresolved type class. Now instead of solving `?instance` first, Coq applies `False_dec` and uses HO-unification to instantiate `?instance` with `λ _ _, False`, i.e., something nonsensical.
By increasing the cost of the `True` and `False` instances we make sure Coq first uses the `elem_of_dec` instance.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/433option.v: Add option_guard_decide and option_guard_bool_decide2022-12-16T12:54:23ZPaolo G. Giarrussooption.v: Add option_guard_decide and option_guard_bool_decideMotivated by https://mattermost.mpi-sws.org/iris/pl/cz6f4bxwsir78jkunk7nt3bawo.Motivated by https://mattermost.mpi-sws.org/iris/pl/cz6f4bxwsir78jkunk7nt3bawo.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/432add some union_with lemmas2023-03-24T11:13:55ZRalf Jungjung@mpi-sws.orgadd some union_with lemmasThese are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.
But the lemmas are kind of weird so I am open for discussions for how to better provide them.
- The...These are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.
But the lemmas are kind of weird so I am open for discussions for how to better provide them.
- The first has a very specific lemma statement with this `λ x' _, Some x'`. This arises from `lookup_union` on maps.
- The second is the same as `left_id`, but never in a hundred years would I have realized I can use that LeftId instance. `union_with` is not a binary operator; I think we need a readable lemma that shows up in `SearchAbout union_with None`. Yes LeftId does show up in that search but I doubt many people will realize that it is useful in this situation -- I have skipped over it myself.
Basically: not everything that can be written as LeftId / RightId, should be written that way. IMO we should only use these classes for things that are actually binary operators, written with infix notation. I don't object to instances also existing in other cases, but those instances should only exist *in addition to* regular lemmas, not instead of them.