stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2019-08-27T11:59:15Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/83Proofs about binders2019-08-27T11:59:15ZMichael SammlerProofs about bindersNow that POPL deadline is over, here are some more lemmata. As always let me know if I should change anything.Now that POPL deadline is over, here are some more lemmata. As always let me know if I should change anything.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/82some list lemmas2019-07-13T10:10:01ZRalf Jungjung@mpi-sws.orgsome list lemmasJust needed these for a proof, seems general enough.Just needed these for a proof, seems general enough.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/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/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/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/77some lemmas for seq and imap2019-07-04T13:25:44ZMichael Sammlersome lemmas for seq and imapSome lemmas regarding `seq` and `imap` that I use in my developmentSome lemmas regarding `seq` and `imap` that I use in my developmenthttps://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/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/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/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/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/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`