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/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/198WIP: Pretty-print 0 as "0" for N, Z, and nat2020-11-10T10:29:06ZTej Chajedtchajed@gmail.comWIP: Pretty-print 0 as "0" for N, Z, and natFormerly printed as an empty string.Formerly printed as an empty string.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/244Random collection of lemmas from RefinedC2021-04-15T13:18:41ZMichael SammlerRandom collection of lemmas from RefinedCThese are some things from RefinedC that I would like to upstream to stdpp. There are still some open questions, see the comments for them. Please let me know which of these changes make sense in stdpp.These are some things from RefinedC that I would like to upstream to stdpp. There are still some open questions, see the comments for them. Please let me know which of these changes make sense in stdpp.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/232Multiset set notation2021-04-20T14:59:03ZRobbert KrebbersMultiset set notationThis MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100This MR adds a notation `{[ x1 ;+ .. ;+ xn ]}` for `{{ x1 ]} ⊎ .. ⊎ {{ xn ]}`.
Todo:
- [x] bikeshed about notation
- [x] port tests in !231 to new notation
Fixes #100https://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.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/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).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/250WIP: bitvector library2021-12-08T16:36:56ZMichael SammlerWIP: bitvector libraryhttps://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/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/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/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/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/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/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/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/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.