stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2020-05-07T11:20:16Zhttps://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/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/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/149Add a way to disable typeclass search in `Program` obligations2020-11-03T12:13:26ZPaolo G. GiarrussoAdd a way to disable typeclass search in `Program` obligationsFrom the coqdoc of the new feature:
```coq
(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Pro...From the coqdoc of the new feature:
```coq
(** When using [Program], you can use [notc_hole] in place of [_] to create
an obligation that does not trigger typeclass search. That is useful if the
search fails slowly, for instance for [Proper] obligations.
Should https://github.com/coq/coq/issues/12147 be fixed, this can be
deprecated or replaced by the new syntax. *)
```
#### Rationale for inclusion
I think https://github.com/coq/coq/issues/12147 is potentially bad enough that it could belong in stdpp. I haven't found very compelling usecases in iris: in part, you already avoid writing `Program Definition foo ...: A -n> B`, at the cost of more boilerplate.
See also: discussion from https://mattermost.mpi-sws.org/iris/pl/r885z6apefr9bjpuctczruogrr onwards.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/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/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/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/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/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/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/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/11Resolve "Disjoint uses ⊥ (U+22A5 -- UP TACK) but should use ⟂ (U+27C2 -- PERP...2017-10-27T12:29:49ZJacques-Henri JourdanResolve "Disjoint uses ⊥ (U+22A5 -- UP TACK) but should use ⟂ (U+27C2 -- PERPENDICULAR)"Closes #3Closes #3https://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).