stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2022-08-16T06:14:30Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/403Refactor and improve documentation of feed and efeed tactics2022-08-16T06:14:30ZMichael SammlerRefactor and improve documentation of feed and efeed tacticsThis MR is based on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/389.
Discussion from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/389#note_82974 :
> The documentation does not even mention the `by` part of this tac...This MR is based on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/389.
Discussion from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/389#note_82974 :
> The documentation does not even mention the `by` part of this tactic. Also, `efeed tac H` (which is what the documentation uses in the first line) is not the correct syntax for this tactic. Maybe `feed` should also be adjusted to be written `feed H using tac`?
> Actually 'using' is a strange verb here, it sounds like `tac` is involved in the feeding, but that's not the case. Is `to` a keyword already, i.e., can we use `efeed H to tac`? Or `into`?
See also the discussion here: https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/389#note_82750
@robbertkrebbers Please feel free to update this MR as you see fit.Michael SammlerMichael Sammlerhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/409add some very basic f_equiv tests2022-08-12T12:12:40ZRalf Jungjung@mpi-sws.orgadd some very basic f_equiv testsRalf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/384[list] restricted version of list_fmap_equiv_ext2022-08-11T12:47:15ZVincent[list] restricted version of list_fmap_equiv_ext`list_fmap_equiv_ext` requires the functions to be equal on every
element of `A` but we could restrict it to the element of `l`.
Note sure about the name I choose, feel free to suggest something more in line with the library :D`list_fmap_equiv_ext` requires the functions to be equal on every
element of `A` but we could restrict it to the element of `l`.
Note sure about the name I choose, feel free to suggest something more in line with the library :Dhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/407Generalize Propers for lists / Add some missing Params2022-08-11T07:51:16ZRobbert KrebbersGeneralize Propers for lists / Add some missing ParamsFor example, for fmap:
- Old: `Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f)`
- New: `Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap`
This means that `solve_proper` can also find a `Proper` instance when the two...For example, for fmap:
- Old: `Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f)`
- New: `Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap`
This means that `solve_proper` can also find a `Proper` instance when the two functions are different, and then prove that they are extensionally equal.
This is similar to what we have done in !276 for maps.Robbert KrebbersRobbert Krebbershttps://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/188Extend the theory of positive rationals `Qp`2022-08-09T14:20:21ZRobbert KrebbersExtend the theory of positive rationals `Qp`This MR extends the theory of positive rationals `Qp`. The most important change is that it fixes the leaky abstraction, adds tons of lemmas, and no longer relies on the coercions to the non-negative rationals `Qc` to obtain notions like...This MR extends the theory of positive rationals `Qp`. The most important change is that it fixes the leaky abstraction, adds tons of lemmas, and no longer relies on the coercions to the non-negative rationals `Qc` to obtain notions like orders.
### New features
- Add the orders `Qc_le` and `Qp_lt`.
- Add a function `Qc_inv` for the multiplicative inverse.
- Define the division function `Qp_div` in terms of `Qp_inv`, and generalize the second argument from `positive` to `Qp`.
- Define a function `pos_to_Qp` that converts a `positive` into a positive rational `Qp`.
- Add many lemmas and missing type class instances, especially for orders, multiplication, multiplicative inverse, division, and the conversion.
### Technical changes:
- Remove the coercion from `Qp` to `Qc`. This follows our recent tradition of getting rid of coercions since they are more often confusing than useful.
- Rename the conversion from `Qp` to `Qc` from `Qp_car` into `Qp_to_Qc` to be consistent with other conversion functions in std++. Also rename the lemma `Qp_eq` into `Qp_to_Qc_inj_iff`.
- Use `let '(..) = ...` in the definitions of `Qp_plus`/`Qp_mult`/`Qp_inv`/`Qp_le`/`Qp_lt` to avoid Coq tactics (like `injection`) to unfold these definitions eagerly. We already used this trick in e.g., `gmap` for the same reason. This works around the Coq issue that @simonfv ran into [here](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/497#note_57334).
- Define the literals 1, 2, 3, 4 in terms of `pos_to_Qp` instead of iterated addition. This avoids weird rewrites. For example, before `2` was defined as `1 + 1`, so rewriting with `1 = stuff` in a goal containing `2` turned it into `stuff + stuff`, which was extremely confusing.
### Things to discuss
- We could use Coq's extensible notation machinery to get proper notations for the literals. AFAIK this is only possible in Coq 8.9+, so that requires us to drop support for Coq 8.8. **Do ▷**
- [x] While we are changing the API anyway, use `add`/`mul` instead of `plus`/`mult`, to be consistent with the lemmas for `nat` and `Z`.
- Also improve the `Qc` library in the same way. **Do ▷**
### Impact on reverse dependencies
This MR will cause some breakage for libraries that rely on the order on fractions, but in my opinion, this is for the better. I have ported some of the developments that use fractions in interesting ways, namely Iris, Iron, and LambdaRust. While stuff broke, I managed to shorten proofs significantly by making use of the new lemmas introduced in this MR. Also, after this MR, none of these developments rely on the conversion to `Qc` anymore, showing that we indeed provide a reasonable API now.
Some stats:
- Iris: 66 insertions, 78 deletions
- LambdaRust: 32 insertions, 63 deletions
- Iron: no changes needed
- Examples: no changed needed, after [removing an unused lemma](https://gitlab.mpi-sws.org/iris/examples/-/commit/5df249005c6f8d906e28022a7c61beaa7578834d)
- gpfls: 8 insertions, 8 deletions
To land this MR, we should first merge https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/497.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/406Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewriting2022-08-09T10:55:48ZPaolo G. GiarrussoIntroduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewritingThis is @dfrumin's !383 (with authorship preserved) + some tweaks to setoid rewriting:
- strengthen set_bind_subset to have the same arity
- add missing Params instance to prevent slow failures in setoid rewriting
- `Proper` instances c...This is @dfrumin's !383 (with authorship preserved) + some tweaks to setoid rewriting:
- strengthen set_bind_subset to have the same arity
- add missing Params instance to prevent slow failures in setoid rewriting
- `Proper` instances can be proven before `set_bind_ext` via `set_solver`.
- `set_bind_ext` is then provable by set_solver directly.
I originally sent https://gitlab.mpi-sws.org/dfrumin/coq-stdpp/-/merge_requests/1 to be added into !383, but maybe it's easier with this MR? @robbertkrebbers up to you.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/383Introduce `set_bind` and associated lemmas.2022-08-09T10:52:18ZDan FruminIntroduce `set_bind` and associated lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/389Add the feed revert, efeed revert, efeed inversion, and efeed destruct tactics2022-08-09T09:34:56ZMichael SammlerAdd the feed revert, efeed revert, efeed inversion, and efeed destruct tacticshttps://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`.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/358Add lemmas about empty `filter` on list, map, and set2022-08-08T13:37:43ZJonas KastbergAdd lemmas about empty `filter` on list, map, and setAdded an advanced lemma about [filter] on lists.
Whenever a filter with a proposition [P] on a list [l] results in an empty list,
we can derive that `x ∉ l` for any [x] where `P x`.Added an advanced lemma about [filter] on lists.
Whenever a filter with a proposition [P] on a list [l] results in an empty list,
we can derive that `x ∉ l` for any [x] where `P x`.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/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/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/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/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/401Add join_length2022-07-31T07:09:08ZMichael SammlerAdd join_lengthhttps://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/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`.