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/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/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/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/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/260add insert_take_drop2021-05-19T09:31:56ZRalf Jungjung@mpi-sws.orgadd insert_take_drophttps://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/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/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/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/254Add little endian encoding of Z2021-05-17T20:30:33ZMichael SammlerAdd little endian encoding of Zhttps://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/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/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/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_65864https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/248Add lemmas about testbit on bounded integers2021-04-19T10:13:23ZMichael SammlerAdd lemmas about testbit on bounded integersThese proofs are originally by @paulzhu, which is why I put him as the author of this commit. This is a part of !244.These proofs are originally by @paulzhu, which is why I put him as the author of this commit. This is a part of !244.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/247Add tactic `learn_hyp`, fixes #732021-04-19T12:30:59ZMichael SammlerAdd tactic `learn_hyp`, fixes #73This is another part of !244 and fixes #73.This is another part of !244 and fixes #73.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/246Add more typeclasses2021-04-15T08:03:48ZMichael SammlerAdd more typeclassesThis adds the typeclasses from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244. See also the discussion here: https://mattermost.mpi-sws.org/iris/pl/37b8m6pmdfr3pfwwjssre3oqjcThis adds the typeclasses from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244. See also the discussion here: https://mattermost.mpi-sws.org/iris/pl/37b8m6pmdfr3pfwwjssre3oqjchttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/245Add more lemmas for FinMaps (for union, filter, difference)2021-07-28T14:24:18ZHai DangAdd more lemmas for FinMaps (for union, filter, difference)Some lemmas that I believe worth upstreaming.Some lemmas that I believe worth upstreaming.