stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-10-12T09:51:39Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/192Draft: Drop misleading gmultiset_simple_set instance2020-10-12T09:51:39ZPaolo G. GiarrussoDraft: Drop misleading gmultiset_simple_set instanceThe problem is that `elem_of_subseteq_singleton` applies to multiset goals, but uses the wrong instance.
> [...] when my goal is a multiset elem-of, then `apply gmultiset_elem_of_singleton_subseteq.` and `apply elem_of_subseteq_singleton...The problem is that `elem_of_subseteq_singleton` applies to multiset goals, but uses the wrong instance.
> [...] when my goal is a multiset elem-of, then `apply gmultiset_elem_of_singleton_subseteq.` and `apply elem_of_subseteq_singleton.` result in different goals that print exactly the same (also btw note the inconsistent lemma name)
Based on a suggestion by Robbert (which I might have misunderstood); but I'm not sure this is the right fix.
This instance appears to not be used, and it allows applying lemmas like `elem_of_subseteq_singleton` which are inappropriate for gmultiset, as they use the `set_subseteq` instance for `SubsetEq`, instead of `gmultiset_subseteq : SubsetEq (gmultiset A)`.
However, the lemmas should be restated in terms of `gmultiset`, since they do hold, and they hold on sensible instances.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/177[simpl_map]: avoid using [rewrite .. by ..]2020-09-29T09:36:43ZArmaël Guéneau[simpl_map]: avoid using [rewrite .. by ..]We've been using a patched version of [simpl_map] in our project for a while, with the changes included here.
The core issue is that it seems that [rewrite .. by ..] is not available when explicitly importing ssreflect.
The patch uses `...We've been using a patched version of [simpl_map] in our project for a while, with the changes included here.
The core issue is that it seems that [rewrite .. by ..] is not available when explicitly importing ssreflect.
The patch uses `by tac` instead, which is in line with what [simplify_map_eq] does later in the file.
I tried to write a quick test to demonstrate the issue; however it seems that triggering it is a bit subtle
(while it does definitely occur on our development, I wasn't able to easily reproduce it on my synthetic example---
I think there is some interaction with the exact order of the Require Import invocations).
If deemed necessary I could try harder and try to minimize a problematic instance from our development.https://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/6Add filter for gmap2017-10-27T14:49:51ZHai DangAdd filter for gmapA filter for (M : gmap K A) creates a submap of M whose (key,value) pairs satisfy the filter predicate (P : K * A → Prop).A filter for (M : gmap K A) creates a submap of M whose (key,value) pairs satisfy the filter predicate (P : K * A → Prop).