stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-03-31T13:36:25Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/132Replace explicit use of Inj instances by inj2020-03-31T13:36:25ZPaolo G. GiarrussoReplace explicit use of Inj instances by injThis was inconsistent and not explained before. And I noticed when talking with Herbelin about view inference.This was inconsistent and not explained before. And I noticed when talking with Herbelin about view inference.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/131random collection of lemmas2020-04-08T07:26:43ZMichael Sammlerrandom collection of lemmasThese are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the `rotate` function. Let me know what you think and which lemmas seem useful. Also better proofs ...These are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the `rotate` function. Let me know what you think and which lemmas seem useful. Also better proofs are always appreciated.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129Fix `Export` order for `length`. Remove `length` hack in strings.2020-04-11T10:35:00ZRobbert KrebbersFix `Export` order for `length`. Remove `length` hack in strings.The notation in `strings` was a hack to shadow the `length` function on strings with those on lists.
@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, `stdpp.base` exports `Coq.Stri...The notation in `strings` was a hack to shadow the `length` function on strings with those on lists.
@msammler and I figured out how to change the imports to fix this problem without the hack. Basically, `stdpp.base` exports `Coq.Strings` and `Coq.List` in the right order, so the shadowing is done right. As a consequence `Coq.Strings` should never be exported by hand.
This approach seems to work among all supported Coq versions.
We also added a test.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/128add sed script for 1.3.02020-04-02T09:31:03ZRalf Jungjung@mpi-sws.orgadd sed script for 1.3.0Original sed script by @tchajed. I added `s/\bdom_map_filter\b/dom_map_filter_subseteq/g` and `s/\bseqZ_fmap\b/fmap_add_seqZ/g`.Original sed script by @tchajed. I added `s/\bdom_map_filter\b/dom_map_filter_subseteq/g` and `s/\bseqZ_fmap\b/fmap_add_seqZ/g`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/127Update CHANGELOG for 1.3 release.2020-03-18T09:20:57ZRobbert KrebbersUpdate CHANGELOG for 1.3 release.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/126Make lemmas for `seq` and `seqZ` consistent.2020-03-18T15:51:22ZRobbert KrebbersMake lemmas for `seq` and `seqZ` consistent.This closes issue #57This closes issue #57https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/125Lookup total lemmas2020-03-17T20:45:23ZRobbert KrebbersLookup total lemmasThis closes issue #50 and is a more complete alternative to !109.
This MR includes all lemmas that I think make sense. See also the discussion there.This closes issue #50 and is a more complete alternative to !109.
This MR includes all lemmas that I think make sense. See also the discussion there.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/124Remove copyright headers, update LICENCE file.2020-03-13T12:39:10ZRobbert KrebbersRemove copyright headers, update LICENCE file.This follows https://gitlab.mpi-sws.org/iris/iris/merge_requests/387.
This closes issue #54.This follows https://gitlab.mpi-sws.org/iris/iris/merge_requests/387.
This closes issue #54.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/123Change mode of `TCEq`.2023-10-06T13:45:12ZRobbert KrebbersChange mode of `TCEq`.See https://gitlab.mpi-sws.org/iris/iris/merge_requests/391See https://gitlab.mpi-sws.org/iris/iris/merge_requests/391https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/122Avoid using Hint Resolve with a term2020-03-10T13:56:24ZTej Chajedtchajed@gmail.comAvoid using Hint Resolve with a termThis feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).
Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).
Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/121Set `Hint Mode` for logical `TCX` type classes2020-03-10T15:33:35ZRobbert KrebbersSet `Hint Mode` for logical `TCX` type classesThis closes issue #55.
Note that both arguments of `TCEq` are outputs, which makes `TCEq` symmetric. We could make one the input argument and the other the output argument, but this requires some change to Iris without obvious benefits....This closes issue #55.
Note that both arguments of `TCEq` are outputs, which makes `TCEq` symmetric. We could make one the input argument and the other the output argument, but this requires some change to Iris without obvious benefits.
/cc @msammler @jannohttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/120Rename `fin_of_nat` → `nat_to_fin` to follow the conventions.2020-03-05T22:13:06ZRobbert KrebbersRename `fin_of_nat` → `nat_to_fin` to follow the conventions.Rename `fin_of_nat` into `nat_to_fin`, `fin_to_of_nat` into `fin_to_nat_to_fin`, and `fin_of_to_nat` into `nat_to_fin_to_nat`, to follow the conventions in Iris, and also the recent rename for the similar `vec` functions.Rename `fin_of_nat` into `nat_to_fin`, `fin_to_of_nat` into `fin_to_nat_to_fin`, and `fin_of_to_nat` into `nat_to_fin_to_nat`, to follow the conventions in Iris, and also the recent rename for the similar `vec` functions.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/117Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption2020-02-28T12:15:58ZArmaël GuéneauAdd destruct_or tactics to (possibly repeatedly) split disjunctions in an assumptionFollowing `split_and`, the new tactics are `split_or H`, `split_or? H` and `split_or! H`. The name `H` is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).
I was pondering wheth...Following `split_and`, the new tactics are `split_or H`, `split_or? H` and `split_or! H`. The name `H` is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).
I was pondering whether the tactic should be `split_or H` or `split_or in H`. The second one follows the usual pattern of `in`+assumption, but at the same time there is not going to be a `split_or` tactic that works on the goal, so...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/116Add `set_solver` support for `dom`2020-02-24T14:12:11ZRobbert KrebbersAdd `set_solver` support for `dom`This MR closes issue #53.
@armael can you review/check if this sufficient for what you had in mind?This MR closes issue #53.
@armael can you review/check if this sufficient for what you had in mind?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/115Countable instance for vec, and rename `vec_to_list_of_list` into `vec_to_list_to_vec`2020-02-24T16:11:55ZRobbert KrebbersCountable instance for vec, and rename `vec_to_list_of_list` into `vec_to_list_to_vec`This is an alternative to !114, which does not involve defining a partial function from lists to vectors, but makes use of the already existing function `list_to_vec`.
Also I renamed `vec_to_list_of_list` into `vec_to_list_to_vec`. The ...This is an alternative to !114, which does not involve defining a partial function from lists to vectors, but makes use of the already existing function `list_to_vec`.
Also I renamed `vec_to_list_of_list` into `vec_to_list_to_vec`. The former appears to be a leftover of the big `X_of_Y` into `Y_to_X` rename.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/113Rename `cogpick` to `coGpick` (oops).2020-02-23T14:44:32ZDavid SwaseyRename `cogpick` to `coGpick` (oops).We renamed `cogset` to `coGset`, but my search and replace missed `cogpick`.
Pinging @robbertkrebbers.We renamed `cogset` to `coGset`, but my search and replace missed `cogpick`.
Pinging @robbertkrebbers.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/112move coPset-generic hint to coPset.v2020-02-19T15:13:29ZRalf Jungjung@mpi-sws.orgmove coPset-generic hint to coPset.vI see no good reason for it to be in `namespaces.v`. The old one that got removed in e09f7ce35f22efb51bc1dd1f04f7b54b30280ea1 was in `coPset.v` as well.I see no good reason for it to be in `namespaces.v`. The old one that got removed in e09f7ce35f22efb51bc1dd1f04f7b54b30280ea1 was in `coPset.v` as well.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/111Add class `TopSet` for sets with ⊤ element2020-02-18T12:14:11ZRobbert KrebbersAdd class `TopSet` for sets with ⊤ elementThis closes issue #49. Some remarks:
- It's called `TopSet`, which corresponds with `SemiSet`.
- We now have a generic `SetUnfoldElemOf` for any `TopSet`.
- The `Hint Resolve coPset_top_subseteq : core` no longer works because the lemma...This closes issue #49. Some remarks:
- It's called `TopSet`, which corresponds with `SemiSet`.
- We now have a generic `SetUnfoldElemOf` for any `TopSet`.
- The `Hint Resolve coPset_top_subseteq : core` no longer works because the lemma is generic in a type class. AFAIK it is only used for `solve_ndisjoint`, so I added a specialized version to the `ndisj` hint database. We already have specialized versions of other set lemmas there.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/110Add decidability instances for Z.gt and Z.ge2020-02-13T21:16:07ZTej Chajedtchajed@gmail.comAdd decidability instances for Z.gt and Z.geUnfortunately these are not just defined as flipped versions of `Z.lt` and `Z.ge`.Unfortunately these are not just defined as flipped versions of `Z.lt` and `Z.ge`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/108cogset2020-02-20T22:24:17ZDavid SwaseycogsetAdd a type `cogset A` of finite/cofinite sets of elements of countable type `A`. When `A` is also infinite, all the usual operations are decidable. The implementation uses a pair of constructors (finite or infinite) each carrying a finit...Add a type `cogset A` of finite/cofinite sets of elements of countable type `A`. When `A` is also infinite, all the usual operations are decidable. The implementation uses a pair of constructors (finite or infinite) each carrying a finite set.
The file includes efficient conversions to and from `gset A` (for finite cogsets) and to `coPset` (for arbitrary cogsets), as well as less efficient conversions to and from other finite sets and other sets with a top element.
Two things are marked TODO in the source, which really means "to discuss".