stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-08-03T13:00:29Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/474make empty operational typeclass TC opaque2023-08-03T13:00:29ZRalf Jungjung@mpi-sws.orgmake empty operational typeclass TC opaqueLike https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/914, but only for the Empty typeclass which (being just a constant) is particularly prone to Coq TC instance "hallucination".Like https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/914, but only for the Empty typeclass which (being just a constant) is particularly prone to Coq TC instance "hallucination".https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/493Better way of writing `Proper` premises in fin sets2023-08-03T13:01:11ZRobbert KrebbersBetter way of writing `Proper` premises in fin setsUse `Proper (.. => impl)` instead of `Proper (.. => iff)` and `∀ x, Proper ..` instead of `Proper ((=) ==> ..)`.
The new premises are easier to prove (both `solve_proper` and manual proof).
This came up in https://gitlab.mpi-sws.org/ir...Use `Proper (.. => impl)` instead of `Proper (.. => iff)` and `∀ x, Proper ..` instead of `Proper ((=) ==> ..)`.
The new premises are easier to prove (both `solve_proper` and manual proof).
This came up in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/478https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/490add pair_equiv2023-08-03T13:03:49ZRalf Jungjung@mpi-sws.orgadd pair_equivWhen having `H: (a1, b1) ≡ (a2, b2)`, it's actually rather annoying to rewrite an `a1` in the goal:
```
destruct H as [H _]; simpl in H; rewrite H
```
This is because destructing `H` yields `(a1, b1).1 ≡ (a2, b2).1`.
So a lemma like thi...When having `H: (a1, b1) ≡ (a2, b2)`, it's actually rather annoying to rewrite an `a1` in the goal:
```
destruct H as [H _]; simpl in H; rewrite H
```
This is because destructing `H` yields `(a1, b1).1 ≡ (a2, b2).1`.
So a lemma like this could be useful, then we should be able to do `apply pair_equiv in H as [-> _]`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/494Correct `Params` instances for `lookup` and `singletonM`.2023-08-03T13:11:04ZRobbert KrebbersCorrect `Params` instances for `lookup` and `singletonM`.We always use Leibniz keys (`nat` for list, `Countable` for maps), so the `Params` should be one higher.
In fact, for `singletonM` and `insert` we already use the correct number for `Params`.We always use Leibniz keys (`nat` for list, `Countable` for maps), so the `Params` should be one higher.
In fact, for `singletonM` and `insert` we already use the correct number for `Params`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/478Add lemmas for commuting funcs with folds2023-08-03T13:22:40ZIsaac van Bakelisaac.vanbakel@inf.ethz.chAdd lemmas for commuting funcs with foldsThese lemmas were helpful to me in recent proofs (in particular, the multiset one is used for iris/iris#923.) They allow for moving a unitary function on a fold accumulator in and out of the fold as necessary, provided the function commu...These lemmas were helpful to me in recent proofs (in particular, the multiset one is used for iris/iris#923.) They allow for moving a unitary function on a fold accumulator in and out of the fold as necessary, provided the function commutes appropriately with the fold function.
~~The location of the multiset lemma in the file is not ideal, since it has to come after `gmultiset_ind`, which is well after all the other fold lemmas. However, proving it without `gmultiset_ind` is much harder, and moving `gmultiset_ind` further up the file is itself non-trivial, so I've opted not to try.~~ Fixed by Robbert's changes.https://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/499Add greater or equal symbol for numbers2023-08-30T09:30:59ZThibaut PéramiAdd greater or equal symbol for numbersI feel it is sometime clearer to write `x ≥ y` than `y ≤ x` in certain specific cases such as
```
match order with
| Lt => x < y
| Le => x ≤ y
| Gt => x > y
| Ge => x ≥ y
end
```
So I added `≥` as an infix for the numbers, as well a...I feel it is sometime clearer to write `x ≥ y` than `y ≤ x` in certain specific cases such as
```
match order with
| Lt => x < y
| Le => x ≤ y
| Gt => x > y
| Ge => x ≥ y
end
```
So I added `≥` as an infix for the numbers, as well as `(>)` and `(≥)`
If that feeling is not shared, I'm happy to keep those for my own developments.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/485Add bitvector number notations2023-09-01T06:47:50ZThibaut PéramiAdd bitvector number notationsThis adds number notations into bv_scope that expand to `Z_to_bv _ {number}`.
This notation is parsing only, printing will print the full `Z_to_bv` call.
Also the bitvector is not computed: The term `4%bv` is literally of the shape
`(Z_t...This adds number notations into bv_scope that expand to `Z_to_bv _ {number}`.
This notation is parsing only, printing will print the full `Z_to_bv` call.
Also the bitvector is not computed: The term `4%bv` is literally of the shape
`(Z_to_bv _ 4)`, it is NOT evaluated to a shape of `BV _ 4 _`. On the other hand
this allows to write `((-1)%bv : bv 32)` to get something that reduces to
`BV 32 0xFFFFFFFF`.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/487Make `unseal` TC opaque2023-09-11T14:46:09ZJannoMake `unseal` TC opaqueThis had a very slight positive impact on our development. But we don't have a lot of things sealed this way so the impact might be bigger in other developments.This had a very slight positive impact on our development. But we don't have a lot of things sealed this way so the impact might be bigger in other developments.https://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/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/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/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/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/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/459Finite map composition2023-09-28T14:01:30ZDorian LesbreFinite map composition- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that...- Add a `map_compose` operator for finite map composition
- Add notation `m ∘ₘ n` for `map_compose m n`
- Add various lemmas to manipulate map composition
This is arguably a niche operator we might not want to include.
If you think that is the case feel free to close without merging.
I'm submitting in case someone else would have a use for it, since this
is now fairly complete (although it could use some compatibility lemmas with `insert`).