stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-10-26T09:46:19Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/183Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.2020-10-26T09:46:19ZHugo HerbelinSwap import of Peano and Utf8 to ensure that Utf8 notations are preferred.Coq PR [#12950](https://github.com/coq/coq/pull/12950), among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing `le n m` as either `m <= n` or `m ≤ n`, due ...Coq PR [#12950](https://github.com/coq/coq/pull/12950), among others changes, gives to import the effect of reactivating the imported notations.
This has an impact for stdpp, e.g. on printing `le n m` as either `m <= n` or `m ≤ n`, due to the order of imports between `Utf8.v` and `Peano.v` in `base.v`.
The Coq PR is still at the beginning of a process of discussion but the change to stdpp is backward compatible (as far as I can judge) and it should be safe to merge it anyway.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/194Add map_fmap_union for FinMap2020-10-21T06:57:40ZTej Chajedtchajed@gmail.comAdd map_fmap_union for FinMaphttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/193Avoid relying on implicit instance generalization, and name some instances.2020-10-15T17:44:59ZRobbert KrebbersAvoid relying on implicit instance generalization, and name some instances.Fix in preparation for https://github.com/coq/coq/pull/13188
I didn't name the `Forall2` instances, since I could not come up with a good naming scheme. So, I just used the `∀`.
There are probably plenty of other unnamed instances, but...Fix in preparation for https://github.com/coq/coq/pull/13188
I didn't name the `Forall2` instances, since I could not come up with a good naming scheme. So, I just used the `∀`.
There are probably plenty of other unnamed instances, but I would prefer defer naming them.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/190Drop support for Coq 8.8 and 8.92020-10-13T15:27:45ZRalf Jungjung@mpi-sws.orgDrop support for Coq 8.8 and 8.9This lets us clean up some little things (see this MR), and it enables some major improvements to `gmap` and `Qp` by relying on definitionally proof-irrelevant propositions.
I asked last evening on Mattermost if anyone still uses std++ ...This lets us clean up some little things (see this MR), and it enables some major improvements to `gmap` and `Qp` by relying on definitionally proof-irrelevant propositions.
I asked last evening on Mattermost if anyone still uses std++ with such old versions of Coq. So far, nobody responded, but it has been less than 24h. On the other hand, such users can just stick to std++ 1.4.0.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/192Draft: Drop misleading gmultiset_simple_set instance2020-10-12T09:51:39ZPaolo G. GiarrussoDraft: Drop misleading gmultiset_simple_set instanceThe problem is that `elem_of_subseteq_singleton` applies to multiset goals, but uses the wrong instance.
> [...] when my goal is a multiset elem-of, then `apply gmultiset_elem_of_singleton_subseteq.` and `apply elem_of_subseteq_singleton...The problem is that `elem_of_subseteq_singleton` applies to multiset goals, but uses the wrong instance.
> [...] when my goal is a multiset elem-of, then `apply gmultiset_elem_of_singleton_subseteq.` and `apply elem_of_subseteq_singleton.` result in different goals that print exactly the same (also btw note the inconsistent lemma name)
Based on a suggestion by Robbert (which I might have misunderstood); but I'm not sure this is the right fix.
This instance appears to not be used, and it allows applying lemmas like `elem_of_subseteq_singleton` which are inappropriate for gmultiset, as they use the `set_subseteq` instance for `SubsetEq`, instead of `gmultiset_subseteq : SubsetEq (gmultiset A)`.
However, the lemmas should be restated in terms of `gmultiset`, since they do hold, and they hold on sensible instances.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/191update Makefile2020-10-06T15:03:28ZRalf Jungjung@mpi-sws.orgupdate MakefileJust using an MR to make sure this builds on CI.Just using an MR to make sure this builds on CI.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/187Add Qp lemmas2020-10-02T11:38:34ZSimon Friis VindumAdd Qp lemmasAdds a two additional lemmas for `Qp`.
Also renames a few lemmas that accidentally had `Qc` in their name instead of `Qp`. These where introduced back in !179 so it's probably safe to assume that no one are using the misnamed ones.Adds a two additional lemmas for `Qp`.
Also renames a few lemmas that accidentally had `Qc` in their name instead of `Qp`. These where introduced back in !179 so it's probably safe to assume that no one are using the misnamed ones.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/186add version of Qp_lower_bound that returns less-than facts2020-10-01T08:39:19ZRalf Jungjung@mpi-sws.orgadd version of Qp_lower_bound that returns less-than factsMainly, this has the advantage of showing up when doing `SearchAbout (_ < _)%Qc`.
Possibly this lemma could be generalized to work with all `Qc`, not just `Qp`, but then we couldn't reuse the existing `Qp_lower_bound`.Mainly, this has the advantage of showing up when doing `SearchAbout (_ < _)%Qc`.
Possibly this lemma could be generalized to work with all `Qc`, not just `Qp`, but then we couldn't reuse the existing `Qp_lower_bound`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/177[simpl_map]: avoid using [rewrite .. by ..]2020-09-29T09:36:43ZArmaël Guéneau[simpl_map]: avoid using [rewrite .. by ..]We've been using a patched version of [simpl_map] in our project for a while, with the changes included here.
The core issue is that it seems that [rewrite .. by ..] is not available when explicitly importing ssreflect.
The patch uses `...We've been using a patched version of [simpl_map] in our project for a while, with the changes included here.
The core issue is that it seems that [rewrite .. by ..] is not available when explicitly importing ssreflect.
The patch uses `by tac` instead, which is in line with what [simplify_map_eq] does later in the file.
I tried to write a quick test to demonstrate the issue; however it seems that triggering it is a bit subtle
(while it does definitely occur on our development, I wasn't able to easily reproduce it on my synthetic example---
I think there is some interaction with the exact order of the Require Import invocations).
If deemed necessary I could try harder and try to minimize a problematic instance from our development.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/185Add "options" file2020-09-29T09:14:09ZRalf Jungjung@mpi-sws.orgAdd "options" fileFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/81
There is a slight chance that setting `Set Default Proof Using "Type*"` in a file where the option was not present before adds some extra assumptions to lemmas. I made sure everyth...Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/81
There is a slight chance that setting `Set Default Proof Using "Type*"` in a file where the option was not present before adds some extra assumptions to lemmas. I made sure everything still compiles and will also test Iris against this branch. But @robbertkrebbers if you want to be extra sure this doesn't add any unnecessary assumptions elsewhere, I will make those files `Unset Default Proof Using`; someone will have to manually investigate each lemma to check the assumptions.
Thanks to @tchajed we can even set the default goal selector. :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/49silence fewer warnings, add comment about overwriting notation2020-09-25T08:44:33ZRalf Jungjung@mpi-sws.orgsilence fewer warnings, add comment about overwriting notation@robbertkrebbers could you expand the comment to explain *why* we are doing this? Seems rather unfortunate.@robbertkrebbers could you expand the comment to explain *why* we are doing this? Seems rather unfortunate.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/184Switch to strict bulleting everywhere2020-09-15T20:51:25ZTej Chajedtchajed@gmail.comSwitch to strict bulleting everywhereSolve iris/stdpp#82.
The flag isn't enforced anywhere, but with this we can add it seamlessly (ideally soon after so there aren't more violations that creep in).Solve iris/stdpp#82.
The flag isn't enforced anywhere, but with this we can add it seamlessly (ideally soon after so there aren't more violations that creep in).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/182make sure std++ does not rely on generated names2020-08-31T16:11:27ZRalf Jungjung@mpi-sws.orgmake sure std++ does not rely on generated nameshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/181fix various uses of generated names2020-08-30T08:50:01ZRalf Jungjung@mpi-sws.orgfix various uses of generated namesThis makes the entire std++ build with name mangling on Coq master.This makes the entire std++ build with name mangling on Coq master.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/178Add `insert_replicate_strong`.2020-08-28T13:21:34ZDan FruminAdd `insert_replicate_strong`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/180list.v: avoid using mangled names2020-08-28T09:47:03ZRalf Jungjung@mpi-sws.orglist.v: avoid using mangled namesThis is needed to fix list.v compilation with name mangling enabled. I stopped after this file.This is needed to fix list.v compilation with name mangling enabled. I stopped after this file.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/176Remove `map` infix in lemmas about `dom` and `filter`.2020-07-17T12:51:49ZRobbert KrebbersRemove `map` infix in lemmas about `dom` and `filter`.The combination of `dom` and `filter` only makes sense for maps, so the `map` infix is useless. Other similar lemmas do not have such an infix either, so it's also inconsistent.
Rename `dom_map filter` → `dom_filter`, `dom_map_filter_...The combination of `dom` and `filter` only makes sense for maps, so the `map` infix is useless. Other similar lemmas do not have such an infix either, so it's also inconsistent.
Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`, and `dom_map_filter_subseteq` → `dom_filter_subseteq`.
This was pointed out by @atrieu in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/175#note_53746https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/175Additional lemmas about map_imap2020-07-16T12:02:33ZAlix TrieuAdditional lemmas about map_imapSome lemmas that were useful to me in a development.Some lemmas that were useful to me in a development.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/172Lemmas about "filter" on maps2020-07-15T17:07:02ZRalf Jungjung@mpi-sws.orgLemmas about "filter" on mapsThese are some lemmas from Perennial about "filter" on maps. Most are by me; `map_filter_insert_not_delete` is by @tchajed (original name: `map_filter_insert_not_strong`).These are some lemmas from Perennial about "filter" on maps. Most are by me; `map_filter_insert_not_delete` is by @tchajed (original name: `map_filter_insert_not_strong`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/173prove NoDup_fmap_2_strong2020-07-15T16:45:29ZRalf Jungjung@mpi-sws.orgprove NoDup_fmap_2_strongAnother lemma that I just needed in Perennial.Another lemma that I just needed in Perennial.