stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-10-02T18:42:20Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/515add make_simple_intropattern2023-10-02T18:42:20ZRalf Jungjung@mpi-sws.orgadd make_simple_intropatternIt's not needed for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/512 after all, but could still be useful in the future.It's not needed for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/512 after all, but could still be useful in the future.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/512add odestruct and other "open term" tactics2023-10-02T19:58:26ZRalf Jungjung@mpi-sws.orgadd odestruct and other "open term" tacticsSee the added testcase for motivation. Every now and then I run into the situation where I need a tactic like this and then not having it is always super frustrating...
Thanks a lot to @janno for help in writing these tactics!See the added testcase for motivation. Every now and then I run into the situation where I need a tactic like this and then not having it is always super frustrating...
Thanks a lot to @janno for help in writing these tactics!https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/507Draft: add lemma lookup_insert_eq2023-09-21T13:44:49ZRalf Jungjung@mpi-sws.orgDraft: add lemma lookup_insert_eqFor most map operations we have a lemma `lookup_foo` that always applies -- except, ironically, for `insert`.
Unfortunately the lemma really should be called `lookup_insert`, but that name is already taken, so I called it `lookup_insert...For most map operations we have a lemma `lookup_foo` that always applies -- except, ironically, for `insert`.
Unfortunately the lemma really should be called `lookup_insert`, but that name is already taken, so I called it `lookup_insert_eq`. Arguably that would be a good name for the `i = j` case and nicely symmetric with `lookup_insert_ne` (well, the really symmetric version would take `i = j` as precondition, which can make it easier to rewrite with). `lookup_insert` is used a lot so I feel renaming might be a bit too disruptive...https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/501Add MRaise typeclass2023-09-27T01:48:24ZThibaut PéramiAdd MRaise typeclassThis is an alternative to `MFail` in [#488](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/488). It allows a monad to present a general error raising mechanism. This includes an example instantiation for option. I didn't do the w...This is an alternative to `MFail` in [#488](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/488). It allows a monad to present a general error raising mechanism. This includes an example instantiation for option. I didn't do the work of #488 to completely replace `MGuard`, but if we decide to use this instead of `MFail`, we can merge the two patches.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/495solve_proper: add support for subrelation2023-08-27T17:22:44ZRalf Jungjung@mpi-sws.orgsolve_proper: add support for subrelationI realized that solve_proper cannot currently prove things like `NonExpansive (λ x, ⌜a = x⌝)`, which is a bit of a bummer. So this adds the infrastructure required to make that work.I realized that solve_proper cannot currently prove things like `NonExpansive (λ x, ⌜a = x⌝)`, which is a bit of a bummer. So this adds the infrastructure required to make that work.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/488Replace `MGuard` with `MFail`2023-09-27T01:43:08ZAdamReplace `MGuard` with `MFail`This MR implements MFail as described in #171. This replaces `mguard` with `guard : P → {Decision P} → M P` using `mfail`. As such I've replaced `guard P; mx` with `_ ← guard P; mx` in all lemmas. This MR further more replaces `case_opti...This MR implements MFail as described in #171. This replaces `mguard` with `guard : P → {Decision P} → M P` using `mfail`. As such I've replaced `guard P; mx` with `_ ← guard P; mx` in all lemmas. This MR further more replaces `case_option_guard` with a more general `case_guard`.
These changes are very much breaking changes.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/435Use hint mode + more often2023-05-02T13:35:21ZRobbert 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/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