stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-01-11T17:18:29Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/209prove take_02021-01-11T17:18:29ZRalf Jungjung@mpi-sws.orgprove take_0This is taken from Perennial.This is taken from Perennial.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/211upstream some list_numbers lemmas from Perennial2021-01-11T19:10:10ZRalf Jungjung@mpi-sws.orgupstream some list_numbers lemmas from PerennialAlso rename `seq_S_end_app` to `seq_S_snoc`, which I think better matches our usual name for lemmas involving `_ ++ [_]`.
The proofs are by @tchajed.Also rename `seq_S_end_app` to `seq_S_snoc`, which I think better matches our usual name for lemmas involving `_ ++ [_]`.
The proofs are by @tchajed.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/212Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib2021-01-11T19:42:41ZRobbert KrebbersRename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlibThe lemma `seq_S` is present in Coq's stdlib since Coq 8.12, and is the same as our lemma `seq_S_snoc`.
MR !211 accidentally used the lemma `seq_S` from the stdlib, and hence CI failed with Coq 8.10 and Coq 8.11.
This MR adds a copy of...The lemma `seq_S` is present in Coq's stdlib since Coq 8.12, and is the same as our lemma `seq_S_snoc`.
MR !211 accidentally used the lemma `seq_S` from the stdlib, and hence CI failed with Coq 8.10 and Coq 8.11.
This MR adds a copy of the lemma from the stdlib, which we can remove once we drop support for Coq 8.10 and Coq 8.11.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/208prove map_size_delete, map_size_insert_Some, map_to_list_delete2021-01-11T19:43:38ZRalf Jungjung@mpi-sws.orgprove map_size_delete, map_size_insert_Some, map_to_list_delete`map_size_insert_Some` exists in Perennial as map_size_insert_overwrite, but with a very different proof.`map_size_insert_Some` exists in Perennial as map_size_insert_overwrite, but with a very different proof.https://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_singletonhttps://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/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/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/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/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/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/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/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/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/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/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/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/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/227add Nat_iter_mul2021-02-09T11:15:11ZRalf Jungjung@mpi-sws.orgadd Nat_iter_mulOriginal proof by Joshua YanovskiOriginal proof by Joshua Yanovski