stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-03-05T06:25:01Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533Allow pattern and type annotations in propset notation2024-03-05T06:25:01ZThibaut PéramiAllow pattern and type annotations in propset notationThis allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break...This allows to use patterns and type annotations in the `propset` notation, Like `{[ (x,y) | ... ]}` or `{[ x : T | ...]}` or even `{[ (x, y) : A * B | ...]}`.
However, for both the old and new notation, this notation immediately break if someone adds a binary infix `|` notation downstream, In which case this will be parsed as a singleton of whatever the result of the `|` operation is. This was already the case before, so anyone that did that already broke the original `propset` notationhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/531Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`2023-10-20T12:54:40ZRobbert KrebbersFix inconsistencies in `lookup` and `elem_of` lemmas for `list`- Rename lemmas `elem_of_list_X` into `list_elem_of_X` to be consistent with the `list_lookup_X` lemmas. Some lemmas contained other inconsistencies (e.g., `_1` and `_2` swapped), see CHANGELOG for details.
- Change the order of the conj...- Rename lemmas `elem_of_list_X` into `list_elem_of_X` to be consistent with the `list_lookup_X` lemmas. Some lemmas contained other inconsistencies (e.g., `_1` and `_2` swapped), see CHANGELOG for details.
- Change the order of the conjunction in `list_lookup_fmap_Some`. The new
version is `(f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x`, which
makes it consistent with `list_elem_of_fmap` and the corresponding lemmas for
sets and maps. **To be continued in other MR, insert link**
- Rename `list_alter_fmap` → `list_fmap_alter` and remove `list_alter_fmap_mono` which was a monomorphic duplicate.
With the exception of the `list_elem_of_fmap` change, all changes in this MR can be applied by `sed`. It would be best to merge it together with !526 so we only have to run a giant `sed` script once on reverse dependencies.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/529Add `prod_swap` and some basic results for it.2023-10-14T16:04:35ZRobbert KrebbersAdd `prod_swap` and some basic results for it.I was surprised this function is not in the stdlib...I was surprised this function is not in the stdlib...https://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/526Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a s...2023-10-17T12:01:36ZRobbert KrebbersProvide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.This has been discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/507. This MR changes all lemmas for list, map, multiset in std++ according to that plan. The CHANGELOG describes all changes.
While performing the refacto...This has been discussed in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/507. This MR changes all lemmas for list, map, multiset in std++ according to that plan. The CHANGELOG describes all changes.
While performing the refactoring, I also added some missing lemmas. They are also described in the CHANGELOG.
I tested the `sed` script on iris, iris-examples, lambdarust, Actris, Iron, GPFSL. No manual fixes were needed.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/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/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/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.