stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-05-11T12:55:42Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/377drop support for Coq 8.112022-05-11T12:55:42ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.11This lets us make progress in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/376.This lets us make progress in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/376.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/376make dom domain type paremeter (D) implicit2022-05-19T18:37:53ZRalf Jungjung@mpi-sws.orgmake dom domain type paremeter (D) implicitFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/137Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/137https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/378Rename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.2022-05-13T07:45:09ZRobbert KrebbersRename seal lemmas from `_eq` to `_unseal` and make sealing stuff `Local`.As discussed in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/778#note_80612As discussed in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/778#note_80612https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/379Set `Hint Mode` for `FinSet`.2022-05-13T14:55:32ZRobbert KrebbersSet `Hint Mode` for `FinSet`.This fixes issue #139.This fixes issue #139.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/380Enable cumulativity for telescopes2022-05-18T02:20:39ZJannoEnable cumulativity for telescopesThis fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/461 by enabling cumulative universe polymorphism in telescopes.v, allowing `tele` at a fixed universe (such as the `Quant` universe in iris) to cumulatively contain telescopes at s...This fixes https://gitlab.mpi-sws.org/iris/iris/-/issues/461 by enabling cumulative universe polymorphism in telescopes.v, allowing `tele` at a fixed universe (such as the `Quant` universe in iris) to cumulatively contain telescopes at smaller universes.
I also re-arranged existing telescope tests slightly in order to make sure the test for `Unset Universe Minimization ToSet` has a chance to fail before the accessor test, which happens to fail for the same reason.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/382Preimage function for finite maps.2022-05-31T11:08:40ZRobbert KrebbersPreimage function for finite maps.This is a possible solution to #140This is a possible solution to #140https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/385prepare for https://github.com/coq/coq/pull/162892022-07-07T16:25:17ZAndrej Dudenhefnerprepare for https://github.com/coq/coq/pull/16289Due to a bug, eauto neglected the cost of the extern hint lia (and applied it first).
However, if lia is applied last, then some non-useful low-cost hints introduce evars beforehand, which breaks the proof.
Changing eauto to auto at the ...Due to a bug, eauto neglected the cost of the extern hint lia (and applied it first).
However, if lia is applied last, then some non-useful low-cost hints introduce evars beforehand, which breaks the proof.
Changing eauto to auto at the specific position would avoid the evar issue.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/397Add list_fmap_delete, omap_app, and omap_option_list2022-07-26T19:27:15ZMichael SammlerAdd list_fmap_delete, omap_app, and omap_option_listMichael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/396Add list_lookup_imap_Some2022-07-26T19:32:39ZMichael SammlerAdd list_lookup_imap_SomeMichael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/393Fix the naming of kmap_subseteq and kmap_subset2022-07-26T19:37:52ZMichael SammlerFix the naming of kmap_subseteq and kmap_subsethttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/390Add map_Exists2022-07-27T06:56:35ZMichael SammlerAdd map_ExistsAs discussed with @robbertkrebbers. I proved most of the lemmas corresponding to `map_Forall`.As discussed with @robbertkrebbers. I proved most of the lemmas corresponding to `map_Forall`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/388Add case_match eqn: tactic for naming hypotheses generated by case_match2022-07-27T08:22:16ZMichael SammlerAdd case_match eqn: tactic for naming hypotheses generated by case_matchAs discussed with @robbertkrebbers. Defining the notation using `"eqn:"` instead of `"eqn" ":"` breaks the `eqn:` notation for `destruct`. I don't know if `"eqn" ":"` potentially breaks anything.As discussed with @robbertkrebbers. Defining the notation using `"eqn:"` instead of `"eqn" ":"` breaks the `eqn:` notation for `destruct`. I don't know if `"eqn" ":"` potentially breaks anything.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/401Add join_length2022-07-31T07:09:08ZMichael SammlerAdd join_lengthhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/399Add lookup lemmas for partial alter and commuting lemmas for alter2022-07-31T07:22:18ZMichael SammlerAdd lookup lemmas for partial alter and commuting lemmas for alterhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/400Add list_subseteq_dec2022-08-01T07:19:19ZMichael SammlerAdd list_subseteq_decI am not sure where to put this instance in this file. The best place would probably be after `elem_of_list_dec`, but there the `Decision` instance for `Forall` is not yet there.I am not sure where to put this instance in this file. The best place would probably be after `elem_of_list_dec`, but there the `Decision` instance for `Forall` is not yet there.Michael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/398Flip direction of `map_disjoint_fmap`.2022-08-01T07:43:58ZRobbert KrebbersFlip direction of `map_disjoint_fmap`.The old way was inconsistent with other lemmas.The old way was inconsistent with other lemmas.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/392Add map_agree2022-08-01T09:48:04ZMichael SammlerAdd map_agreeAs discussed with @robbertkrebbers. I am not sure if there are good lemmas for insert and union of `map_agree` (i.e. corresponding to `map_disjoint_union_l` and `map_disjoint_insert_l`). Do you have ideas for how they would look like?As discussed with @robbertkrebbers. I am not sure if there are good lemmas for insert and union of `map_agree` (i.e. corresponding to `map_disjoint_union_l` and `map_disjoint_insert_l`). Do you have ideas for how they would look like?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/395Add lookup_union_l'2022-08-03T07:35:19ZMichael SammlerAdd lookup_union_l'https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/405Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None2022-08-08T14:48:15ZMichael SammlerAdd _1, _2 lemmas for not_elem_of_dom and lookup_union_NoneSplit from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/394Split from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/394Michael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/391Add map_seqZ2022-08-09T08:05:33ZMichael SammlerAdd map_seqZAs discussed with @robbertkrebbers . I ported the lemmas from `map_seq`, except `insert_map_seq_0` because I was not sure whether to prefer the right to left or the right to left direction (i.e. where to insert the cast between Z and nat...As discussed with @robbertkrebbers . I ported the lemmas from `map_seq`, except `insert_map_seq_0` because I was not sure whether to prefer the right to left or the right to left direction (i.e. where to insert the cast between Z and nat), and except `dom_seq` which would need `set_seqZ`.