stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-10-28T19:21:46Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/195add dom_insert_lookup2020-10-28T19:21:46ZRalf Jungjung@mpi-sws.orgadd dom_insert_lookupI was just looking for this lemma and couldn't find it, so I figured it might be good to add. :)I was just looking for this lemma and couldn't find it, so I figured it might be good to add. :)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/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/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/189Draft: use SProp for well-formedness condition in Pmap and gmap2021-07-27T21:03:00ZTej Chajedtchajed@gmail.comDraft: use SProp for well-formedness condition in Pmap and gmapProof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks th...Proof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks the opacity of proofs).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/188Extend the theory of positive rationals `Qp`2022-08-09T14:20:21ZRobbert KrebbersExtend the theory of positive rationals `Qp`This MR extends the theory of positive rationals `Qp`. The most important change is that it fixes the leaky abstraction, adds tons of lemmas, and no longer relies on the coercions to the non-negative rationals `Qc` to obtain notions like...This MR extends the theory of positive rationals `Qp`. The most important change is that it fixes the leaky abstraction, adds tons of lemmas, and no longer relies on the coercions to the non-negative rationals `Qc` to obtain notions like orders.
### New features
- Add the orders `Qc_le` and `Qp_lt`.
- Add a function `Qc_inv` for the multiplicative inverse.
- Define the division function `Qp_div` in terms of `Qp_inv`, and generalize the second argument from `positive` to `Qp`.
- Define a function `pos_to_Qp` that converts a `positive` into a positive rational `Qp`.
- Add many lemmas and missing type class instances, especially for orders, multiplication, multiplicative inverse, division, and the conversion.
### Technical changes:
- Remove the coercion from `Qp` to `Qc`. This follows our recent tradition of getting rid of coercions since they are more often confusing than useful.
- Rename the conversion from `Qp` to `Qc` from `Qp_car` into `Qp_to_Qc` to be consistent with other conversion functions in std++. Also rename the lemma `Qp_eq` into `Qp_to_Qc_inj_iff`.
- Use `let '(..) = ...` in the definitions of `Qp_plus`/`Qp_mult`/`Qp_inv`/`Qp_le`/`Qp_lt` to avoid Coq tactics (like `injection`) to unfold these definitions eagerly. We already used this trick in e.g., `gmap` for the same reason. This works around the Coq issue that @simonfv ran into [here](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/497#note_57334).
- Define the literals 1, 2, 3, 4 in terms of `pos_to_Qp` instead of iterated addition. This avoids weird rewrites. For example, before `2` was defined as `1 + 1`, so rewriting with `1 = stuff` in a goal containing `2` turned it into `stuff + stuff`, which was extremely confusing.
### Things to discuss
- We could use Coq's extensible notation machinery to get proper notations for the literals. AFAIK this is only possible in Coq 8.9+, so that requires us to drop support for Coq 8.8. **Do ▷**
- [x] While we are changing the API anyway, use `add`/`mul` instead of `plus`/`mult`, to be consistent with the lemmas for `nat` and `Z`.
- Also improve the `Qc` library in the same way. **Do ▷**
### Impact on reverse dependencies
This MR will cause some breakage for libraries that rely on the order on fractions, but in my opinion, this is for the better. I have ported some of the developments that use fractions in interesting ways, namely Iris, Iron, and LambdaRust. While stuff broke, I managed to shorten proofs significantly by making use of the new lemmas introduced in this MR. Also, after this MR, none of these developments rely on the conversion to `Qc` anymore, showing that we indeed provide a reasonable API now.
Some stats:
- Iris: 66 insertions, 78 deletions
- LambdaRust: 32 insertions, 63 deletions
- Iron: no changes needed
- Examples: no changed needed, after [removing an unused lemma](https://gitlab.mpi-sws.org/iris/examples/-/commit/5df249005c6f8d906e28022a7c61beaa7578834d)
- gpfls: 8 insertions, 8 deletions
To land this MR, we should first merge https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/497.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/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/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/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/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/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/179Add lemmas and max for Qp2020-10-27T13:54:55ZSimon Friis VindumAdd lemmas and max for QpAdd a few extra lemmas for `Qp` and adds a `max` operation for `Qp`. The lemmas for `max` are not exhaustive. The names of the lemmas are consistent with those in [GenericMinMax](https://coq.inria.fr/library/Coq.Structures.GenericMinMax....Add a few extra lemmas for `Qp` and adds a `max` operation for `Qp`. The lemmas for `max` are not exhaustive. The names of the lemmas are consistent with those in [GenericMinMax](https://coq.inria.fr/library/Coq.Structures.GenericMinMax.html).
The library `GenericMinMax` contains a way to implement `max` (see for instance [how it's used with `Q`](https://coq.inria.fr/library/Coq.QArith.Qminmax.html)). I'm not sure if that's the better way to do it. But, modules aren't used in this way anywhere in stdpp so I opted to not use it.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/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/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_53746