stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-10-13T15:27:45Zhttps://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_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/174LICENSE: Clarify which BSD license is being used2020-07-10T21:50:17ZPaolo G. GiarrussoLICENSE: Clarify which BSD license is being usedSister MR to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/472.Sister MR to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/472.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.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/171Sketch docs for computation on [gmap], since they're a FAQ2020-07-02T15:14:03ZPaolo G. GiarrussoSketch docs for computation on [gmap], since they're a FAQTODO:
- [x] fix line breaks, when the rest is reviewed (it destructs diffs till then).TODO:
- [x] fix line breaks, when the rest is reviewed (it destructs diffs till then).