stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2019-04-25T09:28:14Zhttps://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/68Fix typo in doc2019-04-26T09:42:21ZPaolo G. GiarrussoFix typo in dochttps://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/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/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/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/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/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/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/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/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/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/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/86std++ 1.2.1 release notes2019-08-13T14:01:01ZRalf Jungjung@mpi-sws.orgstd++ 1.2.1 release notesCc @robbertkrebbersCc @robbertkrebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/84More lemmas about [map_imap].2019-08-13T14:17:31ZRodolphe LepigreMore lemmas about [map_imap].I hope these are at the right place!I hope these are at the right place!https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/85Several simple lemmas.2019-08-14T22:11:03ZPaulo Emílio de VilhenaSeveral simple lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/87relations.nsteps: add inversion lemma for `nsteps R 1 a b`2019-08-23T10:42:50ZPaolo G. Giarrussorelations.nsteps: add inversion lemma for `nsteps R 1 a b`