stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-06-29T09:52:27Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/270Various improvements to `Permutation` lemmas and instances2021-06-29T09:52:27ZRobbert KrebbersVarious improvements to `Permutation` lemmas and instancesVarious changes to `Permutation` lemmas:
+ Rename `Permutation_nil` → `Permutation_nil_r` and
and `Permutation_singleton` → `Permutation_singleton_r`.
+ Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
+ Add new instance ...Various changes to `Permutation` lemmas:
+ Rename `Permutation_nil` → `Permutation_nil_r` and
and `Permutation_singleton` → `Permutation_singleton_r`.
+ Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
+ Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`.
+ Add lemma `Permutation_cross_split`.
+ Make lemma `elem_of_Permutation` a biimplication
Also, I made the following changes that should not affect users:
+ Name `Proper` and `Inj` instances for `Permutation` as `operation_Permutation_{Proper,inj,inj_l,inj_r}`
+ Remove `Proper` instances for `::` and `++` that are already supplied by the std lib.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/269Strengthen `map_filter_strong_ext` and `map_filter_ext`.2021-06-28T17:51:26ZDan FruminStrengthen `map_filter_strong_ext` and `map_filter_ext`.I just added it as another lemma, but it is also possible to change "implies" to "iff" in the `map_filter_strong_ext` itself.I just added it as another lemma, but it is also possible to change "implies" to "iff" in the `map_filter_strong_ext` itself.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/267Add lemma `set_fold_disj_union_strong`.2021-06-02T15:44:40ZRobbert KrebbersAdd lemma `set_fold_disj_union_strong`.Stronger version of a lemma suggested by @jihgfee.
TODO: Not sure about the name.Stronger version of a lemma suggested by @jihgfee.
TODO: Not sure about the name.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/266Add a few lemmas2021-06-02T15:19:21ZSimon Friis VindumAdd a few lemmasAdd a few lemmas.Add a few lemmas.https://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.