stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-12-16T12:52:29Zhttps://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.https://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/424Prevent [finite_countable] from solving unrelated evars2023-05-02T17:21:40ZPaolo G. GiarrussoPrevent [finite_countable] from solving unrelated evarsFix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple appl...Fix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple apply @finite.finite_countable ; trivial` in the trace, and one (or both) the tactics trigger https://github.com/coq/coq/issues/6583. So I've adapted Iris's work around; I've not confirmed whether all of it is needed, but it worked on first try.
Missing (I assume):
- [ ] `trivial` only uses hints with cost 0, but `typeclasses eauto 0` does not appear to work, so `typeclasses eauto 1` is the closest thing I see. This might be a problem.
- [ ] Testcase
- [ ] Changelog? Probably not needed since this is a bugfix
- [x] Mention this in upstream issue.
Also see Coq issue https://github.com/coq/coq/issues/16893.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/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`.