stdpp merge requestshttps://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests2024-04-16T12:04:57Zhttps://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/549Adapt to https://github.com/coq/coq/pull/189282024-04-16T12:04:57ZPierre RouxAdapt to https://github.com/coq/coq/pull/18928Adapt output tests to upstream PR on Coq https://github.com/coq/coq/pull/18928Adapt output tests to upstream PR on Coq https://github.com/coq/coq/pull/18928https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/507Draft: add lemma lookup_insert_eq2023-10-16T17:50:52ZRalf Jungjung@mpi-sws.orgDraft: add lemma lookup_insert_eqFor most map operations we have a lemma `lookup_foo` that always applies -- except, ironically, for `insert`.
Unfortunately the lemma really should be called `lookup_insert`, but that name is already taken, so I called it `lookup_insert...For most map operations we have a lemma `lookup_foo` that always applies -- except, ironically, for `insert`.
Unfortunately the lemma really should be called `lookup_insert`, but that name is already taken, so I called it `lookup_insert_eq`. Arguably that would be a good name for the `i = j` case and nicely symmetric with `lookup_insert_ne` (well, the really symmetric version would take `i = j` as precondition, which can make it easier to rewrite with). `lookup_insert` is used a lot so I feel renaming might be a bit too disruptive...https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/435Use hint mode + more often2023-10-13T09:41:54ZRobbert KrebbersUse hint mode + more oftenThis is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uoThis is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uohttps://gitlab.rts.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.rts.mpi-sws.org/iris/stdpp/-/merge_requests/501Add MRaise typeclass2023-10-06T12:42:02ZThibaut PéramiAdd MRaise typeclassThis is an alternative to `MFail` in [#488](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/488). It allows a monad to present a general error raising mechanism. This includes an example instantiation for option. I didn't do the w...This is an alternative to `MFail` in [#488](https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/488). It allows a monad to present a general error raising mechanism. This includes an example instantiation for option. I didn't do the work of #488 to completely replace `MGuard`, but if we decide to use this instead of `MFail`, we can merge the two patches.https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/515add make_simple_intropattern2023-10-03T07:30:16ZRalf Jungjung@mpi-sws.orgadd make_simple_intropatternIt's not needed for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/512 after all, but could still be useful in the future.It's not needed for https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/512 after all, but could still be useful in the future.https://gitlab.rts.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.rts.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.rts.mpi-sws.org/iris/stdpp/-/merge_requests/424Prevent [finite_countable] from solving unrelated evars2023-05-02T17:21:40ZPaolo G. GiarrussoPrevent [finite_countable] from solving unrelated evarsFix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple appl...Fix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw.
Fixes https://gitlab.mpi-sws.org/iris/stdpp/-/issues/160.
The problem is that `Hint Immediate` translates to (something like) `simple apply @finite.finite_countable ; trivial` in the trace, and one (or both) the tactics trigger https://github.com/coq/coq/issues/6583. So I've adapted Iris's work around; I've not confirmed whether all of it is needed, but it worked on first try.
Missing (I assume):
- [ ] `trivial` only uses hints with cost 0, but `typeclasses eauto 0` does not appear to work, so `typeclasses eauto 1` is the closest thing I see. This might be a problem.
- [ ] Testcase
- [ ] Changelog? Probably not needed since this is a bugfix
- [x] Mention this in upstream issue.
Also see Coq issue https://github.com/coq/coq/issues/16893.https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/437Enable `Hint Mode Equiv` now that stdpp requires Coq 8.122023-05-02T12:48:11ZPaolo G. GiarrussoEnable `Hint Mode Equiv` now that stdpp requires Coq 8.12Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because ...Includes fixes for Coq 8.12/8.13 — but we might want to drop those.
Rationale: while Coq bug https://github.com/coq/coq/issues/14441 is still relevant, Iris chose to pay the costs of _those_ annotations. Back then, stdpp didn't because it still supported Coq 8.11 which suffered from additional bugs (fixed in 8.12) — Iris still has this comment:
```coq
(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12, which Iris depends on. *)
```https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/451Add NoDup_bind, vec_enum, vec_finite.2023-04-18T18:34:33ZHerman BergwerfAdd NoDup_bind, vec_enum, vec_finite.This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can `vec_finite` be used to simplify the proof of `list_finite`?This adds a function to enumerate all vectors of a given type and a helper lemma about NoDup and bind.
@robbertkrebbers Can `vec_finite` be used to simplify the proof of `list_finite`?https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/387Draft: dune build scripts2023-03-07T14:58:45ZPaolo G. GiarrussoDraft: dune build scriptsThis is part of https://gitlab.mpi-sws.org/iris/iris/-/issues/471.
Instructions are needed, but with dune 3.4 this already supports `dune build`, `dune coq top`.This is part of https://gitlab.mpi-sws.org/iris/iris/-/issues/471.
Instructions are needed, but with dune 3.4 this already supports `dune build`, `dune coq top`.https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/436lookup_gset_to_gmap: use decide rather than guard2022-12-22T16:21:39ZRalf Jungjung@mpi-sws.orglookup_gset_to_gmap: use decide rather than guard`guard` is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. `decide` is a lot more common, and so people are more likely to know how to deal with it.`guard` is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. `decide` is a lot more common, and so people are more likely to know how to deal with it.https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/383Introduce `set_bind` and associated lemmas.2022-08-09T10:52:18ZDan FruminIntroduce `set_bind` and associated lemmas.https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/389Add the feed revert, efeed revert, efeed inversion, and efeed destruct tactics2022-08-09T09:34:56ZMichael SammlerAdd the feed revert, efeed revert, efeed inversion, and efeed destruct tacticshttps://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/381Add `set_map_2` and associated lemmas.2022-05-30T19:40:49ZDan FruminAdd `set_map_2` and associated lemmas.The function `set_map_2` generalizes the mapping function `set_map`, in that it ranges over two sets, and applies a given function to all the possible combinations of the elements.
I tried to recreate the same lemmas for set_map_2 as th...The function `set_map_2` generalizes the mapping function `set_map`, in that it ranges over two sets, and applies a given function to all the possible combinations of the elements.
I tried to recreate the same lemmas for set_map_2 as the ones that we already have for set_map.https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/365Draft: Overlay for PR#155182022-05-06T12:11:32ZMatthieu SozeauDraft: Overlay for PR#15518This is an overlay for [Coq PR #15518](https://github.com/coq/coq/pull/15518): moving apply to the evar-based unifier.
This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q ...This is an overlay for [Coq PR #15518](https://github.com/coq/coq/pull/15518): moving apply to the evar-based unifier.
This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q when applying a `P <-> Q` hypothesis. I think the rest is backwards compatible: mostly about using `eapply` in places where new existential are created, which the new `apply` forbids (rightfully).https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/250WIP: bitvector library2021-12-08T16:36:56ZMichael SammlerWIP: bitvector libraryhttps://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/331Add Arguments bool_decide : simpl never2021-10-25T08:01:18ZMichael SammlerAdd Arguments bool_decide : simpl neverAs discussed on Mattermost, I've encountered a case where simpl on a goal containing bool_decide took 1.5 seconds without making any progress, but was instantaneous after adding `Arguments bool_decide : simpl never.` .As discussed on Mattermost, I've encountered a case where simpl on a goal containing bool_decide took 1.5 seconds without making any progress, but was instantaneous after adding `Arguments bool_decide : simpl never.` .https://gitlab.rts.mpi-sws.org/iris/stdpp/-/merge_requests/189Draft: use SProp for well-formedness condition in Pmap and gmap2021-07-27T21:03:00ZTej Chajedtchajed@gmail.comDraft: use SProp for well-formedness condition in Pmap and gmapProof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks th...Proof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only `simpl` (ordinarily you can get this to work with `vm_compute`, which breaks the opacity of proofs).