stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-04-24T09:07:53Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/463Use `positive` in `gmultiset` representation to avoid off-by-one computations.2023-04-24T09:07:53ZRobbert KrebbersUse `positive` in `gmultiset` representation to avoid off-by-one computations.- The only lemma where the use of internal use `nat` appeared was `gmultiset_subseteq_alt`, but that lemma talks about `gmultiset_car`, which should be private. I thus flagged that lemma as `Local`.
- This change also gives rise to more ...- The only lemma where the use of internal use `nat` appeared was `gmultiset_subseteq_alt`, but that lemma talks about `gmultiset_car`, which should be private. I thus flagged that lemma as `Local`.
- This change also gives rise to more compact representations (that is logarithmic instead of linear in terms of the largest multiplicity), but since the multiplicity and scalar_mult functions (as part of the public API) use `nat`, it's difficult to come up with an example where this improvement can be observed.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/462Add `min` and `max` infix notations for `positive`.2023-04-19T12:00:20ZRobbert KrebbersAdd `min` and `max` infix notations for `positive`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/460Extend `set_solver` with support for `set_Forall` and `set_Exists`.2023-04-11T09:33:09ZRobbert KrebbersExtend `set_solver` with support for `set_Forall` and `set_Exists`.This closes issue #178This closes issue #178https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/459Finite map composition2023-09-28T14:01:30ZDorian LesbreFinite map composition- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that...- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that is the case feel free to close without merging.
I'm submitting in case someone else would have a use for it, since this
is now fairly complete (although it could use some compatibility lemmas with `insert`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/458Add NoDup_bind, vec_enum, vec_finite (new version with proper branch)2023-04-18T18:39:40ZRobbert 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-04-18T18:32:41ZDorian 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-04-18T18:34:33ZHerman 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).