stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-08-30T08:50:01Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/181fix various uses of generated names2020-08-30T08:50:01ZRalf Jungjung@mpi-sws.orgfix various uses of generated namesThis makes the entire std++ build with name mangling on Coq master.This makes the entire std++ build with name mangling on Coq master.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/168add singleton_insert_empty2020-06-29T10:17:34ZRalf Jungjung@mpi-sws.orgadd singleton_insert_emptyThis is just an unfolding, but with all the typeclasses that is impossible to find out and also not actually useful when applying lemmas.This is just an unfolding, but with all the typeclasses that is impossible to find out and also not actually useful when applying lemmas.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/165Adapt w.r.t. coq/coq#12512.2020-06-17T18:54:51ZGhost UserAdapt w.r.t. coq/coq#12512.This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
https://github.com/coq/coq/pull/12512This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
https://github.com/coq/coq/pull/12512https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/153overlay for coq/coq#121622020-05-07T11:20:25ZOlivier Laurentoverlay for coq/coq#12162The PR [coq/coq#12162](https://github.com/coq/coq/pull/12162) renames `Bool.leb` into `Bool.le` which is more coherent with the rest of the standard library since it has type `bool -> bool -> Prop`.
This generates possible clashes with `...The PR [coq/coq#12162](https://github.com/coq/coq/pull/12162) renames `Bool.leb` into `Bool.le` which is more coherent with the rest of the standard library since it has type `bool -> bool -> Prop`.
This generates possible clashes with `Nat.le` or `Peano.le` so that additional qualification is required.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/156Alternative take on #153: fix `le` in future versions of Coq2020-05-07T11:20:16ZRobbert KrebbersAlternative take on #153: fix `le` in future versions of CoqThis should provide compatibility for https://github.com/coq/coq/pull/12162
Other changes:
- Use `Arith` instead of `NPeano`, since the latter is deprecated. While it may also be possible to import `NPeano`, numbers export `PArith NAri...This should provide compatibility for https://github.com/coq/coq/pull/12162
Other changes:
- Use `Arith` instead of `NPeano`, since the latter is deprecated. While it may also be possible to import `NPeano`, numbers export `PArith NArith ZArith`, so it seemed logical to also export `Arith`.
- Add test to check for correct version of `le`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/150WIP: rework of naive_solver after discussion with Robbert2020-05-01T17:22:55ZMichael SammlerWIP: rework of naive_solver after discussion with RobbertThis is a slightly reworked version of `naive_solver`, which hopefully fails faster. @robbertkrebbers What do you think? What would be other kinds of goals I should try this version on?This is a slightly reworked version of `naive_solver`, which hopefully fails faster. @robbertkrebbers What do you think? What would be other kinds of goals I should try this version on?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/139Added strings to prelude to fix printing of strings.length2020-04-08T07:28:27ZMichael SammlerAdded strings to prelude to fix printing of strings.lengthThis should hopefully fix `strings.length` showing up in random places. I tested it with iris and RefinedC. Both compile without changes and `length` is no more printed as `strings.length` in RefinedC. See the comment for the reasoning w...This should hopefully fix `strings.length` showing up in random places. I tested it with iris and RefinedC. Both compile without changes and `length` is no more printed as `strings.length` in RefinedC. See the comment for the reasoning why I think this works.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/130Random collection of lemmas2020-03-24T20:09:55ZMichael SammlerRandom collection of lemmasThese are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the `rotate` function. Let me know what you think and which lemmas seem useful. Also better proofs ...These are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the `rotate` function. Let me know what you think and which lemmas seem useful. Also better proofs are always appreciated.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/109WIP: Some lemmas about `list_lookup_total`2020-03-17T15:15:58ZDan FruminWIP: Some lemmas about `list_lookup_total`Partially addresses https://gitlab.mpi-sws.org/iris/stdpp/issues/50Partially addresses https://gitlab.mpi-sws.org/iris/stdpp/issues/50https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/118Generalize (e)feed pose proof to intro patterns2020-03-05T23:03:32ZPaolo G. GiarrussoGeneralize (e)feed pose proof to intro patternsThis appears a simple oversight, since `pose proof` takes an intro pattern
anyway; `feed inversion` and `feed destruct` already take intro patterns, and
I've been using the generalized `efeed pose proof` for a while.This appears a simple oversight, since `pose proof` takes an intro pattern
anyway; `feed inversion` and `feed destruct` already take intro patterns, and
I've been using the generalized `efeed pose proof` for a while.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/119Add a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"2020-02-26T10:29:23ZArmaël GuéneauAdd a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"I found this lemma to be quite useful in situations where one just wants to eliminate an `insert` that only updates a value that we know was already in the map.I found this lemma to be quite useful in situations where one just wants to eliminate an `insert` that only updates a value that we know was already in the map.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/114Add Countable instance for vec2020-02-24T16:12:20ZTej Chajedtchajed@gmail.comAdd Countable instance for vecI was surprised to learn this wasn't available and managed to prove it.
Note that this pulls in stdpp.vector into `countable`. The only reason for this is that the proof is really simple with `vec_to_list` as defined in std++, as oppose...I was surprised to learn this wasn't available and managed to prove it.
Note that this pulls in stdpp.vector into `countable`. The only reason for this is that the proof is really simple with `vec_to_list` as defined in std++, as opposed to with Coq's `Vector.of_list`. This only affects users in that `countable` now loads `vector`, which for example changes the implicits on Coq's vectors.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/92Avoid relying on `Export` bugs2019-09-05T21:39:11ZMaxime DénèsAvoid relying on `Export` bugsSee https://github.com/coq/coq/issues/10480 and
https://github.com/coq/coq/issues/10474.
This should be compatible with Coq's master, but I haven't tested.See https://github.com/coq/coq/issues/10480 and
https://github.com/coq/coq/issues/10474.
This should be compatible with Coq's master, but I haven't tested.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/63Add a .editorconfig file2019-03-22T13:07:53ZJakob Botsch NielsenAdd a .editorconfig filehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/61More efficient `Countable` instance for list and make `namespaces` independen...2019-03-15T12:46:59ZRobbert KrebbersMore efficient `Countable` instance for list and make `namespaces` independent of that.It turns out we once had a more efficient Countable instance for lists, see 54954f55839cdb7a840188fd01c1231669a0c18e.
I have reverted that commit and fixed up namespaces.
This closes #28 ?It turns out we once had a more efficient Countable instance for lists, see 54954f55839cdb7a840188fd01c1231669a0c18e.
I have reverted that commit and fixed up namespaces.
This closes #28 ?https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/22Reserve more notation in `integers.v`.2018-06-20T20:57:26ZDavid SwaseyReserve more notation in `integers.v`.Avoid duplicating details like `at level 35`.
This is a bit of a slippery slope. (I reserved just the notation that
I overload elsewhere.)Avoid duplicating details like `at level 35`.
This is a bit of a slippery slope. (I reserved just the notation that
I overload elsewhere.)https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/28add exact_vm_cast2018-03-01T15:57:30ZRalf Jungjung@mpi-sws.orgadd exact_vm_castThis generalizes https://gitlab.mpi-sws.org/FP/LambdaRust-coq/merge_requests/10 into a reusable tactic.This generalizes https://gitlab.mpi-sws.org/FP/LambdaRust-coq/merge_requests/10 into a reusable tactic.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/478Add lemmas for commuting funcs with folds2023-05-19T12:46:37ZIsaac 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.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/184https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/476Simplify definition of `mapset_dom_with`.2023-05-04T19:01:45ZRobbert KrebbersSimplify definition of `mapset_dom_with`.This fixes issue #183
It is not clear that it fixes similar issues. But regardless, I would say that the simplification of the definition of `dom` is a sensible change.This fixes issue #183
It is not clear that it fixes similar issues. But regardless, I would say that the simplification of the definition of `dom` is a sensible change.