stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2019-07-04T13:14:32Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/78Some list related lemmas2019-07-04T13:14:32ZMichael SammlerSome list related lemmasSome more lemmas that I proved for my development.Some more lemmas that I proved for my development.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/81add inverses of bool_decide_{true,false}2019-07-13T09:56:17ZRalf Jungjung@mpi-sws.orgadd inverses of bool_decide_{true,false}https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/72SeqZ Function2020-03-17T20:34:30ZSimon SpiesSeqZ FunctionThis MR adds a simple range function on integers to stdpp.
Calling `range m n` results in the range `m, m + 1, ..., n - 1` and is empty, if `m >= n`.This MR adds a simple range function on integers to stdpp.
Calling `range m n` results in the range `m, m + 1, ..., n - 1` and is empty, if `m >= n`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/79Define `Involutive` in terms of `Cancel`.2019-06-26T11:14:29ZRobbert KrebbersDefine `Involutive` in terms of `Cancel`.As suggested by @jung in https://gitlab.mpi-sws.org/iris/stdpp/commit/18f83bcb55305001bbec93e74857022e8becaa07#note_37911As suggested by @jung in https://gitlab.mpi-sws.org/iris/stdpp/commit/18f83bcb55305001bbec93e74857022e8becaa07#note_37911https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/80Perform `fast_done` first in `naive_solver`.2019-06-27T08:50:42ZRobbert KrebbersPerform `fast_done` first in `naive_solver`.This avoids `naive_solver` tearing whole goals apart, even if the goal appears exactly as a hypothesis.
In Iris/C I ran into this problem after the recent `set_solver` changes (https://gitlab.mpi-sws.org/iris/stdpp/commit/4ff965b26be9...This avoids `naive_solver` tearing whole goals apart, even if the goal appears exactly as a hypothesis.
In Iris/C I ran into this problem after the recent `set_solver` changes (https://gitlab.mpi-sws.org/iris/stdpp/commit/4ff965b26be968461cb58f84dfc51d66d9da04c3). Since `set_unfold` unfolds more stuff than it used to do, `naive_solver` essentially had to solve `P → P`. However, since it was tearing the entire goal apart, and trying to reestablish it while there were other assumptions in the context that influenced instantiation of existentials, it was not able to solve `P` again. By performing `fast_done` eagerly, it will not simply solve `P → P` immediately without tearing the entire goal apart.
It appears that the impact on e.g. LambdaRust is in the noise range: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=4ad3f8b08c1ff4481d0fab41f878b215257a6462&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Fnaive_solver&var-commit2=11c5f900bf7b1f9fdaf4ba8cfc36d601bb5abdbf&var-config2=coq-8.9.0&var-group=().*&var-metric=instructionshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/76Added two proper instances with permutations2019-06-26T11:05:58ZMichael SammlerAdded two proper instances with permutationsThese are two Proper instances I found useful in my development. My original proofs use `move => /Forall_cons[??]` instead of inversion, but stdpp does not seem to use ssreflect and `intros [??]%Forall_cons` does not work for reasons I d...These are two Proper instances I found useful in my development. My original proofs use `move => /Forall_cons[??]` instead of inversion, but stdpp does not seem to use ssreflect and `intros [??]%Forall_cons` does not work for reasons I don't understand. So please let me know if you know how to do the prrof for `Forall_proper_perm` without inversion.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/74show a Proper instance for dom2019-06-20T21:08:14ZRalf Jungjung@mpi-sws.orgshow a Proper instance for domhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/75make solve_ndisj more powerful2019-06-20T20:36:17ZRalf Jungjung@mpi-sws.orgmake solve_ndisj more powerfulFixes https://gitlab.mpi-sws.org/iris/stdpp/issues/34.Fixes https://gitlab.mpi-sws.org/iris/stdpp/issues/34.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/73add unfolding lemma for bool_decide: bool_decide_decide2019-06-18T08:34:09ZRalf Jungjung@mpi-sws.orgadd unfolding lemma for bool_decide: bool_decide_decidehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/71Some missing results about vectors.2019-06-14T16:02:55ZRobbert KrebbersSome missing results about vectors.This addresses https://gitlab.mpi-sws.org/iris/stdpp/issues/33
I did not include any of the `map` lemmas, since we have versions of them for `fmap` (notation `<$>`).
I find the following lemma pretty weird:
```coq
Lemma vec_to_list_ta...This addresses https://gitlab.mpi-sws.org/iris/stdpp/issues/33
I did not include any of the `map` lemmas, since we have versions of them for `fmap` (notation `<$>`).
I find the following lemma pretty weird:
```coq
Lemma vec_to_list_take_drop {A n} (i : fin n) (v : vec A n) :
vtake i v ++ vdrop i v = v.
Proof. by rewrite vec_to_list_take, vec_to_list_drop, take_drop. Qed.
```
It involves implicit coercions to list, and it uses the append on lists.
Unless @lepigre has a good reason for it, I rather not include it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/70Strings are inhabited2019-05-17T13:04:27ZPaolo G. GiarrussoStrings are inhabitedAdd instance for `Inhabited string`; usually you can rely on stdpp having all the instances you'd expect, which is pretty cool, so let's fix this small exception :smiley:Add instance for `Inhabited string`; usually you can rely on stdpp having all the instances you'd expect, which is pretty cool, so let's fix this small exception :smiley:https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/69Fix typo in instance name2019-05-17T11:19:20ZPaolo G. GiarrussoFix typo in instance nameHoping nothing relies on this name.Hoping nothing relies on this name.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/68Fix typo in doc2019-04-26T09:42:21ZPaolo G. GiarrussoFix typo in dochttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/67Binders library that's used in many Iris developments.2019-04-25T09:28:14ZRobbert KrebbersBinders library that's used in many Iris developments.This is the binders library that's being used in many Iris libraries (e.g. heap-lang, lambdarust, fairis, Iron, ...).
Since it's not Iris specific, I propose to put it in stdpp.This is the binders library that's being used in many Iris libraries (e.g. heap-lang, lambdarust, fairis, Iron, ...).
Since it's not Iris specific, I propose to put it in stdpp.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/66Improve performance of `set_solver`2021-05-25T09:17:29ZRobbert KrebbersImprove performance of `set_solver`This MR improves the performance of the tactic `set_unfold`, which is the core of `set_solver`. It does do this by introducing the following type class:
```coq
Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
{ set_un...This MR improves the performance of the tactic `set_unfold`, which is the core of `set_solver`. It does do this by introducing the following type class:
```coq
Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
{ set_unfold_elem_of : x ∈ X ↔ Q }.
```
This type class is more specific than `SetUnfold` since it only applies to goals of the form `x ∈ X`. As such, type class search is much faster as it will never look through the definition of `∈`, which caused `set_unfold` to be very slow for the case of `gset`; see #29.
Note that compared to my proposal in #29 there is no need for any type class opaqueness anymore. This MR should also be fully backwards compatible, but to obtain optimal performance developments may want to change their `SetUnfold (_ ∈ _) _` instances into `SetUnfoldElemOf _ _ _`. See https://gitlab.mpi-sws.org/iris/iris/commit/fdfed0e96e989e225fa32f89800ae7b189011974 for an example.
Performance stats:
- 69.61% improvement on the dreaded `algebra/gset` file in Iris
- 2.23% overall improvement on Iris
See https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=3f7f9f4e0cb404aa5936255288fa8e15a3be12b6&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Fset_unfold&var-commit2=6d17dc6d21fa2a5bdb40aa915d2748794fe8907c&var-config2=coq-8.9.0&var-group=(.*)%2F%5B%5E%2F%5D*&var-metric=instructions
This MR closes #29 and https://gitlab.mpi-sws.org/iris/iris/issues/232https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/65gmultiset lemmas2019-04-19T15:49:26ZDan Frumingmultiset lemmashttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/64Add `map_delete_zip_with`2019-03-26T17:57:50ZDan FruminAdd `map_delete_zip_with`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/62More efficient list encoding for Countable2019-03-16T12:12:59ZJakob Botsch NielsenMore efficient list encoding for CountableThis changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 1...This changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 10. The top 1-bits are not kept since we
know a 10 is starting a new element which ends with a 1.
Please don't hold back on feedback. I'm sure this could do with some improvements :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/60move the (very brief) contribution guide to the README2019-03-14T14:38:01ZRalf Jungjung@mpi-sws.orgmove the (very brief) contribution guide to the READMEI hope that makes it easier to find -- the README is rendered directly on the project page, after all.I hope that makes it easier to find -- the README is rendered directly on the project page, after all.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/59Make `gset` a `Definition` instead of `Notation`.2019-03-14T16:42:09ZRobbert KrebbersMake `gset` a `Definition` instead of `Notation`.I mainly did do this because it often confused me that when using `Set Printing All` occurrences of `gset` are turned into `mapset ...`.
However, it turned out this also has a positive effect on performance. On my machine, compilation o...I mainly did do this because it often confused me that when using `Set Printing All` occurrences of `gset` are turned into `mapset ...`.
However, it turned out this also has a positive effect on performance. On my machine, compilation of LambdaRust went from 34m2s to 33m1s, so that's an improvement of 3%. It had no significant effect on compilation times of Iris itself.