stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-06-25T15:21:23Zhttps://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/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/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/283Rewrite cross split lemmas so they can more easily be used for forward reasoning.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/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/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/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.