stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2024-04-16T12:04:57Zhttps://gitlab.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.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.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.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.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.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/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.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.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.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.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.mpi-sws.org/iris/stdpp/-/merge_requests/424Prevent [finite_countable] from solving unrelated evars2024-07-26T21:17:27ZPaolo 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.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.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.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.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.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.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.mpi-sws.org/iris/stdpp/-/merge_requests/295strengthened solve_decision ltac2021-07-14T19:40:57ZAbhishek Anandstrengthened solve_decision ltachttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/272check for missing 'Hint Mode'2021-06-17T07:37:40ZRalf Jungjung@mpi-sws.orgcheck for missing 'Hint Mode'As requested in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/271#note_68769
Here's the current list of classes with missing `Hint Mode`:
```
No 'Global Hint Mode' for class 'TCNoBackTrack'
No 'Global Hint Mode' for class 'TCIf...As requested in https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/271#note_68769
Here's the current list of classes with missing `Hint Mode`:
```
No 'Global Hint Mode' for class 'TCNoBackTrack'
No 'Global Hint Mode' for class 'TCIf'
No 'Global Hint Mode' for class 'TCTrue'
No 'Global Hint Mode' for class 'TCFalse'
No 'Global Hint Mode' for class 'Inj'
No 'Global Hint Mode' for class 'Inj2'
No 'Global Hint Mode' for class 'Cancel'
No 'Global Hint Mode' for class 'Surj'
No 'Global Hint Mode' for class 'IdemP'
No 'Global Hint Mode' for class 'Comm'
No 'Global Hint Mode' for class 'LeftId'
No 'Global Hint Mode' for class 'RightId'
No 'Global Hint Mode' for class 'Assoc'
No 'Global Hint Mode' for class 'LeftAbsorb'
No 'Global Hint Mode' for class 'RightAbsorb'
No 'Global Hint Mode' for class 'AntiSymm'
No 'Global Hint Mode' for class 'Total'
No 'Global Hint Mode' for class 'Trichotomy'
No 'Global Hint Mode' for class 'TrichotomyT'
No 'Global Hint Mode' for class 'FinSet'
No 'Global Hint Mode' for class 'MonadSet'
No 'Global Hint Mode' for class 'TCFastDone'
No 'Global Hint Mode' for class 'Maybe'
No 'Global Hint Mode' for class 'Maybe2'
No 'Global Hint Mode' for class 'Maybe3'
No 'Global Hint Mode' for class 'Maybe4'
No 'Global Hint Mode' for class 'DiagNone'
No 'Global Hint Mode' for class 'FinMapDom'
No 'Global Hint Mode' for class 'FinMap'
No 'Global Hint Mode' for class 'SetUnfoldSimpl'
No 'Global Hint Mode' for class 'QuoteLookup'
No 'Global Hint Mode' for class 'Quote'
No 'Global Hint Mode' for class 'MakeNatS'
No 'Global Hint Mode' for class 'MakeNatPlus'
```
This MR is blocked on those getting fixed first.