stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-10-14T10:31:58Zhttps://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.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/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"
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/503Add missing Bind Scope for fin2023-09-21T13:49:16ZThibaut PéramiAdd missing Bind Scope for finThis allows for automatic declaration of fin_scope when in a function argument of type `fin n`. For example in a defined function `f {n}: fin n → T`, you can now do `f 45` instead of `f 45%fin` (assuming the `n` can be deduced of course)...This allows for automatic declaration of fin_scope when in a function argument of type `fin n`. For example in a defined function `f {n}: fin n → T`, you can now do `f 45` instead of `f 45%fin` (assuming the `n` can be deduced of course). This might be a breaking change in very weird circumstances, but it otherwise allows a more convenient use of the fin notations.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/502More efficient `encode`/`decode` for `string`/`ascii`2023-09-05T12:21:02ZRobbert KrebbersMore efficient `encode`/`decode` for `string`/`ascii`When experimenting with the benchmarks in https://github.com/xavierleroy/canonical-binary-tries I noticed that our `encode` function for `Countable` of `string` is slow: it creates a `list` for each char which is then converted to a `pos...When experimenting with the benchmarks in https://github.com/xavierleroy/canonical-binary-tries I noticed that our `encode` function for `Countable` of `string` is slow: it creates a `list` for each char which is then converted to a `positive` and appended to the result.
https://github.com/xavierleroy/canonical-binary-tries/blob/v2/lib/String2pos.v contains a better version, which I have adapted to std++ style. (That repository is BSD licensed so we can use it, our comment contains a link to give credit, of course.).
I also changed the coding of `ascii` by reusing the one for `string`; this one is also faster as the benchmark below shows.
~~The `decode` function still converts to `list`, but I don't know how to avoid that without writing 2^8 = 256 cases.~~
```
From stdpp Require Import strings countable.
Import Ascii.
Definition long := "Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec euismod aliquam dui, non ultrices nisl rhoncus pretium. Donec tristique at diam eget commodo. Ut elit diam, maximus ac metus at, commodo malesuada diam. Morbi vehicula tortor et mauris malesuada, ac congue mauris ultrices. Donec id faucibus tellus. Vestibulum vulputate molestie urna, in sagittis tortor. Pellentesque placerat orci ut velit mattis consectetur. Mauris non nulla sit amet nisi egestas pellentesque. Aenean tincidunt id leo et placerat. Nam fermentum lectus sit amet pretium egestas. Lorem ipsum dolor sit amet, consectetur adipiscing elit.".
Time Eval vm_compute in Pos.iter (λ s, default "" $ decode (encode s)) long 10000.
(* old: 4.759s *)
(* new encode: 1.876s *)
(* new encode/decode: 0.916s *)
Time Eval vm_compute in (Pos.iter (λ s, default "b" $ decode (encode s)) "a" 1000000)%char.
(* old: 2.636s *)
(* new encode: 0.493s *)
(* newer encode/decode: 0.308s *)
```https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/500explain why we don't have 'ge' notation2023-08-30T12:15:38ZRalf Jungjung@mpi-sws.orgexplain why we don't have 'ge' notationThis came up in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/499This came up in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/499https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/498Change Hint Mode of LeibnizEquiv2023-08-28T15:42:45ZIke MulderChange Hint Mode of LeibnizEquivAs discussed in iris!966, the `LeibnizEquiv` typeclass currently has `Hint Mode ! -`, signifying that the type is an input, while the equivalence which is supposed to imply leibniz equality is an output. That should be `Hint Mode ! !`, i...As discussed in iris!966, the `LeibnizEquiv` typeclass currently has `Hint Mode ! -`, signifying that the type is an input, while the equivalence which is supposed to imply leibniz equality is an output. That should be `Hint Mode ! !`, i.e., both are inputs.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/497use ssreflect rewrite for multiset tactics2023-11-25T09:59:44ZRalf Jungjung@mpi-sws.orguse ssreflect rewrite for multiset tacticsFixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/195
Unfortunately I don't know how to condense this into a testcase, the issue needs canonical structure shenanigans to occur.Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/195
Unfortunately I don't know how to condense this into a testcase, the issue needs canonical structure shenanigans to occur.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`)