stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-06-02T15:09:21Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/265Add function `map_kmap` that transforms the keys of a finite map.2021-06-02T15:09:21ZRobbert KrebbersAdd function `map_kmap` that transforms the keys of a finite map.This function `map_kmap f` allows one to turn maps with keys `K1` (e.g., `gmap K1 A`) into maps with keys `K2` (e.g., `gmap K2 A`), where `f : K1 → K2`.
Notes:
- The function `f` should be injective, otherwise `map_kmap f` is ill-behav...This function `map_kmap f` allows one to turn maps with keys `K1` (e.g., `gmap K1 A`) into maps with keys `K2` (e.g., `gmap K2 A`), where `f : K1 → K2`.
Notes:
- The function `f` should be injective, otherwise `map_kmap f` is ill-behaved. Consider `map_kmap (λ _, 0) {[ 0 := 10, 1 := 20 ]}`. What's the result of that? Well, that depends on how the map is exactly represented (for `gmap` that depends on how exactly the `Countable` instances are defined).
- There are tons of generalizations of this function possible, e.g., with functions `f` that go to `option K2` so that elements can be dropped, etc (similar to `omap` versus `fmap`), or that could also take the values into account (similar to `imap` versus `fmap`). I think the version in this MR is useful because it enjoys nice lemmas. Maybe in the future we could define a generic version and define the one in this MR in terms of a more generic version.
- Some of the lemmas hold without `Inj` (e.g. `lookup_map_kmap_None`). I don't think there's a point in doing that because then I can no longer use the generic lemmas about `list_to_map`, also `map_kmap f` where `f` is not injective is ill-behaved (as previously stated).
Thanks @jules for the suggestion and feedback.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/268Comment about `EqDecision` in `Countable`.2021-05-31T06:12:03ZRobbert KrebbersComment about `EqDecision` in `Countable`.Comments based on question by @haidang
@haidang Please review.Comments based on question by @haidang
@haidang Please review.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/263Explicit visibility for Instances2021-05-25T10:13:11ZRalf Jungjung@mpi-sws.orgExplicit visibility for InstancesOur existing check for this missed some cases:
- `Existing Instance`
- `Program Instance`
- `Instance:` (for anonymous instances)
Those are all detected now, so fix all the code accordingly.Our existing check for this missed some cases:
- `Existing Instance`
- `Program Instance`
- `Instance:` (for anonymous instances)
Those are all detected now, so fix all the code accordingly.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/264list lookup lemmas: cons, singleton2021-05-25T09:11:28ZRalf Jungjung@mpi-sws.orglist lookup lemmas: cons, singletonI was quite surprised to not find lemmas like this when I just was looking for them...I was quite surprised to not find lemmas like this when I just was looking for them...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/262explicitly declare visibility of Scope actions2021-05-20T09:33:20ZRalf Jungjung@mpi-sws.orgexplicitly declare visibility of Scope actionsI assume these were deliberately `Global`?I assume these were deliberately `Global`?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/260add insert_take_drop2021-05-19T09:31:56ZRalf Jungjung@mpi-sws.orgadd insert_take_drophttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/261add tactic for solving computable goals2021-05-18T08:57:47ZRalf Jungjung@mpi-sws.orgadd tactic for solving computable goalsFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/83Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/83https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/254Add little endian encoding of Z2021-05-17T20:30:33ZMichael SammlerAdd little endian encoding of Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/255add Countable instance for decidable Sigma types2021-05-06T07:05:11ZSimon Gregersenadd Countable instance for decidable Sigma typesThis instance became useful when working with, e.g., a type for elements of a set `{ a : A | a ∈ X }` and wanting to construct a `gmap` with this domain.This instance became useful when working with, e.g., a type for elements of a set `{ a : A | a ∈ X }` and wanting to construct a `gmap` with this domain.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/256`_True`/`_False` lemmas for `decide` and `mguard`2021-05-04T10:05:59ZRobbert Krebbers`_True`/`_False` lemmas for `decide` and `mguard`For `decide` we currently have the following lemmas:
```coq
Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemm...For `decide` we currently have the following lemmas:
```coq
Lemma decide_True {A} `{Decision P} (x y : A) : P → (if decide P then x else y) = x.
Lemma decide_False {A} `{Decision P} (x y : A) : ¬P → (if decide P then x else y) = y.
Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
```
The first two are most commonly used, whereas the last two are also applicable if you do a `match` on `decide` and use the proof of `P` or `¬P`.
For `guard` we have similar lemmas that correspond to the first two lemmas for `decide`.
```coq
Lemma option_guard_True {A} P `{Decision P} (mx : option A) : P → (guard P; mx) = mx.
Lemma option_guard_False {A} P `{Decision P} (mx : option A) : ¬P → (guard P; mx) = None.
```
However, these don't work for `guard P as HP; ... something containing HP ...`, so I wanted to have lemmas like the last two for `decide`. The one for `False` can be generalized trivially, but (like `decide`) the one for `True` only works if the proposition is proof irrelevant:
```coq
Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A) (HP : P) : mguard P f = f HP.
Lemma option_guard_False {A} P `{Decision P} (f : P → option A) : ¬P → mguard P f = None.
```
(Note that `guard P as HP; y` is notation for `mguard P (λ HP, y)`).
The main problem, as usual, is naming... The `_left` and `_right` suffixes for `decide` make no sense for `guard`. So instead, I propose the `_pi` suffix for proof irrelevant. Opinions about that?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/257make Z.of_nat not a coercion inside std++2021-04-30T14:32:36ZRalf Jungjung@mpi-sws.orgmake Z.of_nat not a coercion inside std++This takes a first step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 by not declaring the coercion in std++. We will add it back in Iris. This can help gauge the fallout of https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102...This takes a first step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 by not declaring the coercion in std++. We will add it back in Iris. This can help gauge the fallout of https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102, and it would have caught [this problem](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/254/diffs#note_66469).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/259Don't use Z.to_nat in definition of rotate2021-04-29T13:39:11ZMichael SammlerDon't use Z.to_nat in definition of rotateSee https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/257#note_66496See https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/257#note_66496https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/258make Qc_of_Z not a Coercion any more2021-04-29T12:00:09ZRalf Jungjung@mpi-sws.orgmake Qc_of_Z not a Coercion any moreThis implements https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 for `Qc_of_Z` -- `Qc` is not a widely used type (any more) so I think the fallout from this should be quite limited.This implements https://gitlab.mpi-sws.org/iris/stdpp/-/issues/102 for `Qc_of_Z` -- `Qc` is not a widely used type (any more) so I think the fallout from this should be quite limited.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/253Fix pretty printing of multset literals + add tests2021-04-21T07:03:32ZRobbert KrebbersFix pretty printing of multset literals + add testshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/251Introduce `SingletonMS` class for multiset singletons.2021-04-20T16:44:32ZRobbert KrebbersIntroduce `SingletonMS` class for multiset singletons.- Define set-like notation `{[+ x1; ..; xn ]}` for multisets in terms of the new
singleton class and disjoint union `⊎`.
- Remove `SemiSet` instance for multisets.
- Prove lemmas regarding `∈` and `∉` for multisets since we no longer g...- Define set-like notation `{[+ x1; ..; xn ]}` for multisets in terms of the new
singleton class and disjoint union `⊎`.
- Remove `SemiSet` instance for multisets.
- Prove lemmas regarding `∈` and `∉` for multisets since we no longer get the
generic versions for sets.
- Provide `SetUnfoldElemOf` instances for multisets since we no longer get the
generic versions for sets.
- Prove lemmas new regarding `∈` and `∉` for `∩`
Fixes #100, #98 and #87.
This MR is an alternative to !232.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/232Multiset set notation2021-04-20T14:59:03ZRobbert KrebbersMultiset set notationThis MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100This MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/252Fix inconsistent arguments of `subset_difference_elem_of`.2021-04-20T09:36:50ZRobbert KrebbersFix inconsistent arguments of `subset_difference_elem_of`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/13Provide an Infinite typeclass and a generic implementation of Fresh.2021-04-20T08:43:36ZGhost UserProvide an Infinite typeclass and a generic implementation of Fresh.This provides a generic implementation of Fresh for infinite types.
In detail, it adds:
- An Infinite type class. A type T is infinite if there is an injection from nat to T.
- A generic implementation of Fresh A C for an infinite type ...This provides a generic implementation of Fresh for infinite types.
In detail, it adds:
- An Infinite type class. A type T is infinite if there is an injection from nat to T.
- A generic implementation of Fresh A C for an infinite type A and a finite collection type C, by way of linear search for a fresh element.
- Instances of Infinite for a handful of types, including positive/natural/integer types and string.
- A generic Fresh for finite collections of strings. As an implementation detail, the generated strings are all of the form "~n" for some natural number n.
- Some minor additions (pretty-printer for nat, Fix unfolding lemma for setoids).Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/249Add list_to_map_app2021-04-20T08:41:11ZMichael SammlerAdd list_to_map_appSee discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244#note_65864See discussion at https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244#note_65864