stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-03-18T16:58:31Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/542create new package for stdpp-bitvector library2024-03-18T16:58:31ZRalf Jungjung@mpi-sws.orgcreate new package for stdpp-bitvector libraryThis is a step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/204.
I was not quite sure which Coq logical path to use for this. For now I used `stdpp.bv` since always typing `stdpp.bitvector` seems a bit annoying, but the incons...This is a step towards https://gitlab.mpi-sws.org/iris/stdpp/-/issues/204.
I was not quite sure which Coq logical path to use for this. For now I used `stdpp.bv` since always typing `stdpp.bitvector` seems a bit annoying, but the inconsistency may also be confusing. Opinions?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/532Draft: Staging MR for various refactorings2023-12-02T09:45:08ZRobbert KrebbersDraft: Staging MR for various refactoringsIt turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_reques...It turns out that properly fixing !507 opened quite a can of worms. We have the following related MRs now:
- [x] !526
- [ ] !530
- [x] !531
- [ ] `non_empty` change as discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/526#note_97794
- [ ] Direction of equality in `fmap`/`omap`/`alter` lemmas, see https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531#note_97789
The plan is to merge all these MRs into a staging branch (the one linked to this MR) and then merge the staging branch to master. This way we have to fix reverse dependencies just once.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/530Add lemma `lookup_total_fmap`.2023-10-16T17:55:15ZRobbert KrebbersAdd lemma `lookup_total_fmap`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/527Add a comment about `cancel_inj` and `cancel_surj`.2023-10-14T17:42:57ZRobbert KrebbersAdd a comment about `cancel_inj` and `cancel_surj`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/357Added some lemmas about [sublist]2023-10-13T09:40:52ZJonas KastbergAdded some lemmas about [sublist]Added some generally useful lemmas about the [sublist] functionAdded some generally useful lemmas about the [sublist] functionhttps://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/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/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/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.