stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-11-26T10:24:52Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/203Replace unused pattern variables with underscore2020-11-26T10:24:52ZTej Chajedtchajed@gmail.comReplace unused pattern variables with underscoreAddresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).
I'm pretty sure the `hlist.v` warning is a bug in Coq's heuristics for this, since those variables are used as implicit ar...Addresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).
I'm pretty sure the `hlist.v` warning is a bug in Coq's heuristics for this, since those variables are used as implicit arguments and I don't see why the pattern matches more than one case (the warning is also printed twice for the same definition). Maybe there's something in the elaborated term I'm missing, which Coq doesn't even print back?
Regardless of what's going on in Coq, it's much easier for us to suppress the warning than to try to fix this upstream.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/202Add explicit Global to hints at top level2020-12-03T17:17:30ZTej Chajedtchajed@gmail.comAdd explicit Global to hints at top levelFixes new Coq master warning deprecated-hint-without-locality: https://github.com/coq/coq/pull/13384.
I created this largely automatically based on the assumption that hints in sections would be indented. If some aren't, this MR will ch...Fixes new Coq master warning deprecated-hint-without-locality: https://github.com/coq/coq/pull/13384.
I created this largely automatically based on the assumption that hints in sections would be indented. If some aren't, this MR will change them to global when they should be left alone (implicitly as local). I haven't carefully audited that this didn't happen.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/201Set `Hint Mode` for `pretty`.2020-11-12T12:17:24ZRobbert KrebbersSet `Hint Mode` for `pretty`.Title says it all.Title says it all.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/200Pretty-print 0 as "0" for N, Z, and nat2020-11-11T16:03:15ZRobbert KrebbersPretty-print 0 as "0" for N, Z, and natAlternative to #198 that is correct. This MR also:
- Adds test cases.
- Proves injectivity of `pretty` for `Z`.
- Refactored the code a bit by turning some results into lemmas.Alternative to #198 that is correct. This MR also:
- Adds test cases.
- Proves injectivity of `pretty` for `Z`.
- Refactored the code a bit by turning some results into lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/199Add lemmas about `list_to_map`2020-11-10T11:51:29ZSimon Friis VindumAdd lemmas about `list_to_map`Adds two lemmas about `list_to_map` that seem generally useful.Adds two lemmas about `list_to_map` that seem generally useful.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/198WIP: Pretty-print 0 as "0" for N, Z, and nat2020-11-10T10:29:06ZTej Chajedtchajed@gmail.comWIP: Pretty-print 0 as "0" for N, Z, and natFormerly printed as an empty string.Formerly printed as an empty string.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/197Remove dead type classes and notations.2020-10-28T19:00:01ZRobbert KrebbersRemove dead type classes and notations.These were very specific, there were no lemmas about them. They were used back in the days for some specific things in my C semantics.
Thanks to @blaisorblade for pointing out.These were very specific, there were no lemmas about them. They were used back in the days for some specific things in my C semantics.
Thanks to @blaisorblade for pointing out.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/196add a function to obtain a set with all elements of a finite type2020-10-29T09:20:15ZRalf Jungjung@mpi-sws.orgadd a function to obtain a set with all elements of a finite typeThis lets us use the existing nice `gmap`/`gset` infrastructure even for total functions when the domain type is finite.This lets us use the existing nice `gmap`/`gset` infrastructure even for total functions when the domain type is finite.https://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).