stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2019-06-18T08:34:09Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/73add unfolding lemma for bool_decide: bool_decide_decide2019-06-18T08:34:09ZRalf Jungjung@mpi-sws.orgadd unfolding lemma for bool_decide: bool_decide_decidehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/72SeqZ Function2020-03-17T20:34:30ZSimon SpiesSeqZ FunctionThis MR adds a simple range function on integers to stdpp.
Calling `range m n` results in the range `m, m + 1, ..., n - 1` and is empty, if `m >= n`.This MR adds a simple range function on integers to stdpp.
Calling `range m n` results in the range `m, m + 1, ..., n - 1` and is empty, if `m >= n`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/71Some missing results about vectors.2019-06-14T16:02:55ZRobbert KrebbersSome missing results about vectors.This addresses https://gitlab.mpi-sws.org/iris/stdpp/issues/33
I did not include any of the `map` lemmas, since we have versions of them for `fmap` (notation `<$>`).
I find the following lemma pretty weird:
```coq
Lemma vec_to_list_ta...This addresses https://gitlab.mpi-sws.org/iris/stdpp/issues/33
I did not include any of the `map` lemmas, since we have versions of them for `fmap` (notation `<$>`).
I find the following lemma pretty weird:
```coq
Lemma vec_to_list_take_drop {A n} (i : fin n) (v : vec A n) :
vtake i v ++ vdrop i v = v.
Proof. by rewrite vec_to_list_take, vec_to_list_drop, take_drop. Qed.
```
It involves implicit coercions to list, and it uses the append on lists.
Unless @lepigre has a good reason for it, I rather not include it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/70Strings are inhabited2019-05-17T13:04:27ZPaolo G. GiarrussoStrings are inhabitedAdd instance for `Inhabited string`; usually you can rely on stdpp having all the instances you'd expect, which is pretty cool, so let's fix this small exception :smiley:Add instance for `Inhabited string`; usually you can rely on stdpp having all the instances you'd expect, which is pretty cool, so let's fix this small exception :smiley:https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/69Fix typo in instance name2019-05-17T11:19:20ZPaolo G. GiarrussoFix typo in instance nameHoping nothing relies on this name.Hoping nothing relies on this name.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/68Fix typo in doc2019-04-26T09:42:21ZPaolo G. GiarrussoFix typo in dochttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/67Binders library that's used in many Iris developments.2019-04-25T09:28:14ZRobbert KrebbersBinders library that's used in many Iris developments.This is the binders library that's being used in many Iris libraries (e.g. heap-lang, lambdarust, fairis, Iron, ...).
Since it's not Iris specific, I propose to put it in stdpp.This is the binders library that's being used in many Iris libraries (e.g. heap-lang, lambdarust, fairis, Iron, ...).
Since it's not Iris specific, I propose to put it in stdpp.https://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/63Add a .editorconfig file2019-03-22T13:07:53ZJakob Botsch NielsenAdd a .editorconfig filehttps://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/61More efficient `Countable` instance for list and make `namespaces` independen...2019-03-15T12:46:59ZRobbert KrebbersMore efficient `Countable` instance for list and make `namespaces` independent of that.It turns out we once had a more efficient Countable instance for lists, see 54954f55839cdb7a840188fd01c1231669a0c18e.
I have reverted that commit and fixed up namespaces.
This closes #28 ?It turns out we once had a more efficient Countable instance for lists, see 54954f55839cdb7a840188fd01c1231669a0c18e.
I have reverted that commit and fixed up namespaces.
This closes #28 ?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.