stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-06-28T17:51:37Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/290Update changelog for filter extensionality lemmas2021-06-28T17:51:37ZSimon Friis VindumUpdate changelog for filter extensionality lemmasI think this MR makes the changes a bit more clear and it adds the rename to the sed script.I think this MR makes the changes a bit more clear and it adds the rename to the sed script.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/289add mk_evar tactic (to replace Coq's strange evar tactic) and use it2021-07-16T13:57:06ZRalf Jungjung@mpi-sws.orgadd mk_evar tactic (to replace Coq's strange evar tactic) and use itSee [discussion on Mattermost](https://mattermost.mpi-sws.org/iris/pl/m88qt68ggiyhmyb3bqa7yant1w)See [discussion on Mattermost](https://mattermost.mpi-sws.org/iris/pl/m88qt68ggiyhmyb3bqa7yant1w)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/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/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 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/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 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/273Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is a...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.