stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-05-25T09:17:29Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/66Improve performance of `set_solver`2021-05-25T09:17:29ZRobbert KrebbersImprove performance of `set_solver`This MR improves the performance of the tactic `set_unfold`, which is the core of `set_solver`. It does do this by introducing the following type class:
```coq
Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
{ set_un...This MR improves the performance of the tactic `set_unfold`, which is the core of `set_solver`. It does do this by introducing the following type class:
```coq
Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
{ set_unfold_elem_of : x ∈ X ↔ Q }.
```
This type class is more specific than `SetUnfold` since it only applies to goals of the form `x ∈ X`. As such, type class search is much faster as it will never look through the definition of `∈`, which caused `set_unfold` to be very slow for the case of `gset`; see #29.
Note that compared to my proposal in #29 there is no need for any type class opaqueness anymore. This MR should also be fully backwards compatible, but to obtain optimal performance developments may want to change their `SetUnfold (_ ∈ _) _` instances into `SetUnfoldElemOf _ _ _`. See https://gitlab.mpi-sws.org/iris/iris/commit/fdfed0e96e989e225fa32f89800ae7b189011974 for an example.
Performance stats:
- 69.61% improvement on the dreaded `algebra/gset` file in Iris
- 2.23% overall improvement on Iris
See https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=3f7f9f4e0cb404aa5936255288fa8e15a3be12b6&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Fset_unfold&var-commit2=6d17dc6d21fa2a5bdb40aa915d2748794fe8907c&var-config2=coq-8.9.0&var-group=(.*)%2F%5B%5E%2F%5D*&var-metric=instructions
This MR closes #29 and https://gitlab.mpi-sws.org/iris/iris/issues/232https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/65gmultiset lemmas2019-04-19T15:49:26ZDan Frumingmultiset lemmashttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/64Add `map_delete_zip_with`2019-03-26T17:57:50ZDan FruminAdd `map_delete_zip_with`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/62More efficient list encoding for Countable2019-03-16T12:12:59ZJakob Botsch NielsenMore efficient list encoding for CountableThis changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 1...This changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 10. The top 1-bits are not kept since we
know a 10 is starting a new element which ends with a 1.
Please don't hold back on feedback. I'm sure this could do with some improvements :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/60move the (very brief) contribution guide to the README2019-03-14T14:38:01ZRalf Jungjung@mpi-sws.orgmove the (very brief) contribution guide to the READMEI hope that makes it easier to find -- the README is rendered directly on the project page, after all.I hope that makes it easier to find -- the README is rendered directly on the project page, after all.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/59Make `gset` a `Definition` instead of `Notation`.2019-03-14T16:42:09ZRobbert KrebbersMake `gset` a `Definition` instead of `Notation`.I mainly did do this because it often confused me that when using `Set Printing All` occurrences of `gset` are turned into `mapset ...`.
However, it turned out this also has a positive effect on performance. On my machine, compilation o...I mainly did do this because it often confused me that when using `Set Printing All` occurrences of `gset` are turned into `mapset ...`.
However, it turned out this also has a positive effect on performance. On my machine, compilation of LambdaRust went from 34m2s to 33m1s, so that's an improvement of 3%. It had no significant effect on compilation times of Iris itself.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/58Overhaul of the `Infinite`/`Fresh` infrastructure2019-03-03T14:51:16ZRobbert KrebbersOverhaul of the `Infinite`/`Fresh` infrastructureOverhaul of the `Infinite`/`Fresh` infrastructure.
- The class `Infinite A` is now defined as having a function
`fresh : list A → A`, that given a list `xs`, gives an element `x ∉ xs`.
- For most types this `fresh` function has a sens...Overhaul of the `Infinite`/`Fresh` infrastructure.
- The class `Infinite A` is now defined as having a function
`fresh : list A → A`, that given a list `xs`, gives an element `x ∉ xs`.
- For most types this `fresh` function has a sensible computable behavior,
for example:
+ For numbers, it yields one added to the maximal element in `xs`.
+ For strings, it yields the first string representation of a number that is
not in `xs`.
- For any type `C` of finite sets with elements of infinite type `A`, we lift
the fresh function to `C → A`.
As a consequence:
- It is now possible to pick fresh elements from _any_ finite set and from
_any_ list with elements of an infinite type. Before it was only possible
for specific finite sets, e.g. `gset`, `pset`, ...
- It makes the code more uniform. There was a lot of overlap between having a
`Fresh` and an `Infinite` instance. This got unified.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/57Rename multiset "union" into "disjoint union"2021-03-10T16:41:16ZRobbert KrebbersRename multiset "union" into "disjoint union"This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heig...This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heights in my font (see `⊎∪`). Is there maybe a better disjoint union symbol in unicode?
- There are probably all kinds of laws about the interaction between `∪`, `∩`, and `⊎`, like distributivity. I did not attempt to prove a comprehensive set of such laws.
- `∖` is still the operation that subtracts multiplicity. I think that's fine, since there is no sensible difference operator for multisets that matches up with the union operator.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/56Notion of (in)finite predicates2019-02-21T20:33:00ZRobbert KrebbersNotion of (in)finite predicatesAs discussed in https://gitlab.mpi-sws.org/iris/iris/merge_requests/217
I have directly taken the opportunity to state `set_finite` using the new `pred_finite`.As discussed in https://gitlab.mpi-sws.org/iris/iris/merge_requests/217
I have directly taken the opportunity to state `set_finite` using the new `pred_finite`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/55Additionally lemmas for insert, nth, take, and list_find2019-02-21T16:57:32ZHai DangAdditionally lemmas for insert, nth, take, and list_findJust some several useful lemmas for lists.Just some several useful lemmas for lists.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/54Seal `fresh_generic`.2019-02-07T13:00:52ZRobbert KrebbersSeal `fresh_generic`.Since `fresh_generic` is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics.
This issue actually occurred in iGPS, as reported by...Since `fresh_generic` is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics.
This issue actually occurred in iGPS, as reported by Hai.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/53Confluent relations2019-02-10T20:44:10ZRobbert KrebbersConfluent relationsThis MR adds:
- The symmetric and reflexive/transitive/symmetric closure of a relation
- Different notions of confluence: diamond property, confluence, local confluence (following the naming conventions in https://www21.in.tum.de/~nipko...This MR adds:
- The symmetric and reflexive/transitive/symmetric closure of a relation
- Different notions of confluence: diamond property, confluence, local confluence (following the naming conventions in https://www21.in.tum.de/~nipkow/TRaAT/)
- Standard properties such as diamond ⊢ confluence ⊢ local confluence, the Church-Rosser property, Newman's lemma
As part of this MR, I removed the hint database `ars`. The name made no sense and it was not used anywhere to my knowledge. If it was used anywhere, it would be very unreliable as it contained hints like `rtc_trans` that would generally lead to loops.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/52fix or silence Coq 8.10 warnings2019-02-20T21:54:22ZRalf Jungjung@mpi-sws.orgfix or silence Coq 8.10 warningshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/51fix λ.. printing and test it2019-01-24T18:27:52ZRalf Jungjung@mpi-sws.orgfix λ.. printing and test ithttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/50Make trivial instances explicit2019-01-24T08:32:46ZMaxime DénèsMake trivial instances explicitThis is in preparation for coq/coq#9274.
Should be backward compatible but that remains to be tested.This is in preparation for coq/coq#9274.
Should be backward compatible but that remains to be tested.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/48`tc_to_bool` to turn a type class into a Boolean that expresses if there is a...2019-02-06T14:01:10ZRobbert Krebbers`tc_to_bool` to turn a type class into a Boolean that expresses if there is an instanceThis MR introduces the following function:
```coq
(** Given a proposition [P] that is a type class, [bool_of_tc P] will return
[true] iff there is an instance of [P]. *)
Definition bool_of_tc (P : Prop)
{p : bool} `{TCIf P (TCEq...This MR introduces the following function:
```coq
(** Given a proposition [P] that is a type class, [bool_of_tc P] will return
[true] iff there is an instance of [P]. *)
Definition bool_of_tc (P : Prop)
{p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : bool := p.
```
It's particularly useful in Ltac, where it's sometimes needed to figure out if an instance exists or not. An example use can be found in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/199https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/47Get rid of the awk.Makefile references2018-12-15T12:01:55ZDan FruminGet rid of the awk.Makefile referencesDoesn't seem that its necessaryDoesn't seem that its necessaryhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/46Add results about deleting and inserting filtered out elements2018-12-16T09:39:46ZMichael SammlerAdd results about deleting and inserting filtered out elementshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/45Consistently use `set_` prefix.2019-02-20T17:58:14ZRobbert KrebbersConsistently use `set_` prefix.The MR closes #24.
- Consistently `set_` prefixes (instead of `collection_`).
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection` is called `SemiSet`, and `FinCollection` is called `FinSet`, and `Collection...The MR closes #24.
- Consistently `set_` prefixes (instead of `collection_`).
- Rename the `Collection` type class into `Set_`. Likewise, `SimpleCollection` is called `SemiSet`, and `FinCollection` is called `FinSet`, and `CollectionMonad` is called `MonadSet`.
- Rename `collections.v` and `fin_collections.v` into `sets.v` and `fin_sets.v`, respectively.
- Rename `set A := A → Prop` (`theories/set.v`) into `propset`, and likewise `bset` into `boolset`.
- Consistently prefer `X_to_Y` for conversion functions, e.g. `list_to_map` instead of the former `map_of_list`.
## Sed script uses
This MR is the result of the following `sed` script. It only had one bug, it wrongly replaced `Vector.of_list` into `Vector.set_of_list`. Note that I'm not using `\b` all the time because I also wanted to fix up lemma names.
```
sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
s/to\_gmap/gset\_to\_gmap/g;
s/of\_bools/bools\_to\_natset/g;
s/to_bools/natset\_to\_bools/g;
' -i $(find -name "*.v")
```
# Impact on dependencies
I have patches for Iris, lambdarust, Iron, fri-coq and iris-examples. The amount of renaming that had to be done was fairly minimal, and was mostly done automatically using the above `sed` script.
- Iris: 42 lines changed
- Iris-examples: 8 lines changed
- Iron: no changes needed
- Lambdarust: 17 lines changed
- Fri-coq: 83 lines changed (mostly changing `set` into `propset` by hand)