stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-10-14T16:00:35Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/528Missing `Params` instances for `prod_map` and `prod_zip`.2023-10-14T16:00:35ZRobbert KrebbersMissing `Params` instances for `prod_map` and `prod_zip`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/525add inv and oinv tactics that are basically a smarter and fixed inversion_clear2023-10-14T15:20:21ZRalf Jungjung@mpi-sws.orgadd inv and oinv tactics that are basically a smarter and fixed inversion_clearFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/40
Sadly I couldn't figure out how to make `inv 1` work. [See Zulip](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Writing.20a.20tactic.20that.20takes.20.22ident.20o...Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/40
Sadly I couldn't figure out how to make `inv 1` work. [See Zulip](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Writing.20a.20tactic.20that.20takes.20.22ident.20or.20term.20number.22.3F)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/519Add lemmas for easy measure/size induction.2023-10-14T10:31:58ZRobbert KrebbersAdd lemmas for easy measure/size induction.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/524remove 'wf' alias for the standard 'well_founded'2023-10-14T08:36:25ZRalf Jungjung@mpi-sws.orgremove 'wf' alias for the standard 'well_founded'I could not find a single use of this alias outside of std++ itself, so the potential for confusion caused by having two different names for the same thing far outweighs the benefit of occasionally saving 9 keystrokes.I could not find a single use of this alias outside of std++ itself, so the potential for confusion caused by having two different names for the same thing far outweighs the benefit of occasionally saving 9 keystrokes.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/495solve_proper: add support for subrelation2023-10-13T16:19:48ZRalf 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/521Add `TCSimpl` type class.2023-10-13T15:52:36ZRobbert KrebbersAdd `TCSimpl` type class.See comment and test case for usage.See comment and test case for usage.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/522Add `MThrow` and replace `MGuard`2023-10-13T10:13:42ZThibaut PéramiAdd `MThrow` and replace `MGuard`The MR is the result of !488 and !501.
This adds the `MThrow E M` type class expresses the fact that the monad `M` allow error of type `E` to be thrown and any point with signature `mthrow : E → M A`. There is an alias `MFail := MThrow ...The MR is the result of !488 and !501.
This adds the `MThrow E M` type class expresses the fact that the monad `M` allow error of type `E` to be thrown and any point with signature `mthrow : E → M A`. There is an alias `MFail := MThrow unit` and `mfail := mthrow ()` for monads that can fail without any error payload like option.
This then replaces `mguard` with `guard : P → {Decision P} → M P` using `mfail`. The original `guard` notation disappears.
As such we'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`.
It also adds `guard_or : E → P → {Decision P} → M P` that throws an `E` instead of unit if `P` is false. Technically `guard` is just a notation for `guard_or ()` like `mfail` and `MFail`.
These changes are very much breaking changes.
This is joint work with @adamAndMath.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/435Use hint mode + more often2023-10-13T09:41:54ZRobbert 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/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/516Release 1.9.02023-10-11T14:46:47ZJohannes HostertRelease 1.9.0This changes the `CHANGELOG.md` in preparation for version 1.9.0.This changes the `CHANGELOG.md` in preparation for version 1.9.0.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/523Improve comment of `TCEq`.2023-10-07T10:15:58ZRobbert KrebbersImprove comment of `TCEq`.Addressing the comment in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/123/diffs#note_45103Addressing the comment in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/123/diffs#note_45103https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/123Change mode of `TCEq`.2023-10-06T13:45:12ZRobbert KrebbersChange mode of `TCEq`.See https://gitlab.mpi-sws.org/iris/iris/merge_requests/391See https://gitlab.mpi-sws.org/iris/iris/merge_requests/391https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/520Add instance `cons_equiv_inj`.2023-10-06T13:15:29ZRobbert KrebbersAdd instance `cons_equiv_inj`.Similar to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/995
Also took the liberty to name the one for `eq`.Similar to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/995
Also took the liberty to name the one for `eq`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/488Replace `MGuard` with `MFail`2023-10-06T12:45:48ZAdamReplace `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/501Add MRaise typeclass2023-10-06T12:42:02ZThibaut 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/496prove general fmap_inj lemmas2023-10-06T09:36:54ZRalf Jungjung@mpi-sws.orgprove general fmap_inj lemmasand derive the existing ones from it (and also in Iris, an equivalent one for `dist`)and derive the existing ones from it (and also in Iris, an equivalent one for `dist`)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/518Rework lemmas for `take/drop` of an `++`:2023-10-05T14:10:28ZRobbert KrebbersRework lemmas for `take/drop` of an `++`:+ Add `take_app` and `drop_app`, which are the strongest versions, and use
`take_app_X` for derived versions.
+ Consistently use `'` suffix for version with premise `n = length`, and have
versions without `'` with `length` inlined.
+...+ Add `take_app` and `drop_app`, which are the strongest versions, and use
`take_app_X` for derived versions.
+ Consistently use `'` suffix for version with premise `n = length`, and have
versions without `'` with `length` inlined.
+ Rename `take_app` → `take_app_length`, `take_app_alt` → `take_app_length'`,
`take_add_app` → `take_app_add'`, `take_app3_alt` → `take_app3_length'`,
`drop_app` → `drop_app_length`, `drop_app_alt` → `drop_app_length'`,
`drop_add_app` → `drop_app_add'`, `drop_app3_alt` → `drop_app3_length'`.
This closes #197.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/517Add lemmas for `reverse` of `take`/`drop`.2023-10-05T12:26:47ZRobbert KrebbersAdd lemmas for `reverse` of `take`/`drop`.The first two lemmas are in the stdlib for `rev` (the quadratic reverse), I use those proofs to establish a version for std++'s `reverse` (the linear version).
I also add two useful corollaries.The first two lemmas are in the stdlib for `rev` (the quadratic reverse), I use those proofs to establish a version for std++'s `reverse` (the linear version).
I also add two useful corollaries.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/512add odestruct and other "open term" tactics2023-10-03T11:53:16ZRalf 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/515add make_simple_intropattern2023-10-03T07:30:16ZRalf 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.