stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-02-06T09:50:33Zhttps://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/422add gset_to_gmap_to_list2022-11-18T10:17:34ZRalf Jungjung@mpi-sws.orgadd gset_to_gmap_to_listThis came up while trying to convert an `own` of a map into a `big_sepL` of its elements.This came up while trying to convert an `own` of a map into a `big_sepL` of its elements.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/421Fix bitvector tests for coq#167482023-05-30T16:35:13ZMichael SammlerFix bitvector tests for coq#16748See https://github.com/coq/coq/pull/16748#issuecomment-1296962224See https://github.com/coq/coq/pull/16748#issuecomment-1296962224https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/420Use `eauto` as default for `set_solver`.2023-04-12T13:54:05ZRobbert KrebbersUse `eauto` as default for `set_solver`.The `set_solver` tactic roughly calls `set_unfold` and then performs `naive_solver`. @jihgfee noticed that `set_solver` (without tactic argument) calls `naive_solver idtac` by default. This is somewhat strange since `naive_solver` (witho...The `set_solver` tactic roughly calls `set_unfold` and then performs `naive_solver`. @jihgfee noticed that `set_solver` (without tactic argument) calls `naive_solver idtac` by default. This is somewhat strange since `naive_solver` (without tactic argument) defaults to `naive_solver eauto`.
Also @jihgfee found an example where `set_solver by idtac` (the current default) is much slower than `set_solver by eauto`.
So I am wondering what's the reason why `set_solver` uses `idtac`? Is that just some arbitrary legacy choice, or does it actually improve performance?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/419Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_co...2022-11-16T12:27:56ZRobbert KrebbersUse `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.In std++ and Iris we do not use native_compute, so relying on it needlessly increases the trusted code base. Since recently an [unsoundness bug in naive_compute](https://github.com/coq/coq/issues/16645) was discovered (which was also fix...In std++ and Iris we do not use native_compute, so relying on it needlessly increases the trusted code base. Since recently an [unsoundness bug in naive_compute](https://github.com/coq/coq/issues/16645) was discovered (which was also fixed immediately), I wonder if it wouldn't make sense to just disable native_compute altogether in std++ and Iris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/418Add some type annotations for prepare for `Hint Mode` for `Equiv`.2022-10-08T09:42:18ZRobbert KrebbersAdd some type annotations for prepare for `Hint Mode` for `Equiv`.I tried to set the hint mode for equiv:
```coq
Global Hint Mode Equiv ! : typeclass_instances.
```
Due to a recently fixed Coq bug, this only works with Coq 8.15+. So, while we cannot merge the hint mode yet, this MR contains some miss...I tried to set the hint mode for equiv:
```coq
Global Hint Mode Equiv ! : typeclass_instances.
```
Due to a recently fixed Coq bug, this only works with Coq 8.15+. So, while we cannot merge the hint mode yet, this MR contains some missing type annotations I discovered in the process.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417Add lemmas `set_fold_union_strong` and `set_fold_union`.2022-11-23T08:38:46ZRobbert KrebbersAdd lemmas `set_fold_union_strong` and `set_fold_union`.[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativit...[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativity/commutativity for the elements in the sets.
Interestingly, the already existing "disjoint" versions of the lemma can be derived.
The proofs are pretty long/tricky, so I tried to add some comments what's going on.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/416Add lemma `foldr_cons`.2022-09-23T13:04:51ZRobbert KrebbersAdd lemma `foldr_cons`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/415Add lemma `lookup_snoc_Some`.2022-09-23T13:01:36ZRobbert KrebbersAdd lemma `lookup_snoc_Some`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/414Add lemma `filter_app_complement`.2022-09-23T12:54:19ZRobbert KrebbersAdd lemma `filter_app_complement`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/413add map_choose_or_empty2022-09-20T13:32:27ZRalf Jungjung@mpi-sws.orgadd map_choose_or_emptyJust a nice little convenience.Just a nice little convenience.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/412add map_fold_delete2022-09-25T18:39:05ZRalf Jungjung@mpi-sws.orgadd map_fold_deletehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/411Fix unfolding logic of bv_simplify2022-11-23T15:05:04ZMichael SammlerFix unfolding logic of bv_simplify`bv_simplify` should always produce equalities on `Z`, but due to a bug it turned `bv_wrap n (bv_unsigned b) = bv_wrap n (bv_unsigned b)` into `b = b`, which means that `bv_solve` fails on `bv_wrap n (bv_unsigned b) = bv_wrap n (bv_unsig...`bv_simplify` should always produce equalities on `Z`, but due to a bug it turned `bv_wrap n (bv_unsigned b) = bv_wrap n (bv_unsigned b)` into `b = b`, which means that `bv_solve` fails on `bv_wrap n (bv_unsigned b) = bv_wrap n (bv_unsigned b)`. This MR fixes this bug which is caused by `apply` applying an `↔` lemma in the wrong direction.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/410Prepare changelog for release 1.82022-08-17T16:20:34ZLennard Gähergaeher@mpi-sws.orgPrepare changelog for release 1.8Lennard Gähergaeher@mpi-sws.orgLennard Gähergaeher@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/409add some very basic f_equiv tests2022-08-12T12:12:40ZRalf Jungjung@mpi-sws.orgadd some very basic f_equiv testsRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/408Add bitvector library with automation2022-08-24T17:47:58ZMichael SammlerAdd bitvector library with automationThis MR adds two new unstable libraries: A library for bitvectors (previously published at https://gitlab.mpi-sws.org/iris/bitvector) and automation for this bitvector library. See the files for some basic description of the functionalit...This MR adds two new unstable libraries: A library for bitvectors (previously published at https://gitlab.mpi-sws.org/iris/bitvector) and automation for this bitvector library. See the files for some basic description of the functionality provided by the libraries.Michael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/407Generalize Propers for lists / Add some missing Params2022-08-11T07:51:16ZRobbert KrebbersGeneralize Propers for lists / Add some missing ParamsFor example, for fmap:
- Old: `Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f)`
- New: `Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap`
This means that `solve_proper` can also find a `Proper` instance when the two...For example, for fmap:
- Old: `Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f)`
- New: `Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap`
This means that `solve_proper` can also find a `Proper` instance when the two functions are different, and then prove that they are extensionally equal.
This is similar to what we have done in !276 for maps.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/406Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid r...2022-08-09T10:55:48ZPaolo G. GiarrussoIntroduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewritingThis is @dfrumin's !383 (with authorship preserved) + some tweaks to setoid rewriting:
- strengthen set_bind_subset to have the same arity
- add missing Params instance to prevent slow failures in setoid rewriting
- `Proper` instances c...This is @dfrumin's !383 (with authorship preserved) + some tweaks to setoid rewriting:
- strengthen set_bind_subset to have the same arity
- add missing Params instance to prevent slow failures in setoid rewriting
- `Proper` instances can be proven before `set_bind_ext` via `set_solver`.
- `set_bind_ext` is then provable by set_solver directly.
I originally sent https://gitlab.mpi-sws.org/dfrumin/coq-stdpp/-/merge_requests/1 to be added into !383, but maybe it's easier with this MR? @robbertkrebbers up to you.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/405Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None2022-08-08T14:48:15ZMichael SammlerAdd _1, _2 lemmas for not_elem_of_dom and lookup_union_NoneSplit from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/394Split from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/394Michael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/404Rename plus/minus → add/sub and put number lemmas in modules to be consistent...2023-04-22T18:02:11ZRobbert KrebbersRename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlibRename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current convention for numbers.
Following the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/821Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current convention for numbers.
Following the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/821Robbert KrebbersRobbert Krebbers