stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-06-25T07:57:21Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/280Misc lemmas for maps2021-06-25T07:57:21ZRobbert KrebbersMisc lemmas for maps- Add lemmas `merge_empty_l` and `merge_empty_r`.
- Add lemma `map_filter_lookup`.
- Add lemma `map_fmap_singleton_inv`.- Add lemmas `merge_empty_l` and `merge_empty_r`.
- Add lemma `map_filter_lookup`.
- Add lemma `map_fmap_singleton_inv`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/279Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.2021-06-11T11:27:08ZRobbert KrebbersDrop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.This fixes issue #94
+ Drop `DiagNone` class.
+ Add `merge_proper` instance.
+ Simplify lemmas about `merge` by dropping the `DiagNone` precondition.
+ Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and `partial_alte...This fixes issue #94
+ Drop `DiagNone` class.
+ Add `merge_proper` instance.
+ Simplify lemmas about `merge` by dropping the `DiagNone` precondition.
+ Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and `partial_alter_merge_r`.
+ Drop unused `merge_assoc'` instance, which seems unused, and seems pointless to generalize.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/278Prove more equivalences for closure operators on relations.2021-06-16T10:13:38ZRobbert KrebbersProve more equivalences for closure operators on relations.Add and extend equivalences between closure operators:
- Add `↔` lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps`.
- Rename `→` lemmas `rtc_nsteps` → `rtc_nsteps_1`,
`nsteps_rtc` → `rtc_nsteps_2`, `rtc_bsteps` → `rtc_bsteps...Add and extend equivalences between closure operators:
- Add `↔` lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps`.
- Rename `→` lemmas `rtc_nsteps` → `rtc_nsteps_1`,
`nsteps_rtc` → `rtc_nsteps_2`, `rtc_bsteps` → `rtc_bsteps_1`, and
`bsteps_rtc` → `rtc_bsteps_2`.
- Add lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps` to path
representations as lists.
The `_list` lemmas were proposed by @jules and he provided an initial proof specific to `rtc`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/277Misc improvements to `head` and `tail` functions for lists2021-06-11T13:29:34ZRobbert KrebbersMisc improvements to `head` and `tail` functions for lists + Define `head` as notation that prints (Coq defines it as `parsing only`).
+ Declare `tail` as `simpl nomatch`.
+ Add lemmas about `head` and `tail`. + Define `head` as notation that prints (Coq defines it as `parsing only`).
+ Declare `tail` as `simpl nomatch`.
+ Add lemmas about `head` and `tail`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/276Misc setoids lemmas and tweaks for maps and option2022-08-10T12:27:42ZRobbert KrebbersMisc setoids lemmas and tweaks for maps and option- Add lemmas `map_singleton_equiv_inj` and `map_fmap_equiv_inj`.
- Add lemma `option_fmap_equiv_inj`.
- Add `Proper`s for maps, and generalize existing ones. Add tests to check that the old ones can be derived.
- Add lemma `map_equiv_loo...- Add lemmas `map_singleton_equiv_inj` and `map_fmap_equiv_inj`.
- Add lemma `option_fmap_equiv_inj`.
- Add `Proper`s for maps, and generalize existing ones. Add tests to check that the old ones can be derived.
- Add lemma `map_equiv_lookup_r`.
- Add lemma `map_equiv_iff`.
Also, rename instances `option_mbind_proper` → `option_bind_proper` and `option_mjoin_proper` → `option_join_proper` to be consistent with similar instances for sets and lists.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/275sum_list_with_in2021-06-07T12:01:35ZJansum_list_with_inAdded sum_list_with_in lemmaAdded sum_list_with_in lemmahttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/274Make filter lemmas for maps and sets consistent + add cross split property for maps2021-06-08T09:36:41ZRobbert KrebbersMake filter lemmas for maps and sets consistent + add cross split property for mapsWe have the following lemmas for the combination of filter and union/disjoint for maps and sets:
```coq
Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
filter P m ∪ filter (λ v, ¬ P v) m = m.
Lemma ma...We have the following lemmas for the combination of filter and union/disjoint for maps and sets:
```coq
Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
filter P m ∪ filter (λ v, ¬ P v) m = m.
Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
filter P m ##ₘ filter (λ v, ¬ P v) m.
Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
```
There are two things that are strange here:
- The naming scheme is inconsistent: `union_filter` vs `filter_union`
- The statements of the union+filter lemmas is inconsistent
This MR aims to make the set of lemmas for maps and sets consistent. Concretely:
- Sets: Add lemmas `disjoint_filter`, `disjoint_filter_complement`, and `filter_union_complement`.
- Maps: Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and `map_union_filter` → `map_filter_union_complement` to be consistent with sets.
- Maps: Add lemmas `map_disjoint_filter` and `map_filter_union` analogous to sets.
- Maps: Use filter lemmas to prove cross split property.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/273Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.2022-01-12T17:33:55ZMatthieu SozeauDeclare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.This makes Iris & Perennial compatible with [Coq PR #13969](https://github.com/coq/coq/pull/13969). Should be entirely backwards compatible.This makes Iris & Perennial compatible with [Coq PR #13969](https://github.com/coq/coq/pull/13969). Should be entirely backwards compatible.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/271More missing `Hint Mode`s.2021-06-06T12:06:37ZRobbert KrebbersMore missing `Hint Mode`s.This MR adds all the `Hint Mode`s from @blaisorblade's https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/696 to std++ with the exception of the controversial one for `Equiv` (see https://github.com/coq/coq/issues/14441), but includin...This MR adds all the `Hint Mode`s from @blaisorblade's https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/696 to std++ with the exception of the controversial one for `Equiv` (see https://github.com/coq/coq/issues/14441), but including the ones for `Set`s.
Iris requires a one line fix, see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/696#note_68611
examples, reloc, iron, actris, and lambdarust all compile without changes.
I think we're still missing more `Hint Mode`s, but I am not sure what's a proper way to detect them.https://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_drop