stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-04-14T18:43:12Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/432add some union_with lemmas2023-04-14T18:43:12ZRalf Jungjung@mpi-sws.orgadd some union_with lemmasThese are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.
But the lemmas are kind of weird so I am open for discussions for how to better provide them.
- The...These are taken verbatim from Perennial, where they already existed and I just needed both of them. So there is clearly some need here.
But the lemmas are kind of weird so I am open for discussions for how to better provide them.
- The first has a very specific lemma statement with this `λ x' _, Some x'`. This arises from `lookup_union` on maps.
- The second is the same as `left_id`, but never in a hundred years would I have realized I can use that LeftId instance. `union_with` is not a binary operator; I think we need a readable lemma that shows up in `SearchAbout union_with None`. Yes LeftId does show up in that search but I doubt many people will realize that it is useful in this situation -- I have skipped over it myself.
Basically: not everything that can be written as LeftId / RightId, should be written that way. IMO we should only use these classes for things that are actually binary operators, written with infix notation. I don't object to instances also existing in other cases, but those instances should only exist *in addition to* regular lemmas, not instead of them.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/431add size_list_to_map2022-12-13T21:52:26ZRalf Jungjung@mpi-sws.orgadd size_list_to_mapThere's probably a way to do this without assuming that the map has some associated domain... but this was the easiest proof, and in practice the map types we work with do have a domain, so it should be fine.There's probably a way to do this without assuming that the map has some associated domain... but this was the easiest proof, and in practice the map types we work with do have a domain, so it should be fine.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/430add map_zip_with_empty lemmas2022-12-12T16:20:43ZRalf Jungjung@mpi-sws.orgadd map_zip_with_empty lemmashttps://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/428Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`.2022-11-30T09:27:45ZRobbert KrebbersTweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`.This solves issue #161This solves issue #161https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/427make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y'2022-11-29T22:32:55ZRalf Jungjung@mpi-sws.orgmake solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y'https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/426Use `notypeclasses refine` for `TCIf` and `TCNoBackTrack`.2022-11-29T18:10:45ZRobbert KrebbersUse `notypeclasses refine` for `TCIf` and `TCNoBackTrack`.This came up here: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/843#note_84069This came up here: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/843#note_84069https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/425Add tactic `tc_solve`.2022-11-30T10:03:59ZRobbert KrebbersAdd tactic `tc_solve`.This is `iSolveTC` from Iris. I think it's good to move this tactic to std++ because it is not specific to Iris.
Also I used the `tc_` prefix to be consistent with other type class related utilities in std++.This is `iSolveTC` from Iris. I think it's good to move this tactic to std++ because it is not specific to Iris.
Also I used the `tc_` prefix to be consistent with other type class related utilities in std++.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/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_compute`.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/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.