stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-11-24T20:50:26Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/338Add reverse_lookup, reverse_lookup_Some and alternative version of sublist_lo...2021-11-24T20:50:26ZMichael SammlerAdd reverse_lookup, reverse_lookup_Some and alternative version of sublist_lookup_SomeThis MR adds `reverse_lookup`, `reverse_lookup_Some` and an alternative version of `sublist_lookup_Some`This MR adds `reverse_lookup`, `reverse_lookup_Some` and an alternative version of `sublist_lookup_Some`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/337Upstreaming a small collection of lemmas2021-11-25T02:33:50ZMichael SammlerUpstreaming a small collection of lemmasThis MR upstreams a small collection of lemmas from Islaris.This MR upstreams a small collection of lemmas from Islaris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/336Fix coq-lint.sh on macOS2021-11-23T20:43:21ZTej Chajedtchajed@gmail.comFix coq-lint.sh on macOSFixes the build on macOS. Once this is merged I'll make the same fix to Iris.Fixes the build on macOS. Once this is merged I'll make the same fix to Iris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/335Add lemma `map_subseteq_inv`.2021-11-22T15:12:14ZRobbert KrebbersAdd lemma `map_subseteq_inv`.As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing
It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the p...As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing
It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the property up, closer towards other properties on the order.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/334normalize for Fail printing locations2021-11-13T02:07:06ZRalf Jungjung@mpi-sws.orgnormalize for Fail printing locationsAdjusts test suite for https://github.com/coq/coq/pull/15174Adjusts test suite for https://github.com/coq/coq/pull/15174https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/333std++ 1.6.0 release notes2021-11-05T17:28:26ZTej Chajedtchajed@gmail.comstd++ 1.6.0 release notesCreating a new std++ release will fix #119, and allow us to release Iris 3.5.0.
This is a pretty big release, with over 400 commits from 14 authors!
I got the author list with `git shortlog --summary coq-stdpp-1.5.0..HEAD | gsed -E 's/...Creating a new std++ release will fix #119, and allow us to release Iris 3.5.0.
This is a pretty big release, with over 400 commits from 14 authors!
I got the author list with `git shortlog --summary coq-stdpp-1.5.0..HEAD | gsed -E 's/[ \\t]+/ /g' | cut -d' ' -f3-100`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/332base.v: fix typo in comment about MonadSet, and extend2021-10-26T14:00:05ZPaolo G. Giarrussobase.v: fix typo in comment about MonadSet, and extendThe comment hints at `listset_nodup`, which does _not_ have a MonadSet instance.The comment hints at `listset_nodup`, which does _not_ have a MonadSet instance.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/330Normalize focused goal output2021-10-13T17:36:37ZTej Chajedtchajed@gmail.comNormalize focused goal outputMerge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.
std++ does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the ...Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.
std++ does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the test normalization.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/329Mark set_size and set_fold as TC opaque2021-10-26T12:51:32ZPaolo G. GiarrussoMark set_size and set_fold as TC opaqueUpdated according to suggestions.
-------
Old title/description:
More TC opaqueness (appropriate???)
Take these as questions, and feel free to edit/close/... . Follow up from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/328.Updated according to suggestions.
-------
Old title/description:
More TC opaqueness (appropriate???)
Take these as questions, and feel free to edit/close/... . Follow up from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/328.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/328fin_sets: add missing Params instance for `set_map`2021-10-05T18:27:36ZPaolo G. Giarrussofin_sets: add missing Params instance for `set_map`Noticed from VERY slow rewrites.Noticed from VERY slow rewrites.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/327countable.v: prove choose_proper2021-11-05T17:07:35ZPaolo G. Giarrussocountable.v: prove choose_proper~~Needs the misplaced `Acc_rect_max`.~~
Add missing properness lemma for choose.
Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.~~Needs the misplaced `Acc_rect_max`.~~
Add missing properness lemma for choose.
Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/326f_equiv: slightly better support for function relations2021-09-27T14:17:27ZRalf Jungjung@mpi-sws.orgf_equiv: slightly better support for function relationsThis makes f_equiv more powerful: with it we can solve goals of the form `f x ≡ g x` where `f, g: X -d> OFE` and `f ≡ g`. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applie...This makes f_equiv more powerful: with it we can solve goals of the form `f x ≡ g x` where `f, g: X -d> OFE` and `f ≡ g`. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applies, it will finish the proof, so I added a `solve`.
I also added the testcases from https://gitlab.mpi-sws.org/iris/stdpp/-/commit/d16ab1aaa77ed3a9b052d12496d92c102288b704.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/325f_equiv optimizations2021-10-02T15:12:18ZRalf Jungjung@mpi-sws.orgf_equiv optimizationsThis makes f_equiv a lot faster.
The first commit is inspired by looking at [this line](https://github.com/mit-pdos/perennial/blob/3ebb6f05456e2378e687e7eb99c30001930ff396/src/program_logic/crash_weakestpre.v#L105) in Perennial: the ver...This makes f_equiv a lot faster.
The first commit is inspired by looking at [this line](https://github.com/mit-pdos/perennial/blob/3ebb6f05456e2378e687e7eb99c30001930ff396/src/program_logic/crash_weakestpre.v#L105) in Perennial: the very first f_equiv there takes 30s. 20s of that are spent in `simple apply (_ : Proper (R ==> R) f)`, where `f` is `bi_and <some complicated term>` -- basically is tries to treat bi_and as a unary function and takes forever to realize that will not work. There is no TC trace for this, so this must be all unification time. By changing the pattern for this arm from `?R (?f _) _` to `?R (?f _) (?f _)` we avoid entering it unless things match *syntactically*. This seeds up the first f_equiv from 30s to 10s.
The second commit is born from looking at that same line more, and also looking at [the equivalent line in Iris itself](https://gitlab.mpi-sws.org/iris/iris/-/blob/467fa48bc66c2f2459f379a69fd9a41840599e23/iris/program_logic/weakestpre.v#L122): according to the ltac profiler, almost all time is spent in `try simple apply reflexivity` -- again, unification of inequal terms being very slow. So we now do entirely syntactic unification before even trying this. This speeds up the `do 23 (f_contractive || f_equiv)` in Iris from 1.3s to 0.6s, and it speeds up the `do 22 (f_contractive || f_equiv)` in Perennial to 0.75s from originally 42s (22s after the previous commit) -- a whopping 50x overall improvement!
Later commits slightly relax this to fix compatibility, so the fallback cases now do perform unification to match up the functions on the left-hand and right-hand side -- but this barely slows down the benchmarks mentioned above since they do not usually hit those cases. In fact, both in the Iris and Perennial case, 66% of the time is now spent in `f_contractive`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/324add size_difference2021-09-10T15:07:06ZRalf Jungjung@mpi-sws.orgadd size_differencehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/323add size_set_seq2021-09-13T21:16:30ZRalf Jungjung@mpi-sws.orgadd size_set_seqhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/322Revert "Merge branch 'robbert/sprop' into 'master'"2021-09-08T21:26:20ZRalf Jungjung@mpi-sws.orgRevert "Merge branch 'robbert/sprop' into 'master'"This reverts merge request !309. It turned out to be a breaking change due to shadowing imports, and also cause performance regression in at least one case (see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/732#note_73457).This reverts merge request !309. It turned out to be a breaking change due to shadowing imports, and also cause performance regression in at least one case (see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/732#note_73457).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/321add map_size_disj_union2021-09-05T02:48:55ZRalf Jungjung@mpi-sws.orgadd map_size_disj_unionhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/320relate size of map to size of its domain2021-09-05T03:04:45ZRalf Jungjung@mpi-sws.orgrelate size of map to size of its domainhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/319add lemma list_in_dec2021-09-06T18:03:40ZRalf Jungjung@mpi-sws.orgadd lemma list_in_decI think this lemma is by @haidang, but it might also be by @lgaeher.
Maybe this should be an `Instance`? Not sure.I think this lemma is by @haidang, but it might also be by @lgaeher.
Maybe this should be an `Instance`? Not sure.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/318treat Forall2 constructors like we treat Forall constructors2021-09-06T16:19:42ZRalf Jungjung@mpi-sws.orgtreat Forall2 constructors like we treat Forall constructorsIn particular, have a lemma `Forall2_cons` that is an `↔`.
For consistency, rename `Forall2_cons_inv` to `Forall2_cons_1` (matching `Forall_cons_1`).
Someone should probably do the same for `Forall3`...In particular, have a lemma `Forall2_cons` that is an `↔`.
For consistency, rename `Forall2_cons_inv` to `Forall2_cons_1` (matching `Forall_cons_1`).
Someone should probably do the same for `Forall3`...