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/272check for missing 'Hint Mode'2021-06-17T07:37:40ZRalf Jungjung@mpi-sws.orgcheck for missing 'Hint Mode'As requested in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/271#note_68769
Here's the current list of classes with missing `Hint Mode`:
```
No 'Global Hint Mode' for class 'TCNoBackTrack'
No 'Global Hint Mode' for class 'TCIf...As requested in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/271#note_68769
Here's the current list of classes with missing `Hint Mode`:
```
No 'Global Hint Mode' for class 'TCNoBackTrack'
No 'Global Hint Mode' for class 'TCIf'
No 'Global Hint Mode' for class 'TCTrue'
No 'Global Hint Mode' for class 'TCFalse'
No 'Global Hint Mode' for class 'Inj'
No 'Global Hint Mode' for class 'Inj2'
No 'Global Hint Mode' for class 'Cancel'
No 'Global Hint Mode' for class 'Surj'
No 'Global Hint Mode' for class 'IdemP'
No 'Global Hint Mode' for class 'Comm'
No 'Global Hint Mode' for class 'LeftId'
No 'Global Hint Mode' for class 'RightId'
No 'Global Hint Mode' for class 'Assoc'
No 'Global Hint Mode' for class 'LeftAbsorb'
No 'Global Hint Mode' for class 'RightAbsorb'
No 'Global Hint Mode' for class 'AntiSymm'
No 'Global Hint Mode' for class 'Total'
No 'Global Hint Mode' for class 'Trichotomy'
No 'Global Hint Mode' for class 'TrichotomyT'
No 'Global Hint Mode' for class 'FinSet'
No 'Global Hint Mode' for class 'MonadSet'
No 'Global Hint Mode' for class 'TCFastDone'
No 'Global Hint Mode' for class 'Maybe'
No 'Global Hint Mode' for class 'Maybe2'
No 'Global Hint Mode' for class 'Maybe3'
No 'Global Hint Mode' for class 'Maybe4'
No 'Global Hint Mode' for class 'DiagNone'
No 'Global Hint Mode' for class 'FinMapDom'
No 'Global Hint Mode' for class 'FinMap'
No 'Global Hint Mode' for class 'SetUnfoldSimpl'
No 'Global Hint Mode' for class 'QuoteLookup'
No 'Global Hint Mode' for class 'Quote'
No 'Global Hint Mode' for class 'MakeNatS'
No 'Global Hint Mode' for class 'MakeNatPlus'
```
This MR is blocked on those getting fixed first.https://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/83