stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-03-12T17:55:50Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/543Cleanup bitblast_mod after dropping support for Coq 8.132024-03-12T17:55:50ZMichael SammlerCleanup bitblast_mod after dropping support for Coq 8.13https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/542create new package for stdpp-bitvector library2024-03-18T16:58:31ZRalf Jungjung@mpi-sws.orgcreate new package for stdpp-bitvector libraryThis is a step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/204.
I was not quite sure which Coq logical path to use for this. For now I used `stdpp.bv` since always typing `stdpp.bitvector` seems a bit annoying, but the incons...This is a step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/204.
I was not quite sure which Coq logical path to use for this. For now I used `stdpp.bv` since always typing `stdpp.bitvector` seems a bit annoying, but the inconsistency may also be confusing. Opinions?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/541Fix slowdown in bv_saturate from https://github.com/coq/coq/pull/179842024-03-11T20:52:26ZMichael SammlerFix slowdown in bv_saturate from https://github.com/coq/coq/pull/17984https://github.com/coq/coq/pull/17984 causes a significant slowdown in Islaris since the changed `Z.euclidean_division_equations_cleanup` function can be become very slow if there are many hypothesis of the form `0 <= ... < ...` in the c...https://github.com/coq/coq/pull/17984 causes a significant slowdown in Islaris since the changed `Z.euclidean_division_equations_cleanup` function can be become very slow if there are many hypothesis of the form `0 <= ... < ...` in the context. This MR works around this by changing `bv_saturate` to generate hypothesis of the form `-1 < ... < ...` instead of `0 <= ... < ...`. This change speeds up some case studies in Islaris by up to 30%, see [here](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=isla-coq&var-branch1=time%2Fcoq-8.19&var-commit1=4e341b0cc59a121860f224e6237156fad40b2cb1&var-config1=build-coq.8.19.0-timing&var-branch2=time%2Fcoq-8.19&var-commit2=2ccb19c5025a147047121188dd9b5b638b6143df&var-config2=build-coq.8.19.0-timing&var-metric=instructions&var-group=%28.%2A%29).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/540Add lemma `join_app`.2024-03-05T06:15:18ZRobbert KrebbersAdd lemma `join_app`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/539drop support for Coq 8.16 and 8.172024-02-07T14:50:35ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.16 and 8.17https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/538test on Coq 8.192024-02-02T10:50:57ZRalf Jungjung@mpi-sws.orgtest on Coq 8.19https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/537Adapt to https://github.com/coq/coq/pull/185902024-02-09T12:48:28ZPierre RouxAdapt to https://github.com/coq/coq/pull/18590Note that this requires dropping support for Coq 8.16 and 8.17.
Alternatively, we could implement a less ice intermediate solution that would still support 8.16.
Also note that there is a mention of 8.17 in numbers.v which I didn't han...Note that this requires dropping support for Coq 8.16 and 8.17.
Alternatively, we could implement a less ice intermediate solution that would still support 8.16.
Also note that there is a mention of 8.17 in numbers.v which I didn't handle here.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/536Adapt to https://github.com/coq/coq/pull/182242024-02-02T15:26:23ZPierre RouxAdapt to https://github.com/coq/coq/pull/18224This should be backward compatibleThis should be backward compatiblehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/535Remove Import NPeano2023-11-17T06:59:47ZPierre RousselinRemove Import NPeanoRemove Import NPeano in numbers: this is necessary for
https://github.com/coq/coq/pull/18164Remove Import NPeano in numbers: this is necessary for
https://github.com/coq/coq/pull/18164https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/534Make `inv` and `oinv` work with numbers2023-10-30T20:51:23ZRalf Jungjung@mpi-sws.orgMake `inv` and `oinv` work with numbersI also replaced all `inversion_clear` by `inv`. In `list.v` I furthermore replaced most `inversion` by `inv` just to get a whole lot of extra testcases. However sometimes, follow-up automation fails when the inverted hypothesis is cleare...I also replaced all `inversion_clear` by `inv`. In `list.v` I furthermore replaced most `inversion` by `inv` just to get a whole lot of extra testcases. However sometimes, follow-up automation fails when the inverted hypothesis is cleared.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/199https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533Allow pattern and type annotations in propset notation2024-03-05T06:25:01ZThibaut PéramiAllow pattern and type annotations in propset notationThis allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break...This allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break if someone adds a binary infix `|` notation downstream, In which case this will be parsed as a singleton of whatever the result of the `|` operation is. This was already the case before, so anyone that did that already broke the original `propset` notationhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/532Draft: Staging MR for various refactorings2023-12-02T09:45:08ZRobbert KrebbersDraft: Staging MR for various refactoringsIt turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_reques...It turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/526#note_97794
- [ ] Direction of equality in `fmap`/`omap`/`alter` lemmas, see https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97789
The plan is to merge all these MRs into a staging branch (the one linked to this MR) and then merge the staging branch to master. This way we have to fix reverse dependencies just once.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`2023-10-20T12:54:40ZRobbert KrebbersFix inconsistencies in `lookup` and `elem_of` lemmas for `list`- Rename lemmas `elem_of_list_X` into `list_elem_of_X` to be consistent with the `list_lookup_X` lemmas. Some lemmas contained other inconsistencies (e.g., `_1` and `_2` swapped), see CHANGELOG for details.
- Change the order of the conj...- Rename lemmas `elem_of_list_X` into `list_elem_of_X` to be consistent with the `list_lookup_X` lemmas. Some lemmas contained other inconsistencies (e.g., `_1` and `_2` swapped), see CHANGELOG for details.
- Change the order of the conjunction in `list_lookup_fmap_Some`. The new
version is `(f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x`, which
makes it consistent with `list_elem_of_fmap` and the corresponding lemmas for
sets and maps. **To be continued in other MR, insert link**
- Rename `list_alter_fmap` → `list_fmap_alter` and remove `list_alter_fmap_mono` which was a monomorphic duplicate.
With the exception of the `list_elem_of_fmap` change, all changes in this MR can be applied by `sed`. It would be best to merge it together with !526 so we only have to run a giant `sed` script once on reverse dependencies.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/530Add lemma `lookup_total_fmap`.2023-10-16T17:55:15ZRobbert KrebbersAdd lemma `lookup_total_fmap`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/529Add `prod_swap` and some basic results for it.2023-10-14T16:04:35ZRobbert KrebbersAdd `prod_swap` and some basic results for it.I was surprised this function is not in the stdlib...I was surprised this function is not in the stdlib...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/528Missing `Params` instances for `prod_map` and `prod_zip`.2023-10-14T16:00:35ZRobbert KrebbersMissing `Params` instances for `prod_map` and `prod_zip`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/527Add a comment about `cancel_inj` and `cancel_surj`.2023-10-14T17:42:57ZRobbert KrebbersAdd a comment about `cancel_inj` and `cancel_surj`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/526Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a s...2023-10-17T12:01:36ZRobbert KrebbersProvide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.This has been discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/507. This MR changes all lemmas for list, map, multiset in std++ according to that plan. The CHANGELOG describes all changes.
While performing the refacto...This has been discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/507. This MR changes all lemmas for list, map, multiset in std++ according to that plan. The CHANGELOG describes all changes.
While performing the refactoring, I also added some missing lemmas. They are also described in the CHANGELOG.
I tested the `sed` script on iris, iris-examples, lambdarust, Actris, Iron, GPFSL. No manual fixes were needed.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/525add inv and oinv tactics that are basically a smarter and fixed inversion_clear2023-10-14T15:20:21ZRalf Jungjung@mpi-sws.orgadd inv and oinv tactics that are basically a smarter and fixed inversion_clearFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/40
Sadly I couldn't figure out how to make `inv 1` work. [See Zulip](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Writing.20a.20tactic.20that.20takes.20.22ident.20o...Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/40
Sadly I couldn't figure out how to make `inv 1` work. [See Zulip](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Writing.20a.20tactic.20that.20takes.20.22ident.20or.20term.20number.22.3F)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/524remove 'wf' alias for the standard 'well_founded'2023-10-14T08:36:25ZRalf Jungjung@mpi-sws.orgremove 'wf' alias for the standard 'well_founded'I could not find a single use of this alias outside of std++ itself, so the potential for confusion caused by having two different names for the same thing far outweighs the benefit of occasionally saving 9 keystrokes.I could not find a single use of this alias outside of std++ itself, so the potential for confusion caused by having two different names for the same thing far outweighs the benefit of occasionally saving 9 keystrokes.