stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-06-28T17:51:26Zhttps://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/288Make sum_inhabited_r not a copy of sum_inhabited_l2021-06-27T11:41:34ZPaolo G. GiarrussoMake sum_inhabited_r not a copy of sum_inhabited_lThis existed at least as far back as
iris/stdpp@361308c7b173f353afd99499e8bfcf168fdab1ca, 8 years ago.This existed at least as far back as
iris/stdpp@361308c7b173f353afd99499e8bfcf168fdab1ca, 8 years ago.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/285add {fst,snd}_map_zip2021-06-27T11:25:50ZRalf Jungjung@mpi-sws.orgadd {fst,snd}_map_zipLemmas and proofs by @msammlerLemmas and proofs by @msammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/287rename insert_delete → insert_delete_insert; add new insert_delete matching d...2021-06-26T20:45:07ZRalf Jungjung@mpi-sws.orgrename insert_delete → insert_delete_insert; add new insert_delete matching delete_insertAs [discussed](https://mattermost.mpi-sws.org/iris/pl/kcrrarwgt3bhikewccqxyrb3za) this is currently inconsistent.
I propose we use `insert_delete` for the lemma with a precondition since it is used 7 times in std++ after this MR; the on...As [discussed](https://mattermost.mpi-sws.org/iris/pl/kcrrarwgt3bhikewccqxyrb3za) this is currently inconsistent.
I propose we use `insert_delete` for the lemma with a precondition since it is used 7 times in std++ after this MR; the one without a precondition is used just 3 times (one of which is to prove `insert_delete`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/286Fix potential stack overflow related to `Pretty N`.2021-06-25T15:21:23ZRobbert KrebbersFix potential stack overflow related to `Pretty N`.As reported by @simongregersen at https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E, lemmas involving `Pretty N` could lead to stack overflow. I minimized his problem as follows:
```coq
Lemma...As reported by @simongregersen at https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E, lemmas involving `Pretty N` could lead to stack overflow. I minimized his problem as follows:
```coq
Lemma test_no_stack_overflow p n :
get n (pretty (N.pos p)) ≠ Some "_"%char →
get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
Proof. intros Hlem. apply Hlem. (* stack overflow *) Qed.
```
The problem is that Coq's conversion unfolds too much, and triggers the `wf_guard 32` in:
```coq
Definition pretty_N_go (x : N) : string → string :=
pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
```
The `wf_guard` is needed to make sure that computation of `pretty n` for concrete numbers `n` works (see tests in `tests/pretty.v`). However, due to concrete number 32, which adds `2 ^ n` `Acc_intro` constructors to the opaque accessibility proof `N.lt_wf_0` for the well-founded recursion, Coq's conversion might unfold `wf_guard 32` too eagerly.
I hence changed the `32` into `S (N.size_nat x)`, which causes the tests in `tests/pretty.v` to still work, and the stack overflow to disappear. The key idea is that `S (N.size_nat x)` is not a concrete number if `x` is an open term, thus preventing `wf_guard` from unfolding.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/284Add a few set and map related lemmas2021-06-25T10:08:08ZSimon Friis VindumAdd a few set and map related lemmasTodo
- [x] Update changelogTodo
- [x] Update changeloghttps://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/283Rewrite cross split lemmas so they can more easily be used for forward reason...2021-06-18T13:29:51ZRobbert KrebbersRewrite cross split lemmas so they can more easily be used for forward reasoning.Before our cross split lemmas looked like (we have such lemmas for Permutation, Qp, and maps):
```coq
la ++ lb ≡ₚ l →
lc ++ ld ≡ₚ l →
∃ lac lad lbc lbd,
lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld...Before our cross split lemmas looked like (we have such lemmas for Permutation, Qp, and maps):
```coq
la ++ lb ≡ₚ l →
lc ++ ld ≡ₚ l →
∃ lac lad lbc lbd,
lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.
```
This MR changes them to look like:
```coq
la ++ lb ≡ₚ lc ++ ld →
∃ lac lad lbc lbd,
lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.
```
The explicit `l` in the old lemma statement was rather annoying. First, it made the proof longer (we immediately substituted it). Second, it made the lemma harder to use because you cannot use it with `apply .. in ..` or the `%` introduction pattern. Example in Iron that shows that the new lemma is easier:
```diff
diff --git a/theories/iron_logic/iron.v b/theories/iron_logic/iron.v
index 2723897..f8864da 100644
--- a/theories/iron_logic/iron.v
+++ b/theories/iron_logic/iron.v
@@ -171,8 +171,7 @@ Proof.
rewrite /Uniform=> HP1 HP2 π1 π2. rewrite !fracPred_at_sep. apply (anti_symm _).
- apply bi.exist_elim=> -[π1'|]; apply bi.exist_elim=> -[π2'|];
apply bi.pure_elim_l; rewrite ?(inj_iff Some) //.
- + intros. destruct (Qp_cross_split (π1 + π2) π1 π2 π1' π2')
- as (π'&π''&π'''&π''''&<-&<-&<-&<-)=> //.
+ + intros (π'&π''&π'''&π''''&<-&<-&<-&<-)%Qp_cross_split.
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/281Various setoids lemmas for maps, lists, and option2021-06-17T21:32:02ZRobbert KrebbersVarious setoids lemmas for maps, lists, and optionThis MR adds various setoid lemmas.
Primarily: it's often useful to turn a setoid equality into a Leibniz equality. For boring elements like None, nil, and empty we have `ma ≡ None ↔ ma = None`, `l ≡ [] ↔ l = []`, and `m ≡ ∅ ↔ m = ∅`. F...This MR adds various setoid lemmas.
Primarily: it's often useful to turn a setoid equality into a Leibniz equality. For boring elements like None, nil, and empty we have `ma ≡ None ↔ ma = None`, `l ≡ [] ↔ l = []`, and `m ≡ ∅ ↔ m = ∅`. For other functions, this is a bit more complicated, but there are useful results nonetheless. For example:
```coq
Lemma Some_equiv_eq mx y : mx ≡ Some y ↔ ∃ y', mx = Some y' ∧ y' ≡ y.
Lemma app_equiv_eq l k1 k2 :
l ≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡ k1 ∧ k2' ≡ k2.
Lemma map_union_equiv_eq (m1 m2a m2b : M A) :
m1 ≡ m2a ∪ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∪ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
```
This MR adds such lemmas for all map operations, some lists operations.
For `Some` we had like 4 variants of the lemma. I removed all of those, and created a new lemma `equiv_Some` that follows the scheme for the other operations.
----
## Concrete changes
Option:
- Add `Proper` instances for `union`, `union_with`, `intersection_with`, and `difference_with`.
- Rename `equiv_None` → `None_equiv_eq`.
- Replace `equiv_Some_inv_l`, `equiv_Some_inv_r`, `equiv_Some_inv_l'`, and `equiv_Some_inv_r'` by new lemma `Some_equiv_eq` that follows the pattern of other ≡-inversion lemmas: it uses a `↔` and puts the arguments of `≡` and `=` in consistent order.
List:
- Add ≡-inversion lemmas `nil_equiv_eq`, `cons_equiv_eq`, `list_singleton_equiv_eq`, and `app_equiv_eq`.
- Add lemmas `Permutation_equiv` and `equiv_Permutation`.
Maps:
- Add `map_filter_proper`
- Rename `map_equiv_empty` → `map_empty_equiv_eq`.
- Add ≡-inversion lemmas `insert_equiv_eq`, `delete_equiv_eq`, `map_union_equiv_eq`, etc.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/282Add lemmas `map_intersection_filter` and `map_difference_filter`.2021-06-17T14:31:41ZRobbert KrebbersAdd lemmas `map_intersection_filter` and `map_difference_filter`.See also the discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/697/diffs#note_69805See also the discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/697/diffs#note_69805https://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/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/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/274Make filter lemmas for maps and sets consistent + add cross split property fo...2021-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/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/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/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.