stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-10-07T10:15:58Zhttps://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/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/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/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/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/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/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/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.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/514remove some lemmas that exist in Coq's stdlib2023-09-28T15:55:36ZRalf Jungjung@mpi-sws.orgremove some lemmas that exist in Coq's stdlibThese lemmas were added in https://github.com/coq/coq/commit/ea05377f19404e0627a105b07c10ce72fb010af9, which was included in Coq 8.6. Time to remove our copies of them. :)These lemmas were added in https://github.com/coq/coq/commit/ea05377f19404e0627a105b07c10ce72fb010af9, which was included in Coq 8.6. Time to remove our copies of them. :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/513add some number instances for Assoc, Comm, ...2023-09-29T09:09:07ZRalf Jungjung@mpi-sws.orgadd some number instances for Assoc, Comm, ...Inspired by https://github.com/bedrocksystems/BRiCk/blob/614b303aa6370ecfcb354ec9715e65a5a5a28630/theories/prelude/numbers.v, but I didn't add all of their instances, there's so many of them... so I went for the key properties (assoc, co...Inspired by https://github.com/bedrocksystems/BRiCk/blob/614b303aa6370ecfcb354ec9715e65a5a5a28630/theories/prelude/numbers.v, but I didn't add all of their instances, there's so many of them... so I went for the key properties (assoc, comm, neutral and absorbing elements) of the core operations (add, sub, mul, div).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/511clarify efeed_core a bit and add some tests2023-09-27T11:50:30ZRalf Jungjung@mpi-sws.orgclarify efeed_core a bit and add some testshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/510fix some instance names2023-09-27T11:52:08ZRalf Jungjung@mpi-sws.orgfix some instance names`(λ _ _ : A, x)` is not `id`, it is a two-argument form of `const.`
`(λ x _ : A, x)` is not constant, it is the identity in the first argument.`(λ _ _ : A, x)` is not `id`, it is a two-argument form of `const.`
`(λ x _ : A, x)` is not constant, it is the identity in the first argument.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/509fix inconsistent Lemma name: sub_add' → add_sub'2023-09-21T13:42:56ZRalf Jungjung@mpi-sws.orgfix inconsistent Lemma name: sub_add' → add_sub'https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/508drop support for Coq 8.152023-09-15T07:18:19ZRalf Jungjung@mpi-sws.orgdrop support for Coq 8.15After this landed we should finally be able to make use of https://github.com/coq/coq/pull/13969. :)After this landed we should finally be able to make use of https://github.com/coq/coq/pull/13969. :)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/507Draft: add lemma lookup_insert_eq2023-10-16T17:50:52ZRalf 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/506Rename `map_filter_lookup` → `map_lookup_filter`.2023-09-21T13:58:20ZRobbert KrebbersRename `map_filter_lookup` → `map_lookup_filter`.All the other lemmas are called `lookup_OPERATION` or `map_lookup_OPERATION`; only the filter one is off. This MR fixes that.
I discovered this while reviewing !459.All the other lemmas are called `lookup_OPERATION` or `map_lookup_OPERATION`; only the filter one is off. This MR fixes that.
I discovered this while reviewing !459.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/505Generalize some map/finset results from `Set_` to `SemiSet`.2023-09-21T14:41:01ZRobbert KrebbersGeneralize some map/finset results from `Set_` to `SemiSet`.I noticed this while reviewing !459I noticed this while reviewing !459https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/504Revert "Merge branch 'janno/tc-opaque-unseal' into 'master'"2023-09-11T14:51:34ZRalf Jungjung@mpi-sws.orgRevert "Merge branch 'janno/tc-opaque-unseal' into 'master'"This reverts merge request !487. It broke the Iris build:
```
File "./iris/base_logic/lib/ghost_var.v", line 119, characters 9-32:
Error: Could not fill dependent hole in "apply"
File "./iris/base_logic/lib/gen_heap.v", line 194, charac...This reverts merge request !487. It broke the Iris build:
```
File "./iris/base_logic/lib/ghost_var.v", line 119, characters 9-32:
Error: Could not fill dependent hole in "apply"
File "./iris/base_logic/lib/gen_heap.v", line 194, characters 9-32:
Error: Could not fill dependent hole in "apply"
```