stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-03-15T16:15:32Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/235Add more underscores to f_equiv2021-03-15T16:15:32ZMichael SammlerAdd more underscores to f_equivhttps://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/21#note_64914 requires a version of f_equiv with 5 underscores instead of 4. This is the minimal patch to fulfil this usecase, but we could add even more underscores while we a...https://gitlab.mpi-sws.org/iris/lambda-rust/-/merge_requests/21#note_64914 requires a version of f_equiv with 5 underscores instead of 4. This is the minimal patch to fulfil this usecase, but we could add even more underscores while we are at it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/234some map lemmas2021-03-14T14:22:00ZRalf Jungjung@mpi-sws.orgsome map lemmasThis upstreams some lemmas from Perennial (so I assume the proofs are by @tchajed; I ported them to the non-ssreflect world of std++).This upstreams some lemmas from Perennial (so I assume the proofs are by @tchajed; I ported them to the non-ssreflect world of std++).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/231Many improvements to `multiset_solver`2021-03-13T07:24:13ZRobbert KrebbersMany improvements to `multiset_solver`1. Support `∈`
2. Support `⊂`
3. Support case splitting on `multiplicity x {[ y ]}`, but only do this when there's no other way.
With the improved `multiset_solver` I am able to solve pretty much all lemmas in the `gmultiset` file autom...1. Support `∈`
2. Support `⊂`
3. Support case splitting on `multiplicity x {[ y ]}`, but only do this when there's no other way.
With the improved `multiset_solver` I am able to solve pretty much all lemmas in the `gmultiset` file automatically (apart from those that involve `elements`, `size`, and other connectives that are out of scope).
The new version also handles @fpottier's test case `x ∈ X → {[x]} ⊆ X` from #86.
In addition, I added a bunch of other test cases.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/233Remove singleton notations for tuples2021-03-12T06:14:55ZRobbert KrebbersRemove singleton notations for tuplesRemove singleton notations `{[ x,y ]}` and `{[ x,y,z ]}` for `{[ (x,y) ]}` and `{[ (x,y,z) ]}`. They date back to the time we used the `singleton` class with a product for maps (there's now the `singletonM` class).Remove singleton notations `{[ x,y ]}` and `{[ x,y,z ]}` for `{[ (x,y) ]}` and `{[ (x,y,z) ]}`. They date back to the time we used the `singleton` class with a product for maps (there's now the `singletonM` class).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/57Rename multiset "union" into "disjoint union"2021-03-10T16:41:16ZRobbert KrebbersRename multiset "union" into "disjoint union"This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heig...This fixes #13. Now `∪` and `∩` are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas `⊎` is the "sum" (i.e. adding the multiplicities).
Some questions/remarks:
- `⊎` and `∪` have different heights in my font (see `⊎∪`). Is there maybe a better disjoint union symbol in unicode?
- There are probably all kinds of laws about the interaction between `∪`, `∩`, and `⊎`, like distributivity. I did not attempt to prove a comprehensive set of such laws.
- `∖` is still the operation that subtracts multiplicity. I think that's fine, since there is no sensible difference operator for multisets that matches up with the union operator.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/230coPset: some lemmas about infinity2021-03-05T21:02:23ZRalf Jungjung@mpi-sws.orgcoPset: some lemmas about infinityProofs by Joshua YanowskiProofs by Joshua Yanowskihttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/229clarify Pmap_raw comment2021-02-17T13:15:51ZRalf Jungjung@mpi-sws.orgclarify Pmap_raw commentMaking this an MR so @robbertkrebbers can check if it makes sense.Making this an MR so @robbertkrebbers can check if it makes sense.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/226Add several simple lemmas (mostly about list and map filter).2021-02-15T08:40:42ZPaulo Emílio de VilhenaAdd several simple lemmas (mostly about list and map filter).Some simple lemmas about lists and maps. The lemma `map_filter_lookup_eq'` generalises `map_filter_lookup_eq` and can be used to shorten the proof of `map_filter_iff`.Some simple lemmas about lists and maps. The lemma `map_filter_lookup_eq'` generalises `map_filter_lookup_eq` and can be used to shorten the proof of `map_filter_iff`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/228Avoid relying on buggy simpl never behavior2021-02-12T13:33:42ZTej Chajedtchajed@gmail.comAvoid relying on buggy simpl never behaviorWhat's going on in this proof is that `simpl` is unfolding both `decode_nat` _and_ `decode`, even though `decode` is marked `simpl never`. This is a bug in Coq and std++ should not rely on it.
Alternate take on
https://gitlab.inria.fr/b...What's going on in this proof is that `simpl` is unfolding both `decode_nat` _and_ `decode`, even though `decode` is marked `simpl never`. This is a bug in Coq and std++ should not rely on it.
Alternate take on
https://gitlab.inria.fr/bertot/stdpp/-/commit/895121f919c6f1332f41f658ce7f850e391eb49e,
which is used as an overlay in Coq for
https://github.com/coq/coq/pull/13448.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/227add Nat_iter_mul2021-02-09T11:15:11ZRalf Jungjung@mpi-sws.orgadd Nat_iter_mulOriginal proof by Joshua YanovskiOriginal proof by Joshua Yanovskihttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/210rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq2021-02-01T11:56:08ZRalf Jungjung@mpi-sws.orgrename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteqThis hopefully makes the lemmas easier to find.This hopefully makes the lemmas easier to find.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/224Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`2021-01-29T16:09:15ZRobbert KrebbersAdd `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/223Rename `Forall_Forall2` → `Forall_Forall2_diag`2021-01-28T11:49:19ZRobbert KrebbersRename `Forall_Forall2` → `Forall_Forall2_diag`This is to be consistent with the names for big operators in Iris.This is to be consistent with the names for big operators in Iris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/222Rename `_11` and `_12` suffixes into `_1_1` and `_1_2`2021-01-28T09:18:33ZRobbert KrebbersRename `_11` and `_12` suffixes into `_1_1` and `_1_2`Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
The previous suffixes looked like lemma number 11 and 12, respectively.Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
The previous suffixes looked like lemma number 11 and 12, respectively.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/221Fix documentation of `select` to state that it selects the "last" hypothesis.2021-01-27T17:30:44ZRobbert KrebbersFix documentation of `select` to state that it selects the "last" hypothesis.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/206Various `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.2021-01-23T10:14:39ZRobbert KrebbersVarious `omap` lemmas for finite maps; generalize `map_size_{insert,delete}`.- Add lemma `map_omap_union`.
- Add lemmas `map_disjoint_fmap` and `map_disjoint_omap`.
- Add lemmas `fmap_merge` and `omap_merge`.
- Add lemma `omap_delete`.
- Generalize `omap_insert` and `omap_singleton` to cover both the `Some` and `...- Add lemma `map_omap_union`.
- Add lemmas `map_disjoint_fmap` and `map_disjoint_omap`.
- Add lemmas `fmap_merge` and `omap_merge`.
- Add lemma `omap_delete`.
- Generalize `omap_insert` and `omap_singleton` to cover both the `Some` and `None` case. Add `_Some` and `_None` versions of the lemmas for the specific cases.
- Generalize `map_size_insert` and `map_size_delete` in the same way.
- Add lemmas `lookup_fmap_Some`, `lookup_omap_Some`, and `lookup_omap_id_Some`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/220Rename instance `finmap_lookup_total` → `map_lookup_total`.2021-01-20T12:58:57ZRobbert KrebbersRename instance `finmap_lookup_total` → `map_lookup_total`.This this is an instance, not a definition, it _should_ not affect anyone.This this is an instance, not a definition, it _should_ not affect anyone.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/217add map_zip_diag and the lemmas required for that2021-01-20T12:58:41ZRalf Jungjung@mpi-sws.orgadd map_zip_diag and the lemmas required for thatIs `map_fmap_omap` truly new? I was surprised to not find an existing lemma like that.Is `map_fmap_omap` truly new? I was surprised to not find an existing lemma like that.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/219remove unused find_pat tactic2021-01-20T11:44:26ZRalf Jungjung@mpi-sws.orgremove unused find_pat tacticCloses https://gitlab.mpi-sws.org/iris/stdpp/-/issues/93Closes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/93https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/218add rename-by-pattern tactic2021-01-20T11:31:14ZRalf Jungjung@mpi-sws.orgadd rename-by-pattern tactic`rename_pat` would be a shorter name, but OTOH this is more consistent with the existing `select`-style tactics so maybe that's the better choice.`rename_pat` would be a shorter name, but OTOH this is more consistent with the existing `select`-style tactics so maybe that's the better choice.