stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2023-10-06T09:36:54Zhttps://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/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/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/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/492Change premise `Equivalence` into `PreOrder` for `set_fold_proper`.2023-08-02T11:16:48ZRobbert KrebbersChange premise `Equivalence` into `PreOrder` for `set_fold_proper`.Factored out of https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/478Factored out of https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/478https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/491Add a number of missing intersection lemmas2023-08-02T09:47:49ZMarijn van Wezelmarijn.vanwezel@ru.nlAdd a number of missing intersection lemmasThis pull request adds a number of missing lemmas about the intersection on options (closes #166). The `lookup_intersection` lemma was added in !466.This pull request adds a number of missing lemmas about the intersection on options (closes #166). The `lookup_intersection` lemma was added in !466.https://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/489add some map-fmap lemmas2023-08-02T21:22:21ZRalf Jungjung@mpi-sws.orgadd some map-fmap lemmashttps://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/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/486Remove Permutation Proper workaround that is not needed in Coq >= 8.15.2023-07-25T10:11:14ZRobbert KrebbersRemove Permutation Proper workaround that is not needed in Coq >= 8.15.Fixed by https://github.com/coq/coq/issues/14571
I checked that the test cases in https://gitlab.mpi-sws.org/iris/stdpp/-/issues/114 still succeed instantly after removing the workaround.Fixed by https://github.com/coq/coq/issues/14571
I checked that the test cases in https://gitlab.mpi-sws.org/iris/stdpp/-/issues/114 still succeed instantly after removing the workaround.https://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/484Add fin notations2023-07-21T10:38:44ZThibaut PéramiAdd fin notationsIn my own project, I need fin notation up to 32, but I added them up to 50 here. I put the Python script in a comment so that people can tweak it and re-run it for a larger number if needed.
EDIT: Now support all numbers using Coq's Num...In my own project, I need fin notation up to 32, but I added them up to 50 here. I put the Python script in a comment so that people can tweak it and re-run it for a larger number if needed.
EDIT: Now support all numbers using Coq's Number Notationhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/483Remove FIXME in `fin_map_dom`.2023-06-02T15:59:15ZRobbert KrebbersRemove FIXME in `fin_map_dom`.Let's see if CI agrees with me.Let's see if CI agrees with me.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/482add filter_dom (from Perennial)2023-06-02T16:08:35ZRalf Jungjung@mpi-sws.orgadd filter_dom (from Perennial)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/481Stop using revert dependent2023-06-01T16:02:32ZTej Chajedtchajed@gmail.comStop using revert dependentSee https://github.com/coq/coq/pull/17669. `revert dependent` is an
alias for `generalize dependent` and is going away soon.See https://github.com/coq/coq/pull/17669. `revert dependent` is an
alias for `generalize dependent` and is going away soon.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/480Coq support policy: we support 2 Coq versions2023-06-02T16:25:59ZRalf Jungjung@mpi-sws.orgCoq support policy: we support 2 Coq versionsAs discussed at the Iris workshop, we are aligning our policy with that of Coq itself.As discussed at the Iris workshop, we are aligning our policy with that of Coq itself.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/479Fix tests for coq#176482023-05-30T16:39:39ZMichael SammlerFix tests for coq#17648See https://github.com/coq/coq/pull/17648#issuecomment-1568700456 . This MR simply removes the offending test because the test has already caused problems previously (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/421) and does n...See https://github.com/coq/coq/pull/17648#issuecomment-1568700456 . This MR simply removes the offending test because the test has already caused problems previously (https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/421) and does not seem that useful.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/477Revert "Merge branch 'ralf/mangled' into 'master'"2023-05-10T06:45:06ZRobbert KrebbersRevert "Merge branch 'ralf/mangled' into 'master'"This reverts commit 6a7d163ca1b3d7ebccbb089c39ff1cd69799451b, reversing
changes made to 40e5274f6235ddbea3a187da79bc4871aebb6688.
See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/184This reverts commit 6a7d163ca1b3d7ebccbb089c39ff1cd69799451b, reversing
changes made to 40e5274f6235ddbea3a187da79bc4871aebb6688.
See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/184