stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-12-22T16:21:39Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/436lookup_gset_to_gmap: use decide rather than guard2022-12-22T16:21:39ZRalf Jungjung@mpi-sws.orglookup_gset_to_gmap: use decide rather than guard`guard` is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. `decide` is a lot more common, and so people are more likely to know how to deal with it.`guard` is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. `decide` is a lot more common, and so people are more likely to know how to deal with it.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/423Fix typo in lemma name2023-02-06T09:50:33ZPaolo G. GiarrussoFix typo in lemma nameDoes this need a changelog?Does this need a changelog?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/372Draft: Very preliminary version of a quick start guide for sets.2023-02-06T14:42:57ZRobbert KrebbersDraft: Very preliminary version of a quick start guide for sets.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/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/387Draft: dune build scripts2023-03-07T14:58:45ZPaolo G. GiarrussoDraft: dune build scriptsThis is part of https://gitlab.mpi-sws.org/iris/iris/-/issues/471.
Instructions are needed, but with dune 3.4 this already supports `dune build`, `dune coq top`.This is part of https://gitlab.mpi-sws.org/iris/iris/-/issues/471.
Instructions are needed, but with dune 3.4 this already supports `dune build`, `dune coq top`.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/429Make sure that `naive_solver` does not create any new evars on leafs.2023-03-17T13:43:10ZRobbert KrebbersMake sure that `naive_solver` does not create any new evars on leafs.This fixes issue #163.This fixes issue #163.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/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/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/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/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/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/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/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/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.