stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-03-19T18:21:39Zhttps://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).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/440drop support for Coq 8.12 and 8.132023-04-24T09:15:28ZRalf 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.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/437Enable `Hint Mode Equiv` now that stdpp requires Coq 8.122023-05-02T12:48:11ZPaolo G. GiarrussoEnable `Hint Mode Equiv` now that stdpp requires Coq 8.12Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because ...Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because it still supported Coq 8.11 which suffered from additional bugs (fixed in 8.12) — Iris still has this comment:
```coq
(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12, which Iris depends on. *)
```https://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/435Use hint mode + more often2023-10-13T09:41:54ZRobbert KrebbersUse hint mode + more oftenThis is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uoThis is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uohttps://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.