stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-09-23T13:01:36Zhttps://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/416Add lemma `foldr_cons`.2022-09-23T13:04:51ZRobbert KrebbersAdd lemma `foldr_cons`.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/386Added set lemmas about difference and union2022-09-29T07:00:02ZJonas KastbergAdded set lemmas about difference and unionAdded some set lemmas about difference and union that I was missing in my local development.Added some set lemmas about difference and union that I was missing in my local development.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/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/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/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/394Add some _1, _2 lemmas for map_filter2022-11-23T08:43:44ZMichael SammlerAdd some _1, _2 lemmas for map_filterAs discussed with @robbertkrebbersAs discussed with @robbertkrebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/402Create stdpp-unstable package and add bitblast library2022-11-23T08:49:35ZMichael SammlerCreate stdpp-unstable package and add bitblast libraryThis MR adds a `stdpp-unstable` library similar to the corresponding library in Iris. In general, the process for `stdpp-unstable` follows the process for the corresponding Iris library and the most important points are documented in the...This MR adds a `stdpp-unstable` library similar to the corresponding library in Iris. In general, the process for `stdpp-unstable` follows the process for the corresponding Iris library and the most important points are documented in the README changes of this MR.
Additionally, this MR adds a bitblast tactic as the first unstable library.Michael SammlerMichael Sammlerhttps://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/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/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/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/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/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/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/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/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.