stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-03-12T06:14:55Zhttps://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/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/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/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/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/225add pred_infinite_surj2021-03-22T11:56:18ZRalf Jungjung@mpi-sws.orgadd pred_infinite_surjI wondered when `pred_infinite (P ∘ f)` holds. This is the best lemma I could come up with so far. It's not the lemma I hoped for, but I realized the lemma I hoped for is wrong.^^ However, now that I did this proof, I figured it'd be a w...I wondered when `pred_infinite (P ∘ f)` holds. This is the best lemma I could come up with so far. It's not the lemma I hoped for, but I realized the lemma I hoped for is wrong.^^ However, now that I did this proof, I figured it'd be a waste to throw it away.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/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/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.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/216Remove hint db and import of omega, since omega will be removed from Coq.2021-01-19T11:33:34ZRobbert KrebbersRemove hint db and import of omega, since omega will be removed from Coq.See https://github.com/coq/coq/pull/13741#issuecomment-762761112See https://github.com/coq/coq/pull/13741#issuecomment-762761112https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/215add zip_with_diag and zip_diag2021-01-19T10:57:10ZRalf Jungjung@mpi-sws.orgadd zip_with_diag and zip_diaghttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/214fix and reject warnings on Coq 8.132021-01-19T10:57:59ZRalf Jungjung@mpi-sws.orgfix and reject warnings on Coq 8.13https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/213add set_map_union, set_map_singleton2021-01-15T10:36:34ZRalf Jungjung@mpi-sws.orgadd set_map_union, set_map_singleton