stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-03-29T09:06:14Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/459Finite map composition2023-03-29T09:06:14ZDorian LesbreFinite map composition- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that...- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that is the case feel free to close without merging.
I'm submitting in case someone else would have a use for it, since this
is now fairly complete (although it could use some compatibility lemmas with `insert`).https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/458Add NoDup_bind, vec_enum, vec_finite (new version with proper branch)2023-03-24T15:55:51ZRobbert KrebbersAdd NoDup_bind, vec_enum, vec_finite (new version with proper branch)Follow up of !451, but with a branch where I can push.Follow up of !451, but with a branch where I can push.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/456Add set_omap to finite sets2023-03-24T16:50:23ZDorian LesbreAdd set_omap to finite setsAdd `omap`-like function to finite sets, aka OCaml's `filter_map` operation.
I needed it to destruct a set of `X + Y` into a set of `X` and a set of `Y`.
Also add a few lemmas to reason about it.Add `omap`-like function to finite sets, aka OCaml's `filter_map` operation.
I needed it to destruct a set of `X + Y` into a set of `X` and a set of `Y`.
Also add a few lemmas to reason about it.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/439add basic list functionality with Z-based indexing2023-03-23T22:10:13ZRalf Jungjung@mpi-sws.orgadd basic list functionality with Z-based indexingThis starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g...This starts the work on https://gitlab.mpi-sws.org/iris/stdpp/-/issues/108 by implementing `insert` and `index` for `Z` as well as `lengthZ`, `takeZ`, `dropZ`, and porting much of the associated theory.
I have not ported everything, e.g. the interactions with `Forall3`, `subseteq`, `submseteq`, `filter`, `mask` are missing. Also there are more operations that would need a Z-based version, such as `lookup_total`, `alter`, `delete`, `inserts`, `find`, `imap`, `imap2`, `resize`, `rotate`, `rotate_take`, `sublist_lookup`, `sublist_alter`. There are also some tactics that will not handle these new operations and so might need adjustments or Z-based tactics: `solve_length`, `simplify_list_eq`.
Still I think this is a useful start that can serve as a foundation for later extensions. :)
Blocked on https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/441.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/437Enable `Hint Mode Equiv` now that stdpp requires Coq 8.122023-02-06T09:47:59ZPaolo G. GiarrussoEnable `Hint Mode Equiv` now that stdpp requires Coq 8.12Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because ...Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because it still supported Coq 8.11 which suffered from additional bugs (fixed in 8.12) — Iris still has this comment:
```coq
(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12, which Iris depends on. *)
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/435Use hint mode + more often2022-12-15T15:59:24ZRobbert KrebbersUse hint mode + more oftenThis is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uoThis is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uohttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/424Prevent [finite_countable] from solving unrelated evars2023-03-20T10:30:11ZPaolo G. GiarrussoPrevent [finite_countable] from solving unrelated evarsFix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple appl...Fix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple apply @finite.finite_countable ; trivial` in the trace, and one (or both) the tactics trigger https://github.com/coq/coq/issues/6583. So I've adapted Iris's work around; I've not confirmed whether all of it is needed, but it worked on first try.
Missing (I assume):
- [ ] `trivial` only uses hints with cost 0, but `typeclasses eauto 0` does not appear to work, so `typeclasses eauto 1` is the closest thing I see. This might be a problem.
- [ ] Testcase
- [ ] Changelog? Probably not needed since this is a bugfix
- [x] Mention this in upstream issue.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/417Add lemmas `set_fold_union_strong` and `set_fold_union`.2022-11-23T08:38:46ZRobbert KrebbersAdd lemmas `set_fold_union_strong` and `set_fold_union`.[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativit...[This discussion at Mattermost](https://mattermost.mpi-sws.org/iris/pl/hf4fown633gtpxf39u1fuqsqfh) nerdsniped me to add the lemma `set_fold_union` and the stronger lemma `set_fold_union_strong` that only requires idempotence/associativity/commutativity for the elements in the sets.
Interestingly, the already existing "disjoint" versions of the lemma can be derived.
The proofs are pretty long/tricky, so I tried to add some comments what's going on.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/394Add some _1, _2 lemmas for map_filter2022-11-23T08:43:44ZMichael SammlerAdd some _1, _2 lemmas for map_filterAs discussed with @robbertkrebbersAs discussed with @robbertkrebbershttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/372Draft: Very preliminary version of a quick start guide for sets.2023-02-06T14:42:57ZRobbert KrebbersDraft: Very preliminary version of a quick start guide for sets.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/357Added some lemmas about [sublist]2022-08-29T13:41:31ZJonas KastbergAdded some lemmas about [sublist]Added some generally useful lemmas about the [sublist] functionAdded some generally useful lemmas about the [sublist] function